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 


12 
(* stronger version of Suc_leD *)


13 
goalw Nat.thy [le_def]

1465

14 
"!!m. Suc m <= n ==> m < n";

1669

15 
by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);

1300

16 
by (cut_facts_tac [less_linear] 1);


17 
by (fast_tac HOL_cs 1);


18 
qed "Suc_le_lessD";


19 
Addsimps [Suc_le_lessD];


20 


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

1525

22 
goal W.thy


23 
"!a s t m n . Ok (s,t,m) = W e a n > $s a  e :: t";

1300

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


25 
(* case Var n *)


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


27 
(* case Abs e *)


28 
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]


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


30 
by (strip_tac 1);


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


32 
by( fast_tac (HOL_cs addss (!simpset addsimps [eq_sym_conv])) 1);


33 
(* case App e1 e2 *)


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


35 
by (strip_tac 1);


36 
by( rename_tac "sa ta na sb tb nb sc" 1);


37 
by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);


38 
by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1);


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

1525

40 
by (res_inst_tac [("t","$sc(tb > (TVar nb))"),("s","$sc($sb ta)")] subst 1);

1300

41 
by (Asm_full_simp_tac 1);


42 
by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);


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


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

1669

45 
by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);

1486

46 
qed_spec_mp "W_correct";

1300

47 


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

1465

49 
[" s  Var n :: t"," s  Abs e :: t","s  App e1 e2 ::t"];

1300

50 


51 


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


53 
goal thy

1465

54 
"!a n s t m. W e a n = Ok (s,t,m) > n<=m";

1300

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


56 
(* case Var(n) *)


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


58 
(* case Abs e *)


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


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


61 
(* case App e1 e2 *)


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


63 
by (strip_tac 1);


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


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


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


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


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


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


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


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


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


73 
by (etac conjE 1);


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


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


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


77 
by (etac conjE 1);


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


79 
by (Asm_simp_tac 1);

1669

80 
by (Asm_simp_tac 1);

1486

81 
qed_spec_mp "W_var_ge";

1300

82 


83 
Addsimps [W_var_ge];


84 


85 
goal thy

1465

86 
"!! s. Ok (s,t,m) = W e a n ==> n<=m";

1300

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


88 
qed "W_var_geD";


89 


90 


91 
(* auxiliary lemma *)


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


93 
by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);


94 
qed "rotate_Ok";


95 


96 


97 
(* resulting type variable is new *)


98 
goal thy


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

1525

100 
\ new_tv m s & new_tv m t";

1300

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


102 
(* case Var n *)


103 
by (fast_tac (HOL_cs addss (!simpset

1465

104 
addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst]

1300

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


106 


107 
(* case Abs e *)


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


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


110 
by (strip_tac 1);


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


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


113 
by (fast_tac (HOL_cs addss (!simpset

1465

114 
addsimps [new_tv_subst,new_tv_Suc_list])) 1);

1300

115 


116 
(* case App e1 e2 *)


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


118 
by (strip_tac 1);


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


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


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


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


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


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


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


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


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


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


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


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

1669

131 
by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);

1300

132 
by (rtac conjI 1);


133 
by (rtac new_tv_subst_comp_2 1);


134 
by (rtac new_tv_subst_comp_2 1);


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


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


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


138 
by (Asm_simp_tac 1);


139 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs


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


141 
1);

1465

142 
by (etac (sym RS mgu_new) 1);

1300

143 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs [new_tv_subst_te,new_tv_list_le,


144 
new_tv_subst_tel,lessI RS less_imp_le RS new_tv_le,lessI RS less_imp_le RS


145 
new_tv_subst_le,new_tv_le]) 1);


146 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs


147 
[new_tv_list_le,new_tv_subst_tel,new_tv_le]

1465

148 
addss (!simpset)) 1);


149 
by (rtac (lessI RS new_tv_subst_var) 1);


150 
by (etac (sym RS mgu_new) 1);

