author  nipkow 
Fri, 17 Jan 1997 18:32:24 +0100  
changeset 2523  0ccea141409b 
parent 2513  d708d8cdc8e8 
child 2525  477c05586286 
permissions  rwrr 
1300  1 
(* Title: HOL/MiniML/W.ML 
2 
ID: $Id$ 

3 
Author: Dieter Nazareth and Tobias Nipkow 

4 
Copyright 1995 TU Muenchen 

5 

6 
Correctness and completeness of type inference algorithm W 

7 
*) 

8 

9 
open W; 

10 

11 
Addsimps [Suc_le_lessD]; 

1950
97f1c6bf3ace
Miniscoping rules are deleted, as these brittle proofs
paulson
parents:
1925
diff
changeset

12 
Delsimps (ex_simps @ all_simps); 
1300  13 

14 
(* correctness of W with respect to has_type *) 

1525  15 
goal W.thy 
16 
"!a s t m n . Ok (s,t,m) = W e a n > $s a  e :: t"; 

1300  17 
by (expr.induct_tac "e" 1); 
18 
(* case Var n *) 

19 
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); 

20 
(* case Abs e *) 

21 
by (asm_full_simp_tac (!simpset addsimps [app_subst_list] 

22 
setloop (split_tac [expand_bind])) 1); 

23 
by (strip_tac 1); 

24 
by (eres_inst_tac [("x","TVar(n) # a")] allE 1); 

2031  25 
by ( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1); 
1300  26 
(* case App e1 e2 *) 
27 
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 

28 
by (strip_tac 1); 

2031  29 
by ( rename_tac "sa ta na sb tb nb sc" 1); 
1300  30 
by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1); 
31 
by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1); 

32 
by (rtac (app_subst_Fun RS subst) 1); 

1525  33 
by (res_inst_tac [("t","$sc(tb > (TVar nb))"),("s","$sc($sb ta)")] subst 1); 
1300  34 
by (Asm_full_simp_tac 1); 
35 
by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1); 

36 
by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1)); 

37 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); 

1669  38 
by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1); 
1486  39 
qed_spec_mp "W_correct"; 
1300  40 

41 
val has_type_casesE = map(has_type.mk_cases expr.simps) 

1465  42 
[" s  Var n :: t"," s  Abs e :: t","s  App e1 e2 ::t"]; 
1300  43 

44 

45 
(* the resulting type variable is always greater or equal than the given one *) 

46 
goal thy 

1465  47 
"!a n s t m. W e a n = Ok (s,t,m) > n<=m"; 
1300  48 
by (expr.induct_tac "e" 1); 
49 
(* case Var(n) *) 

50 
by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1); 

51 
(* case Abs e *) 

52 
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 

53 
by (fast_tac (HOL_cs addDs [Suc_leD]) 1); 

54 
(* case App e1 e2 *) 

55 
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 

56 
by (strip_tac 1); 

57 
by (rename_tac "s t na sa ta nb sb sc tb m" 1); 

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

59 
by (eres_inst_tac [("x","n")] allE 1); 

60 
by (eres_inst_tac [("x","$ s a")] allE 1); 

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

62 
by (eres_inst_tac [("x","t")] allE 1); 

63 
by (eres_inst_tac [("x","na")] allE 1); 

64 
by (eres_inst_tac [("x","na")] allE 1); 

65 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); 

66 
by (etac conjE 1); 

67 
by (eres_inst_tac [("x","sa")] allE 1); 

68 
by (eres_inst_tac [("x","ta")] allE 1); 

69 
by (eres_inst_tac [("x","nb")] allE 1); 

70 
by (etac conjE 1); 

71 
by (res_inst_tac [("j","na")] le_trans 1); 

72 
by (Asm_simp_tac 1); 

1669  73 
by (Asm_simp_tac 1); 
1486  74 
qed_spec_mp "W_var_ge"; 
1300  75 

76 
Addsimps [W_var_ge]; 

77 

78 
goal thy 

1465  79 
"!! s. Ok (s,t,m) = W e a n ==> n<=m"; 
1300  80 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); 
81 
qed "W_var_geD"; 

