1 (* Title: CCL/Type.ML |
|
2 ID: $Id$ |
|
3 Author: Martin Coen, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 *) |
|
6 |
|
7 val simp_type_defs = [Subtype_def,Unit_def,Bool_def,Plus_def,Sigma_def,Pi_def, |
|
8 Lift_def,Tall_def,Tex_def]; |
|
9 val ind_type_defs = [Nat_def,List_def]; |
|
10 |
|
11 val simp_data_defs = [one_def,inl_def,inr_def]; |
|
12 val ind_data_defs = [zero_def,succ_def,nil_def,cons_def]; |
|
13 |
|
14 goal (the_context ()) "A <= B <-> (ALL x. x:A --> x:B)"; |
|
15 by (fast_tac set_cs 1); |
|
16 qed "subsetXH"; |
|
17 |
|
18 (*** Exhaustion Rules ***) |
|
19 |
|
20 fun mk_XH_tac thy defs rls s = prove_goalw thy defs s (fn _ => [cfast_tac rls 1]); |
|
21 val XH_tac = mk_XH_tac (the_context ()) simp_type_defs []; |
|
22 |
|
23 val EmptyXH = XH_tac "a : {} <-> False"; |
|
24 val SubtypeXH = XH_tac "a : {x:A. P(x)} <-> (a:A & P(a))"; |
|
25 val UnitXH = XH_tac "a : Unit <-> a=one"; |
|
26 val BoolXH = XH_tac "a : Bool <-> a=true | a=false"; |
|
27 val PlusXH = XH_tac "a : A+B <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))"; |
|
28 val PiXH = XH_tac "a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))"; |
|
29 val SgXH = XH_tac "a : SUM x:A. B(x) <-> (EX x:A. EX y:B(x).a=<x,y>)"; |
|
30 |
|
31 val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH]; |
|
32 |
|
33 val LiftXH = XH_tac "a : [A] <-> (a=bot | a:A)"; |
|
34 val TallXH = XH_tac "a : TALL X. B(X) <-> (ALL X. a:B(X))"; |
|
35 val TexXH = XH_tac "a : TEX X. B(X) <-> (EX X. a:B(X))"; |
|
36 |
|
37 val case_rls = XH_to_Es XHs; |
|
38 |
|
39 (*** Canonical Type Rules ***) |
|
40 |
|
41 fun mk_canT_tac thy xhs s = prove_goal thy s |
|
42 (fn prems => [fast_tac (set_cs addIs (prems @ (xhs RL [iffD2]))) 1]); |
|
43 val canT_tac = mk_canT_tac (the_context ()) XHs; |
|
44 |
|
45 val oneT = canT_tac "one : Unit"; |
|
46 val trueT = canT_tac "true : Bool"; |
|
47 val falseT = canT_tac "false : Bool"; |
|
48 val lamT = canT_tac "[| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)"; |
|
49 val pairT = canT_tac "[| a:A; b:B(a) |] ==> <a,b>:Sigma(A,B)"; |
|
50 val inlT = canT_tac "a:A ==> inl(a) : A+B"; |
|
51 val inrT = canT_tac "b:B ==> inr(b) : A+B"; |
|
52 |
|
53 val canTs = [oneT,trueT,falseT,pairT,lamT,inlT,inrT]; |
|
54 |
|
55 (*** Non-Canonical Type Rules ***) |
|
56 |
|
57 local |
|
58 val lemma = prove_goal (the_context ()) "[| a:B(u); u=v |] ==> a : B(v)" |
|
59 (fn prems => [cfast_tac prems 1]); |
|
60 in |
|
61 fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s |
|
62 (fn major::prems => [(resolve_tac ([major] RL top_crls) 1), |
|
63 (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), |
|
64 (ALLGOALS (asm_simp_tac term_ss)), |
|
65 (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' |
|
66 etac bspec )), |
|
67 (safe_tac (ccl_cs addSIs prems))]); |
|
68 end; |
|
69 |
|
70 val ncanT_tac = mk_ncanT_tac (the_context ()) [] case_rls case_rls; |
|
71 |
|
72 val ifT = ncanT_tac |
|
73 "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> \ |
|
74 \ if b then t else u : A(b)"; |
|
75 |
|
76 val applyT = ncanT_tac |
|
77 "[| f : Pi(A,B); a:A |] ==> f ` a : B(a)"; |
|
78 |
|
79 val splitT = ncanT_tac |
|
80 "[| p:Sigma(A,B); !!x y. [| x:A; y:B(x); p=<x,y> |] ==> c(x,y):C(<x,y>) |] ==> \ |
|
81 \ split(p,c):C(p)"; |
|
82 |
|
83 val whenT = ncanT_tac |
|
84 "[| p:A+B; !!x.[| x:A; p=inl(x) |] ==> a(x):C(inl(x)); \ |
|
85 \ !!y.[| y:B; p=inr(y) |] ==> b(y):C(inr(y)) |] ==> \ |
|
86 \ when(p,a,b) : C(p)"; |
|
87 |
|
88 val ncanTs = [ifT,applyT,splitT,whenT]; |
|
89 |
|
90 (*** Subtypes ***) |
|
91 |
|
92 val SubtypeD1 = standard ((SubtypeXH RS iffD1) RS conjunct1); |
|
93 val SubtypeD2 = standard ((SubtypeXH RS iffD1) RS conjunct2); |
|
94 |
|
95 val prems = goal (the_context ()) |
|
96 "[| a:A; P(a) |] ==> a : {x:A. P(x)}"; |
|
97 by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1)); |
|
98 qed "SubtypeI"; |
|
99 |
|
100 val prems = goal (the_context ()) |
|
101 "[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> Q |] ==> Q"; |
|
102 by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1)); |
|
103 qed "SubtypeE"; |
|
104 |
|
105 (*** Monotonicity ***) |
|
106 |
|
107 Goal "mono (%X. X)"; |
|
108 by (REPEAT (ares_tac [monoI] 1)); |
|
109 qed "idM"; |
|
110 |
|
111 Goal "mono(%X. A)"; |
|
112 by (REPEAT (ares_tac [monoI,subset_refl] 1)); |
|
113 qed "constM"; |
|
114 |
|
115 val major::prems = goal (the_context ()) |
|
116 "mono(%X. A(X)) ==> mono(%X.[A(X)])"; |
|
117 by (rtac (subsetI RS monoI) 1); |
|
118 by (dtac (LiftXH RS iffD1) 1); |
|
119 by (etac disjE 1); |
|
120 by (etac (disjI1 RS (LiftXH RS iffD2)) 1); |
|
121 by (rtac (disjI2 RS (LiftXH RS iffD2)) 1); |
|
122 by (etac (major RS monoD RS subsetD) 1); |
|
123 by (assume_tac 1); |
|
124 qed "LiftM"; |
|
125 |
|
126 val prems = goal (the_context ()) |
|
127 "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> \ |
|
128 \ mono(%X. Sigma(A(X),B(X)))"; |
|
129 by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE |
|
130 eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE |
|
131 (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE |
|
132 hyp_subst_tac 1)); |
|
133 qed "SgM"; |
|
134 |
|
135 val prems = goal (the_context ()) |
|
136 "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))"; |
|
137 by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE |
|
138 eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE |
|
139 (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE |
|
140 hyp_subst_tac 1)); |
|
141 qed "PiM"; |
|
142 |
|
143 val prems = goal (the_context ()) |
|
144 "[| mono(%X. A(X)); mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))"; |
|
145 by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE |
|
146 eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE |
|
147 (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE |
|
148 hyp_subst_tac 1)); |
|
149 qed "PlusM"; |
|
150 |
|
151 (**************** RECURSIVE TYPES ******************) |
|
152 |
|
153 (*** Conversion Rules for Fixed Points via monotonicity and Tarski ***) |
|
154 |
|
155 Goal "mono(%X. Unit+X)"; |
|
156 by (REPEAT (ares_tac [PlusM,constM,idM] 1)); |
|
157 qed "NatM"; |
|
158 bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski)); |
|
159 |
|
160 Goal "mono(%X.(Unit+Sigma(A,%y. X)))"; |
|
161 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1)); |
|
162 qed "ListM"; |
|
163 bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski)); |
|
164 bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski)); |
|
165 |
|
166 Goal "mono(%X.({} + Sigma(A,%y. X)))"; |
|
167 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1)); |
|
168 qed "IListsM"; |
|
169 bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski)); |
|
170 |
|
171 val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB]; |
|
172 |
|
173 (*** Exhaustion Rules ***) |
|
174 |
|
175 fun mk_iXH_tac teqs ddefs rls s = prove_goalw (the_context ()) ddefs s |
|
176 (fn _ => [resolve_tac (teqs RL [XHlemma1]) 1, |
|
177 fast_tac (set_cs addSIs canTs addSEs case_rls) 1]); |
|
178 |
|
179 val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs []; |
|
180 |
|
181 val NatXH = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat. a=succ(x)))"; |
|
182 val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))"; |
|
183 val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))"; |
|
184 val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A. EX xs:ILists(A).a=x$xs)"; |
|
185 |
|
186 val iXHs = [NatXH,ListXH]; |
|
187 val icase_rls = XH_to_Es iXHs; |
|
188 |
|
189 (*** Type Rules ***) |
|
190 |
|
191 val icanT_tac = mk_canT_tac (the_context ()) iXHs; |
|
192 val incanT_tac = mk_ncanT_tac (the_context ()) [] icase_rls case_rls; |
|
193 |
|
194 val zeroT = icanT_tac "zero : Nat"; |
|
195 val succT = icanT_tac "n:Nat ==> succ(n) : Nat"; |
|
196 val nilT = icanT_tac "[] : List(A)"; |
|
197 val consT = icanT_tac "[| h:A; t:List(A) |] ==> h$t : List(A)"; |
|
198 |
|
199 val icanTs = [zeroT,succT,nilT,consT]; |
|
200 |
|
201 val ncaseT = incanT_tac |
|
202 "[| n:Nat; n=zero ==> b:C(zero); \ |
|
203 \ !!x.[| x:Nat; n=succ(x) |] ==> c(x):C(succ(x)) |] ==> \ |
|
204 \ ncase(n,b,c) : C(n)"; |
|
205 |
|
206 val lcaseT = incanT_tac |
|
207 "[| l:List(A); l=[] ==> b:C([]); \ |
|
208 \ !!h t.[| h:A; t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \ |
|
209 \ lcase(l,b,c) : C(l)"; |
|
210 |
|
211 val incanTs = [ncaseT,lcaseT]; |
|
212 |
|
213 (*** Induction Rules ***) |
|
214 |
|
215 val ind_Ms = [NatM,ListM]; |
|
216 |
|
217 fun mk_ind_tac ddefs tdefs Ms canTs case_rls s = prove_goalw (the_context ()) ddefs s |
|
218 (fn major::prems => [resolve_tac (Ms RL ([major] RL (tdefs RL [def_induct]))) 1, |
|
219 fast_tac (set_cs addSIs (prems @ canTs) addSEs case_rls) 1]); |
|
220 |
|
221 val ind_tac = mk_ind_tac ind_data_defs ind_type_defs ind_Ms canTs case_rls; |
|
222 |
|
223 val Nat_ind = ind_tac |
|
224 "[| n:Nat; P(zero); !!x.[| x:Nat; P(x) |] ==> P(succ(x)) |] ==> \ |
|
225 \ P(n)"; |
|
226 |
|
227 val List_ind = ind_tac |
|
228 "[| l:List(A); P([]); \ |
|
229 \ !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \ |
|
230 \ P(l)"; |
|
231 |
|
232 val inds = [Nat_ind,List_ind]; |
|
233 |
|
234 (*** Primitive Recursive Rules ***) |
|
235 |
|
236 fun mk_prec_tac inds s = prove_goal (the_context ()) s |
|
237 (fn major::prems => [resolve_tac ([major] RL inds) 1, |
|
238 ALLGOALS (simp_tac term_ss THEN' |
|
239 fast_tac (set_cs addSIs prems))]); |
|
240 val prec_tac = mk_prec_tac inds; |
|
241 |
|
242 val nrecT = prec_tac |
|
243 "[| n:Nat; b:C(zero); \ |
|
244 \ !!x g.[| x:Nat; g:C(x) |] ==> c(x,g):C(succ(x)) |] ==> \ |
|
245 \ nrec(n,b,c) : C(n)"; |
|
246 |
|
247 val lrecT = prec_tac |
|
248 "[| l:List(A); b:C([]); \ |
|
249 \ !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==> \ |
|
250 \ lrec(l,b,c) : C(l)"; |
|
251 |
|
252 val precTs = [nrecT,lrecT]; |
|
253 |
|
254 |
|
255 (*** Theorem proving ***) |
|
256 |
|
257 val [major,minor] = goal (the_context ()) |
|
258 "[| <a,b> : Sigma(A,B); [| a:A; b:B(a) |] ==> P \ |
|
259 \ |] ==> P"; |
|
260 by (rtac (major RS (XH_to_E SgXH)) 1); |
|
261 by (rtac minor 1); |
|
262 by (ALLGOALS (fast_tac term_cs)); |
|
263 qed "SgE2"; |
|
264 |
|
265 (* General theorem proving ignores non-canonical term-formers, *) |
|
266 (* - intro rules are type rules for canonical terms *) |
|
267 (* - elim rules are case rules (no non-canonical terms appear) *) |
|
268 |
|
269 val type_cs = term_cs addSIs (SubtypeI::(canTs @ icanTs)) |
|
270 addSEs (SubtypeE::(XH_to_Es XHs)); |
|
271 |
|
272 |
|
273 (*** Infinite Data Types ***) |
|
274 |
|
275 val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) <= gfp(f)"; |
|
276 by (rtac (lfp_lowerbound RS subset_trans) 1); |
|
277 by (rtac (mono RS gfp_lemma3) 1); |
|
278 by (rtac subset_refl 1); |
|
279 qed "lfp_subset_gfp"; |
|
280 |
|
281 val prems = goal (the_context ()) |
|
282 "[| a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \ |
|
283 \ t(a) : gfp(B)"; |
|
284 by (rtac coinduct 1); |
|
285 by (res_inst_tac [("P","%x. EX y:A. x=t(y)")] CollectI 1); |
|
286 by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); |
|
287 qed "gfpI"; |
|
288 |
|
289 val rew::prem::prems = goal (the_context ()) |
|
290 "[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \ |
|
291 \ t(a) : C"; |
|
292 by (rewtac rew); |
|
293 by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1)); |
|
294 qed "def_gfpI"; |
|
295 |
|
296 (* EG *) |
|
297 |
|
298 val prems = goal (the_context ()) |
|
299 "letrec g x be zero$g(x) in g(bot) : Lists(Nat)"; |
|
300 by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1); |
|
301 by (stac letrecB 1); |
|
302 by (rewtac cons_def); |
|
303 by (fast_tac type_cs 1); |
|
304 result(); |
|