2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Dieter Nazareth and Tobias Nipkow |
3 Author: Dieter Nazareth and Tobias Nipkow |
4 Copyright 1995 TU Muenchen |
4 Copyright 1995 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 open MiniML; |
|
8 |
|
9 Addsimps has_type.intrs; |
7 Addsimps has_type.intrs; |
10 Addsimps [Un_upper1,Un_upper2]; |
8 Addsimps [Un_upper1,Un_upper2]; |
11 |
9 |
|
10 Addsimps [is_bound_typ_instance_closed_subst]; |
|
11 |
|
12 |
|
13 goal thy "!!t::typ. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t = $S t"; |
|
14 by (rtac typ_substitutions_only_on_free_variables 1); |
|
15 by (asm_full_simp_tac (!simpset addsimps [Ball_def]) 1); |
|
16 qed "s'_t_equals_s_t"; |
|
17 |
|
18 Addsimps [s'_t_equals_s_t]; |
|
19 |
|
20 goal thy "!!A::type_scheme list. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A = $S A"; |
|
21 by (rtac scheme_list_substitutions_only_on_free_variables 1); |
|
22 by (asm_full_simp_tac (!simpset addsimps [Ball_def]) 1); |
|
23 qed "s'_a_equals_s_a"; |
|
24 |
|
25 Addsimps [s'_a_equals_s_a]; |
|
26 |
|
27 goal thy "!!S.($ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A |- e :: \ |
|
28 \ $ (%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t) ==> \ |
|
29 \ $S A |- e :: $S t"; |
|
30 |
|
31 by (res_inst_tac [("P","%A. A |- e :: $S t")] ssubst 1); |
|
32 by (rtac (s'_a_equals_s_a RS sym) 1); |
|
33 by (res_inst_tac [("P","%t. $ (%n. if n : free_tv A Un free_tv (?t1 S) then S n else TVar n) A |- e :: t")] ssubst 1); |
|
34 by (rtac (s'_t_equals_s_t RS sym) 1); |
|
35 by (Asm_full_simp_tac 1); |
|
36 qed "replace_s_by_s'"; |
|
37 |
|
38 goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = $ id_subst A"; |
|
39 by (rtac scheme_list_substitutions_only_on_free_variables 1); |
|
40 by (asm_full_simp_tac (!simpset addsimps [id_subst_def]) 1); |
|
41 qed "alpha_A'"; |
|
42 |
|
43 goal thy "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A"; |
|
44 by (rtac (alpha_A' RS ssubst) 1); |
|
45 by (Asm_full_simp_tac 1); |
|
46 qed "alpha_A"; |
|
47 |
|
48 goal thy "!!alpha. $ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)"; |
|
49 by (typ.induct_tac "t" 1); |
|
50 by (ALLGOALS (Asm_full_simp_tac)); |
|
51 qed "S_o_alpha_typ"; |
|
52 |
|
53 goal thy "!!alpha. $ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)"; |
|
54 by (typ.induct_tac "t" 1); |
|
55 by (ALLGOALS (Asm_full_simp_tac)); |
|
56 val S_o_alpha_typ' = result (); |
|
57 |
|
58 goal thy "!!alpha. $ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)"; |
|
59 by (type_scheme.induct_tac "sch" 1); |
|
60 by (ALLGOALS (Asm_full_simp_tac)); |
|
61 qed "S_o_alpha_type_scheme"; |
|
62 |
|
63 goal thy "!!alpha. $ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)"; |
|
64 by (list.induct_tac "A" 1); |
|
65 by (ALLGOALS (Asm_full_simp_tac)); |
|
66 by (rtac (rewrite_rule [o_def] S_o_alpha_type_scheme) 1); |
|
67 qed "S_o_alpha_type_scheme_list"; |
|
68 |
|
69 goal thy "!!A::type_scheme list. \ |
|
70 \ ($ (%n. if n : free_tv A Un free_tv t \ |
|
71 \ then S n else TVar n) \ |
|
72 \ A) = \ |
|
73 \ ($ ((%x. if x : free_tv A Un free_tv t then S x \ |
|
74 \ else TVar x) o \ |
|
75 \ (%x. if x : free_tv A \ |
|
76 \ then x else n + x)) A)"; |
|
77 by (rtac (S_o_alpha_type_scheme_list RS ssubst) 1); |
|
78 by (rtac (alpha_A RS ssubst) 1); |
|
79 by (rtac refl 1); |
|
80 qed "S'_A_eq_S'_alpha_A"; |
|
81 |
|
82 goalw thy [free_tv_subst,dom_def] |
|
83 "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \ |
|
84 \ free_tv A Un free_tv t"; |
|
85 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
86 by (Fast_tac 1); |
|
87 qed "dom_S'"; |
|
88 |
|
89 goalw thy [free_tv_subst,cod_def,subset_def] |
|
90 "!!(A::type_scheme list) (t::typ). \ |
|
91 \ cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \ |
|
92 \ free_tv ($ S A) Un free_tv ($ S t)"; |
|
93 by (rtac ballI 1); |
|
94 by (etac UN_E 1); |
|
95 by (dtac (dom_S' RS subsetD) 1); |
|
96 by (rotate_tac 1 1); |
|
97 by (Asm_full_simp_tac 1); |
|
98 by (fast_tac (!claset addDs [free_tv_of_substitutions_extend_to_scheme_lists] |
|
99 addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1); |
|
100 qed "cod_S'"; |
|
101 |
|
102 goalw thy [free_tv_subst] |
|
103 "!!(A::type_scheme list) (t::typ). \ |
|
104 \ free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \ |
|
105 \ free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)"; |
|
106 by (fast_tac (!claset addDs [dom_S' RS subsetD,cod_S' RS subsetD]) 1); |
|
107 qed "free_tv_S'"; |
|
108 |
|
109 goal thy "!!t1::typ. \ |
|
110 \ (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \ |
|
111 \ {x. ? y. x = n + y}"; |
|
112 by (typ.induct_tac "t1" 1); |
|
113 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
|
114 by (Fast_tac 1); |
|
115 by (Simp_tac 1); |
|
116 by (Fast_tac 1); |
|
117 qed "free_tv_alpha"; |
|
118 |
|
119 goal thy "!!(k::nat). n <= n + k"; |
|
120 by (res_inst_tac [("n","k")] nat_induct 1); |
|
121 by (Simp_tac 1); |
|
122 by (Asm_simp_tac 1); |
|
123 val aux_plus = result(); |
|
124 |
|
125 Addsimps [aux_plus]; |
|
126 |
|
127 goal thy "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}"; |
|
128 by (step_tac (!claset) 1); |
|
129 by (cut_facts_tac [aux_plus] 1); |
|
130 by (dtac new_tv_le 1); |
|
131 ba 1; |
|
132 by (rotate_tac 1 1); |
|
133 by (dtac new_tv_not_free_tv 1); |
|
134 by (Fast_tac 1); |
|
135 val new_tv_Int_free_tv_empty_type = result (); |
|
136 |
|
137 goal thy "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}"; |
|
138 by (step_tac (!claset) 1); |
|
139 by (cut_facts_tac [aux_plus] 1); |
|
140 by (dtac new_tv_le 1); |
|
141 ba 1; |
|
142 by (rotate_tac 1 1); |
|
143 by (dtac new_tv_not_free_tv 1); |
|
144 by (Fast_tac 1); |
|
145 val new_tv_Int_free_tv_empty_scheme = result (); |
|
146 |
|
147 goal thy "!!n. !A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}"; |
|
148 by (rtac allI 1); |
|
149 by (list.induct_tac "A" 1); |
|
150 by (Simp_tac 1); |
|
151 by (Simp_tac 1); |
|
152 by (fast_tac (!claset addDs [new_tv_Int_free_tv_empty_scheme ]) 1); |
|
153 val new_tv_Int_free_tv_empty_scheme_list = result (); |
|
154 |
|
155 goalw thy [le_type_scheme_def,is_bound_typ_instance] |
|
156 "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"; |
|
157 by (strip_tac 1); |
|
158 by (etac exE 1); |
|
159 by (hyp_subst_tac 1); |
|
160 by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1); |
|
161 by (typ.induct_tac "t" 1); |
|
162 by (Simp_tac 1); |
|
163 by (case_tac "nat : free_tv A" 1); |
|
164 by (Asm_simp_tac 1); |
|
165 by (subgoal_tac "n <= n + nat" 1); |
|
166 by (dtac new_tv_le 1); |
|
167 ba 1; |
|
168 by (dtac new_tv_not_free_tv 1); |
|
169 by (dtac new_tv_not_free_tv 1); |
|
170 by (asm_simp_tac (!simpset addsimps [diff_add_inverse ]) 1); |
|
171 by (Simp_tac 1); |
|
172 by (Asm_simp_tac 1); |
|
173 qed_spec_mp "gen_t_le_gen_alpha_t"; |
|
174 |
|
175 AddSIs has_type.intrs; |
|
176 |
|
177 goal thy "!!e. A |- e::t ==> !B. A <= B --> B |- e::t"; |
|
178 by(etac has_type.induct 1); |
|
179 by(simp_tac (!simpset addsimps [le_env_def]) 1); |
|
180 by(fast_tac (!claset addEs [bound_typ_instance_trans] addss !simpset) 1); |
|
181 by(Asm_full_simp_tac 1); |
|
182 by(Fast_tac 1); |
|
183 by(slow_tac (!claset addEs [le_env_free_tv RS free_tv_subset_gen_le]) 1); |
|
184 qed_spec_mp "has_type_le_env"; |
12 |
185 |
13 (* has_type is closed w.r.t. substitution *) |
186 (* has_type is closed w.r.t. substitution *) |
14 goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t"; |
187 goal thy "!!a. A |- e :: t ==> !S. $S A |- e :: $S t"; |
15 by (etac has_type.induct 1); |
188 by (etac has_type.induct 1); |
16 (* case VarI *) |
189 (* case VarI *) |
17 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1); |
190 by (rtac allI 1); |
18 by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1); |
191 by (rtac has_type.VarI 1); |
19 by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1); |
192 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1); |
20 (* case AbsI *) |
193 by (asm_simp_tac (!simpset addsimps [app_subst_list]) 1); |
21 by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1); |
194 (* case AbsI *) |
22 (* case AppI *) |
195 by (rtac allI 1); |
23 by (Asm_full_simp_tac 1); |
196 by (Simp_tac 1); |
|
197 by (rtac has_type.AbsI 1); |
|
198 by (Asm_full_simp_tac 1); |
|
199 (* case AppI *) |
|
200 by (rtac allI 1); |
|
201 by (rtac has_type.AppI 1); |
|
202 by (Asm_full_simp_tac 1); |
|
203 by (etac spec 1); |
|
204 by (etac spec 1); |
|
205 (* case LetI *) |
|
206 by (rtac allI 1); |
|
207 by (rtac replace_s_by_s' 1); |
|
208 by (cut_inst_tac [("A","$ S A"), |
|
209 ("A'","A"), |
|
210 ("t","t"), |
|
211 ("t'","$ S t")] |
|
212 ex_fresh_variable 1); |
|
213 by (etac exE 1); |
|
214 by (REPEAT (etac conjE 1)); |
|
215 by (res_inst_tac [("t1.0","$((%x. if x : free_tv A Un free_tv t then S x else TVar x) o \ |
|
216 \ (%x. if x : free_tv A then x else n + x)) t1")] |
|
217 has_type.LETI 1); |
|
218 by (dres_inst_tac [("x","(%x. if x : free_tv A Un free_tv t then S x else TVar x) o \ |
|
219 \ (%x. if x : free_tv A then x else n + x)")] spec 1); |
|
220 val o_apply = prove_goalw HOL.thy [o_def] "(f o g) x = f (g x)" |
|
221 (fn _ => [rtac refl 1]); |
|
222 by (stac (S'_A_eq_S'_alpha_A) 1); |
|
223 ba 1; |
|
224 by (stac S_o_alpha_typ 1); |
|
225 by (stac gen_subst_commutes 1); |
|
226 by (rtac subset_antisym 1); |
|
227 by (rtac subsetI 1); |
|
228 by (etac IntE 1); |
|
229 by (dtac (free_tv_S' RS subsetD) 1); |
|
230 by (dtac (free_tv_alpha RS subsetD) 1); |
|
231 by (Asm_full_simp_tac 1); |
|
232 by (etac exE 1); |
|
233 by (hyp_subst_tac 1); |
|
234 by (subgoal_tac "new_tv (n + y) ($ S A)" 1); |
|
235 by (subgoal_tac "new_tv (n + y) ($ S t)" 1); |
|
236 by (subgoal_tac "new_tv (n + y) A" 1); |
|
237 by (subgoal_tac "new_tv (n + y) t" 1); |
|
238 by (REPEAT (dtac new_tv_not_free_tv 1)); |
|
239 by (Fast_tac 1); |
|
240 by (REPEAT ((rtac new_tv_le 1) THEN (assume_tac 2) THEN (Simp_tac 1))); |
|
241 by (Fast_tac 1); |
|
242 by (rtac has_type_le_env 1); |
|
243 by (dtac spec 1); |
|
244 by (dtac spec 1); |
|
245 ba 1; |
|
246 by (rtac (app_subst_Cons RS subst) 1); |
|
247 by (rtac S_compatible_le_scheme_lists 1); |
|
248 by (Asm_simp_tac 1); |
24 qed "has_type_cl_sub"; |
249 qed "has_type_cl_sub"; |