82 

83 

84 
(* auxiliary lemma *) 

85 
goal Maybe.thy "(y = Ok x) = (Ok x = y)"; 

2031  86 
by ( simp_tac (!simpset addsimps [eq_sym_conv]) 1); 
1300  87 
qed "rotate_Ok"; 
88 

89 

90 
(* resulting type variable is new *) 

91 
goal thy 

92 
"!n a s t m. new_tv n a > W e a n = Ok (s,t,m) > \ 

1525  93 
\ new_tv m s & new_tv m t"; 
1300  94 
by (expr.induct_tac "e" 1); 
95 
(* case Var n *) 

96 
by (fast_tac (HOL_cs addss (!simpset 

1465  97 
addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
1300  98 
setloop (split_tac [expand_if]))) 1); 
99 

100 
(* case Abs e *) 

101 
by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 

102 
setloop (split_tac [expand_bind])) 1); 

103 
by (strip_tac 1); 

104 
by (eres_inst_tac [("x","Suc n")] allE 1); 

105 
by (eres_inst_tac [("x","(TVar n)#a")] allE 1); 

106 
by (fast_tac (HOL_cs addss (!simpset 

1465  107 
addsimps [new_tv_subst,new_tv_Suc_list])) 1); 
1300  108 

109 
(* case App e1 e2 *) 

110 
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 

111 
by (strip_tac 1); 

112 
by (rename_tac "s t na sa ta nb sb sc tb m" 1); 

113 
by (eres_inst_tac [("x","n")] allE 1); 

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

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

116 
by (eres_inst_tac [("x","t")] allE 1); 

117 
by (eres_inst_tac [("x","na")] allE 1); 

118 
by (eres_inst_tac [("x","na")] allE 1); 

119 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); 

120 
by (eres_inst_tac [("x","$ s a")] allE 1); 

121 
by (eres_inst_tac [("x","sa")] allE 1); 

122 
by (eres_inst_tac [("x","ta")] allE 1); 

123 
by (eres_inst_tac [("x","nb")] allE 1); 

2031  124 
by ( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1); 
1300  125 
by (rtac conjI 1); 
126 
by (rtac new_tv_subst_comp_2 1); 

127 
by (rtac new_tv_subst_comp_2 1); 

128 
by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1); 

129 
by (res_inst_tac [("n","na")] new_tv_subst_le 1); 

130 
by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1); 

131 
by (Asm_simp_tac 1); 

132 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs 

133 
[new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le]) 

134 
1); 

1465  135 
by (etac (sym RS mgu_new) 1); 
1925  136 
by (best_tac (HOL_cs addDs [W_var_geD] 
2031  137 
addIs [new_tv_subst_te,new_tv_list_le, 
138 
new_tv_subst_tel, 

139 
lessI RS less_imp_le RS new_tv_le, 

140 
lessI RS less_imp_le RS new_tv_subst_le, 

141 
new_tv_le]) 1); 

1925  142 
by (fast_tac (HOL_cs addDs [W_var_geD] 
2031  143 
addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
144 
addss (!simpset)) 1); 

1465  145 
by (rtac (lessI RS new_tv_subst_var) 1); 
146 
by (etac (sym RS mgu_new) 1); 

1925  147 
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te] 
148 
addDs [W_var_geD] 

2031  149 
addIs [new_tv_list_le, 
150 
new_tv_subst_tel, 

151 
lessI RS less_imp_le RS new_tv_subst_le, 

152 
new_tv_le] 

153 
addss !simpset) 1); 

1925  154 
by (fast_tac (HOL_cs addDs [W_var_geD] 
2031  155 
addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] 
1925  156 
addss (!simpset)) 1); 
1486  157 
qed_spec_mp "new_tv_W"; 
1300  158 

159 

160 
goal thy 

1465  161 
"!n a s t m v. W e a n = Ok (s,t,m) > \ 
1300  162 
\ (v:free_tv s  v:free_tv t) > v<n > v:free_tv a"; 
163 
by (expr.induct_tac "e" 1); 

