18 by (rtac impI 1); |
18 by (rtac impI 1); |
19 by (eresolve_tac prems 1); |
19 by (eresolve_tac prems 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 val letrecT = result(); |
23 qed "letrecT"; |
24 |
24 |
25 goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)"; |
25 goalw Wfd.thy [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 val SPLITB = result(); |
28 qed "SPLITB"; |
29 |
29 |
30 val prems = goalw Wfd.thy [letrec2_def] |
30 val prems = goalw Wfd.thy [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) |] ==>\ |
38 by (rtac (SPLITB RS ssubst) 1); |
38 by (rtac (SPLITB RS ssubst) 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 val letrec2T = result(); |
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 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 addsimps [SPLITB]) 1); |
46 by (simp_tac (ccl_ss addsimps [SPLITB]) 1); |
47 val lemma = result(); |
47 qed "lemma"; |
48 |
48 |
49 val prems = goalw Wfd.thy [letrec3_def] |
49 val prems = goalw Wfd.thy [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)}. \ |
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 val letrec3T = result(); |
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 ***) |
70 val major::prems = goal Wfd.thy |
70 val major::prems = goal Wfd.thy |
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 val rcallT = result(); |
75 qed "rcallT"; |
76 |
76 |
77 val major::prems = goal Wfd.thy |
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); \ |
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 val rcall2T = result(); |
82 qed "rcall2T"; |
83 |
83 |
84 val major::prems = goal Wfd.thy |
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); \ |
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)); |
90 val rcall3T = result(); |
90 qed "rcall3T"; |
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 |
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 val hyprcallT = result(); |
116 qed "hyprcallT"; |
117 |
117 |
118 val prems = goal Wfd.thy |
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); \ |
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 val hyprcall2T = result(); |
127 qed "hyprcall2T"; |
128 |
128 |
129 val prems = goal Wfd.thy |
129 val prems = goal Wfd.thy |
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; \ |
134 \ P"; |
134 \ P"; |
135 by (resolve_tac (prems) 1); |
135 by (resolve_tac (prems) 1); |
136 by (resolve_tac (prems RL [sym]) 1); |
136 by (resolve_tac (prems RL [sym]) 1); |
137 by (rtac rcall3T 1); |
137 by (rtac rcall3T 1); |
138 by (REPEAT (ares_tac prems 1)); |
138 by (REPEAT (ares_tac prems 1)); |
139 val hyprcall3T = result(); |
139 qed "hyprcall3T"; |
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 Wfd.thy |
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 val rmIH1 = result(); |
149 qed "rmIH1"; |
150 |
150 |
151 val prems = goal Wfd.thy |
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 |] ==> \ |
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 val rmIH2 = result(); |
155 qed "rmIH2"; |
156 |
156 |
157 val prems = goal Wfd.thy |
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); \ |
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 val rmIH3 = result(); |
162 qed "rmIH3"; |
163 |
163 |
164 val rmIHs = [rmIH1,rmIH2,rmIH3]; |
164 val rmIHs = [rmIH1,rmIH2,rmIH3]; |
165 |
165 |