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