164 
(* case Var n *) 

165 
by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 

166 
addss (!simpset setloop (split_tac [expand_if]))) 1); 

167 

168 
(* case Abs e *) 

169 
by (asm_full_simp_tac (!simpset addsimps 

170 
[free_tv_subst] setloop (split_tac [expand_bind])) 1); 

171 
by (strip_tac 1); 

172 
by (rename_tac "s t na sa ta m v" 1); 

173 
by (eres_inst_tac [("x","Suc n")] allE 1); 

174 
by (eres_inst_tac [("x","TVar n # a")] allE 1); 

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

176 
by (eres_inst_tac [("x","t")] allE 1); 

177 
by (eres_inst_tac [("x","na")] allE 1); 

178 
by (eres_inst_tac [("x","v")] allE 1); 

2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

179 
by (fast_tac (HOL_cs addSEs [allE] 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

180 
addIs [cod_app_subst] 
1669  181 
addss (!simpset addsimps [less_Suc_eq])) 1); 
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

182 
(** LEVEL 12 **) 
1300  183 
(* case App e1 e2 *) 
184 
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 

185 
by (strip_tac 1); 

186 
by (rename_tac "s t na sa ta nb sb sc tb m v" 1); 

187 
by (eres_inst_tac [("x","n")] allE 1); 

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

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

190 
by (eres_inst_tac [("x","t")] allE 1); 

191 
by (eres_inst_tac [("x","na")] allE 1); 

192 
by (eres_inst_tac [("x","na")] allE 1); 

193 
by (eres_inst_tac [("x","v")] allE 1); 

2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

194 
(** LEVEL 22 **) 
1300  195 
(* second case *) 
196 
by (eres_inst_tac [("x","$ s a")] allE 1); 

197 
by (eres_inst_tac [("x","sa")] allE 1); 

198 
by (eres_inst_tac [("x","ta")] allE 1); 

199 
by (eres_inst_tac [("x","nb")] allE 1); 

200 
by (eres_inst_tac [("x","v")] allE 1); 

201 
by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 

1669  202 
by (asm_full_simp_tac (!simpset addsimps [rotate_Ok,o_def]) 1); 
1465  203 
by (dtac W_var_geD 1); 
204 
by (dtac W_var_geD 1); 

1300  205 
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); 
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

206 
(** LEVEL 32 **) 
1300  207 
by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, 
208 
codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD, 

209 
less_le_trans,less_not_refl2,subsetD] 

210 
addEs [UnE] 

211 
addss !simpset) 1); 

212 
by (Asm_full_simp_tac 1); 

1465  213 
by (dtac (sym RS W_var_geD) 1); 
214 
by (dtac (sym RS W_var_geD) 1); 

1300  215 
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); 
216 
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD, 

2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

217 
free_tv_app_subst_te RS subsetD, 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

218 
free_tv_app_subst_tel RS subsetD, 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

219 
less_le_trans,subsetD] 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

220 
addSEs [UnE] 
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2083
diff
changeset

221 
addss !simpset) 1); 
1486  222 
qed_spec_mp "free_tv_W"; 
1300  223 

2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

224 

1300  225 
(* Completeness of W w.r.t. has_type *) 
226 
goal thy 

1525  227 
"!s' a t' n. $s' a  e :: t' > new_tv n a > \ 
228 
\ (? s t. (? m. W e a n = Ok (s,t,m)) & \ 

229 
\ (? r. $s' a = $r ($s a) & t' = $r t))"; 

1300  230 
by (expr.induct_tac "e" 1); 
231 
(* case Var n *) 

232 
by (strip_tac 1); 

233 
by (simp_tac (!simpset addcongs [conj_cong] 

2031  234 
setloop (split_tac [expand_if])) 1); 
1300  235 
by (eresolve_tac has_type_casesE 1); 
236 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1); 

237 
by (res_inst_tac [("x","id_subst")] exI 1); 

238 
by (res_inst_tac [("x","nth nat a")] exI 1); 

239 
by (Simp_tac 1); 

