1300

1 
open I;


2 


3 
goal thy


4 
"! a m s s' t n. \


5 
\ (new_tv m a & new_tv m s) > I e a m s = Ok(s',t,n) > \


6 
\ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";


7 
by (expr.induct_tac "e" 1);


8 

1669

9 
(* case Var n *)


10 
by (simp_tac (!simpset addsimps [app_subst_list]

1723

11 
setloop (split_inside_tac [expand_if])) 1);

1669

12 
by (fast_tac (HOL_cs addss !simpset) 1);

1300

13 

1669

14 
(* case Abs e *)

1723

15 
by (asm_full_simp_tac (!simpset setloop (split_inside_tac [expand_bind])) 1);

1669

16 
by (strip_tac 1);


17 
by (rtac conjI 1);


18 
by (strip_tac 1);


19 
by (REPEAT (etac allE 1));


20 
by (etac impE 1);


21 
by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);


22 
by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,


23 
less_imp_le,lessI]) 1);

1300

24 

1669

25 
by (strip_tac 1);


26 
by (REPEAT (etac allE 1));


27 
by (etac impE 1);


28 
by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);


29 
by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,


30 
less_imp_le,lessI]) 1);

1300

31 


32 
(* case App e1 e2 *)

1723

33 
by (simp_tac (!simpset setloop (split_inside_tac [expand_bind])) 1);

1300

34 
by (strip_tac 1);


35 
by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);

1465

36 
by (rtac conjI 1);

1669

37 
by (fast_tac (HOL_cs addss !simpset) 1);

1300

38 
by (strip_tac 1);


39 
by (rename_tac "s1 t1' n1'" 1);


40 
by (eres_inst_tac [("x","a")] allE 1);


41 
by (eres_inst_tac [("x","m")] allE 1);


42 
by (eres_inst_tac [("x","s")] allE 1);


43 
by (eres_inst_tac [("x","s1'")] allE 1);


44 
by (eres_inst_tac [("x","t1")] allE 1);


45 
by (eres_inst_tac [("x","n1")] allE 1);


46 
by (eres_inst_tac [("x","a")] allE 1);


47 
by (eres_inst_tac [("x","n1")] allE 1);


48 
by (eres_inst_tac [("x","s1'")] allE 1);


49 
by (eres_inst_tac [("x","s2'")] allE 1);


50 
by (eres_inst_tac [("x","t2")] allE 1);


51 
by (eres_inst_tac [("x","n2")] allE 1);

1465

52 
by (rtac conjI 1);

1669

53 
by (strip_tac 1);


54 
by (mp_tac 1);


55 
by (mp_tac 1);


56 
by (etac exE 1);


57 
by (etac conjE 1);


58 
by (etac impE 1);


59 
by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));


60 
by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));


61 
by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]


62 
addss !simpset) 1);


63 
by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1);

1300

64 
by (strip_tac 1);


65 
by (rename_tac "s2 t2' n2'" 1);

1465

66 
by (rtac conjI 1);

1669

67 
by (strip_tac 1);


68 
by (mp_tac 1);


69 
by (mp_tac 1);


70 
by (etac exE 1);


71 
by (etac conjE 1);


72 
by (etac impE 1);


73 
by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));


74 
by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));


75 
by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]


76 
addss !simpset) 1);


77 
by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1);

1300

78 
by (strip_tac 1);


79 
by (mp_tac 1);


80 
by (mp_tac 1);

1465

81 
by (etac exE 1);


82 
by (etac conjE 1);


83 
by (etac impE 1);

1669

84 
by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));


85 
by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));


86 
by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]


87 
addss !simpset) 1);

1300

88 
by (mp_tac 1);


89 
by (REPEAT (eresolve_tac [exE,conjE] 1));

1669

90 
by (REPEAT(EVERY1


91 
[asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]),


92 
REPEAT o etac conjE, hyp_subst_tac]));

1465

93 
by (rtac exI 1);

1300

94 
by (safe_tac HOL_cs);

1669

95 
by (fast_tac HOL_cs 1);


96 
by (simp_tac (!simpset addsimps [o_def,subst_comp_te]) 2);

1300

97 
by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);

1669

98 
by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);

1300

99 
by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));

1486

100 
by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));

1300

101 
by (safe_tac HOL_cs);

1669

102 
by (fast_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]


