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