240 
by (res_inst_tac [("x","s'")] exI 1); 

241 
by (Asm_simp_tac 1); 

242 

2058  243 
(** LEVEL 10 **) 
1300  244 
(* case Abs e *) 
245 
by (strip_tac 1); 

246 
by (eresolve_tac has_type_casesE 1); 

247 
by (eres_inst_tac [("x","%x.if x=n then t1 else (s' x)")] allE 1); 

248 
by (eres_inst_tac [("x","(TVar n)#a")] allE 1); 

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

250 
by (eres_inst_tac [("x","Suc n")] allE 1); 

251 
by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong] 

2031  252 
setloop (split_tac [expand_bind]))) 1); 
1300  253 

2058  254 
(** LEVEL 17 **) 
1300  255 
(* case App e1 e2 *) 
256 
by (strip_tac 1); 

257 
by (eresolve_tac has_type_casesE 1); 

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

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

1400  260 
by (eres_inst_tac [("x","t2 > t'")] allE 1); 
1300  261 
by (eres_inst_tac [("x","n")] allE 1); 
262 
by (safe_tac HOL_cs); 

263 
by (eres_inst_tac [("x","r")] allE 1); 

264 
by (eres_inst_tac [("x","$ s a")] allE 1); 

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

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

1465  267 
by (dtac asm_rl 1); 
268 
by (dtac asm_rl 1); 

269 
by (dtac asm_rl 1); 

1300  270 
by (Asm_full_simp_tac 1); 
271 
by (safe_tac HOL_cs); 

272 
by (fast_tac HOL_cs 1); 

273 
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS 

2031  274 
conjunct1,new_tv_list_le,new_tv_subst_tel]) 1); 
1300  275 

2058  276 
(** LEVEL 35 **) 
1300  277 
by (subgoal_tac 
278 
"$ (%x.if x=ma then t' else (if x:(free_tv t  free_tv sa) then r x \ 

279 
\ else ra x)) ($ sa t) = \ 

280 
\ $ (%x.if x=ma then t' else (if x:(free_tv t  free_tv sa) then r x \ 

1400  281 
\ else ra x)) (ta > (TVar ma))" 1); 
1300  282 
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \ 
283 
\ (if x:(free_tv t  free_tv sa) then r x else ra x)) ($ sa t)"), 

1400  284 
("s","($ ra ta) > t'")] ssubst 2); 
1300  285 
by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2); 
1465  286 
by (rtac eq_free_eq_subst_te 2); 
1300  287 
by (strip_tac 2); 
288 
by (subgoal_tac "na ~=ma" 2); 

289 
by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD, 

2031  290 
new_tv_not_free_tv,new_tv_le]) 3); 
2058  291 
(** LEVEL 42 **) 
1300  292 
by (case_tac "na:free_tv sa" 2); 
293 
(* na ~: free_tv sa *) 

294 
by (asm_simp_tac (!simpset addsimps [not_free_impl_id] 

2031  295 
setloop (split_tac [expand_if])) 3); 
1300  296 
(* na : free_tv sa *) 
1400  297 
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2); 
1465  298 
by (dtac eq_subst_tel_eq_free 2); 
1300  299 
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); 
300 
by (Asm_simp_tac 2); 

301 
by (case_tac "na:dom sa" 2); 

302 
(* na ~: dom sa *) 

303 
by (asm_full_simp_tac (!simpset addsimps [dom_def] 

2031  304 
setloop (split_tac [expand_if])) 3); 
2058  305 
(** LEVEL 50 **) 
1300  306 
(* na : dom sa *) 
1465  307 
by (rtac eq_free_eq_subst_te 2); 
1300  308 
by (strip_tac 2); 
309 
by (subgoal_tac "nb ~= ma" 2); 

310 
by ((forward_tac [new_tv_W] 3) THEN (atac 3)); 

1465  311 
by (etac conjE 3); 
312 
by (dtac new_tv_subst_tel 3); 

1300  313 
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3); 
314 
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 

