author | wenzelm |
Mon, 22 Jun 1998 17:26:46 +0200 | |
changeset 5069 | 3ea049f7979d |
parent 4831 | dae4d63a1318 |
child 5148 | 74919e8f221c |
permissions | -rw-r--r-- |
2520 | 1 |
(* Title: HOL/W0/W.ML |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
3 |
Author: Dieter Nazareth and Tobias Nipkow |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
4 |
Copyright 1995 TU Muenchen |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
5 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
6 |
Correctness and completeness of type inference algorithm W |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
7 |
*) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
8 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
9 |
Addsimps [Suc_le_lessD]; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
10 |
Delsimps (ex_simps @ all_simps); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
11 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
12 |
(* correctness of W with respect to has_type *) |
5069 | 13 |
Goal |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
14 |
"!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
15 |
by (expr.induct_tac "e" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
16 |
(* case Var n *) |
4686 | 17 |
by (Asm_simp_tac 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
18 |
(* case Abs e *) |
4089 | 19 |
by (asm_full_simp_tac (simpset() addsimps [app_subst_list] |
4831 | 20 |
addsplits [split_bind]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
21 |
by (strip_tac 1); |
3018 | 22 |
by (dtac sym 1); |
4089 | 23 |
by (fast_tac (HOL_cs addss simpset()) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
24 |
(* case App e1 e2 *) |
4831 | 25 |
by (simp_tac (simpset() addsplits [split_bind]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
26 |
by (strip_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
27 |
by ( rename_tac "sa ta na sb tb nb sc" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
28 |
by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
29 |
by (res_inst_tac [("s1","sc")] (app_subst_TVar RS subst) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
30 |
by (rtac (app_subst_Fun RS subst) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
31 |
by (res_inst_tac [("t","$sc(tb -> (TVar nb))"),("s","$sc($sb ta)")] subst 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
32 |
by (Asm_full_simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
33 |
by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
34 |
by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1)); |
4089 | 35 |
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
36 |
by (asm_full_simp_tac (simpset() addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1); |
|
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
37 |
qed_spec_mp "W_correct"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
38 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
39 |
val has_type_casesE = map(has_type.mk_cases expr.simps) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
40 |
[" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"]; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
41 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
42 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
43 |
(* the resulting type variable is always greater or equal than the given one *) |
5069 | 44 |
Goal |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
45 |
"!a n s t m. W e a n = Ok (s,t,m) --> n<=m"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
46 |
by (expr.induct_tac "e" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
47 |
(* case Var(n) *) |
4686 | 48 |
by (fast_tac (HOL_cs addss simpset()) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
49 |
(* case Abs e *) |
4831 | 50 |
by (simp_tac (simpset() addsplits [split_bind]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
51 |
by (fast_tac (HOL_cs addDs [Suc_leD]) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
52 |
(* case App e1 e2 *) |
4831 | 53 |
by (simp_tac (simpset() addsplits [split_bind]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
54 |
by (strip_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
55 |
by (rename_tac "s t na sa ta nb sb sc tb m" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
56 |
by (eres_inst_tac [("x","a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
57 |
by (eres_inst_tac [("x","n")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
58 |
by (eres_inst_tac [("x","$ s a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
59 |
by (eres_inst_tac [("x","s")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
60 |
by (eres_inst_tac [("x","t")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
61 |
by (eres_inst_tac [("x","na")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
62 |
by (eres_inst_tac [("x","na")] allE 1); |
4089 | 63 |
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
64 |
by (etac conjE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
65 |
by (eres_inst_tac [("x","sa")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
66 |
by (eres_inst_tac [("x","ta")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
67 |
by (eres_inst_tac [("x","nb")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
68 |
by (res_inst_tac [("j","na")] le_trans 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
69 |
by (Asm_simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
70 |
by (Asm_simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
71 |
qed_spec_mp "W_var_ge"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
72 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
73 |
Addsimps [W_var_ge]; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
74 |
|
5069 | 75 |
Goal |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
76 |
"!! s. Ok (s,t,m) = W e a n ==> n<=m"; |
4089 | 77 |
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
78 |
qed "W_var_geD"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
79 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
80 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
81 |
(* auxiliary lemma *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
82 |
goal Maybe.thy "(y = Ok x) = (Ok x = y)"; |
4089 | 83 |
by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
84 |
qed "rotate_Ok"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
85 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
86 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
87 |
(* resulting type variable is new *) |
5069 | 88 |
Goal |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
89 |
"!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) --> \ |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
90 |
\ new_tv m s & new_tv m t"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
91 |
by (expr.induct_tac "e" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
92 |
(* case Var n *) |
4089 | 93 |
by (fast_tac (HOL_cs addDs [list_all_nth] addss (simpset() |
4686 | 94 |
addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
95 |
(* case Abs e *) |
4089 | 96 |
by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] |
4831 | 97 |
addsplits [split_bind]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
98 |
by (strip_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
99 |
by (eres_inst_tac [("x","Suc n")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
100 |
by (eres_inst_tac [("x","(TVar n)#a")] allE 1); |
4089 | 101 |
by (fast_tac (HOL_cs addss (simpset() |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
102 |
addsimps [new_tv_subst,new_tv_Suc_list])) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
103 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
104 |
(* case App e1 e2 *) |
4831 | 105 |
by (simp_tac (simpset() addsplits [split_bind]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
106 |
by (strip_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
107 |
by (rename_tac "s t na sa ta nb sb sc tb m" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
108 |
by (eres_inst_tac [("x","n")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
109 |
by (eres_inst_tac [("x","a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
110 |
by (eres_inst_tac [("x","s")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
111 |
by (eres_inst_tac [("x","t")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
112 |
by (eres_inst_tac [("x","na")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
113 |
by (eres_inst_tac [("x","na")] allE 1); |
4089 | 114 |
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
115 |
by (eres_inst_tac [("x","$ s a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
116 |
by (eres_inst_tac [("x","sa")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
117 |
by (eres_inst_tac [("x","ta")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
118 |
by (eres_inst_tac [("x","nb")] allE 1); |
4089 | 119 |
by ( asm_full_simp_tac (simpset() addsimps [o_def,rotate_Ok]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
120 |
by (rtac conjI 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
121 |
by (rtac new_tv_subst_comp_2 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
122 |
by (rtac new_tv_subst_comp_2 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
123 |
by (rtac (lessI RS less_imp_le RS new_tv_subst_le) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
124 |
by (res_inst_tac [("n","na")] new_tv_subst_le 1); |
4089 | 125 |
by (asm_full_simp_tac (simpset() addsimps [rotate_Ok]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
126 |
by (Asm_simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
127 |
by (fast_tac (HOL_cs addDs [W_var_geD] addIs |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
128 |
[new_tv_list_le,new_tv_subst_tel,lessI RS less_imp_le RS new_tv_subst_le]) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
129 |
1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
130 |
by (etac (sym RS mgu_new) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
131 |
by (best_tac (HOL_cs addDs [W_var_geD] |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
132 |
addIs [new_tv_subst_te,new_tv_list_le, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
133 |
new_tv_subst_tel, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
134 |
lessI RS less_imp_le RS new_tv_le, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
135 |
lessI RS less_imp_le RS new_tv_subst_le, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
136 |
new_tv_le]) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
137 |
by (fast_tac (HOL_cs addDs [W_var_geD] |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
138 |
addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] |
4089 | 139 |
addss (simpset())) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
140 |
by (rtac (lessI RS new_tv_subst_var) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
141 |
by (etac (sym RS mgu_new) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
142 |
by (best_tac (HOL_cs addSIs [lessI RS less_imp_le RS new_tv_le,new_tv_subst_te] |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
143 |
addDs [W_var_geD] |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
144 |
addIs [new_tv_list_le, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
145 |
new_tv_subst_tel, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
146 |
lessI RS less_imp_le RS new_tv_subst_le, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
147 |
new_tv_le] |
4089 | 148 |
addss simpset()) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
149 |
by (fast_tac (HOL_cs addDs [W_var_geD] |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
150 |
addIs [new_tv_list_le,new_tv_subst_tel,new_tv_le] |
4089 | 151 |
addss (simpset())) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
152 |
qed_spec_mp "new_tv_W"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
153 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
154 |
|
5069 | 155 |
Goal |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
156 |
"!n a s t m v. W e a n = Ok (s,t,m) --> \ |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
157 |
\ (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
158 |
by (expr.induct_tac "e" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
159 |
(* case Var n *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
160 |
by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] |
4686 | 161 |
addss simpset()) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
162 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
163 |
(* case Abs e *) |
4089 | 164 |
by (asm_full_simp_tac (simpset() addsimps |
4831 | 165 |
[free_tv_subst] addsplits [split_bind]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
166 |
by (strip_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
167 |
by (rename_tac "s t na sa ta m v" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
168 |
by (eres_inst_tac [("x","Suc n")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
169 |
by (eres_inst_tac [("x","TVar n # a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
170 |
by (eres_inst_tac [("x","s")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
171 |
by (eres_inst_tac [("x","t")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
172 |
by (eres_inst_tac [("x","na")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
173 |
by (eres_inst_tac [("x","v")] allE 1); |
2520 | 174 |
by (fast_tac (HOL_cs addSEs [allE] |
3008 | 175 |
addIs [cod_app_subst] |
4089 | 176 |
addss (simpset() addsimps [less_Suc_eq])) 1); |
2520 | 177 |
(** LEVEL 12 **) |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
178 |
(* case App e1 e2 *) |
4831 | 179 |
by (simp_tac (simpset() addsplits [split_bind]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
180 |
by (strip_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
181 |
by (rename_tac "s t na sa ta nb sb sc tb m v" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
182 |
by (eres_inst_tac [("x","n")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
183 |
by (eres_inst_tac [("x","a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
184 |
by (eres_inst_tac [("x","s")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
185 |
by (eres_inst_tac [("x","t")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
186 |
by (eres_inst_tac [("x","na")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
187 |
by (eres_inst_tac [("x","na")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
188 |
by (eres_inst_tac [("x","v")] allE 1); |
2520 | 189 |
(** LEVEL 22 **) |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
190 |
(* second case *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
191 |
by (eres_inst_tac [("x","$ s a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
192 |
by (eres_inst_tac [("x","sa")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
193 |
by (eres_inst_tac [("x","ta")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
194 |
by (eres_inst_tac [("x","nb")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
195 |
by (eres_inst_tac [("x","v")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
196 |
by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); |
4089 | 197 |
by (asm_full_simp_tac (simpset() addsimps [rotate_Ok,o_def]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
198 |
by (dtac W_var_geD 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
199 |
by (dtac W_var_geD 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
200 |
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); |
2520 | 201 |
(** LEVEL 32 **) |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
202 |
by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
203 |
codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
204 |
less_le_trans,less_not_refl2,subsetD] |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
205 |
addEs [UnE] |
4089 | 206 |
addss simpset()) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
207 |
by (Asm_full_simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
208 |
by (dtac (sym RS W_var_geD) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
209 |
by (dtac (sym RS W_var_geD) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
210 |
by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
211 |
by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD, |
3008 | 212 |
free_tv_app_subst_te RS subsetD, |
213 |
free_tv_app_subst_tel RS subsetD, |
|
214 |
less_le_trans,subsetD] |
|
215 |
addSEs [UnE] |
|
4089 | 216 |
addss simpset()) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
217 |
qed_spec_mp "free_tv_W"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
218 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
219 |
(* Completeness of W w.r.t. has_type *) |
5069 | 220 |
Goal |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
221 |
"!s' a t' n. $s' a |- e :: t' --> new_tv n a --> \ |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
222 |
\ (? s t. (? m. W e a n = Ok (s,t,m)) & \ |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
223 |
\ (? r. $s' a = $r ($s a) & t' = $r t))"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
224 |
by (expr.induct_tac "e" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
225 |
(* case Var n *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
226 |
by (strip_tac 1); |
4686 | 227 |
by (simp_tac (simpset() addcongs [conj_cong]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
228 |
by (eresolve_tac has_type_casesE 1); |
4089 | 229 |
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv,app_subst_list]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
230 |
by (res_inst_tac [("x","s'")] exI 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
231 |
by (Asm_simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
232 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
233 |
(** LEVEL 10 **) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
234 |
(* case Abs e *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
235 |
by (strip_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
236 |
by (eresolve_tac has_type_casesE 1); |
3842 | 237 |
by (eres_inst_tac [("x","%x. if x=n then t1 else (s' x)")] allE 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
238 |
by (eres_inst_tac [("x","(TVar n)#a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
239 |
by (eres_inst_tac [("x","t2")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
240 |
by (eres_inst_tac [("x","Suc n")] allE 1); |
4089 | 241 |
by (fast_tac (HOL_cs addss (simpset() addcongs [conj_cong] |
4831 | 242 |
addsplits [split_bind])) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
243 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
244 |
(** LEVEL 17 **) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
245 |
(* case App e1 e2 *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
246 |
by (strip_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
247 |
by (eresolve_tac has_type_casesE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
248 |
by (eres_inst_tac [("x","s'")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
249 |
by (eres_inst_tac [("x","a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
250 |
by (eres_inst_tac [("x","t2 -> t'")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
251 |
by (eres_inst_tac [("x","n")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
252 |
by (safe_tac HOL_cs); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
253 |
by (eres_inst_tac [("x","r")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
254 |
by (eres_inst_tac [("x","$ s a")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
255 |
by (eres_inst_tac [("x","t2")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
256 |
by (eres_inst_tac [("x","m")] allE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
257 |
by (Asm_full_simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
258 |
by (safe_tac HOL_cs); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
259 |
by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
260 |
conjunct1,new_tv_list_le,new_tv_subst_tel]) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
261 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
262 |
(** LEVEL 35 **) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
263 |
by (subgoal_tac |
3842 | 264 |
"$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \ |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
265 |
\ else ra x)) ($ sa t) = \ |
3842 | 266 |
\ $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \ |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
267 |
\ else ra x)) (ta -> (TVar ma))" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
268 |
by (res_inst_tac [("t","$ (%x. if x = ma then t' else \ |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
269 |
\ (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"), |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
270 |
("s","($ ra ta) -> t'")] ssubst 2); |
4089 | 271 |
by (asm_simp_tac (simpset() addsimps [subst_comp_te]) 2); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
272 |
by (rtac eq_free_eq_subst_te 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
273 |
by (strip_tac 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
274 |
by (subgoal_tac "na ~=ma" 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
275 |
by (fast_tac (HOL_cs addDs [new_tv_W,sym RS W_var_geD, |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
276 |
new_tv_not_free_tv,new_tv_le]) 3); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
277 |
(** LEVEL 42 **) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
278 |
by (case_tac "na:free_tv sa" 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
279 |
(* na ~: free_tv sa *) |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
280 |
by (forward_tac [not_free_impl_id] 3); |
4686 | 281 |
by (Asm_simp_tac 3); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
282 |
(* na : free_tv sa *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
283 |
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
284 |
by (dtac eq_subst_tel_eq_free 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
285 |
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
286 |
by (Asm_simp_tac 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
287 |
by (case_tac "na:dom sa" 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
288 |
(* na ~: dom sa *) |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
289 |
(** LEVEL 50 **) |
4686 | 290 |
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
291 |
(* na : dom sa *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
292 |
by (rtac eq_free_eq_subst_te 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
293 |
by (strip_tac 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
294 |
by (subgoal_tac "nb ~= ma" 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
295 |
by ((forward_tac [new_tv_W] 3) THEN (atac 3)); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
296 |
by (etac conjE 3); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
297 |
by (dtac new_tv_subst_tel 3); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
298 |
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
299 |
by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss |
4089 | 300 |
(simpset() addsimps [cod_def,free_tv_subst])) 3); |
4686 | 301 |
by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
302 |
|
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
303 |
(** LEVEL 60 **) |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
304 |
by (Simp_tac 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
305 |
by (rtac eq_free_eq_subst_te 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
306 |
by (strip_tac 2 ); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
307 |
by (subgoal_tac "na ~= ma" 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
308 |
by ((forward_tac [new_tv_W] 3) THEN (atac 3)); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
309 |
by (etac conjE 3); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
310 |
by (dtac (sym RS W_var_geD) 3); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
311 |
by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
312 |
by (case_tac "na: free_tv t - free_tv sa" 2); |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
313 |
(** LEVEL 69 **) |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
314 |
(* case na ~: free_tv t - free_tv sa *) |
4686 | 315 |
by (Asm_full_simp_tac 3); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
316 |
(* case na : free_tv t - free_tv sa *) |
4686 | 317 |
by (Asm_full_simp_tac 2); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
318 |
by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
319 |
by (dtac eq_subst_tel_eq_free 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
320 |
by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2); |
4089 | 321 |
by (asm_full_simp_tac (simpset() addsimps [free_tv_subst,dom_def]) 2); |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
322 |
by (Fast_tac 2); |
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
323 |
(** LEVEL 76 **) |
4831 | 324 |
by (asm_simp_tac (simpset() addsplits [split_bind]) 1); |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
325 |
by (safe_tac HOL_cs); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
326 |
by (dtac mgu_Ok 1); |
4089 | 327 |
by ( fast_tac (HOL_cs addss simpset()) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
328 |
by ((dtac mgu_mg 1) THEN (atac 1)); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
329 |
by (etac exE 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
330 |
by (res_inst_tac [("x","rb")] exI 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
331 |
by (rtac conjI 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
332 |
by (dres_inst_tac [("x","ma")] fun_cong 2); |
4089 | 333 |
by ( asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 2); |
334 |
by (simp_tac (simpset() addsimps [o_def,subst_comp_tel RS sym]) 1); |
|
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
335 |
(** LEVEL 90 **) |
2596
3b4ad6c7726f
Modified proofs because of added "triv_forall_equality".
nipkow
parents:
2520
diff
changeset
|
336 |
by (rtac ((subst_comp_tel RS sym) RSN (2,trans)) 1); |
4089 | 337 |
by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
338 |
by (rtac eq_free_eq_subst_tel 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
339 |
by ( safe_tac HOL_cs ); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
340 |
by (subgoal_tac "ma ~= na" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
341 |
by ((forward_tac [new_tv_W] 2) THEN (atac 2)); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
342 |
by (etac conjE 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
343 |
by (dtac new_tv_subst_tel 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
344 |
by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2); |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
345 |
by (forw_inst_tac [("n","m")] new_tv_W 2 THEN atac 2); |
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
346 |
(** LEVEL 100 **) |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
347 |
by (etac conjE 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
348 |
by (dtac (free_tv_app_subst_tel RS subsetD) 2); |
2793
b30c41754c86
Modified proofs because simplifier does not eta-contract any longer.
nipkow
parents:
2637
diff
changeset
|
349 |
by (fast_tac (set_cs addDs [sym RS W_var_geD,new_tv_list_le,codD, |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
350 |
new_tv_not_free_tv]) 2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
351 |
by (case_tac "na: free_tv t - free_tv sa" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
352 |
(* case na ~: free_tv t - free_tv sa *) |
4686 | 353 |
by (Asm_full_simp_tac 2); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
354 |
(* case na : free_tv t - free_tv sa *) |
4686 | 355 |
by (Asm_full_simp_tac 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
356 |
by (dtac (free_tv_app_subst_tel RS subsetD) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
357 |
by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans), |
3008 | 358 |
eq_subst_tel_eq_free] |
4089 | 359 |
addss ((simpset() addsimps [free_tv_subst,dom_def]))) 1); |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
360 |
(** LEVEL 106 **) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
361 |
by (Fast_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
362 |
qed_spec_mp "W_complete_lemma"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
363 |
|
5069 | 364 |
Goal |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
365 |
"!!e. [] |- e :: t' ==> (? s t. (? m. W e [] n = Ok(s,t,m)) & \ |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
366 |
\ (? r. t' = $r t))"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
367 |
by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")] |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
368 |
W_complete_lemma 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
369 |
by (ALLGOALS Asm_full_simp_tac); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
370 |
qed "W_complete"; |