17 by (fast_tac HOL_cs 1); |
17 by (fast_tac HOL_cs 1); |
18 qed "Suc_le_lessD"; |
18 qed "Suc_le_lessD"; |
19 Addsimps [Suc_le_lessD]; |
19 Addsimps [Suc_le_lessD]; |
20 |
20 |
21 (* correctness of W with respect to has_type *) |
21 (* correctness of W with respect to has_type *) |
22 goal thy |
22 goal W.thy |
23 "!a s t m n . Ok (s,t,m) = W e a n --> ($ s a |- e :: t)"; |
23 "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t"; |
24 by (expr.induct_tac "e" 1); |
24 by (expr.induct_tac "e" 1); |
25 (* case Var n *) |
25 (* case Var n *) |
26 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
26 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
27 (* case Abs e *) |
27 (* case Abs e *) |
28 by (asm_full_simp_tac (!simpset addsimps [app_subst_list] |
28 by (asm_full_simp_tac (!simpset addsimps [app_subst_list] |
35 by (strip_tac 1); |
35 by (strip_tac 1); |
36 by( rename_tac "sa ta na sb tb nb sc" 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); |
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); |
38 by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1); |
39 by (rtac (app_subst_Fun RS subst) 1); |
39 by (rtac (app_subst_Fun RS subst) 1); |
40 by (res_inst_tac [("t","$ sc (tb -> (TVar nb))"),("s","$ sc ($ sb ta)")] subst 1); |
40 by (res_inst_tac [("t","$sc(tb -> (TVar nb))"),("s","$sc($sb ta)")] subst 1); |
41 by (Asm_full_simp_tac 1); |
41 by (Asm_full_simp_tac 1); |
42 by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 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)); |
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); |
44 by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
45 by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,has_type_cl_sub,eq_sym_conv]) 1); |
45 by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,has_type_cl_sub,eq_sym_conv]) 1); |
95 |
95 |
96 |
96 |
97 (* resulting type variable is new *) |
97 (* resulting type variable is new *) |
98 goal thy |
98 goal thy |
99 "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) --> \ |
99 "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) --> \ |
100 \ (new_tv m s & new_tv m t)"; |
100 \ new_tv m s & new_tv m t"; |
101 by (expr.induct_tac "e" 1); |
101 by (expr.induct_tac "e" 1); |
102 (* case Var n *) |
102 (* case Var n *) |
103 by (fast_tac (HOL_cs addss (!simpset |
103 by (fast_tac (HOL_cs addss (!simpset |
104 addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] |
104 addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] |
105 setloop (split_tac [expand_if]))) 1); |
105 setloop (split_tac [expand_if]))) 1); |
217 addss !simpset) 1); |
217 addss !simpset) 1); |
218 qed_spec_mp "free_tv_W"; |
218 qed_spec_mp "free_tv_W"; |
219 |
219 |
220 (* Completeness of W w.r.t. has_type *) |
220 (* Completeness of W w.r.t. has_type *) |
221 goal thy |
221 goal thy |
222 "!s' a t' n. ($ s' a |- e :: t') --> new_tv n a --> \ |
222 "!s' a t' n. $s' a |- e :: t' --> new_tv n a --> \ |
223 \ (? s t. (? m. W e a n = Ok (s,t,m) ) & \ |
223 \ (? s t. (? m. W e a n = Ok (s,t,m)) & \ |
224 \ (? r. $ s' a = $ r ($ s a) & \ |
224 \ (? r. $s' a = $r ($s a) & t' = $r t))"; |
225 \ t' = $ r t ) )"; |
|
226 by (expr.induct_tac "e" 1); |
225 by (expr.induct_tac "e" 1); |
227 (* case Var n *) |
226 (* case Var n *) |
228 by (strip_tac 1); |
227 by (strip_tac 1); |
229 by (simp_tac (!simpset addcongs [conj_cong] |
228 by (simp_tac (!simpset addcongs [conj_cong] |
230 setloop (split_tac [expand_if])) 1); |
229 setloop (split_tac [expand_if])) 1); |
361 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
360 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
362 by (dtac (free_tv_app_subst_tel RS subsetD) 1); |
361 by (dtac (free_tv_app_subst_tel RS subsetD) 1); |
363 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans), |
362 by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans), |
364 eq_subst_tel_eq_free] addss ((!simpset addsimps |
363 eq_subst_tel_eq_free] addss ((!simpset addsimps |
365 [de_Morgan_disj,free_tv_subst,dom_def]))) 1); |
364 [de_Morgan_disj,free_tv_subst,dom_def]))) 1); |
366 qed_spec_mp "W_complete"; |
365 qed_spec_mp "W_complete_lemma"; |
|
366 |
|
367 goal W.thy |
|
368 "!!e. [] |- e :: t' ==> (? s t. (? m. W e [] n = Ok(s,t,m)) & \ |
|
369 \ (? r. t' = $r t))"; |
|
370 by(cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")] |
|
371 W_complete_lemma 1); |
|
372 by(ALLGOALS Asm_full_simp_tac); |
|
373 qed "W_complete"; |