1300

151 
by (fast_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te]


152 
addDs [W_var_geD] addIs


153 
[new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS


154 
new_tv_subst_le,new_tv_le] addss !simpset) 1);


155 
by (fast_tac (HOL_cs addDs [W_var_geD] addIs


156 
[new_tv_list_le,new_tv_subst_tel,new_tv_le]


157 
addss (!simpset)) 1);

1486

158 
qed_spec_mp "new_tv_W";

1300

159 


160 


161 
goal thy

1465

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

1300

163 
\ (v:free_tv s  v:free_tv t) > v<n > v:free_tv a";


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


165 
(* case Var n *)


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


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


168 


169 
(* case Abs e *)


170 
by (asm_full_simp_tac (!simpset addsimps


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


172 
by (strip_tac 1);


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


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


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


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


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


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


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

1669

180 
by (fast_tac (HOL_cs addIs [cod_app_subst]


181 
addss (!simpset addsimps [less_Suc_eq])) 1);

1300

182 


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);


194 
(* second case *)


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


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


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


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


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


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

1669

201 
by (asm_full_simp_tac (!simpset addsimps [rotate_Ok,o_def]) 1);

1465

202 
by (dtac W_var_geD 1);


203 
by (dtac W_var_geD 1);

1300

204 
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );


205 
by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free,


206 
codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,


207 
less_le_trans,less_not_refl2,subsetD]


208 
addEs [UnE]


209 
addss !simpset) 1);


210 
by (Asm_full_simp_tac 1);

1465

211 
by (dtac (sym RS W_var_geD) 1);


212 
by (dtac (sym RS W_var_geD) 1);

1300

213 
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );


214 
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD,


215 
free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD,


216 
less_le_trans,subsetD]


217 
addEs [UnE]


218 
addss !simpset) 1);

1486

219 
qed_spec_mp "free_tv_W";

1300

220 


221 
(* Completeness of W w.r.t. has_type *)


222 
goal thy

1525

223 
"!s' a t' n. $s' a  e :: t' > new_tv n a > \


224 
\ (? s t. (? m. W e a n = Ok (s,t,m)) & \


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

1300

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


227 
(* case Var n *)


228 
by (strip_tac 1);


229 
by (simp_tac (!simpset addcongs [conj_cong]


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


231 
by (eresolve_tac has_type_casesE 1);


232 
by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);


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


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


235 
by (Simp_tac 1);


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


237 
by (Asm_simp_tac 1);


238 


239 
(* case Abs e *)


240 
by (strip_tac 1);


241 
by (eresolve_tac has_type_casesE 1);


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


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


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


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


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


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


248 


249 
(* case App e1 e2 *)


250 
by (strip_tac 1);


251 
by (eresolve_tac has_type_casesE 1);


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


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

1400

254 
by (eres_inst_tac [("x","t2 > t'")] allE 1);

1300

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


256 
by (safe_tac HOL_cs);


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


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


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


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

1465

261 
by (dtac asm_rl 1);


262 
by (dtac asm_rl 1);


263 
by (dtac asm_rl 1);

1300

264 
by (Asm_full_simp_tac 1);


265 
by (safe_tac HOL_cs);


266 
by (fast_tac HOL_cs 1);


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

1465

268 
conjunct1,new_tv_list_le,new_tv_subst_tel]) 1);

1300

269 


270 
by (subgoal_tac


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


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


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

1400

274 
\ else ra x)) (ta > (TVar ma))" 1);

1300

275 
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \


276 
\ (if x:(free_tv t  free_tv sa) then r x else ra x)) ($ sa t)"),

1400

277 
("s","($ ra ta) > t'")] ssubst 2);

1300

278 
by (asm_simp_tac (!simpset addsimps [subst_comp_te]) 2);

1465

279 
by (rtac eq_free_eq_subst_te 2);

1300

280 
by (strip_tac 2);


