author | wenzelm |
Sat, 21 Nov 2009 17:01:44 +0100 | |
changeset 33834 | 7c06e19f717c |
parent 33317 | b4534348b8fd |
child 36319 | 8feb2c4bef1a |
permissions | -rw-r--r-- |
17456 | 1 |
(* Title: CCL/Wfd.thy |
1474 | 2 |
Author: Martin Coen, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1993 University of Cambridge |
4 |
*) |
|
5 |
||
17456 | 6 |
header {* Well-founded relations in CCL *} |
7 |
||
8 |
theory Wfd |
|
9 |
imports Trancl Type Hered |
|
10 |
begin |
|
0 | 11 |
|
12 |
consts |
|
13 |
(*** Predicates ***) |
|
14 |
Wfd :: "[i set] => o" |
|
15 |
(*** Relations ***) |
|
16 |
wf :: "[i set] => i set" |
|
17 |
wmap :: "[i=>i,i set] => i set" |
|
24825 | 18 |
lex :: "[i set,i set] => i set" (infixl "**" 70) |
0 | 19 |
NatPR :: "i set" |
20 |
ListPR :: "i set => i set" |
|
21 |
||
24825 | 22 |
defs |
0 | 23 |
|
17456 | 24 |
Wfd_def: |
3837 | 25 |
"Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)" |
0 | 26 |
|
17456 | 27 |
wf_def: "wf(R) == {x. x:R & Wfd(R)}" |
0 | 28 |
|
17456 | 29 |
wmap_def: "wmap(f,R) == {p. EX x y. p=<x,y> & <f(x),f(y)> : R}" |
30 |
lex_def: |
|
3837 | 31 |
"ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}" |
0 | 32 |
|
17456 | 33 |
NatPR_def: "NatPR == {p. EX x:Nat. p=<x,succ(x)>}" |
34 |
ListPR_def: "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}" |
|
35 |
||
20140 | 36 |
|
37 |
lemma wfd_induct: |
|
38 |
assumes 1: "Wfd(R)" |
|
39 |
and 2: "!!x.[| ALL y. <y,x>: R --> P(y) |] ==> P(x)" |
|
40 |
shows "P(a)" |
|
41 |
apply (rule 1 [unfolded Wfd_def, rule_format, THEN CollectD]) |
|
42 |
using 2 apply blast |
|
43 |
done |
|
44 |
||
45 |
lemma wfd_strengthen_lemma: |
|
46 |
assumes 1: "!!x y.<x,y> : R ==> Q(x)" |
|
47 |
and 2: "ALL x. (ALL y. <y,x> : R --> y : P) --> x : P" |
|
48 |
and 3: "!!x. Q(x) ==> x:P" |
|
49 |
shows "a:P" |
|
50 |
apply (rule 2 [rule_format]) |
|
51 |
using 1 3 |
|
52 |
apply blast |
|
53 |
done |
|
54 |
||
55 |
ML {* |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset
|
56 |
fun wfd_strengthen_tac ctxt s i = |
27239 | 57 |
res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1) |
20140 | 58 |
*} |
59 |
||
60 |
lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P" |
|
61 |
apply (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P") |
|
62 |
apply blast |
|
63 |
apply (erule wfd_induct) |
|
64 |
apply blast |
|
65 |
done |
|
66 |
||
67 |
lemma wf_anti_refl: "[| Wfd(r); <a,a>: r |] ==> P" |
|
68 |
apply (rule wf_anti_sym) |
|
69 |
apply assumption+ |
|
70 |
done |
|
71 |
||
72 |
||
73 |
subsection {* Irreflexive transitive closure *} |
|
74 |
||
75 |
lemma trancl_wf: |
|
76 |
assumes 1: "Wfd(R)" |
|
77 |
shows "Wfd(R^+)" |
|
78 |
apply (unfold Wfd_def) |
|
79 |
apply (rule allI ballI impI)+ |
|
80 |
(*must retain the universal formula for later use!*) |
|
81 |
apply (rule allE, assumption) |
|
82 |
apply (erule mp) |
|
83 |
apply (rule 1 [THEN wfd_induct]) |
|
84 |
apply (rule impI [THEN allI]) |
|
85 |
apply (erule tranclE) |
|
86 |
apply blast |
|
87 |
apply (erule spec [THEN mp, THEN spec, THEN mp]) |
|
88 |
apply assumption+ |
|
89 |
done |
|
90 |
||
91 |
||
92 |
subsection {* Lexicographic Ordering *} |
|
93 |
||
94 |
lemma lexXH: |
|
95 |
"p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))" |
|
96 |
unfolding lex_def by blast |
|
97 |
||
98 |
lemma lexI1: "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb" |
|
99 |
by (blast intro!: lexXH [THEN iffD2]) |
|
100 |
||
101 |
lemma lexI2: "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb" |
|
102 |
by (blast intro!: lexXH [THEN iffD2]) |
|
103 |
||
104 |
lemma lexE: |
|
105 |
assumes 1: "p : ra**rb" |
|
106 |
and 2: "!!a a' b b'.[| <a,a'> : ra; p=<<a,b>,<a',b'>> |] ==> R" |
|
107 |
and 3: "!!a b b'.[| <b,b'> : rb; p = <<a,b>,<a,b'>> |] ==> R" |
|
108 |
shows R |
|
109 |
apply (rule 1 [THEN lexXH [THEN iffD1], THEN exE]) |
|
110 |
using 2 3 |
|
111 |
apply blast |
|
112 |
done |
|
113 |
||
114 |
lemma lex_pair: "[| p : r**s; !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P" |
|
115 |
apply (erule lexE) |
|
116 |
apply blast+ |
|
117 |
done |
|
118 |
||
119 |
lemma lex_wf: |
|
120 |
assumes 1: "Wfd(R)" |
|
121 |
and 2: "Wfd(S)" |
|
122 |
shows "Wfd(R**S)" |
|
123 |
apply (unfold Wfd_def) |
|
124 |
apply safe |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset
|
125 |
apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=<a,b>" 1 *}) |
20140 | 126 |
apply (blast elim!: lex_pair) |
127 |
apply (subgoal_tac "ALL a b.<a,b>:P") |
|
128 |
apply blast |
|
129 |
apply (rule 1 [THEN wfd_induct, THEN allI]) |
|
130 |
apply (rule 2 [THEN wfd_induct, THEN allI]) back |
|
131 |
apply (fast elim!: lexE) |
|
132 |
done |
|
133 |
||
134 |
||
135 |
subsection {* Mapping *} |
|
136 |
||
137 |
lemma wmapXH: "p : wmap(f,r) <-> (EX x y. p=<x,y> & <f(x),f(y)> : r)" |
|
138 |
unfolding wmap_def by blast |
|
139 |
||
140 |
lemma wmapI: "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)" |
|
141 |
by (blast intro!: wmapXH [THEN iffD2]) |
|
142 |
||
143 |
lemma wmapE: "[| p : wmap(f,r); !!a b.[| <f(a),f(b)> : r; p=<a,b> |] ==> R |] ==> R" |
|
144 |
by (blast dest!: wmapXH [THEN iffD1]) |
|
145 |
||
146 |
lemma wmap_wf: |
|
147 |
assumes 1: "Wfd(r)" |
|
148 |
shows "Wfd(wmap(f,r))" |
|
149 |
apply (unfold Wfd_def) |
|
150 |
apply clarify |
|
151 |
apply (subgoal_tac "ALL b. ALL a. f (a) =b-->a:P") |
|
152 |
apply blast |
|
153 |
apply (rule 1 [THEN wfd_induct, THEN allI]) |
|
154 |
apply clarify |
|
155 |
apply (erule spec [THEN mp]) |
|
156 |
apply (safe elim!: wmapE) |
|
157 |
apply (erule spec [THEN mp, THEN spec, THEN mp]) |
|
158 |
apply assumption |
|
159 |
apply (rule refl) |
|
160 |
done |
|
161 |
||
162 |
||
163 |
subsection {* Projections *} |
|
164 |
||
165 |
lemma wfstI: "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)" |
|
166 |
apply (rule wmapI) |
|
167 |
apply simp |
|
168 |
done |
|
169 |
||
170 |
lemma wsndI: "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)" |
|
171 |
apply (rule wmapI) |
|
172 |
apply simp |
|
173 |
done |
|
174 |
||
175 |
lemma wthdI: "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)" |
|
176 |
apply (rule wmapI) |
|
177 |
apply simp |
|
178 |
done |
|
179 |
||
180 |
||
181 |
subsection {* Ground well-founded relations *} |
|
182 |
||
183 |
lemma wfI: "[| Wfd(r); a : r |] ==> a : wf(r)" |
|
184 |
unfolding wf_def by blast |
|
185 |
||
186 |
lemma Empty_wf: "Wfd({})" |
|
187 |
unfolding Wfd_def by (blast elim: EmptyXH [THEN iffD1, THEN FalseE]) |
|
188 |
||
189 |
lemma wf_wf: "Wfd(wf(R))" |
|
190 |
unfolding wf_def |
|
191 |
apply (rule_tac Q = "Wfd(R)" in excluded_middle [THEN disjE]) |
|
192 |
apply simp_all |
|
193 |
apply (rule Empty_wf) |
|
194 |
done |
|
195 |
||
196 |
lemma NatPRXH: "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)" |
|
197 |
unfolding NatPR_def by blast |
|
198 |
||
199 |
lemma ListPRXH: "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)" |
|
200 |
unfolding ListPR_def by blast |
|
201 |
||
202 |
lemma NatPRI: "x : Nat ==> <x,succ(x)> : NatPR" |
|
203 |
by (auto simp: NatPRXH) |
|
204 |
||
205 |
lemma ListPRI: "[| t : List(A); h : A |] ==> <t,h $ t> : ListPR(A)" |
|
206 |
by (auto simp: ListPRXH) |
|
207 |
||
208 |
lemma NatPR_wf: "Wfd(NatPR)" |
|
209 |
apply (unfold Wfd_def) |
|
210 |
apply clarify |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset
|
211 |
apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *}) |
20140 | 212 |
apply (fastsimp iff: NatPRXH) |
213 |
apply (erule Nat_ind) |
|
214 |
apply (fastsimp iff: NatPRXH)+ |
|
215 |
done |
|
216 |
||
217 |
lemma ListPR_wf: "Wfd(ListPR(A))" |
|
218 |
apply (unfold Wfd_def) |
|
219 |
apply clarify |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset
|
220 |
apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *}) |
20140 | 221 |
apply (fastsimp iff: ListPRXH) |
222 |
apply (erule List_ind) |
|
223 |
apply (fastsimp iff: ListPRXH)+ |
|
224 |
done |
|
225 |
||
226 |
||
227 |
subsection {* General Recursive Functions *} |
|
228 |
||
229 |
lemma letrecT: |
|
230 |
assumes 1: "a : A" |
|
231 |
and 2: "!!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==> h(p,g) : D(p)" |
|
232 |
shows "letrec g x be h(x,g) in g(a) : D(a)" |
|
233 |
apply (rule 1 [THEN rev_mp]) |
|
234 |
apply (rule wf_wf [THEN wfd_induct]) |
|
235 |
apply (subst letrecB) |
|
236 |
apply (rule impI) |
|
237 |
apply (erule 2) |
|
238 |
apply blast |
|
239 |
done |
|
240 |
||
241 |
lemma SPLITB: "SPLIT(<a,b>,B) = B(a,b)" |
|
242 |
unfolding SPLIT_def |
|
243 |
apply (rule set_ext) |
|
244 |
apply blast |
|
245 |
done |
|
17456 | 246 |
|
20140 | 247 |
lemma letrec2T: |
248 |
assumes "a : A" |
|
249 |
and "b : B" |
|
250 |
and "!!p q g.[| p:A; q:B; |
|
251 |
ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==> |
|
252 |
h(p,q,g) : D(p,q)" |
|
253 |
shows "letrec g x y be h(x,y,g) in g(a,b) : D(a,b)" |
|
254 |
apply (unfold letrec2_def) |
|
255 |
apply (rule SPLITB [THEN subst]) |
|
256 |
apply (assumption | rule letrecT pairT splitT prems)+ |
|
257 |
apply (subst SPLITB) |
|
258 |
apply (assumption | rule ballI SubtypeI prems)+ |
|
259 |
apply (rule SPLITB [THEN subst]) |
|
260 |
apply (assumption | rule letrecT SubtypeI pairT splitT prems | |
|
261 |
erule bspec SubtypeE sym [THEN subst])+ |
|
262 |
done |
|
263 |
||
264 |
lemma lem: "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)" |
|
265 |
by (simp add: SPLITB) |
|
266 |
||
267 |
lemma letrec3T: |
|
268 |
assumes "a : A" |
|
269 |
and "b : B" |
|
270 |
and "c : C" |
|
271 |
and "!!p q r g.[| p:A; q:B; r:C; |
|
272 |
ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. |
|
273 |
g(x,y,z) : D(x,y,z) |] ==> |
|
274 |
h(p,q,r,g) : D(p,q,r)" |
|
275 |
shows "letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)" |
|
276 |
apply (unfold letrec3_def) |
|
277 |
apply (rule lem [THEN subst]) |
|
278 |
apply (assumption | rule letrecT pairT splitT prems)+ |
|
279 |
apply (simp add: SPLITB) |
|
280 |
apply (assumption | rule ballI SubtypeI prems)+ |
|
281 |
apply (rule lem [THEN subst]) |
|
282 |
apply (assumption | rule letrecT SubtypeI pairT splitT prems | |
|
283 |
erule bspec SubtypeE sym [THEN subst])+ |
|
284 |
done |
|
285 |
||
286 |
lemmas letrecTs = letrecT letrec2T letrec3T |
|
287 |
||
288 |
||
289 |
subsection {* Type Checking for Recursive Calls *} |
|
290 |
||
291 |
lemma rcallT: |
|
292 |
"[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); |
|
293 |
g(a) : D(a) ==> g(a) : E; a:A; <a,p>:wf(R) |] ==> |
|
294 |
g(a) : E" |
|
295 |
by blast |
|
296 |
||
297 |
lemma rcall2T: |
|
298 |
"[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); |
|
299 |
g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> |
|
300 |
g(a,b) : E" |
|
301 |
by blast |
|
302 |
||
303 |
lemma rcall3T: |
|
304 |
"[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); |
|
305 |
g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; |
|
306 |
a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> |
|
307 |
g(a,b,c) : E" |
|
308 |
by blast |
|
309 |
||
310 |
lemmas rcallTs = rcallT rcall2T rcall3T |
|
311 |
||
312 |
||
313 |
subsection {* Instantiating an induction hypothesis with an equality assumption *} |
|
314 |
||
315 |
lemma hyprcallT: |
|
316 |
assumes 1: "g(a) = b" |
|
317 |
and 2: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x)" |
|
318 |
and 3: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> b=g(a) ==> g(a) : D(a) ==> P" |
|
319 |
and 4: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A" |
|
320 |
and 5: "ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R)" |
|
321 |
shows P |
|
322 |
apply (rule 3 [OF 2, OF 1 [symmetric]]) |
|
323 |
apply (rule rcallT [OF 2]) |
|
324 |
apply assumption |
|
325 |
apply (rule 4 [OF 2]) |
|
326 |
apply (rule 5 [OF 2]) |
|
327 |
done |
|
328 |
||
329 |
lemma hyprcall2T: |
|
330 |
assumes 1: "g(a,b) = c" |
|
331 |
and 2: "ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y)" |
|
332 |
and 3: "[| c=g(a,b); g(a,b) : D(a,b) |] ==> P" |
|
333 |
and 4: "a:A" |
|
334 |
and 5: "b:B" |
|
335 |
and 6: "<<a,b>,<p,q>>:wf(R)" |
|
336 |
shows P |
|
337 |
apply (rule 3) |
|
338 |
apply (rule 1 [symmetric]) |
|
339 |
apply (rule rcall2T) |
|
23467 | 340 |
apply (rule 2) |
341 |
apply assumption |
|
342 |
apply (rule 4) |
|
343 |
apply (rule 5) |
|
344 |
apply (rule 6) |
|
20140 | 345 |
done |
346 |
||
347 |
lemma hyprcall3T: |
|
348 |
assumes 1: "g(a,b,c) = d" |
|
349 |
and 2: "ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z)" |
|
350 |
and 3: "[| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P" |
|
351 |
and 4: "a:A" |
|
352 |
and 5: "b:B" |
|
353 |
and 6: "c:C" |
|
354 |
and 7: "<<a,<b,c>>,<p,<q,r>>> : wf(R)" |
|
355 |
shows P |
|
356 |
apply (rule 3) |
|
357 |
apply (rule 1 [symmetric]) |
|
358 |
apply (rule rcall3T) |
|
23467 | 359 |
apply (rule 2) |
360 |
apply assumption |
|
361 |
apply (rule 4) |
|
362 |
apply (rule 5) |
|
363 |
apply (rule 6) |
|
364 |
apply (rule 7) |
|
20140 | 365 |
done |
366 |
||
367 |
lemmas hyprcallTs = hyprcallT hyprcall2T hyprcall3T |
|
368 |
||
369 |
||
370 |
subsection {* Rules to Remove Induction Hypotheses after Type Checking *} |
|
371 |
||
372 |
lemma rmIH1: "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> P" . |
|
373 |
||
374 |
lemma rmIH2: "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> P" . |
|
375 |
||
376 |
lemma rmIH3: |
|
377 |
"[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); |
|
378 |
P |] ==> |
|
379 |
P" . |
|
380 |
||
381 |
lemmas rmIHs = rmIH1 rmIH2 rmIH3 |
|
382 |
||
383 |
||
384 |
subsection {* Lemmas for constructors and subtypes *} |
|
385 |
||
386 |
(* 0-ary constructors do not need additional rules as they are handled *) |
|
387 |
(* correctly by applying SubtypeI *) |
|
388 |
||
389 |
lemma Subtype_canTs: |
|
390 |
"!!a b A B P. a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}" |
|
391 |
"!!a A B P. a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}" |
|
392 |
"!!b A B P. b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}" |
|
393 |
"!!a P. a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}" |
|
394 |
"!!h t A P. h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}" |
|
395 |
by (assumption | rule SubtypeI canTs icanTs | erule SubtypeE)+ |
|
396 |
||
397 |
lemma letT: "[| f(t):B; ~t=bot |] ==> let x be t in f(x) : B" |
|
398 |
apply (erule letB [THEN ssubst]) |
|
399 |
apply assumption |
|
400 |
done |
|
401 |
||
402 |
lemma applyT2: "[| a:A; f : Pi(A,B) |] ==> f ` a : B(a)" |
|
403 |
apply (erule applyT) |
|
404 |
apply assumption |
|
405 |
done |
|
406 |
||
407 |
lemma rcall_lemma1: "[| a:A; a:A ==> P(a) |] ==> a : {x:A. P(x)}" |
|
408 |
by blast |
|
409 |
||
410 |
lemma rcall_lemma2: "[| a:{x:A. Q(x)}; [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}" |
|
411 |
by blast |
|
412 |
||
413 |
lemmas rcall_lemmas = asm_rl rcall_lemma1 SubtypeD1 rcall_lemma2 |
|
414 |
||
415 |
||
416 |
subsection {* Typechecking *} |
|
417 |
||
418 |
ML {* |
|
419 |
||
420 |
local |
|
421 |
||
422 |
val type_rls = |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
423 |
@{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @ |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
424 |
@{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs}; |
20140 | 425 |
|
426 |
fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l) |
|
427 |
| bvars _ l = l |
|
428 |
||
429 |
fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t |
|
430 |
| get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t |
|
431 |
| get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t |
|
24825 | 432 |
| get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t |
20140 | 433 |
| get_bno l n (t $ s) = get_bno l n t |
434 |
| get_bno l n (Bound m) = (m-length(l),n) |
|
435 |
||
436 |
(* Not a great way of identifying induction hypothesis! *) |
|
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29264
diff
changeset
|
437 |
fun could_IH x = Term.could_unify(x,hd (prems_of @{thm rcallT})) orelse |
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29264
diff
changeset
|
438 |
Term.could_unify(x,hd (prems_of @{thm rcall2T})) orelse |
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29264
diff
changeset
|
439 |
Term.could_unify(x,hd (prems_of @{thm rcall3T})) |
20140 | 440 |
|
441 |
fun IHinst tac rls = SUBGOAL (fn (Bi,i) => |
|
442 |
let val bvs = bvars Bi [] |
|
33317 | 443 |
val ihs = filter could_IH (Logic.strip_assums_hyp Bi) |
20140 | 444 |
val rnames = map (fn x=> |
445 |
let val (a,b) = get_bno [] 0 x |
|
446 |
in (List.nth(bvs,a),b) end) ihs |
|
447 |
fun try_IHs [] = no_tac |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
448 |
| try_IHs ((x,y)::xs) = tac [(("g", 0), x)] (List.nth(rls,y-1)) i ORELSE (try_IHs xs) |
20140 | 449 |
in try_IHs rnames end) |
450 |
||
451 |
fun is_rigid_prog t = |
|
452 |
case (Logic.strip_assums_concl t) of |
|
29264 | 453 |
(Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => null (Term.add_vars a []) |
20140 | 454 |
| _ => false |
455 |
in |
|
456 |
||
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
457 |
fun rcall_tac ctxt i = |
27239 | 458 |
let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i |
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
459 |
in IHinst tac @{thms rcallTs} i end |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
460 |
THEN eresolve_tac @{thms rcall_lemmas} i |
20140 | 461 |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
462 |
fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
463 |
rcall_tac ctxt i ORELSE |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
464 |
ematch_tac [@{thm SubtypeE}] i ORELSE |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
465 |
match_tac [@{thm SubtypeI}] i |
20140 | 466 |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
467 |
fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) => |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
468 |
if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac) |
20140 | 469 |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
470 |
fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i |
20140 | 471 |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
472 |
fun tac ctxt = typechk_tac ctxt [] 1 |
20140 | 473 |
|
474 |
(*** Clean up Correctness Condictions ***) |
|
475 |
||
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
476 |
val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' |
20140 | 477 |
hyp_subst_tac) |
478 |
||
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
479 |
fun clean_ccs_tac ctxt = |
27239 | 480 |
let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in |
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
481 |
TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE' |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
482 |
eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
483 |
hyp_subst_tac)) |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
484 |
end |
20140 | 485 |
|
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
486 |
fun gen_ccs_tac ctxt rls i = |
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27208
diff
changeset
|
487 |
SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls) THEN clean_ccs_tac ctxt) i |
17456 | 488 |
|
0 | 489 |
end |
20140 | 490 |
*} |
491 |
||
492 |
||
493 |
subsection {* Evaluation *} |
|
494 |
||
495 |
ML {* |
|
496 |
||
497 |
local |
|
31902 | 498 |
structure Data = Named_Thms(val name = "eval" val description = "evaluation rules"); |
20140 | 499 |
in |
500 |
||
32282
853ef99c04cc
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
wenzelm
parents:
32211
diff
changeset
|
501 |
fun eval_tac ths = |
32283 | 502 |
Subgoal.FOCUS_PREMS (fn {context, prems, ...} => |
32282
853ef99c04cc
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
wenzelm
parents:
32211
diff
changeset
|
503 |
DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1)); |
20140 | 504 |
|
505 |
val eval_setup = |
|
24034 | 506 |
Data.setup #> |
30515 | 507 |
Method.setup @{binding eval} |
32282
853ef99c04cc
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
wenzelm
parents:
32211
diff
changeset
|
508 |
(Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))) |
30515 | 509 |
"evaluation"; |
20140 | 510 |
|
511 |
end; |
|
512 |
||
513 |
*} |
|
514 |
||
515 |
setup eval_setup |
|
516 |
||
517 |
lemmas eval_rls [eval] = trueV falseV pairV lamV caseVtrue caseVfalse caseVpair caseVlam |
|
518 |
||
519 |
lemma applyV [eval]: |
|
520 |
assumes "f ---> lam x. b(x)" |
|
521 |
and "b(a) ---> c" |
|
522 |
shows "f ` a ---> c" |
|
523 |
unfolding apply_def by (eval prems) |
|
524 |
||
525 |
lemma letV: |
|
526 |
assumes 1: "t ---> a" |
|
527 |
and 2: "f(a) ---> c" |
|
528 |
shows "let x be t in f(x) ---> c" |
|
529 |
apply (unfold let_def) |
|
530 |
apply (rule 1 [THEN canonical]) |
|
531 |
apply (tactic {* |
|
26391 | 532 |
REPEAT (DEPTH_SOLVE_1 (resolve_tac (@{thms assms} @ @{thms eval_rls}) 1 ORELSE |
533 |
etac @{thm substitute} 1)) *}) |
|
20140 | 534 |
done |
535 |
||
536 |
lemma fixV: "f(fix(f)) ---> c ==> fix(f) ---> c" |
|
537 |
apply (unfold fix_def) |
|
538 |
apply (rule applyV) |
|
539 |
apply (rule lamV) |
|
540 |
apply assumption |
|
541 |
done |
|
542 |
||
543 |
lemma letrecV: |
|
544 |
"h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==> |
|
545 |
letrec g x be h(x,g) in g(t) ---> c" |
|
546 |
apply (unfold letrec_def) |
|
547 |
apply (assumption | rule fixV applyV lamV)+ |
|
548 |
done |
|
549 |
||
550 |
lemmas [eval] = letV letrecV fixV |
|
551 |
||
552 |
lemma V_rls [eval]: |
|
553 |
"true ---> true" |
|
554 |
"false ---> false" |
|
555 |
"!!b c t u. [| b--->true; t--->c |] ==> if b then t else u ---> c" |
|
556 |
"!!b c t u. [| b--->false; u--->c |] ==> if b then t else u ---> c" |
|
557 |
"!!a b. <a,b> ---> <a,b>" |
|
558 |
"!!a b c t h. [| t ---> <a,b>; h(a,b) ---> c |] ==> split(t,h) ---> c" |
|
559 |
"zero ---> zero" |
|
560 |
"!!n. succ(n) ---> succ(n)" |
|
561 |
"!!c n t u. [| n ---> zero; t ---> c |] ==> ncase(n,t,u) ---> c" |
|
562 |
"!!c n t u x. [| n ---> succ(x); u(x) ---> c |] ==> ncase(n,t,u) ---> c" |
|
563 |
"!!c n t u. [| n ---> zero; t ---> c |] ==> nrec(n,t,u) ---> c" |
|
564 |
"!!c n t u x. [| n--->succ(x); u(x,nrec(x,t,u))--->c |] ==> nrec(n,t,u)--->c" |
|
565 |
"[] ---> []" |
|
566 |
"!!h t. h$t ---> h$t" |
|
567 |
"!!c l t u. [| l ---> []; t ---> c |] ==> lcase(l,t,u) ---> c" |
|
568 |
"!!c l t u x xs. [| l ---> x$xs; u(x,xs) ---> c |] ==> lcase(l,t,u) ---> c" |
|
569 |
"!!c l t u. [| l ---> []; t ---> c |] ==> lrec(l,t,u) ---> c" |
|
570 |
"!!c l t u x xs. [| l--->x$xs; u(x,xs,lrec(xs,t,u))--->c |] ==> lrec(l,t,u)--->c" |
|
571 |
unfolding data_defs by eval+ |
|
572 |
||
573 |
||
574 |
subsection {* Factorial *} |
|
575 |
||
576 |
lemma |
|
577 |
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) |
|
578 |
in f(succ(succ(zero))) ---> ?a" |
|
579 |
by eval |
|
580 |
||
581 |
lemma |
|
582 |
"letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) |
|
583 |
in f(succ(succ(succ(zero)))) ---> ?a" |
|
584 |
by eval |
|
585 |
||
586 |
subsection {* Less Than Or Equal *} |
|
587 |
||
588 |
lemma |
|
589 |
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) |
|
590 |
in f(<succ(zero), succ(zero)>) ---> ?a" |
|
591 |
by eval |
|
592 |
||
593 |
lemma |
|
594 |
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) |
|
595 |
in f(<succ(zero), succ(succ(succ(succ(zero))))>) ---> ?a" |
|
596 |
by eval |
|
597 |
||
598 |
lemma |
|
599 |
"letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) |
|
600 |
in f(<succ(succ(succ(succ(succ(zero))))), succ(succ(succ(succ(zero))))>) ---> ?a" |
|
601 |
by eval |
|
602 |
||
603 |
||
604 |
subsection {* Reverse *} |
|
605 |
||
606 |
lemma |
|
607 |
"letrec id l be lcase(l,[],%x xs. x$id(xs)) |
|
608 |
in id(zero$succ(zero)$[]) ---> ?a" |
|
609 |
by eval |
|
610 |
||
611 |
lemma |
|
612 |
"letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) |
|
613 |
in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a" |
|
614 |
by eval |
|
615 |
||
616 |
end |