author | kleing |
Thu, 29 Jun 2006 01:08:08 +0200 | |
changeset 19960 | a0e3f2df9b0e |
parent 17456 | bcf7544875b2 |
permissions | -rw-r--r-- |
17456 | 1 |
(* Title: CCL/Type.ML |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
0 | 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 |
||
17456 | 14 |
goal (the_context ()) "A <= B <-> (ALL x. x:A --> x:B)"; |
0 | 15 |
by (fast_tac set_cs 1); |
757 | 16 |
qed "subsetXH"; |
0 | 17 |
|
18 |
(*** Exhaustion Rules ***) |
|
19 |
||
20 |
fun mk_XH_tac thy defs rls s = prove_goalw thy defs s (fn _ => [cfast_tac rls 1]); |
|
17456 | 21 |
val XH_tac = mk_XH_tac (the_context ()) simp_type_defs []; |
0 | 22 |
|
23 |
val EmptyXH = XH_tac "a : {} <-> False"; |
|
3837 | 24 |
val SubtypeXH = XH_tac "a : {x:A. P(x)} <-> (a:A & P(a))"; |
0 | 25 |
val UnitXH = XH_tac "a : Unit <-> a=one"; |
26 |
val BoolXH = XH_tac "a : Bool <-> a=true | a=false"; |
|
3837 | 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>)"; |
|
0 | 30 |
|
31 |
val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH]; |
|
32 |
||
33 |
val LiftXH = XH_tac "a : [A] <-> (a=bot | a:A)"; |
|
3837 | 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))"; |
|
0 | 36 |
|
37 |
val case_rls = XH_to_Es XHs; |
|
38 |
||
39 |
(*** Canonical Type Rules ***) |
|
40 |
||
17456 | 41 |
fun mk_canT_tac thy xhs s = prove_goal thy s |
0 | 42 |
(fn prems => [fast_tac (set_cs addIs (prems @ (xhs RL [iffD2]))) 1]); |
17456 | 43 |
val canT_tac = mk_canT_tac (the_context ()) XHs; |
0 | 44 |
|
45 |
val oneT = canT_tac "one : Unit"; |
|
46 |
val trueT = canT_tac "true : Bool"; |
|
47 |
val falseT = canT_tac "false : Bool"; |
|
3837 | 48 |
val lamT = canT_tac "[| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)"; |
0 | 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 |
|
17456 | 58 |
val lemma = prove_goal (the_context ()) "[| a:B(u); u=v |] ==> a : B(v)" |
0 | 59 |
(fn prems => [cfast_tac prems 1]); |
60 |
in |
|
17456 | 61 |
fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s |
0 | 62 |
(fn major::prems => [(resolve_tac ([major] RL top_crls) 1), |
63 |
(REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), |
|
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
64 |
(ALLGOALS (asm_simp_tac term_ss)), |
17456 | 65 |
(ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
66 |
etac bspec )), |
0 | 67 |
(safe_tac (ccl_cs addSIs prems))]); |
68 |
end; |
|
69 |
||
17456 | 70 |
val ncanT_tac = mk_ncanT_tac (the_context ()) [] case_rls case_rls; |
0 | 71 |
|
17456 | 72 |
val ifT = ncanT_tac |
0 | 73 |
"[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> \ |
74 |
\ if b then t else u : A(b)"; |
|
75 |
||
17456 | 76 |
val applyT = ncanT_tac |
0 | 77 |
"[| f : Pi(A,B); a:A |] ==> f ` a : B(a)"; |
78 |
||
17456 | 79 |
val splitT = ncanT_tac |
0 | 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 |
||
17456 | 83 |
val whenT = ncanT_tac |
0 | 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 |
||
17456 | 95 |
val prems = goal (the_context ()) |
0 | 96 |
"[| a:A; P(a) |] ==> a : {x:A. P(x)}"; |
97 |
by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1)); |
|
757 | 98 |
qed "SubtypeI"; |
0 | 99 |
|
17456 | 100 |
val prems = goal (the_context ()) |
0 | 101 |
"[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> Q |] ==> Q"; |
102 |
by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1)); |
|
757 | 103 |
qed "SubtypeE"; |
0 | 104 |
|
105 |
(*** Monotonicity ***) |
|
106 |
||
5062 | 107 |
Goal "mono (%X. X)"; |
0 | 108 |
by (REPEAT (ares_tac [monoI] 1)); |
757 | 109 |
qed "idM"; |
0 | 110 |
|
5062 | 111 |
Goal "mono(%X. A)"; |
0 | 112 |
by (REPEAT (ares_tac [monoI,subset_refl] 1)); |
757 | 113 |
qed "constM"; |
0 | 114 |
|
17456 | 115 |
val major::prems = goal (the_context ()) |
3837 | 116 |
"mono(%X. A(X)) ==> mono(%X.[A(X)])"; |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
117 |
by (rtac (subsetI RS monoI) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
118 |
by (dtac (LiftXH RS iffD1) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
119 |
by (etac disjE 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
120 |
by (etac (disjI1 RS (LiftXH RS iffD2)) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
121 |
by (rtac (disjI2 RS (LiftXH RS iffD2)) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
122 |
by (etac (major RS monoD RS subsetD) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
123 |
by (assume_tac 1); |
757 | 124 |
qed "LiftM"; |
0 | 125 |
|
17456 | 126 |
val prems = goal (the_context ()) |
3837 | 127 |
"[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> \ |
128 |
\ mono(%X. Sigma(A(X),B(X)))"; |
|
0 | 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)); |
|
757 | 133 |
qed "SgM"; |
0 | 134 |
|
17456 | 135 |
val prems = goal (the_context ()) |
3837 | 136 |
"[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))"; |
0 | 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)); |
|
757 | 141 |
qed "PiM"; |
0 | 142 |
|
17456 | 143 |
val prems = goal (the_context ()) |
3837 | 144 |
"[| mono(%X. A(X)); mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))"; |
0 | 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)); |
|
757 | 149 |
qed "PlusM"; |
0 | 150 |
|
151 |
(**************** RECURSIVE TYPES ******************) |
|
152 |
||
153 |
(*** Conversion Rules for Fixed Points via monotonicity and Tarski ***) |
|
154 |
||
5062 | 155 |
Goal "mono(%X. Unit+X)"; |
0 | 156 |
by (REPEAT (ares_tac [PlusM,constM,idM] 1)); |
757 | 157 |
qed "NatM"; |
1087 | 158 |
bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski)); |
0 | 159 |
|
5062 | 160 |
Goal "mono(%X.(Unit+Sigma(A,%y. X)))"; |
0 | 161 |
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1)); |
757 | 162 |
qed "ListM"; |
1087 | 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)); |
|
0 | 165 |
|
5062 | 166 |
Goal "mono(%X.({} + Sigma(A,%y. X)))"; |
0 | 167 |
by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1)); |
757 | 168 |
qed "IListsM"; |
1087 | 169 |
bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski)); |
0 | 170 |
|
171 |
val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB]; |
|
172 |
||
173 |
(*** Exhaustion Rules ***) |
|
174 |
||
17456 | 175 |
fun mk_iXH_tac teqs ddefs rls s = prove_goalw (the_context ()) ddefs s |
0 | 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 |
||
3837 | 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)"; |
|
0 | 185 |
|
186 |
val iXHs = [NatXH,ListXH]; |
|
187 |
val icase_rls = XH_to_Es iXHs; |
|
188 |
||
189 |
(*** Type Rules ***) |
|
190 |
||
17456 | 191 |
val icanT_tac = mk_canT_tac (the_context ()) iXHs; |
192 |
val incanT_tac = mk_ncanT_tac (the_context ()) [] icase_rls case_rls; |
|
0 | 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)"; |
|
289 | 197 |
val consT = icanT_tac "[| h:A; t:List(A) |] ==> h$t : List(A)"; |
0 | 198 |
|
199 |
val icanTs = [zeroT,succT,nilT,consT]; |
|
200 |
||
17456 | 201 |
val ncaseT = incanT_tac |
0 | 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([]); \ |
|
289 | 208 |
\ !!h t.[| h:A; t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \ |
0 | 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 |
||
17456 | 217 |
fun mk_ind_tac ddefs tdefs Ms canTs case_rls s = prove_goalw (the_context ()) ddefs s |
0 | 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([]); \ |
|
289 | 229 |
\ !!x xs.[| x:A; xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \ |
0 | 230 |
\ P(l)"; |
231 |
||
232 |
val inds = [Nat_ind,List_ind]; |
|
233 |
||
234 |
(*** Primitive Recursive Rules ***) |
|
235 |
||
17456 | 236 |
fun mk_prec_tac inds s = prove_goal (the_context ()) s |
0 | 237 |
(fn major::prems => [resolve_tac ([major] RL inds) 1, |
8
c3d2c6dcf3f0
Installation of new simplfier. Previously appeared to set up the old
lcp
parents:
0
diff
changeset
|
238 |
ALLGOALS (simp_tac term_ss THEN' |
0 | 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([]); \ |
|
289 | 249 |
\ !!x xs g.[| x:A; xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==> \ |
0 | 250 |
\ lrec(l,b,c) : C(l)"; |
251 |
||
252 |
val precTs = [nrecT,lrecT]; |
|
253 |
||
254 |
||
255 |
(*** Theorem proving ***) |
|
256 |
||
17456 | 257 |
val [major,minor] = goal (the_context ()) |
0 | 258 |
"[| <a,b> : Sigma(A,B); [| a:A; b:B(a) |] ==> P \ |
259 |
\ |] ==> P"; |
|
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
260 |
by (rtac (major RS (XH_to_E SgXH)) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
261 |
by (rtac minor 1); |
0 | 262 |
by (ALLGOALS (fast_tac term_cs)); |
757 | 263 |
qed "SgE2"; |
0 | 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 |
||
17456 | 275 |
val [mono] = goal (the_context ()) "mono(f) ==> lfp(f) <= gfp(f)"; |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
276 |
by (rtac (lfp_lowerbound RS subset_trans) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
277 |
by (rtac (mono RS gfp_lemma3) 1); |
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
278 |
by (rtac subset_refl 1); |
757 | 279 |
qed "lfp_subset_gfp"; |
0 | 280 |
|
17456 | 281 |
val prems = goal (the_context ()) |
3837 | 282 |
"[| a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \ |
0 | 283 |
\ t(a) : gfp(B)"; |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
284 |
by (rtac coinduct 1); |
3837 | 285 |
by (res_inst_tac [("P","%x. EX y:A. x=t(y)")] CollectI 1); |
0 | 286 |
by (ALLGOALS (fast_tac (ccl_cs addSIs prems))); |
757 | 287 |
qed "gfpI"; |
0 | 288 |
|
17456 | 289 |
val rew::prem::prems = goal (the_context ()) |
3837 | 290 |
"[| C==gfp(B); a:A; !!x X.[| x:A; ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \ |
0 | 291 |
\ t(a) : C"; |
292 |
by (rewtac rew); |
|
293 |
by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1)); |
|
757 | 294 |
qed "def_gfpI"; |
0 | 295 |
|
296 |
(* EG *) |
|
297 |
||
17456 | 298 |
val prems = goal (the_context ()) |
289 | 299 |
"letrec g x be zero$g(x) in g(bot) : Lists(Nat)"; |
0 | 300 |
by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1); |
2035 | 301 |
by (stac letrecB 1); |
642
0db578095e6a
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents:
289
diff
changeset
|
302 |
by (rewtac cons_def); |
0 | 303 |
by (fast_tac type_cs 1); |
304 |
result(); |