103 
addss !simpset) 1);


104 
by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le]


105 
addss !simpset) 1);

1300

106 
by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);


107 
by ((dtac new_tv_subst_tel 1) THEN (atac 1));

1400

108 
by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));

1300

109 
by ((dtac new_tv_subst_tel 1) THEN (atac 1));


110 
by (fast_tac (HOL_cs addDs [new_tv_W] addss


111 
(!simpset addsimps [subst_comp_tel])) 1);

1486

112 
qed_spec_mp "I_correct_wrt_W";

1751

113 


114 
(***


115 
We actually want the corollary


116 


117 
goal I.thy


118 
"I e [] m id_subst = Ok(s,t,n) > W e [] m = Ok(s, $s t, n)";


119 
by(cut_facts_tac [(read_instantiate[("x","id_subst")]


120 
(read_instantiate[("x","[]")](thm RS spec)


121 
RS spec RS spec))] 1);


122 
by(Full_simp_tac 1);


123 
by(fast_tac HOL_cs 1);


124 
qed;


125 


126 
assuming that thm is the undischarged version of I_correct_wrt_W.


127 


128 
Wait until simplification of thms is possible.


129 
***)


130 

1757

131 
val lemma = I_correct_wrt_W COMP swap_prems_rl;


132 

1751

133 
goal I.thy "!a m s. \


134 
\ new_tv m a & new_tv m s > I e a m s = Fail > W e ($s a) m = Fail";


135 
by (expr.induct_tac "e" 1);


136 
by(simp_tac (!simpset addsimps [app_subst_list]


137 
setloop (split_tac [expand_if])) 1);

1757

138 
by(Simp_tac 1);


139 
by(strip_tac 1);


140 
br conjI 1;


141 
by(strip_tac 1);


142 
by(subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);


143 
by(asm_simp_tac (HOL_ss addsimps


144 
[new_tv_Suc_list, lessI RS less_imp_le RS new_tv_subst_le]) 1);


145 
be conjE 1;


146 
bd (new_tv_not_free_tv RS not_free_impl_id) 1;


147 
by(Asm_simp_tac 1);

1751

148 
by(strip_tac 1);

1757

149 
be exE 1;


150 
by(split_all_tac 1);


151 
by(Full_simp_tac 1);


152 
by(Asm_simp_tac 1);

1751

153 
by(strip_tac 1);

1757

154 
be exE 1;


155 
by(REPEAT(etac conjE 1));


156 
by(split_all_tac 1);


157 
by(Full_simp_tac 1);


158 
bd lemma 1;


159 
by(fast_tac HOL_cs 1);


160 
be exE 1;


161 
be conjE 1;


162 
by(hyp_subst_tac 1);


163 
by(Asm_simp_tac 1);


164 
br exI 1;

1751

165 
br conjI 1;

1757

166 
br refl 1;


167 
by(Simp_tac 1);


168 
be disjE 1;


169 
br disjI1 1;

1751

170 
by(full_simp_tac (!simpset addsimps [o_def,subst_comp_tel]) 1);

1757

171 
by(EVERY[etac allE 1, etac allE 1, etac allE 1,

1751

172 
etac impE 1, etac impE 2, atac 2, atac 2]);


173 
br conjI 1;


174 
by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);


175 
br new_tv_subst_comp_2 1;


176 
by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);


177 
by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);

1757

178 
br disjI2 1;

1751

179 
be exE 1;

1757

180 
by(split_all_tac 1);


181 
be conjE 1;


182 
by(Full_simp_tac 1);


183 
bd lemma 1;


184 
br conjI 1;


185 
by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);


186 
br new_tv_subst_comp_1 1;


187 
by(fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);


188 
by(fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);


189 
be exE 1;


190 
be conjE 1;

1751

191 
by(hyp_subst_tac 1);


192 
by(asm_full_simp_tac (!simpset addsimps


193 
[o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);

1757

194 
by(asm_simp_tac (!simpset addcongs [conj_cong] addsimps


195 
[eq_sym_conv,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);

1751

196 
qed_spec_mp "I_complete_wrt_W";


197 


198 
(***


199 
We actually want the corollary


200 


201 
"I e [] m id_subst = Fail ==> W e [] m = Fail";


202 


203 
Wait until simplification of thms is possible.


204 
***)
