theory test10st_metatheory = "test10st_snapshot_out":


(* Tom Ridge, Peter Sewell  Fri Aug 25 16:18:06 BST 2006

Proof of type preservation and progress for the test10st simply typed lambda calculus.
This is the non-cleaned-up first proof, without making heavy use of the automation, and
with a novice second author. *)

lemma Weakening_on_the_left:
"(G0,t,T):GtT  --> (! G . (G0@G,t,T):GtT)"
apply(intro impI)
apply(rule_tac GtT.induct)
apply(auto intro:GtT.intros)
apply(rule_tac GtT_value_nameI)
apply(force)
done


lemma Weakening_from_empty:
"([],t,T):GtT --> (G,t,T):GtT"
using Weakening_on_the_left [of Nil t T] apply(force)
done

lemma strength: "! G t T. (G, t, T) : GtT --> (! x T1 G0 G1 Tv. G = G1 @ (x, T1) # G0 @ [(x, Tv)] --> (G1 @ (x, T1) # G0, t, T) : GtT)"
  apply(intro allI)
  apply(rule ) apply(erule GtT.induct)
  apply(intro allI impI, elim exE conjE) apply(rule GtT_value_nameI) apply(simp) apply(clarify)
  apply(rule_tac x=G1a in exI) apply(simp) apply(rule_tac x="butlast G2" in exI) apply(case_tac G2 rule: rev_cases) apply(simp) apply(simp)
  
  apply(intro allI impI) apply(rule GtT_applyI) apply(force) apply(force)

  apply(intro allI impI)
  apply(rule GtT_lambdaI)
  apply(simp) apply(clarify)
  apply(drule_tac x=T1a in spec) apply(drule_tac x=G0 in spec) apply(drule_tac x="(x1,T1)#G1" in spec) apply(simp)
  done

lemma strength: "(! t T x T1 G0 G1 Tv. (G1 @ (x, T1) # G0 @ [(x, Tv)], t, T) : GtT --> (G1 @ (x, T1) # G0, t, T) : GtT)"
  using strength apply(force) done
  
lemma Substitution : 
"(G,t,T):GtT
--> 
(!v x Tv G0.
(
  G = G0 @[(x,Tv)]) 
& x ~: set ( List.map fst G0) 
& ([],v,Tv):GtT 
-->
((G0,tsubst_t v x t, T) : GtT))
"
apply(intro impI)
apply(erule GtT.induct)
apply(intro allI impI)
apply(elim exE conjE)
apply(simp)
apply(intro conjI impI)
apply(simp)
apply(subgoal_tac "filter (%(x,y).x=xa) (G1 @ (xa, T) # G2) = filter (%(x,y).x=xa) (G0 @ [(xa, Tv)])")
apply(simp (no_asm_use) add: List.filter_append)
apply(subgoal_tac "[(x, y):G1. x = xa] = [] &[(x, y):G0. x = xa] = [] ") prefer 2 
apply(force intro: filter_False)
apply(simp) apply(rule Weakening_from_empty [ rule_format]) apply(assumption)
apply(simp)

apply(rule GtT_value_nameI) apply(rule_tac x=G1 in exI) apply(rule_tac x="butlast G2" in exI) apply(case_tac G2 rule: rev_cases) apply(simp) apply(simp)

apply(force intro: GtT_applyI)


(* lambda case *)
apply(intro allI impI) apply(elim exE conjE)
apply(simp) apply(intro conjI impI)

(* x1=x *)
apply(rule GtT_lambdaI) apply(simp) (* point is that we would like to use the I.H. for all G, but we can only use it for structural G from GtT *)
using strength apply(simp) apply(drule_tac x=t in spec) apply(drule_tac x=T in spec) apply(drule_tac x=x in spec)apply(drule_tac x=T1 in spec) apply(drule_tac x=G0 in spec) apply(drule_tac x="[]" in spec) apply(force)

(* x1~=x *)
apply(force intro: GtT_lambdaI)
done

lemma Substitution_tmp : 
"(([(x,Tv)],t,T):GtT
 & 
