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)";
|
|
15 |
br (major RS rev_mp) 1;
|
|
16 |
br (wf_wf RS wfd_induct) 1;
|
|
17 |
br (letrecB RS ssubst) 1;
|
|
18 |
br impI 1;
|
|
19 |
bes prems 1;
|
|
20 |
br ballI 1;
|
|
21 |
be (spec RS mp RS mp) 1;
|
|
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)";
|
|
26 |
br set_ext 1;
|
|
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)";
|
|
36 |
br (SPLITB RS subst) 1;
|
|
37 |
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
|
|
38 |
br (SPLITB RS ssubst) 1;
|
|
39 |
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
|
|
40 |
br (SPLITB RS subst) 1;
|
|
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)";
|
|
46 |
by (SIMP_TAC (ccl_ss addrews [SPLITB]) 1);
|
|
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)";
|
|
56 |
br (lemma RS subst) 1;
|
|
57 |
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
|
|
58 |
by (SIMP_TAC (ccl_ss addrews [SPLITB]) 1);
|
|
59 |
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
|
|
60 |
br (lemma RS subst) 1;
|
|
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";
|
|
102 |
brs (prems RL prems) 1;
|
|
103 |
brs (prems RL [sym]) 1;
|
|
104 |
br rcallT 1;
|
|
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";
|
|
112 |
brs (prems) 1;
|
|
113 |
brs (prems RL [sym]) 1;
|
|
114 |
br rcallT 1;
|
|
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";
|
|
123 |
brs (prems) 1;
|
|
124 |
brs (prems RL [sym]) 1;
|
|
125 |
br rcall2T 1;
|
|
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";
|
|
135 |
brs (prems) 1;
|
|
136 |
brs (prems RL [sym]) 1;
|
|
137 |
br rcall3T 1;
|
|
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 |
|