author | lcp |
Wed, 19 Oct 1994 09:23:56 +0100 | |
changeset 642 | 0db578095e6a |
parent 10 | e37080f41102 |
child 757 | 2ca12511676d |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: 92/CCL/genrec |
2 |
ID: $Id$ |
|
3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
*) |
|
7 |
||
8 |
(*** General Recursive Functions ***) |
|
9 |
||
10 |
val major::prems = goal Wfd.thy |
|
11 |
"[| a : A; \ |
|
12 |
\ !!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==>\ |
|
13 |
\ h(p,g) : D(p) |] ==> \ |
|
14 |
\ letrec g x be h(x,g) in g(a) : D(a)"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
15 |
by (rtac (major RS rev_mp) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
16 |
by (rtac (wf_wf RS wfd_induct) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
17 |
by (rtac (letrecB RS ssubst) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
18 |
by (rtac impI 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
19 |
by (eresolve_tac prems 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
20 |
by (rtac ballI 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
21 |
by (etac (spec RS mp RS mp) 1); |
0 | 22 |
by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1)); |
23 |
val letrecT = result(); |
|
24 |
||
25 |
goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
26 |
by (rtac set_ext 1); |
0 | 27 |
by (fast_tac ccl_cs 1); |
28 |
val SPLITB = result(); |
|
29 |
||
30 |
val prems = goalw Wfd.thy [letrec2_def] |
|
31 |
"[| a : A; b : B; \ |
|
32 |
\ !!p q g.[| p:A; q:B; \ |
|
33 |
\ ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\ |
|
34 |
\ h(p,q,g) : D(p,q) |] ==> \ |
|
35 |
\ letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
36 |
by (rtac (SPLITB RS subst) 1); |
0 | 37 |
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
38 |
by (rtac (SPLITB RS ssubst) 1); |
0 | 39 |
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
40 |
by (rtac (SPLITB RS subst) 1); |
0 | 41 |
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE |
42 |
eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); |
|
43 |
val letrec2T = result(); |
|
44 |
||
45 |
goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)"; |
|
10
e37080f41102
This commit should not have been necessary. For some reason, the previous
lcp
parents:
0
diff
changeset
|
46 |
by (simp_tac (ccl_ss addsimps [SPLITB]) 1); |
0 | 47 |
val lemma = result(); |
48 |
||
49 |
val prems = goalw Wfd.thy [letrec3_def] |
|
50 |
"[| a : A; b : B; c : C; \ |
|
51 |
\ !!p q r g.[| p:A; q:B; r:C; \ |
|
52 |
\ ALL x:A.ALL y:B.ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \ |
|
53 |
\ g(x,y,z) : D(x,y,z) |] ==>\ |
|
54 |
\ h(p,q,r,g) : D(p,q,r) |] ==> \ |
|
55 |
\ letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
56 |
by (rtac (lemma RS subst) 1); |
0 | 57 |
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
10
e37080f41102
This commit should not have been necessary. For some reason, the previous
lcp
parents:
0
diff
changeset
|
58 |
by (simp_tac (ccl_ss addsimps [SPLITB]) 1); |
0 | 59 |
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
60 |
by (rtac (lemma RS subst) 1); |
0 | 61 |
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE |
62 |
eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); |
|
63 |
val letrec3T = result(); |
|
64 |
||
65 |
val letrecTs = [letrecT,letrec2T,letrec3T]; |
|
66 |
||
67 |
||
68 |
(*** Type Checking for Recursive Calls ***) |
|
69 |
||
70 |
val major::prems = goal Wfd.thy |
|
71 |
"[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); \ |
|
72 |
\ g(a) : D(a) ==> g(a) : E; a:A; <a,p>:wf(R) |] ==> \ |
|
73 |
\ g(a) : E"; |
|
74 |
by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1)); |
|
75 |
val rcallT = result(); |
|
76 |
||
77 |
val major::prems = goal Wfd.thy |
|
78 |
"[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ |
|
79 |
\ g(a,b) : D(a,b) ==> g(a,b) : E; a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \ |
|
80 |
\ g(a,b) : E"; |
|
81 |
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1)); |
|
82 |
val rcall2T = result(); |
|
83 |
||
84 |
val major::prems = goal Wfd.thy |
|
85 |
"[| 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); \ |
|
86 |
\ g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E; \ |
|
87 |
\ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \ |
|
88 |
\ g(a,b,c) : E"; |
|
89 |
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1)); |
|
90 |
val rcall3T = result(); |
|
91 |
||
92 |
val rcallTs = [rcallT,rcall2T,rcall3T]; |
|
93 |
||
94 |
(*** Instantiating an induction hypothesis with an equality assumption ***) |
|
95 |
||
96 |
val prems = goal Wfd.thy |
|
97 |
"[| g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); \ |
|
98 |
\ [| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); b=g(a); g(a) : D(a) |] ==> P; \ |
|
99 |
\ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A; \ |
|
100 |
\ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R) |] ==> \ |
|
101 |
\ P"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
102 |
by (resolve_tac (prems RL prems) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
103 |
by (resolve_tac (prems RL [sym]) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
104 |
by (rtac rcallT 1); |
0 | 105 |
by (REPEAT (ares_tac prems 1)); |
106 |
val hyprcallT = result(); |
|
107 |
||
108 |
val prems = goal Wfd.thy |
|
109 |
"[| g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);\ |
|
110 |
\ [| b=g(a); g(a) : D(a) |] ==> P; a:A; <a,p>:wf(R) |] ==> \ |
|
111 |
\ P"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
112 |
by (resolve_tac (prems) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
113 |
by (resolve_tac (prems RL [sym]) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
114 |
by (rtac rcallT 1); |
0 | 115 |
by (REPEAT (ares_tac prems 1)); |
116 |
val hyprcallT = result(); |
|
117 |
||
118 |
val prems = goal Wfd.thy |
|
119 |
"[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ |
|
120 |
\ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \ |
|
121 |
\ a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \ |
|
122 |
\ P"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
123 |
by (resolve_tac (prems) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
124 |
by (resolve_tac (prems RL [sym]) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
125 |
by (rtac rcall2T 1); |
0 | 126 |
by (REPEAT (ares_tac prems 1)); |
127 |
val hyprcall2T = result(); |
|
128 |
||
129 |
val prems = goal Wfd.thy |
|
130 |
"[| g(a,b,c) = d; \ |
|
131 |
\ 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); \ |
|
132 |
\ [| d=g(a,b,c); g(a,b,c) : D(a,b,c) |] ==> P; \ |
|
133 |
\ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \ |
|
134 |
\ P"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
135 |
by (resolve_tac (prems) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
136 |
by (resolve_tac (prems RL [sym]) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
10
diff
changeset
|
137 |
by (rtac rcall3T 1); |
0 | 138 |
by (REPEAT (ares_tac prems 1)); |
139 |
val hyprcall3T = result(); |
|
140 |
||
141 |
val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T]; |
|
142 |
||
143 |
(*** Rules to Remove Induction Hypotheses after Type Checking ***) |
|
144 |
||
145 |
val prems = goal Wfd.thy |
|
146 |
"[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> \ |
|
147 |
\ P"; |
|
148 |
by (REPEAT (ares_tac prems 1)); |
|
149 |
val rmIH1 = result(); |
|
150 |
||
151 |
val prems = goal Wfd.thy |
|
152 |
"[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \ |
|
153 |
\ P"; |
|
154 |
by (REPEAT (ares_tac prems 1)); |
|
155 |
val rmIH2 = result(); |
|
156 |
||
157 |
val prems = goal Wfd.thy |
|
158 |
"[| 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); \ |
|
159 |
\ P |] ==> \ |
|
160 |
\ P"; |
|
161 |
by (REPEAT (ares_tac prems 1)); |
|
162 |
val rmIH3 = result(); |
|
163 |
||
164 |
val rmIHs = [rmIH1,rmIH2,rmIH3]; |
|
165 |