([],v,Tv):GtT )
-->
(([],tsubst_t v x t, T) : GtT)
"
apply(intro impI conjI)
apply(rule Substitution [rule_format])
apply(elim conjE)
apply(assumption)
apply(force)
done



theorem "(G,t,T):GtT --> (!t'. G=[] & (t,t'):E --> (G,t',T):GtT)" 


apply(rule impI);
apply(rule_tac GtT.induct);

 apply(assumption)

 (* vars don't reduce *)
 apply(intro allI impI)
 apply(elim conjE)
 apply(rule_tac E.cases)
 apply(assumption)
 apply(simp)
 apply(simp)
 apply(simp)

 (* lambdas don't reduce *)
 defer
 apply(intro allI impI)
 apply(elim conjE)
 apply(rule_tac E.cases)
 apply(assumption)
 apply(simp)
 apply(simp)
 apply(simp)

 (* apps might reduce, unfortunately *)
 apply(intro allI impI)
 apply(elim conjE)
 apply(thin_tac "(G, t, T) : GtT")
 apply(simp)
 apply(thin_tac "G=[]")


 apply(erule_tac E.cases)
 defer
 apply(simp)
 apply(elim conjE)
 apply(clarify)
 apply(drule_tac x=t1' in spec)
 apply(erule impE)
 apply(assumption)
 apply(rule GtT.GtT_applyI)
 apply(assumption)
 apply(assumption)

 apply(simp)
 apply(elim conjE)
 apply(clarify)
 apply(drule_tac x=t1' in spec)
 back
 apply(erule impE)
 apply(assumption)
 apply(rule GtT.GtT_applyI)
 apply(assumption)
 apply(assumption)

 apply(simp)
 apply(elim conjE)
 apply(clarify)
 apply(thin_tac "ALL t'. (t_Lam x t12, t') : E --> ([], t', T_arrow T1 T2) : GtT")
 apply(thin_tac "is_v v2")

 apply(erule_tac GtT.cases)
 apply(simp)
 apply(simp)
 apply(simp)
 apply(clarify)
 apply(thin_tac "ALL t'. (v2, t') : E --> ([], t', T1a) : GtT")

 apply(rule_tac Substitution_tmp [rule_format])
 apply(force)
 done


lemma tmp: "([],t_Var x,T) : GtT ==> False"
  apply(erule GtT.cases) 
  apply(force)
  apply(force)
  apply(force)
  done

(* need that something of function type in the empty env must be a lambda *)
lemma tmp2: "([],t,Arr T1 t2) : GtT ==> is_v t ==> (? x t1'. t = t_Lam x t1')"
  apply(erule GtT.cases)
  apply(force)
  apply(simp)
  apply(simp)
  done



lemma "(G,t,T) : GtT --> G = [] & ~ (is_v t) --> (? t'. (t,t') : E)"
  apply(rule, erule GtT.induct)

  (* t_Var *)
  apply(simp) (* can't type var in empty context *) apply(force dest: tmp)
  
  (* App *)
  apply(simp) apply(rule)
  apply(rename_tac t1 t2)
  apply(case_tac "is_v t1")
  (* is_v t1 *)
  apply(case_tac "is_v t2")
  (* is_v t1, is_v t2 use AX_APP *)
  apply(simp)
  apply(subgoal_tac "? x t1'. t1 = t_Lam x t1'") prefer 2 apply(rule tmp2) apply(assumption) apply(assumption)
  apply(elim exE conjE) apply(simp)
  apply(rule_tac x="tsubst_t t2 x t1'" in exI) apply(rule_tac E.ax_appI) apply(assumption)

  (* is_v t1, ~ is_v t2 reduce t2 *)
  apply(simp) apply(elim exE) apply(rename_tac "t2'")
  apply(rule_tac x="t_App t1 t2'" in exI) 
  apply(rule_tac E.ctx_app_argI) apply(assumption) apply(assumption)
  (* ~ is_v t1 *)
  apply(simp) apply(elim exE conjE) apply(rename_tac t1')
  apply(rule_tac x="t_App t1' t2" in exI)
  apply(rule_tac E.ctx_app_funI) apply(assumption)


  (* Lam *)
  apply(intro impI)
  apply(force)
  done