1 (* Title: HOL/W0/W0.thy |
|
2 ID: $Id$ |
|
3 Author: Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel |
|
4 *) |
|
5 |
|
6 theory W0 |
|
7 imports Main |
|
8 begin |
|
9 |
|
10 section {* Universal error monad *} |
|
11 |
|
12 datatype 'a maybe = Ok 'a | Fail |
|
13 |
|
14 definition |
|
15 bind :: "'a maybe \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe" (infixl "\<bind>" 60) where |
|
16 "m \<bind> f = (case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail)" |
|
17 |
|
18 syntax |
|
19 "_bind" :: "patterns \<Rightarrow> 'a maybe \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ := _;//_)" 0) |
|
20 translations |
|
21 "P := E; F" == "E \<bind> (\<lambda>P. F)" |
|
22 |
|
23 lemma bind_Ok [simp]: "(Ok s) \<bind> f = (f s)" |
|
24 by (simp add: bind_def) |
|
25 |
|
26 lemma bind_Fail [simp]: "Fail \<bind> f = Fail" |
|
27 by (simp add: bind_def) |
|
28 |
|
29 lemma split_bind: |
|
30 "P (res \<bind> f) = ((res = Fail \<longrightarrow> P Fail) \<and> (\<forall>s. res = Ok s \<longrightarrow> P (f s)))" |
|
31 by (induct res) simp_all |
|
32 |
|
33 lemma split_bind_asm: |
|
34 "P (res \<bind> f) = (\<not> (res = Fail \<and> \<not> P Fail \<or> (\<exists>s. res = Ok s \<and> \<not> P (f s))))" |
|
35 by (simp split: split_bind) |
|
36 |
|
37 lemmas bind_splits = split_bind split_bind_asm |
|
38 |
|
39 lemma bind_eq_Fail [simp]: |
|
40 "((m \<bind> f) = Fail) = ((m = Fail) \<or> (\<exists>p. m = Ok p \<and> f p = Fail))" |
|
41 by (simp split: split_bind) |
|
42 |
|
43 lemma rotate_Ok: "(y = Ok x) = (Ok x = y)" |
|
44 by (rule eq_sym_conv) |
|
45 |
|
46 |
|
47 section {* MiniML-types and type substitutions *} |
|
48 |
|
49 axclass type_struct \<subseteq> type |
|
50 -- {* new class for structures containing type variables *} |
|
51 |
|
52 datatype "typ" = TVar nat | TFun "typ" "typ" (infixr "->" 70) |
|
53 -- {* type expressions *} |
|
54 |
|
55 types subst = "nat => typ" |
|
56 -- {* type variable substitution *} |
|
57 |
|
58 instance "typ" :: type_struct .. |
|
59 instance list :: (type_struct) type_struct .. |
|
60 instance "fun" :: (type, type_struct) type_struct .. |
|
61 |
|
62 |
|
63 subsection {* Substitutions *} |
|
64 |
|
65 consts |
|
66 app_subst :: "subst \<Rightarrow> 'a::type_struct \<Rightarrow> 'a::type_struct" ("$") |
|
67 -- {* extension of substitution to type structures *} |
|
68 primrec (app_subst_typ) |
|
69 app_subst_TVar: "$s (TVar n) = s n" |
|
70 app_subst_Fun: "$s (t1 -> t2) = $s t1 -> $s t2" |
|
71 |
|
72 defs (overloaded) |
|
73 app_subst_list: "$s \<equiv> map ($s)" |
|
74 |
|
75 consts |
|
76 free_tv :: "'a::type_struct \<Rightarrow> nat set" |
|
77 -- {* @{text "free_tv s"}: the type variables occuring freely in the type structure @{text s} *} |
|
78 |
|
79 primrec (free_tv_typ) |
|
80 "free_tv (TVar m) = {m}" |
|
81 "free_tv (t1 -> t2) = free_tv t1 \<union> free_tv t2" |
|
82 |
|
83 primrec (free_tv_list) |
|
84 "free_tv [] = {}" |
|
85 "free_tv (x # xs) = free_tv x \<union> free_tv xs" |
|
86 |
|
87 definition |
|
88 dom :: "subst \<Rightarrow> nat set" where |
|
89 "dom s = {n. s n \<noteq> TVar n}" |
|
90 -- {* domain of a substitution *} |
|
91 |
|
92 definition |
|
93 cod :: "subst \<Rightarrow> nat set" where |
|
94 "cod s = (\<Union>m \<in> dom s. free_tv (s m))" |
|
95 -- {* codomain of a substitutions: the introduced variables *} |
|
96 |
|
97 defs (overloaded) |
|
98 free_tv_subst: "free_tv s \<equiv> dom s \<union> cod s" |
|
99 |
|
100 text {* |
|
101 @{text "new_tv s n"} checks whether @{text n} is a new type variable |
|
102 wrt.\ a type structure @{text s}, i.e.\ whether @{text n} is greater |
|
103 than any type variable occuring in the type structure. |
|
104 *} |
|
105 |
|
106 definition |
|
107 new_tv :: "nat \<Rightarrow> 'a::type_struct \<Rightarrow> bool" where |
|
108 "new_tv n ts = (\<forall>m. m \<in> free_tv ts \<longrightarrow> m < n)" |
|
109 |
|
110 |
|
111 subsubsection {* Identity substitution *} |
|
112 |
|
113 definition |
|
114 id_subst :: subst where |
|
115 "id_subst = (\<lambda>n. TVar n)" |
|
116 |
|
117 lemma app_subst_id_te [simp]: |
|
118 "$id_subst = (\<lambda>t::typ. t)" |
|
119 -- {* application of @{text id_subst} does not change type expression *} |
|
120 proof |
|
121 fix t :: "typ" |
|
122 show "$id_subst t = t" |
|
123 by (induct t) (simp_all add: id_subst_def) |
|
124 qed |
|
125 |
|
126 lemma app_subst_id_tel [simp]: "$id_subst = (\<lambda>ts::typ list. ts)" |
|
127 -- {* application of @{text id_subst} does not change list of type expressions *} |
|
128 proof |
|
129 fix ts :: "typ list" |
|
130 show "$id_subst ts = ts" |
|
131 by (induct ts) (simp_all add: app_subst_list) |
|
132 qed |
|
133 |
|
134 lemma o_id_subst [simp]: "$s o id_subst = s" |
|
135 by (rule ext) (simp add: id_subst_def) |
|
136 |
|
137 lemma dom_id_subst [simp]: "dom id_subst = {}" |
|
138 by (simp add: dom_def id_subst_def) |
|
139 |
|
140 lemma cod_id_subst [simp]: "cod id_subst = {}" |
|
141 by (simp add: cod_def) |
|
142 |
|
143 lemma free_tv_id_subst [simp]: "free_tv id_subst = {}" |
|
144 by (simp add: free_tv_subst) |
|
145 |
|
146 |
|
147 lemma cod_app_subst [simp]: |
|
148 assumes free: "v \<in> free_tv (s n)" |
|
149 and neq: "v \<noteq> n" |
|
150 shows "v \<in> cod s" |
|
151 proof - |
|
152 have "s n \<noteq> TVar n" |
|
153 proof |
|
154 assume "s n = TVar n" |
|
155 with free have "v = n" by simp |
|
156 with neq show False .. |
|
157 qed |
|
158 with free show ?thesis |
|
159 by (auto simp add: dom_def cod_def) |
|
160 qed |
|
161 |
|
162 lemma subst_comp_te: "$g ($f t :: typ) = $(\<lambda>x. $g (f x)) t" |
|
163 -- {* composition of substitutions *} |
|
164 by (induct t) simp_all |
|
165 |
|
166 lemma subst_comp_tel: "$g ($f ts :: typ list) = $(\<lambda>x. $g (f x)) ts" |
|
167 by (induct ts) (simp_all add: app_subst_list subst_comp_te) |
|
168 |
|
169 |
|
170 lemma app_subst_Nil [simp]: "$s [] = []" |
|
171 by (simp add: app_subst_list) |
|
172 |
|
173 lemma app_subst_Cons [simp]: "$s (t # ts) = ($s t) # ($s ts)" |
|
174 by (simp add: app_subst_list) |
|
175 |
|
176 lemma new_tv_TVar [simp]: "new_tv n (TVar m) = (m < n)" |
|
177 by (simp add: new_tv_def) |
|
178 |
|
179 lemma new_tv_Fun [simp]: |
|
180 "new_tv n (t1 -> t2) = (new_tv n t1 \<and> new_tv n t2)" |
|
181 by (auto simp add: new_tv_def) |
|
182 |
|
183 lemma new_tv_Nil [simp]: "new_tv n []" |
|
184 by (simp add: new_tv_def) |
|
185 |
|
186 lemma new_tv_Cons [simp]: "new_tv n (t # ts) = (new_tv n t \<and> new_tv n ts)" |
|
187 by (auto simp add: new_tv_def) |
|
188 |
|
189 lemma new_tv_id_subst [simp]: "new_tv n id_subst" |
|
190 by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def) |
|
191 |
|
192 lemma new_tv_subst: |
|
193 "new_tv n s = |
|
194 ((\<forall>m. n \<le> m \<longrightarrow> s m = TVar m) \<and> |
|
195 (\<forall>l. l < n \<longrightarrow> new_tv n (s l)))" |
|
196 apply (unfold new_tv_def) |
|
197 apply (tactic "safe_tac HOL_cs") |
|
198 -- {* @{text \<Longrightarrow>} *} |
|
199 apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (@{simpset} |
|
200 addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *}) |
|
201 apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l") |
|
202 apply (tactic "safe_tac HOL_cs") |
|
203 apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (@{simpset} |
|
204 addsimps [thm "free_tv_subst"])) 1 *}) |
|
205 apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption) |
|
206 apply simp |
|
207 apply (unfold free_tv_subst cod_def dom_def) |
|
208 apply clarsimp |
|
209 apply safe |
|
210 apply metis |
|
211 apply (metis linorder_not_less)+ |
|
212 done |
|
213 |
|
214 lemma new_tv_list: "new_tv n x = (\<forall>y \<in> set x. new_tv n y)" |
|
215 by (induct x) simp_all |
|
216 |
|
217 lemma subst_te_new_tv [simp]: |
|
218 "new_tv n (t::typ) \<Longrightarrow> $(\<lambda>x. if x = n then t' else s x) t = $s t" |
|
219 -- {* substitution affects only variables occurring freely *} |
|
220 by (induct t) simp_all |
|
221 |
|
222 lemma subst_tel_new_tv [simp]: |
|
223 "new_tv n (ts::typ list) \<Longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts" |
|
224 by (induct ts) simp_all |
|
225 |
|
226 lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv m t" |
|
227 -- {* all greater variables are also new *} |
|
228 proof (induct t) |
|
229 case (TVar n) |
|
230 then show ?case by (auto intro: less_le_trans) |
|
231 next |
|
232 case TFun |
|
233 then show ?case by simp |
|
234 qed |
|
235 |
|
236 lemma [simp]: "new_tv n t \<Longrightarrow> new_tv (Suc n) (t::typ)" |
|
237 by (rule lessI [THEN less_imp_le [THEN new_tv_le]]) |
|
238 |
|
239 lemma new_tv_list_le: |
|
240 assumes "n \<le> m" |
|
241 shows "new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts" |
|
242 proof (induct ts) |
|
243 case Nil |
|
244 then show ?case by simp |
|
245 next |
|
246 case Cons |
|
247 with `n \<le> m` show ?case by (auto intro: new_tv_le) |
|
248 qed |
|
249 |
|
250 lemma [simp]: "new_tv n ts \<Longrightarrow> new_tv (Suc n) (ts::typ list)" |
|
251 by (rule lessI [THEN less_imp_le [THEN new_tv_list_le]]) |
|
252 |
|
253 lemma new_tv_subst_le: "n \<le> m \<Longrightarrow> new_tv n (s::subst) \<Longrightarrow> new_tv m s" |
|
254 apply (simp add: new_tv_subst) |
|
255 apply clarify |
|
256 apply (rule_tac P = "l < n" and Q = "n <= l" in disjE) |
|
257 apply clarify |
|
258 apply (simp_all add: new_tv_le) |
|
259 done |
|
260 |
|
261 lemma [simp]: "new_tv n s \<Longrightarrow> new_tv (Suc n) (s::subst)" |
|
262 by (rule lessI [THEN less_imp_le [THEN new_tv_subst_le]]) |
|
263 |
|
264 lemma new_tv_subst_var: |
|
265 "n < m \<Longrightarrow> new_tv m (s::subst) \<Longrightarrow> new_tv m (s n)" |
|
266 -- {* @{text new_tv} property remains if a substitution is applied *} |
|
267 by (simp add: new_tv_subst) |
|
268 |
|
269 lemma new_tv_subst_te [simp]: |
|
270 "new_tv n s \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv n ($s t)" |
|
271 by (induct t) (auto simp add: new_tv_subst) |
|
272 |
|
273 lemma new_tv_subst_tel [simp]: |
|
274 "new_tv n s \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> new_tv n ($s ts)" |
|
275 by (induct ts) (fastsimp simp add: new_tv_subst)+ |
|
276 |
|
277 lemma new_tv_Suc_list: "new_tv n ts --> new_tv (Suc n) (TVar n # ts)" |
|
278 -- {* auxilliary lemma *} |
|
279 by (simp add: new_tv_list) |
|
280 |
|
281 lemma new_tv_subst_comp_1 [simp]: |
|
282 "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n ($r o s)" |
|
283 -- {* composition of substitutions preserves @{text new_tv} proposition *} |
|
284 by (simp add: new_tv_subst) |
|
285 |
|
286 lemma new_tv_subst_comp_2 [simp]: |
|
287 "new_tv n (s::subst) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n (\<lambda>v. $r (s v))" |
|
288 by (simp add: new_tv_subst) |
|
289 |
|
290 lemma new_tv_not_free_tv [simp]: "new_tv n ts \<Longrightarrow> n \<notin> free_tv ts" |
|
291 -- {* new type variables do not occur freely in a type structure *} |
|
292 by (auto simp add: new_tv_def) |
|
293 |
|
294 lemma ftv_mem_sub_ftv_list [simp]: |
|
295 "(t::typ) \<in> set ts \<Longrightarrow> free_tv t \<subseteq> free_tv ts" |
|
296 by (induct ts) auto |
|
297 |
|
298 text {* |
|
299 If two substitutions yield the same result if applied to a type |
|
300 structure the substitutions coincide on the free type variables |
|
301 occurring in the type structure. |
|
302 *} |
|
303 |
|
304 lemma eq_subst_te_eq_free: |
|
305 "$s1 (t::typ) = $s2 t \<Longrightarrow> n \<in> free_tv t \<Longrightarrow> s1 n = s2 n" |
|
306 by (induct t) auto |
|
307 |
|
308 lemma eq_free_eq_subst_te: |
|
309 "(\<forall>n. n \<in> free_tv t --> s1 n = s2 n) \<Longrightarrow> $s1 (t::typ) = $s2 t" |
|
310 by (induct t) auto |
|
311 |
|
312 lemma eq_subst_tel_eq_free: |
|
313 "$s1 (ts::typ list) = $s2 ts \<Longrightarrow> n \<in> free_tv ts \<Longrightarrow> s1 n = s2 n" |
|
314 by (induct ts) (auto intro: eq_subst_te_eq_free) |
|
315 |
|
316 lemma eq_free_eq_subst_tel: |
|
317 "(\<forall>n. n \<in> free_tv ts --> s1 n = s2 n) \<Longrightarrow> $s1 (ts::typ list) = $s2 ts" |
|
318 by (induct ts) (auto intro: eq_free_eq_subst_te) |
|
319 |
|
320 text {* |
|
321 \medskip Some useful lemmas. |
|
322 *} |
|
323 |
|
324 lemma codD: "v \<in> cod s \<Longrightarrow> v \<in> free_tv s" |
|
325 by (simp add: free_tv_subst) |
|
326 |
|
327 lemma not_free_impl_id: "x \<notin> free_tv s \<Longrightarrow> s x = TVar x" |
|
328 by (simp add: free_tv_subst dom_def) |
|
329 |
|
330 lemma free_tv_le_new_tv: "new_tv n t \<Longrightarrow> m \<in> free_tv t \<Longrightarrow> m < n" |
|
331 by (unfold new_tv_def) fast |
|
332 |
|
333 lemma free_tv_subst_var: "free_tv (s (v::nat)) \<le> insert v (cod s)" |
|
334 by (cases "v \<in> dom s") (auto simp add: cod_def dom_def) |
|
335 |
|
336 lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \<subseteq> cod s \<union> free_tv t" |
|
337 by (induct t) (auto simp add: free_tv_subst_var) |
|
338 |
|
339 lemma free_tv_app_subst_tel: "free_tv ($s (ts::typ list)) \<subseteq> cod s \<union> free_tv ts" |
|
340 apply (induct ts) |
|
341 apply simp |
|
342 apply (cut_tac free_tv_app_subst_te) |
|
343 apply fastsimp |
|
344 done |
|
345 |
|
346 lemma free_tv_comp_subst: |
|
347 "free_tv (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> free_tv s2" |
|
348 apply (unfold free_tv_subst dom_def) |
|
349 apply (auto dest!: free_tv_subst_var [THEN subsetD] free_tv_app_subst_te [THEN subsetD] |
|
350 simp add: cod_def dom_def simp del: bex_simps) |
|
351 done |
|
352 |
|
353 |
|
354 subsection {* Most general unifiers *} |
|
355 |
|
356 consts |
|
357 mgu :: "typ \<Rightarrow> typ \<Rightarrow> subst maybe" |
|
358 axioms |
|
359 mgu_eq [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $u t1 = $u t2" |
|
360 mgu_mg [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $s t1 = $s t2 \<Longrightarrow> \<exists>r. s = $r o u" |
|
361 mgu_Ok: "$s t1 = $s t2 \<Longrightarrow> \<exists>u. mgu t1 t2 = Ok u" |
|
362 mgu_free [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> free_tv u \<subseteq> free_tv t1 \<union> free_tv t2" |
|
363 |
|
364 lemma mgu_new: "mgu t1 t2 = Ok u \<Longrightarrow> new_tv n t1 \<Longrightarrow> new_tv n t2 \<Longrightarrow> new_tv n u" |
|
365 -- {* @{text mgu} does not introduce new type variables *} |
|
366 by (unfold new_tv_def) (blast dest: mgu_free) |
|
367 |
|
368 |
|
369 section {* Mini-ML with type inference rules *} |
|
370 |
|
371 datatype |
|
372 expr = Var nat | Abs expr | App expr expr |
|
373 |
|
374 |
|
375 text {* Type inference rules. *} |
|
376 |
|
377 inductive |
|
378 has_type :: "typ list \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool" ("((_) |-/ (_) :: (_))" [60, 0, 60] 60) |
|
379 where |
|
380 Var: "n < length a \<Longrightarrow> a |- Var n :: a ! n" |
|
381 | Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2" |
|
382 | App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2 |
|
383 \<Longrightarrow> a |- App e1 e2 :: t1" |
|
384 |
|
385 |
|
386 text {* Type assigment is closed wrt.\ substitution. *} |
|
387 |
|
388 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t" |
|
389 proof (induct set: has_type) |
|
390 case (Var n a) |
|
391 then have "n < length (map ($ s) a)" by simp |
|
392 then have "map ($ s) a |- Var n :: map ($ s) a ! n" |
|
393 by (rule has_type.Var) |
|
394 also have "map ($ s) a ! n = $ s (a ! n)" |
|
395 by (rule nth_map) (rule Var) |
|
396 also have "map ($ s) a = $ s a" |
|
397 by (simp only: app_subst_list) |
|
398 finally show ?case . |
|
399 next |
|
400 case (Abs t1 a e t2) |
|
401 then have "$ s t1 # map ($ s) a |- e :: $ s t2" |
|
402 by (simp add: app_subst_list) |
|
403 then have "map ($ s) a |- Abs e :: $ s t1 -> $ s t2" |
|
404 by (rule has_type.Abs) |
|
405 then show ?case |
|
406 by (simp add: app_subst_list) |
|
407 next |
|
408 case App |
|
409 then show ?case by (simp add: has_type.App) |
|
410 qed |
|
411 |
|
412 |
|
413 section {* Correctness and completeness of the type inference algorithm W *} |
|
414 |
|
415 consts |
|
416 "\<W>" :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe" |
|
417 primrec |
|
418 "\<W> (Var i) a n = |
|
419 (if i < length a then Ok (id_subst, a ! i, n) else Fail)" |
|
420 "\<W> (Abs e) a n = |
|
421 ((s, t, m) := \<W> e (TVar n # a) (Suc n); |
|
422 Ok (s, (s n) -> t, m))" |
|
423 "\<W> (App e1 e2) a n = |
|
424 ((s1, t1, m1) := \<W> e1 a n; |
|
425 (s2, t2, m2) := \<W> e2 ($s1 a) m1; |
|
426 u := mgu ($ s2 t1) (t2 -> TVar m2); |
|
427 Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))" |
|
428 |
|
429 theorem W_correct: "Ok (s, t, m) = \<W> e a n ==> $s a |- e :: t" |
|
430 proof (induct e arbitrary: a s t m n) |
|
431 case (Var i) |
|
432 from `Ok (s, t, m) = \<W> (Var i) a n` |
|
433 show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits) |
|
434 next |
|
435 case (Abs e) |
|
436 from `Ok (s, t, m) = \<W> (Abs e) a n` |
|
437 obtain t' where "t = s n -> t'" |
|
438 and "Ok (s, t', m) = \<W> e (TVar n # a) (Suc n)" |
|
439 by (auto split: bind_splits) |
|
440 with Abs.hyps show "$s a |- Abs e :: t" |
|
441 by (force intro: has_type.Abs) |
|
442 next |
|
443 case (App e1 e2) |
|
444 from `Ok (s, t, m) = \<W> (App e1 e2) a n` |
|
445 obtain s1 t1 n1 s2 t2 n2 u where |
|
446 s: "s = $u o $s2 o s1" |
|
447 and t: "t = u n2" |
|
448 and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u" |
|
449 and W1_ok: "Ok (s1, t1, n1) = \<W> e1 a n" |
|
450 and W2_ok: "Ok (s2, t2, n2) = \<W> e2 ($s1 a) n1" |
|
451 by (auto split: bind_splits simp: that) |
|
452 show "$s a |- App e1 e2 :: t" |
|
453 proof (rule has_type.App) |
|
454 from s have s': "$u ($s2 ($s1 a)) = $s a" |
|
455 by (simp add: subst_comp_tel o_def) |
|
456 show "$s a |- e1 :: $u t2 -> t" |
|
457 proof - |
|
458 from W1_ok have "$s1 a |- e1 :: t1" by (rule App.hyps(1)) |
|
459 then have "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)" |
|
460 by (intro has_type_subst_closed) |
|
461 with s' t mgu_ok show ?thesis by simp |
|
462 qed |
|
463 show "$s a |- e2 :: $u t2" |
|
464 proof - |
|
465 from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule App.hyps(2)) |
|
466 then have "$u ($s2 ($s1 a)) |- e2 :: $u t2" |
|
467 by (rule has_type_subst_closed) |
|
468 with s' show ?thesis by simp |
|
469 qed |
|
470 qed |
|
471 qed |
|
472 |
|
473 |
|
474 inductive_cases has_type_casesE: |
|
475 "s |- Var n :: t" |
|
476 "s |- Abs e :: t" |
|
477 "s |- App e1 e2 ::t" |
|
478 |
|
479 |
|
480 lemmas [simp] = Suc_le_lessD |
|
481 and [simp del] = less_imp_le ex_simps all_simps |
|
482 |
|
483 lemma W_var_ge [simp]: "!!a n s t m. \<W> e a n = Ok (s, t, m) \<Longrightarrow> n \<le> m" |
|
484 -- {* the resulting type variable is always greater or equal than the given one *} |
|
485 apply (atomize (full)) |
|
486 apply (induct e) |
|
487 txt {* case @{text "Var n"} *} |
|
488 apply clarsimp |
|
489 txt {* case @{text "Abs e"} *} |
|
490 apply (simp split add: split_bind) |
|
491 apply (fast dest: Suc_leD) |
|
492 txt {* case @{text "App e1 e2"} *} |
|
493 apply (simp (no_asm) split add: split_bind) |
|
494 apply (intro strip) |
|
495 apply (rename_tac s t na sa ta nb sb) |
|
496 apply (erule_tac x = a in allE) |
|
497 apply (erule_tac x = n in allE) |
|
498 apply (erule_tac x = "$s a" in allE) |
|
499 apply (erule_tac x = s in allE) |
|
500 apply (erule_tac x = t in allE) |
|
501 apply (erule_tac x = na in allE) |
|
502 apply (erule_tac x = na in allE) |
|
503 apply (simp add: eq_sym_conv) |
|
504 done |
|
505 |
|
506 lemma W_var_geD: "Ok (s, t, m) = \<W> e a n \<Longrightarrow> n \<le> m" |
|
507 by (simp add: eq_sym_conv) |
|
508 |
|
509 lemma new_tv_W: "!!n a s t m. |
|
510 new_tv n a \<Longrightarrow> \<W> e a n = Ok (s, t, m) \<Longrightarrow> new_tv m s & new_tv m t" |
|
511 -- {* resulting type variable is new *} |
|
512 apply (atomize (full)) |
|
513 apply (induct e) |
|
514 txt {* case @{text "Var n"} *} |
|
515 apply clarsimp |
|
516 apply (force elim: list_ball_nth simp add: id_subst_def new_tv_list new_tv_subst) |
|
517 txt {* case @{text "Abs e"} *} |
|
518 apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_bind) |
|
519 apply (intro strip) |
|
520 apply (erule_tac x = "Suc n" in allE) |
|
521 apply (erule_tac x = "TVar n # a" in allE) |
|
522 apply (fastsimp simp add: new_tv_subst new_tv_Suc_list) |
|
523 txt {* case @{text "App e1 e2"} *} |
|
524 apply (simp (no_asm) split add: split_bind) |
|
525 apply (intro strip) |
|
526 apply (rename_tac s t na sa ta nb sb) |
|
527 apply (erule_tac x = n in allE) |
|
528 apply (erule_tac x = a in allE) |
|
529 apply (erule_tac x = s in allE) |
|
530 apply (erule_tac x = t in allE) |
|
531 apply (erule_tac x = na in allE) |
|
532 apply (erule_tac x = na in allE) |
|
533 apply (simp add: eq_sym_conv) |
|
534 apply (erule_tac x = "$s a" in allE) |
|
535 apply (erule_tac x = sa in allE) |
|
536 apply (erule_tac x = ta in allE) |
|
537 apply (erule_tac x = nb in allE) |
|
538 apply (simp add: o_def rotate_Ok) |
|
539 apply (rule conjI) |
|
540 apply (rule new_tv_subst_comp_2) |
|
541 apply (rule new_tv_subst_comp_2) |
|
542 apply (rule lessI [THEN less_imp_le, THEN new_tv_subst_le]) |
|
543 apply (rule_tac n = na in new_tv_subst_le) |
|
544 apply (simp add: rotate_Ok) |
|
545 apply (simp (no_asm_simp)) |
|
546 apply (fast dest: W_var_geD intro: new_tv_list_le new_tv_subst_tel |
|
547 lessI [THEN less_imp_le, THEN new_tv_subst_le]) |
|
548 apply (erule sym [THEN mgu_new]) |
|
549 apply (best dest: W_var_geD intro: new_tv_subst_te new_tv_list_le new_tv_subst_tel |
|
550 lessI [THEN less_imp_le, THEN new_tv_le] lessI [THEN less_imp_le, THEN new_tv_subst_le] |
|
551 new_tv_le) |
|
552 apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"] |
|
553 addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"] |
|
554 addss @{simpset}) 1 *}) |
|
555 apply (rule lessI [THEN new_tv_subst_var]) |
|
556 apply (erule sym [THEN mgu_new]) |
|
557 apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te |
|
558 dest!: W_var_geD intro: new_tv_list_le new_tv_subst_tel |
|
559 lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le) |
|
560 apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"] |
|
561 addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"] |
|
562 addss @{simpset}) 1 *}) |
|
563 done |
|
564 |
|
565 lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow> |
|
566 (v \<in> free_tv s \<or> v \<in> free_tv t) \<Longrightarrow> v < n \<Longrightarrow> v \<in> free_tv a" |
|
567 apply (atomize (full)) |
|
568 apply (induct e) |
|
569 txt {* case @{text "Var n"} *} |
|
570 apply clarsimp |
|
571 apply (tactic {* fast_tac (HOL_cs addIs [thm "nth_mem", subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *}) |
|
572 txt {* case @{text "Abs e"} *} |
|
573 apply (simp add: free_tv_subst split add: split_bind) |
|
574 apply (intro strip) |
|
575 apply (rename_tac s t n1 v) |
|
576 apply (erule_tac x = "Suc n" in allE) |
|
577 apply (erule_tac x = "TVar n # a" in allE) |
|
578 apply (erule_tac x = s in allE) |
|
579 apply (erule_tac x = t in allE) |
|
580 apply (erule_tac x = n1 in allE) |
|
581 apply (erule_tac x = v in allE) |
|
582 apply (force elim!: allE intro: cod_app_subst) |
|
583 txt {* case @{text "App e1 e2"} *} |
|
584 apply (simp (no_asm) split add: split_bind) |
|
585 apply (intro strip) |
|
586 apply (rename_tac s t n1 s1 t1 n2 s3 v) |
|
587 apply (erule_tac x = n in allE) |
|
588 apply (erule_tac x = a in allE) |
|
589 apply (erule_tac x = s in allE) |
|
590 apply (erule_tac x = t in allE) |
|
591 apply (erule_tac x = n1 in allE) |
|
592 apply (erule_tac x = n1 in allE) |
|
593 apply (erule_tac x = v in allE) |
|
594 txt {* second case *} |
|
595 apply (erule_tac x = "$ s a" in allE) |
|
596 apply (erule_tac x = s1 in allE) |
|
597 apply (erule_tac x = t1 in allE) |
|
598 apply (erule_tac x = n2 in allE) |
|
599 apply (erule_tac x = v in allE) |
|
600 apply (tactic "safe_tac (empty_cs addSIs [conjI, impI] addSEs [conjE])") |
|
601 apply (simp add: rotate_Ok o_def) |
|
602 apply (drule W_var_geD) |
|
603 apply (drule W_var_geD) |
|
604 apply (frule less_le_trans, assumption) |
|
605 apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD |
|
606 free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_tel [THEN subsetD] subsetD elim: UnE) |
|
607 apply simp |
|
608 apply (drule sym [THEN W_var_geD]) |
|
609 apply (drule sym [THEN W_var_geD]) |
|
610 apply (frule less_le_trans, assumption) |
|
611 apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD", |
|
612 thm "free_tv_subst_var" RS subsetD, |
|
613 thm "free_tv_app_subst_te" RS subsetD, |
|
614 thm "free_tv_app_subst_tel" RS subsetD, @{thm less_le_trans}, subsetD] |
|
615 addSEs [UnE] addss (@{simpset} setSolver unsafe_solver)) 1 *}) |
|
616 -- {* builtin arithmetic in simpset messes things up *} |
|
617 done |
|
618 |
|
619 text {* |
|
620 \medskip Completeness of @{text \<W>} wrt.\ @{text has_type}. |
|
621 *} |
|
622 |
|
623 lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \<Longrightarrow> new_tv n a \<Longrightarrow> |
|
624 (\<exists>s t. (\<exists>m. \<W> e a n = Ok (s, t, m)) \<and> (\<exists>r. $s' a = $r ($s a) \<and> t' = $r t))" |
|
625 apply (atomize (full)) |
|
626 apply (induct e) |
|
627 txt {* case @{text "Var n"} *} |
|
628 apply (intro strip) |
|
629 apply (simp (no_asm) cong add: conj_cong) |
|
630 apply (erule has_type_casesE) |
|
631 apply (simp add: eq_sym_conv app_subst_list) |
|
632 apply (rule_tac x = s' in exI) |
|
633 apply simp |
|
634 txt {* case @{text "Abs e"} *} |
|
635 apply (intro strip) |
|
636 apply (erule has_type_casesE) |
|
637 apply (erule_tac x = "\<lambda>x. if x = n then t1 else (s' x)" in allE) |
|
638 apply (erule_tac x = "TVar n # a" in allE) |
|
639 apply (erule_tac x = t2 in allE) |
|
640 apply (erule_tac x = "Suc n" in allE) |
|
641 apply (fastsimp cong add: conj_cong split add: split_bind) |
|
642 txt {* case @{text "App e1 e2"} *} |
|
643 apply (intro strip) |
|
644 apply (erule has_type_casesE) |
|
645 apply (erule_tac x = s' in allE) |
|
646 apply (erule_tac x = a in allE) |
|
647 apply (erule_tac x = "t2 -> t'" in allE) |
|
648 apply (erule_tac x = n in allE) |
|
649 apply (tactic "safe_tac HOL_cs") |
|
650 apply (erule_tac x = r in allE) |
|
651 apply (erule_tac x = "$s a" in allE) |
|
652 apply (erule_tac x = t2 in allE) |
|
653 apply (erule_tac x = m in allE) |
|
654 apply simp |
|
655 apply (tactic "safe_tac HOL_cs") |
|
656 apply (tactic {* fast_tac (HOL_cs addIs [sym RS thm "W_var_geD", |
|
657 thm "new_tv_W" RS conjunct1, thm "new_tv_list_le", thm "new_tv_subst_tel"]) 1 *}) |
|
658 apply (subgoal_tac |
|
659 "$(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x |
|
660 else ra x)) ($ sa t) = |
|
661 $(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x |
|
662 else ra x)) (ta -> (TVar ma))") |
|
663 apply (rule_tac [2] t = "$(\<lambda>x. if x = ma then t' |
|
664 else (if x \<in> (free_tv t - free_tv sa) then r x else ra x)) ($sa t)" and |
|
665 s = "($ ra ta) -> t'" in ssubst) |
|
666 prefer 2 |
|
667 apply (simp add: subst_comp_te) |
|
668 apply (rule eq_free_eq_subst_te) |
|
669 apply (intro strip) |
|
670 apply (subgoal_tac "na \<noteq> ma") |
|
671 prefer 2 |
|
672 apply (fast dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le) |
|
673 apply (case_tac "na \<in> free_tv sa") |
|
674 txt {* @{text "na \<notin> free_tv sa"} *} |
|
675 prefer 2 |
|
676 apply (frule not_free_impl_id) |
|
677 apply simp |
|
678 txt {* @{text "na \<in> free_tv sa"} *} |
|
679 apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans]) |
|
680 apply (drule_tac eq_subst_tel_eq_free) |
|
681 apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W) |
|
682 apply simp |
|
683 apply (case_tac "na \<in> dom sa") |
|
684 prefer 2 |
|
685 txt {* @{text "na \<noteq> dom sa"} *} |
|
686 apply (simp add: dom_def) |
|
687 txt {* @{text "na \<in> dom sa"} *} |
|
688 apply (rule eq_free_eq_subst_te) |
|
689 apply (intro strip) |
|
690 apply (subgoal_tac "nb \<noteq> ma") |
|
691 prefer 2 |
|
692 apply (frule new_tv_W, assumption) |
|
693 apply (erule conjE) |
|
694 apply (drule new_tv_subst_tel) |
|
695 apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD]) |
|
696 apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst) |
|
697 apply (fastsimp simp add: cod_def free_tv_subst) |
|
698 prefer 2 |
|
699 apply (simp (no_asm)) |
|
700 apply (rule eq_free_eq_subst_te) |
|
701 apply (intro strip) |
|
702 apply (subgoal_tac "na \<noteq> ma") |
|
703 prefer 2 |
|
704 apply (frule new_tv_W, assumption) |
|
705 apply (erule conjE) |
|
706 apply (drule sym [THEN W_var_geD]) |
|
707 apply (fast dest: new_tv_list_le new_tv_subst_tel new_tv_W new_tv_not_free_tv) |
|
708 apply (case_tac "na \<in> free_tv t - free_tv sa") |
|
709 prefer 2 |
|
710 txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *} |
|
711 apply simp |
|
712 defer |
|
713 txt {* case @{text "na \<in> free_tv t - free_tv sa"} *} |
|
714 apply simp |
|
715 apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans]) |
|
716 apply (drule eq_subst_tel_eq_free) |
|
717 apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W) |
|
718 apply (simp add: free_tv_subst dom_def) |
|
719 prefer 2 apply fast |
|
720 apply (simp (no_asm_simp) split add: split_bind) |
|
721 apply (tactic "safe_tac HOL_cs") |
|
722 apply (drule mgu_Ok) |
|
723 apply fastsimp |
|
724 apply (drule mgu_mg, assumption) |
|
725 apply (erule exE) |
|
726 apply (rule_tac x = rb in exI) |
|
727 apply (rule conjI) |
|
728 prefer 2 |
|
729 apply (drule_tac x = ma in fun_cong) |
|
730 apply (simp add: eq_sym_conv) |
|
731 apply (simp (no_asm) add: o_def subst_comp_tel [symmetric]) |
|
732 apply (rule subst_comp_tel [symmetric, THEN [2] trans]) |
|
733 apply (simp add: o_def eq_sym_conv) |
|
734 apply (rule eq_free_eq_subst_tel) |
|
735 apply (tactic "safe_tac HOL_cs") |
|
736 apply (subgoal_tac "ma \<noteq> na") |
|
737 prefer 2 |
|
738 apply (frule new_tv_W, assumption) |
|
739 apply (erule conjE) |
|
740 apply (drule new_tv_subst_tel) |
|
741 apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD]) |
|
742 apply (frule_tac n = m in new_tv_W, assumption) |
|
743 apply (erule conjE) |
|
744 apply (drule free_tv_app_subst_tel [THEN subsetD]) |
|
745 apply (auto dest: W_var_geD [OF sym] new_tv_list_le |
|
746 codD new_tv_not_free_tv) |
|
747 apply (case_tac "na \<in> free_tv t - free_tv sa") |
|
748 prefer 2 |
|
749 txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *} |
|
750 apply simp |
|
751 defer |
|
752 txt {* case @{text "na \<in> free_tv t - free_tv sa"} *} |
|
753 apply simp |
|
754 apply (drule free_tv_app_subst_tel [THEN subsetD]) |
|
755 apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans] |
|
756 eq_subst_tel_eq_free simp add: free_tv_subst dom_def) |
|
757 done |
|
758 |
|
759 lemma W_complete: "[] |- e :: t' ==> |
|
760 \<exists>s t. (\<exists>m. \<W> e [] n = Ok (s, t, m)) \<and> (\<exists>r. t' = $r t)" |
|
761 apply (cut_tac a = "[]" and s' = id_subst and e = e and t' = t' in W_complete_aux) |
|
762 apply simp_all |
|
763 done |
|
764 |
|
765 |
|
766 section {* Equivalence of W and I *} |
|
767 |
|
768 text {* |
|
769 Recursive definition of type inference algorithm @{text \<I>} for |
|
770 Mini-ML. |
|
771 *} |
|
772 |
|
773 consts |
|
774 "\<I>" :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> subst \<Rightarrow> (subst \<times> typ \<times> nat) maybe" |
|
775 primrec |
|
776 "\<I> (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)" |
|
777 "\<I> (Abs e) a n s = ((s, t, m) := \<I> e (TVar n # a) (Suc n) s; |
|
778 Ok (s, TVar n -> t, m))" |
|
779 "\<I> (App e1 e2) a n s = |
|
780 ((s1, t1, m1) := \<I> e1 a n s; |
|
781 (s2, t2, m2) := \<I> e2 a m1 s1; |
|
782 u := mgu ($s2 t1) ($s2 t2 -> TVar m2); |
|
783 Ok($u o s2, TVar m2, Suc m2))" |
|
784 |
|
785 text {* \medskip Correctness. *} |
|
786 |
|
787 lemma I_correct_wrt_W: "!!a m s s' t n. |
|
788 new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Ok (s', t, n) \<Longrightarrow> |
|
789 \<exists>r. \<W> e ($s a) m = Ok (r, $s' t, n) \<and> s' = ($r o s)" |
|
790 apply (atomize (full)) |
|
791 apply (induct e) |
|
792 txt {* case @{text "Var n"} *} |
|
793 apply (simp add: app_subst_list split: split_if) |
|
794 txt {* case @{text "Abs e"} *} |
|
795 apply (tactic {* asm_full_simp_tac |
|
796 (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *}) |
|
797 apply (intro strip) |
|
798 apply (rule conjI) |
|
799 apply (intro strip) |
|
800 apply (erule allE)+ |
|
801 apply (erule impE) |
|
802 prefer 2 apply (fastsimp simp add: new_tv_subst) |
|
803 apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp, |
|
804 thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *}) |
|
805 apply (intro strip) |
|
806 apply (erule allE)+ |
|
807 apply (erule impE) |
|
808 prefer 2 apply (fastsimp simp add: new_tv_subst) |
|
809 apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp, |
|
810 thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *}) |
|
811 txt {* case @{text "App e1 e2"} *} |
|
812 apply (tactic {* simp_tac (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *}) |
|
813 apply (intro strip) |
|
814 apply (rename_tac s1' t1 n1 s2' t2 n2 sa) |
|
815 apply (rule conjI) |
|
816 apply fastsimp |
|
817 apply (intro strip) |
|
818 apply (rename_tac s1 t1' n1') |
|
819 apply (erule_tac x = a in allE) |
|
820 apply (erule_tac x = m in allE) |
|
821 apply (erule_tac x = s in allE) |
|
822 apply (erule_tac x = s1' in allE) |
|
823 apply (erule_tac x = t1 in allE) |
|
824 apply (erule_tac x = n1 in allE) |
|
825 apply (erule_tac x = a in allE) |
|
826 apply (erule_tac x = n1 in allE) |
|
827 apply (erule_tac x = s1' in allE) |
|
828 apply (erule_tac x = s2' in allE) |
|
829 apply (erule_tac x = t2 in allE) |
|
830 apply (erule_tac x = n2 in allE) |
|
831 apply (rule conjI) |
|
832 apply (intro strip) |
|
833 apply (rule notI) |
|
834 apply simp |
|
835 apply (erule impE) |
|
836 apply (frule new_tv_subst_tel, assumption) |
|
837 apply (drule_tac a = "$s a" in new_tv_W, assumption) |
|
838 apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) |
|
839 apply (fastsimp simp add: subst_comp_tel) |
|
840 apply (intro strip) |
|
841 apply (rename_tac s2 t2' n2') |
|
842 apply (rule conjI) |
|
843 apply (intro strip) |
|
844 apply (rule notI) |
|
845 apply simp |
|
846 apply (erule impE) |
|
847 apply (frule new_tv_subst_tel, assumption) |
|
848 apply (drule_tac a = "$s a" in new_tv_W, assumption) |
|
849 apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) |
|
850 apply (fastsimp simp add: subst_comp_tel subst_comp_te) |
|
851 apply (intro strip) |
|
852 apply (erule (1) notE impE) |
|
853 apply (erule (1) notE impE) |
|
854 apply (erule exE) |
|
855 apply (erule conjE) |
|
856 apply (erule impE) |
|
857 apply (frule new_tv_subst_tel, assumption) |
|
858 apply (drule_tac a = "$s a" in new_tv_W, assumption) |
|
859 apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) |
|
860 apply (erule (1) notE impE) |
|
861 apply (erule exE conjE)+ |
|
862 apply (simp (asm_lr) add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+ |
|
863 apply (subgoal_tac "new_tv n2 s \<and> new_tv n2 r \<and> new_tv n2 ra") |
|
864 apply (simp add: new_tv_subst) |
|
865 apply (frule new_tv_subst_tel, assumption) |
|
866 apply (drule_tac a = "$s a" in new_tv_W, assumption) |
|
867 apply (tactic "safe_tac HOL_cs") |
|
868 apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) |
|
869 apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) |
|
870 apply (drule_tac e = e1 in sym [THEN W_var_geD]) |
|
871 apply (drule new_tv_subst_tel, assumption) |
|
872 apply (drule_tac ts = "$s a" in new_tv_list_le, assumption) |
|
873 apply (drule new_tv_subst_tel, assumption) |
|
874 apply (bestsimp dest: new_tv_W simp add: subst_comp_tel) |
|
875 done |
|
876 |
|
877 lemma I_complete_wrt_W: "!!a m s. |
|
878 new_tv m a \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Fail \<Longrightarrow> \<W> e ($s a) m = Fail" |
|
879 apply (atomize (full)) |
|
880 apply (induct e) |
|
881 apply (simp add: app_subst_list) |
|
882 apply (simp (no_asm)) |
|
883 apply (intro strip) |
|
884 apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)") |
|
885 apply (tactic {* asm_simp_tac (HOL_ss addsimps |
|
886 [thm "new_tv_Suc_list", @{thm lessI} RS @{thm less_imp_le} RS thm "new_tv_subst_le"]) 1 *}) |
|
887 apply (erule conjE) |
|
888 apply (drule new_tv_not_free_tv [THEN not_free_impl_id]) |
|
889 apply (simp (no_asm_simp)) |
|
890 apply (simp (no_asm_simp)) |
|
891 apply (intro strip) |
|
892 apply (erule exE)+ |
|
893 apply (erule conjE)+ |
|
894 apply (drule I_correct_wrt_W [COMP swap_prems_rl]) |
|
895 apply fast |
|
896 apply (erule exE) |
|
897 apply (erule conjE) |
|
898 apply hypsubst |
|
899 apply (simp (no_asm_simp)) |
|
900 apply (erule disjE) |
|
901 apply (rule disjI1) |
|
902 apply (simp (no_asm_use) add: o_def subst_comp_tel) |
|
903 apply (erule allE, erule allE, erule allE, erule impE, erule_tac [2] impE, |
|
904 erule_tac [2] asm_rl, erule_tac [2] asm_rl) |
|
905 apply (rule conjI) |
|
906 apply (fast intro: W_var_ge [THEN new_tv_list_le]) |
|
907 apply (rule new_tv_subst_comp_2) |
|
908 apply (fast intro: W_var_ge [THEN new_tv_subst_le]) |
|
909 apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1]) |
|
910 apply (rule disjI2) |
|
911 apply (erule exE)+ |
|
912 apply (erule conjE) |
|
913 apply (drule I_correct_wrt_W [COMP swap_prems_rl]) |
|
914 apply (rule conjI) |
|
915 apply (fast intro: W_var_ge [THEN new_tv_list_le]) |
|
916 apply (rule new_tv_subst_comp_1) |
|
917 apply (fast intro: W_var_ge [THEN new_tv_subst_le]) |
|
918 apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1]) |
|
919 apply (erule exE) |
|
920 apply (erule conjE) |
|
921 apply hypsubst |
|
922 apply (simp add: o_def subst_comp_te [symmetric] subst_comp_tel [symmetric]) |
|
923 done |
|
924 |
|
925 end |
|