1 (* Title: 92/CCL/genrec |
1 (* Title: CCL/genrec.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 (*** General Recursive Functions ***) |
8 (*** General Recursive Functions ***) |
9 |
9 |
10 val major::prems = goal Wfd.thy |
10 val major::prems = goal (the_context ()) |
11 "[| a : A; \ |
11 "[| a : A; \ |
12 \ !!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==>\ |
12 \ !!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==>\ |
13 \ h(p,g) : D(p) |] ==> \ |
13 \ h(p,g) : D(p) |] ==> \ |
14 \ letrec g x be h(x,g) in g(a) : D(a)"; |
14 \ letrec g x be h(x,g) in g(a) : D(a)"; |
15 by (rtac (major RS rev_mp) 1); |
15 by (rtac (major RS rev_mp) 1); |
20 by (rtac ballI 1); |
20 by (rtac ballI 1); |
21 by (etac (spec RS mp RS mp) 1); |
21 by (etac (spec RS mp RS mp) 1); |
22 by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1)); |
22 by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1)); |
23 qed "letrecT"; |
23 qed "letrecT"; |
24 |
24 |
25 goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)"; |
25 goalw (the_context ()) [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)"; |
26 by (rtac set_ext 1); |
26 by (rtac set_ext 1); |
27 by (fast_tac ccl_cs 1); |
27 by (fast_tac ccl_cs 1); |
28 qed "SPLITB"; |
28 qed "SPLITB"; |
29 |
29 |
30 val prems = goalw Wfd.thy [letrec2_def] |
30 val prems = goalw (the_context ()) [letrec2_def] |
31 "[| a : A; b : B; \ |
31 "[| a : A; b : B; \ |
32 \ !!p q g.[| p:A; q: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) |] ==>\ |
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) |] ==> \ |
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)"; |
35 \ letrec g x y be h(x,y,g) in g(a,b) : D(a,b)"; |
36 by (rtac (SPLITB RS subst) 1); |
36 by (rtac (SPLITB RS subst) 1); |
37 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
37 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
38 by (stac SPLITB 1); |
38 by (stac SPLITB 1); |
39 by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); |
39 by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); |
40 by (rtac (SPLITB RS subst) 1); |
40 by (rtac (SPLITB RS subst) 1); |
41 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE |
41 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE |
42 eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); |
42 eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); |
43 qed "letrec2T"; |
43 qed "letrec2T"; |
44 |
44 |
45 goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"; |
45 goal (the_context ()) "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)"; |
46 by (simp_tac (ccl_ss addsimps [SPLITB]) 1); |
46 by (simp_tac (ccl_ss addsimps [SPLITB]) 1); |
47 qed "lemma"; |
47 qed "lemma"; |
48 |
48 |
49 val prems = goalw Wfd.thy [letrec3_def] |
49 val prems = goalw (the_context ()) [letrec3_def] |
50 "[| a : A; b : B; c : C; \ |
50 "[| a : A; b : B; c : C; \ |
51 \ !!p q r g.[| p:A; q:B; r: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)}. \ |
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) |] ==>\ |
53 \ g(x,y,z) : D(x,y,z) |] ==>\ |
54 \ h(p,q,r,g) : D(p,q,r) |] ==> \ |
54 \ h(p,q,r,g) : D(p,q,r) |] ==> \ |
56 by (rtac (lemma RS subst) 1); |
56 by (rtac (lemma RS subst) 1); |
57 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
57 by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); |
58 by (simp_tac (ccl_ss addsimps [SPLITB]) 1); |
58 by (simp_tac (ccl_ss addsimps [SPLITB]) 1); |
59 by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); |
59 by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); |
60 by (rtac (lemma RS subst) 1); |
60 by (rtac (lemma RS subst) 1); |
61 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE |
61 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE |
62 eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); |
62 eresolve_tac [bspec,SubtypeE,sym RS subst] 1)); |
63 qed "letrec3T"; |
63 qed "letrec3T"; |
64 |
64 |
65 val letrecTs = [letrecT,letrec2T,letrec3T]; |
65 val letrecTs = [letrecT,letrec2T,letrec3T]; |
66 |
66 |
67 |
67 |
68 (*** Type Checking for Recursive Calls ***) |
68 (*** Type Checking for Recursive Calls ***) |
69 |
69 |
70 val major::prems = goal Wfd.thy |
70 val major::prems = goal (the_context ()) |
71 "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); \ |
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) |] ==> \ |
72 \ g(a) : D(a) ==> g(a) : E; a:A; <a,p>:wf(R) |] ==> \ |
73 \ g(a) : E"; |
73 \ g(a) : E"; |
74 by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1)); |
74 by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1)); |
75 qed "rcallT"; |
75 qed "rcallT"; |
76 |
76 |
77 val major::prems = goal Wfd.thy |
77 val major::prems = goal (the_context ()) |
78 "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ |
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) |] ==> \ |
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"; |
80 \ g(a,b) : E"; |
81 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1)); |
81 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1)); |
82 qed "rcall2T"; |
82 qed "rcall2T"; |
83 |
83 |
84 val major::prems = goal Wfd.thy |
84 val major::prems = goal (the_context ()) |
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); \ |
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; \ |
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) |] ==> \ |
87 \ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \ |
88 \ g(a,b,c) : E"; |
88 \ g(a,b,c) : E"; |
89 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1)); |
89 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1)); |
91 |
91 |
92 val rcallTs = [rcallT,rcall2T,rcall3T]; |
92 val rcallTs = [rcallT,rcall2T,rcall3T]; |
93 |
93 |
94 (*** Instantiating an induction hypothesis with an equality assumption ***) |
94 (*** Instantiating an induction hypothesis with an equality assumption ***) |
95 |
95 |
96 val prems = goal Wfd.thy |
96 val prems = goal (the_context ()) |
97 "[| g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); \ |
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; \ |
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; \ |
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) |] ==> \ |
100 \ ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R) |] ==> \ |
101 \ P"; |
101 \ P"; |
103 by (resolve_tac (prems RL [sym]) 1); |
103 by (resolve_tac (prems RL [sym]) 1); |
104 by (rtac rcallT 1); |
104 by (rtac rcallT 1); |
105 by (REPEAT (ares_tac prems 1)); |
105 by (REPEAT (ares_tac prems 1)); |
106 val hyprcallT = result(); |
106 val hyprcallT = result(); |
107 |
107 |
108 val prems = goal Wfd.thy |
108 val prems = goal (the_context ()) |
109 "[| g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);\ |
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) |] ==> \ |
110 \ [| b=g(a); g(a) : D(a) |] ==> P; a:A; <a,p>:wf(R) |] ==> \ |
111 \ P"; |
111 \ P"; |
112 by (resolve_tac (prems) 1); |
112 by (resolve_tac (prems) 1); |
113 by (resolve_tac (prems RL [sym]) 1); |
113 by (resolve_tac (prems RL [sym]) 1); |
114 by (rtac rcallT 1); |
114 by (rtac rcallT 1); |
115 by (REPEAT (ares_tac prems 1)); |
115 by (REPEAT (ares_tac prems 1)); |
116 qed "hyprcallT"; |
116 qed "hyprcallT"; |
117 |
117 |
118 val prems = goal Wfd.thy |
118 val prems = goal (the_context ()) |
119 "[| g(a,b) = c; ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \ |
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; \ |
120 \ [| c=g(a,b); g(a,b) : D(a,b) |] ==> P; \ |
121 \ a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \ |
121 \ a:A; b:B; <<a,b>,<p,q>>:wf(R) |] ==> \ |
122 \ P"; |
122 \ P"; |
123 by (resolve_tac (prems) 1); |
123 by (resolve_tac (prems) 1); |
124 by (resolve_tac (prems RL [sym]) 1); |
124 by (resolve_tac (prems RL [sym]) 1); |
125 by (rtac rcall2T 1); |
125 by (rtac rcall2T 1); |
126 by (REPEAT (ares_tac prems 1)); |
126 by (REPEAT (ares_tac prems 1)); |
127 qed "hyprcall2T"; |
127 qed "hyprcall2T"; |
128 |
128 |
129 val prems = goal Wfd.thy |
129 val prems = goal (the_context ()) |
130 "[| g(a,b,c) = d; \ |
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); \ |
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; \ |
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) |] ==> \ |
133 \ a:A; b:B; c:C; <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \ |
134 \ P"; |
134 \ P"; |
140 |
140 |
141 val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T]; |
141 val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T]; |
142 |
142 |
143 (*** Rules to Remove Induction Hypotheses after Type Checking ***) |
143 (*** Rules to Remove Induction Hypotheses after Type Checking ***) |
144 |
144 |
145 val prems = goal Wfd.thy |
145 val prems = goal (the_context ()) |
146 "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> \ |
146 "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> \ |
147 \ P"; |
147 \ P"; |
148 by (REPEAT (ares_tac prems 1)); |
148 by (REPEAT (ares_tac prems 1)); |
149 qed "rmIH1"; |
149 qed "rmIH1"; |
150 |
150 |
151 val prems = goal Wfd.thy |
151 val prems = goal (the_context ()) |
152 "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \ |
152 "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \ |
153 \ P"; |
153 \ P"; |
154 by (REPEAT (ares_tac prems 1)); |
154 by (REPEAT (ares_tac prems 1)); |
155 qed "rmIH2"; |
155 qed "rmIH2"; |
156 |
156 |
157 val prems = goal Wfd.thy |
157 val prems = goal (the_context ()) |
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); \ |
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 |] ==> \ |
159 \ P |] ==> \ |
160 \ P"; |
160 \ P"; |
161 by (REPEAT (ares_tac prems 1)); |
161 by (REPEAT (ares_tac prems 1)); |
162 qed "rmIH3"; |
162 qed "rmIH3"; |