author | lcp |
Tue, 16 Aug 1994 19:03:45 +0200 | |
changeset 534 | cd8bec47e175 |
parent 524 | b1bf18e83302 |
child 692 | 0ca24b09f4a6 |
permissions | -rw-r--r-- |
488 | 1 |
(* Title: ZF/InfDatatype.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
534 | 6 |
Datatype Definitions involving function space and/or infinite-branching |
488 | 7 |
*) |
8 |
||
534 | 9 |
(*** FINITE BRANCHING ***) |
10 |
||
11 |
(** Closure under finite powerset **) |
|
516 | 12 |
|
13 |
val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy); |
|
14 |
||
15 |
goal Fin_Univ_thy |
|
16 |
"!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"; |
|
17 |
by (eresolve_tac [Fin_induct] 1); |
|
18 |
by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1); |
|
19 |
by (safe_tac ZF_cs); |
|
20 |
by (eresolve_tac [Limit_VfromE] 1); |
|
21 |
by (assume_tac 1); |
|
22 |
by (res_inst_tac [("x", "xa Un j")] exI 1); |
|
23 |
by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD, |
|
24 |
Un_least_lt]) 1); |
|
25 |
val Fin_Vfrom_lemma = result(); |
|
26 |
||
27 |
goal Fin_Univ_thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"; |
|
28 |
by (rtac subsetI 1); |
|
29 |
by (dresolve_tac [Fin_Vfrom_lemma] 1); |
|
30 |
by (safe_tac ZF_cs); |
|
31 |
by (resolve_tac [Vfrom RS ssubst] 1); |
|
32 |
by (fast_tac (ZF_cs addSDs [ltD]) 1); |
|
33 |
val Fin_VLimit = result(); |
|
34 |
||
35 |
val Fin_subset_VLimit = |
|
36 |
[Fin_mono, Fin_VLimit] MRS subset_trans |> standard; |
|
37 |
||
534 | 38 |
goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)"; |
39 |
by (rtac (Limit_nat RS Fin_VLimit) 1); |
|
40 |
val Fin_univ = result(); |
|
41 |
||
42 |
(** Closure under finite powers (functions from a fixed natural number) **) |
|
43 |
||
516 | 44 |
goal Fin_Univ_thy |
45 |
"!!i. [| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"; |
|
46 |
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1); |
|
47 |
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, |
|
48 |
nat_subset_VLimit, subset_refl] 1)); |
|
49 |
val nat_fun_VLimit = result(); |
|
50 |
||
51 |
val nat_fun_subset_VLimit = |
|
52 |
[Pi_mono, nat_fun_VLimit] MRS subset_trans |> standard; |
|
53 |
||
54 |
goalw Fin_Univ_thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)"; |
|
55 |
by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1); |
|
56 |
val nat_fun_univ = result(); |
|
57 |
||
58 |
||
534 | 59 |
(** Closure under finite function space **) |
60 |
||
61 |
(*General but seldom-used version; normally the domain is fixed*) |
|
62 |
goal Fin_Univ_thy |
|
63 |
"!!i. Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"; |
|
64 |
by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1); |
|
65 |
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1)); |
|
66 |
val FiniteFun_VLimit1 = result(); |
|
67 |
||
68 |
goalw Fin_Univ_thy [univ_def] "univ(A) -||> univ(A) <= univ(A)"; |
|
69 |
by (rtac (Limit_nat RS FiniteFun_VLimit1) 1); |
|
70 |
val FiniteFun_univ1 = result(); |
|
71 |
||
72 |
(*Version for a fixed domain*) |
|
73 |
goal Fin_Univ_thy |
|
74 |
"!!i. [| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"; |
|
75 |
by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1); |
|
76 |
by (eresolve_tac [FiniteFun_VLimit1] 1); |
|
77 |
val FiniteFun_VLimit = result(); |
|
78 |
||
79 |
goalw Fin_Univ_thy [univ_def] |
|
80 |
"!!W. W <= univ(A) ==> W -||> univ(A) <= univ(A)"; |
|
81 |
by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1); |
|
82 |
val FiniteFun_univ = result(); |
|
83 |
||
84 |
goal Fin_Univ_thy |
|
85 |
"!!W. [| f: W -||> univ(A); W <= univ(A) |] ==> f : univ(A)"; |
|
86 |
by (eresolve_tac [FiniteFun_univ RS subsetD] 1); |
|
87 |
by (assume_tac 1); |
|
88 |
val FiniteFun_in_univ = result(); |
|
89 |
||
90 |
(*Remove <= from the rule above*) |
|
91 |
val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ); |
|
92 |
||
93 |
||
94 |
(*** INFINITE BRANCHING ***) |
|
516 | 95 |
|
488 | 96 |
val fun_Limit_VfromE = |
97 |
[apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE |
|
98 |
|> standard; |
|
99 |
||
100 |
goal InfDatatype.thy |
|
517 | 101 |
"!!K. [| f: W -> Vfrom(A,csucc(K)); |W| le K; InfCard(K) \ |
102 |
\ |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)"; |
|
103 |
by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : Vfrom(A,i)")] exI 1); |
|
516 | 104 |
by (resolve_tac [conjI] 1); |
517 | 105 |
by (resolve_tac [le_UN_Ord_lt_csucc] 2); |
106 |
by (rtac ballI 4 THEN |
|
107 |
eresolve_tac [fun_Limit_VfromE] 4 THEN REPEAT_SOME assume_tac); |
|
516 | 108 |
by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2); |
109 |
by (resolve_tac [Pi_type] 1); |
|
517 | 110 |
by (rename_tac "w" 2); |
516 | 111 |
by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac); |
517 | 112 |
by (subgoal_tac "f`w : Vfrom(A, LEAST i. f`w : Vfrom(A,i))" 1); |
516 | 113 |
by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2); |
114 |
by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1); |
|
115 |
by (assume_tac 1); |
|
116 |
val fun_Vcsucc_lemma = result(); |
|
117 |
||
118 |
goal InfDatatype.thy |
|
517 | 119 |
"!!K. [| W <= Vfrom(A,csucc(K)); |W| le K; InfCard(K) \ |
120 |
\ |] ==> EX j. W <= Vfrom(A,j) & j < csucc(K)"; |
|
121 |
by (asm_full_simp_tac (ZF_ss addsimps [subset_iff_id, fun_Vcsucc_lemma]) 1); |
|
122 |
val subset_Vcsucc = result(); |
|
488 | 123 |
|
517 | 124 |
(*Version for arbitrary index sets*) |
488 | 125 |
goal InfDatatype.thy |
534 | 126 |
"!!K. [| |W| le K; InfCard(K); W <= Vfrom(A,csucc(K)) |] ==> \ |
517 | 127 |
\ W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
128 |
by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc])); |
|
488 | 129 |
by (resolve_tac [Vfrom RS ssubst] 1); |
130 |
by (eresolve_tac [PiE] 1); |
|
131 |
(*This level includes the function, and is below csucc(K)*) |
|
517 | 132 |
by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1); |
488 | 133 |
by (eresolve_tac [subset_trans RS PowI] 2); |
517 | 134 |
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2); |
488 | 135 |
by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit, |
136 |
Limit_has_succ, Un_least_lt] 1)); |
|
516 | 137 |
val fun_Vcsucc = result(); |
488 | 138 |
|
139 |
goal InfDatatype.thy |
|
517 | 140 |
"!!K. [| f: W -> Vfrom(A, csucc(K)); |W| le K; InfCard(K); \ |
141 |
\ W <= Vfrom(A,csucc(K)) \ |
|
142 |
\ |] ==> f: Vfrom(A,csucc(K))"; |
|
143 |
by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1)); |
|
144 |
val fun_in_Vcsucc = result(); |
|
145 |
||
524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
146 |
(*Remove <= from the rule above*) |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
147 |
val fun_in_Vcsucc' = subsetI RSN (4, fun_in_Vcsucc); |
517 | 148 |
|
524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
149 |
(** Version where K itself is the index set **) |
517 | 150 |
|
151 |
goal InfDatatype.thy |
|
152 |
"!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"; |
|
153 |
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); |
|
154 |
by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le, |
|
155 |
i_subset_Vfrom, |
|
156 |
lt_csucc RS leI RS le_imp_subset RS subset_trans] 1)); |
|
157 |
val Card_fun_Vcsucc = result(); |
|
158 |
||
159 |
goal InfDatatype.thy |
|
488 | 160 |
"!!K. [| f: K -> Vfrom(A, csucc(K)); InfCard(K) \ |
161 |
\ |] ==> f: Vfrom(A,csucc(K))"; |
|
517 | 162 |
by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1)); |
163 |
val Card_fun_in_Vcsucc = result(); |
|
488 | 164 |
|
516 | 165 |
val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard; |
166 |
val Inl_in_Vcsucc = Limit_csucc RSN (2, Inl_in_VLimit) |> standard; |
|
167 |
val Inr_in_Vcsucc = Limit_csucc RSN (2, Inr_in_VLimit) |> standard; |
|
168 |
val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard; |
|
169 |
val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard; |
|
488 | 170 |
|
524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
171 |
(*For handling Cardinals of the form (nat Un |X|) *) |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
172 |
|
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
173 |
val InfCard_nat_Un_cardinal = [InfCard_nat, Card_cardinal] MRS InfCard_Un |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
174 |
|> standard; |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
175 |
|
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
176 |
val le_nat_Un_cardinal = |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
177 |
[Ord_nat, Card_cardinal RS Card_is_Ord] MRS Un_upper2_le |> standard; |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
178 |
|
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
179 |
val UN_upper_cardinal = UN_upper RS subset_imp_lepoll RS lepoll_imp_le |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
180 |
|> standard; |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
181 |
|
488 | 182 |
(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *) |
183 |
val inf_datatype_intrs = |
|
524
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
184 |
[InfCard_nat, InfCard_nat_Un_cardinal, |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
185 |
Pair_in_Vcsucc, Inl_in_Vcsucc, Inr_in_Vcsucc, |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
186 |
zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc, |
b1bf18e83302
ZF/InfDatatype: simplified, extended results for infinite branching
lcp
parents:
517
diff
changeset
|
187 |
Card_fun_in_Vcsucc, fun_in_Vcsucc', UN_I] @ datatype_intrs; |