281 
by (subgoal_tac "na ~=ma" 2);


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


283 
new_tv_not_free_tv,new_tv_le]) 3);


284 
by (case_tac "na:free_tv sa" 2);


285 
(* na ~: free_tv sa *)


286 
by (asm_simp_tac (!simpset addsimps [not_free_impl_id]


287 
setloop (split_tac [expand_if])) 3);


288 
(* na : free_tv sa *)

1400

289 
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);

1465

290 
by (dtac eq_subst_tel_eq_free 2);

1300

291 
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);


292 
by (Asm_simp_tac 2);


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


294 
(* na ~: dom sa *)


295 
by (asm_full_simp_tac (!simpset addsimps [dom_def]


296 
setloop (split_tac [expand_if])) 3);


297 
(* na : dom sa *)

1465

298 
by (rtac eq_free_eq_subst_te 2);

1300

299 
by (strip_tac 2);


300 
by (subgoal_tac "nb ~= ma" 2);


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

1465

302 
by (etac conjE 3);


303 
by (dtac new_tv_subst_tel 3);

1300

304 
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);


305 
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss


306 
(!simpset addsimps [cod_def,free_tv_subst])) 3);


307 
by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst]


308 
setloop (split_tac [expand_if]))) 2);


309 


310 
by (Simp_tac 2);

1465

311 
by (rtac eq_free_eq_subst_te 2);

1300

312 
by (strip_tac 2 );


313 
by (subgoal_tac "na ~= ma" 2);


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

1465

315 
by (etac conjE 3);


316 
by (dtac (sym RS W_var_geD) 3);

1300

317 
by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3);


318 
by (case_tac "na: free_tv t  free_tv sa" 2);


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


320 
by( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);


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


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

1400

323 
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);

1465

324 
by (dtac eq_subst_tel_eq_free 2);

1300

325 
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);

1486

326 
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 2);

1300

327 


328 
by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);


329 
by (safe_tac HOL_cs );

1465

330 
by (dtac mgu_Ok 1);

1300

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


332 
by (REPEAT (resolve_tac [exI,conjI] 1));


333 
by (fast_tac HOL_cs 1);


334 
by (fast_tac HOL_cs 1);


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

1465

336 
by (etac exE 1);

1300

337 
by (res_inst_tac [("x","rb")] exI 1);

1465

338 
by (rtac conjI 1);

1300

339 
by (dres_inst_tac [("x","ma")] fun_cong 2);


340 
by( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);


341 
by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);

1400

342 
by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN

1300

343 
(2,trans)) 1);


344 
by( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);

1465

345 
by (rtac eq_free_eq_subst_tel 1);

1300

346 
by( safe_tac HOL_cs );


347 
by (subgoal_tac "ma ~= na" 1);


348 
by ((forward_tac [new_tv_W] 2) THEN (atac 2));

1465

349 
by (etac conjE 2);


350 
by (dtac new_tv_subst_tel 2);

1300

351 
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2);

1486

352 
by (( forw_inst_tac [("n","m")] (sym RSN (2,new_tv_W)) 2) THEN (atac 2));

1465

353 
by (etac conjE 2);


354 
by (dtac (free_tv_app_subst_tel RS subsetD) 2);

1300

355 
by (fast_tac (set_cs addDs [W_var_geD,new_tv_list_le,codD,


356 
new_tv_not_free_tv]) 2);


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


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


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


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


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

1465

362 
by (dtac (free_tv_app_subst_tel RS subsetD) 1);

1300

363 
by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),


364 
eq_subst_tel_eq_free] addss ((!simpset addsimps

1486

365 
[de_Morgan_disj,free_tv_subst,dom_def]))) 1);

1525

366 
qed_spec_mp "W_complete_lemma";


367 


368 
goal W.thy


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


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


371 
by(cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]


372 
W_complete_lemma 1);


373 
by(ALLGOALS Asm_full_simp_tac);


374 
qed "W_complete";
