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