2031  315 
(!simpset addsimps [cod_def,free_tv_subst])) 3); 
1300  316 
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
2031  317 
setloop (split_tac [expand_if]))) 2); 
1300  318 

319 
by (Simp_tac 2); 

2058  320 
(** LEVEL 60 **) 
1465  321 
by (rtac eq_free_eq_subst_te 2); 
1300  322 
by (strip_tac 2 ); 
323 
by (subgoal_tac "na ~= ma" 2); 

324 
by ((forward_tac [new_tv_W] 3) THEN (atac 3)); 

1465  325 
by (etac conjE 3); 
326 
by (dtac (sym RS W_var_geD) 3); 

1300  327 
by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3); 
328 
by (case_tac "na: free_tv t  free_tv sa" 2); 

2058  329 
(** LEVEL 68 **) 
1300  330 
(* case na ~: free_tv t  free_tv sa *) 
2031  331 
by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3); 
1300  332 
(* case na : free_tv t  free_tv sa *) 
2031  333 
by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2); 
1400  334 
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2); 
1465  335 
by (dtac eq_subst_tel_eq_free 2); 
1300  336 
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); 
1486  337 
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 2); 
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

338 
(** LEVEL 74 **) 
1300  339 
by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1); 
340 
by (safe_tac HOL_cs ); 

1465  341 
by (dtac mgu_Ok 1); 
2031  342 
by ( fast_tac (HOL_cs addss !simpset) 1); 
1300  343 
by (REPEAT (resolve_tac [exI,conjI] 1)); 
344 
by (fast_tac HOL_cs 1); 

345 
by (fast_tac HOL_cs 1); 

346 
by ((dtac mgu_mg 1) THEN (atac 1)); 

1465  347 
by (etac exE 1); 
1300  348 
by (res_inst_tac [("x","rb")] exI 1); 
1465  349 
by (rtac conjI 1); 
1300  350 
by (dres_inst_tac [("x","ma")] fun_cong 2); 
2031  351 
by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2); 
1300  352 
by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1); 
1400  353 
by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
1300  354 
(2,trans)) 1); 
2031  355 
by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1); 
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

356 
(** LEVEL 90 **) 
1465  357 
by (rtac eq_free_eq_subst_tel 1); 
2031  358 
by ( safe_tac HOL_cs ); 
1300  359 
by (subgoal_tac "ma ~= na" 1); 
360 
by ((forward_tac [new_tv_W] 2) THEN (atac 2)); 

1465  361 
by (etac conjE 2); 
362 
by (dtac new_tv_subst_tel 2); 

1300  363 
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2); 
1486  364 
by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2)); 
1465  365 
by (etac conjE 2); 
366 
by (dtac (free_tv_app_subst_tel RS subsetD) 2); 

2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

367 
(** LEVEL 100 **) 
1300  368 
by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD, 
369 
new_tv_not_free_tv]) 2); 

370 
by (case_tac "na: free_tv t  free_tv sa" 1); 

371 
(* case na ~: free_tv t  free_tv sa *) 

372 
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2); 

373 
(* case na : free_tv t  free_tv sa *) 

374 
by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); 

1465  375 
by (dtac (free_tv_app_subst_tel RS subsetD) 1); 
1300  376 
by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans), 
2083
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

377 
eq_subst_tel_eq_free] 
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

378 
addss ((!simpset addsimps [de_Morgan_disj,free_tv_subst,dom_def]))) 1); 
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

379 
(** LEVEL 106 **) 
b56425a385b9
Tidied some proofs: changed needed for de Morgan laws
paulson
parents:
2058
diff
changeset

380 
by (Fast_tac 1); 
1525  381 
qed_spec_mp "W_complete_lemma"; 
382 

383 
goal W.thy 

384 
"!!e. []  e :: t' ==> (? s t. (? m. W e [] n = Ok(s,t,m)) & \ 

385 
\ (? r. t' = $r t))"; 

2031  386 
by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")] 
1525  387 
W_complete_lemma 1); 
2031  388 
by (ALLGOALS Asm_full_simp_tac); 
1525  389 
qed "W_complete"; 