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 |
|
516
|
6 |
Datatype Definitions involving ->
|
|
7 |
Even infinite-branching!
|
488
|
8 |
*)
|
|
9 |
|
516
|
10 |
(*** Closure under finite powerset ***)
|
|
11 |
|
|
12 |
val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);
|
|
13 |
|
|
14 |
goal Fin_Univ_thy
|
|
15 |
"!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i";
|
|
16 |
by (eresolve_tac [Fin_induct] 1);
|
|
17 |
by (fast_tac (ZF_cs addSDs [Limit_has_0]) 1);
|
|
18 |
by (safe_tac ZF_cs);
|
|
19 |
by (eresolve_tac [Limit_VfromE] 1);
|
|
20 |
by (assume_tac 1);
|
|
21 |
by (res_inst_tac [("x", "xa Un j")] exI 1);
|
|
22 |
by (best_tac (ZF_cs addIs [subset_refl RS Vfrom_mono RS subsetD,
|
|
23 |
Un_least_lt]) 1);
|
|
24 |
val Fin_Vfrom_lemma = result();
|
|
25 |
|
|
26 |
goal Fin_Univ_thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
|
|
27 |
by (rtac subsetI 1);
|
|
28 |
by (dresolve_tac [Fin_Vfrom_lemma] 1);
|
|
29 |
by (safe_tac ZF_cs);
|
|
30 |
by (resolve_tac [Vfrom RS ssubst] 1);
|
|
31 |
by (fast_tac (ZF_cs addSDs [ltD]) 1);
|
|
32 |
val Fin_VLimit = result();
|
|
33 |
|
|
34 |
val Fin_subset_VLimit =
|
|
35 |
[Fin_mono, Fin_VLimit] MRS subset_trans |> standard;
|
|
36 |
|
|
37 |
goal Fin_Univ_thy
|
|
38 |
"!!i. [| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)";
|
|
39 |
by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1);
|
|
40 |
by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit,
|
|
41 |
nat_subset_VLimit, subset_refl] 1));
|
|
42 |
val nat_fun_VLimit = result();
|
|
43 |
|
|
44 |
val nat_fun_subset_VLimit =
|
|
45 |
[Pi_mono, nat_fun_VLimit] MRS subset_trans |> standard;
|
|
46 |
|
|
47 |
|
|
48 |
goalw Fin_Univ_thy [univ_def] "Fin(univ(A)) <= univ(A)";
|
|
49 |
by (rtac (Limit_nat RS Fin_VLimit) 1);
|
|
50 |
val Fin_univ = result();
|
|
51 |
|
|
52 |
val Fin_subset_univ = [Fin_mono, Fin_univ] 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 |
val nat_fun_subset_univ = [Pi_mono, nat_fun_univ] MRS subset_trans |> standard;
|
|
59 |
|
|
60 |
goal Fin_Univ_thy
|
|
61 |
"!!f. [| f: n -> B; B <= univ(A); n : nat |] ==> f : univ(A)";
|
|
62 |
by (REPEAT (ares_tac [nat_fun_subset_univ RS subsetD] 1));
|
|
63 |
val nat_fun_into_univ = result();
|
|
64 |
|
|
65 |
|
|
66 |
(*** Infinite branching ***)
|
|
67 |
|
488
|
68 |
val fun_Limit_VfromE =
|
|
69 |
[apply_funtype, InfCard_csucc RS InfCard_is_Limit] MRS Limit_VfromE
|
|
70 |
|> standard;
|
|
71 |
|
|
72 |
goal InfDatatype.thy
|
517
|
73 |
"!!K. [| f: W -> Vfrom(A,csucc(K)); |W| le K; InfCard(K) \
|
|
74 |
\ |] ==> EX j. f: W -> Vfrom(A,j) & j < csucc(K)";
|
|
75 |
by (res_inst_tac [("x", "UN w:W. LEAST i. f`w : Vfrom(A,i)")] exI 1);
|
516
|
76 |
by (resolve_tac [conjI] 1);
|
517
|
77 |
by (resolve_tac [le_UN_Ord_lt_csucc] 2);
|
|
78 |
by (rtac ballI 4 THEN
|
|
79 |
eresolve_tac [fun_Limit_VfromE] 4 THEN REPEAT_SOME assume_tac);
|
516
|
80 |
by (fast_tac (ZF_cs addEs [Least_le RS lt_trans1, ltE]) 2);
|
|
81 |
by (resolve_tac [Pi_type] 1);
|
517
|
82 |
by (rename_tac "w" 2);
|
516
|
83 |
by (eresolve_tac [fun_Limit_VfromE] 2 THEN REPEAT_SOME assume_tac);
|
517
|
84 |
by (subgoal_tac "f`w : Vfrom(A, LEAST i. f`w : Vfrom(A,i))" 1);
|
516
|
85 |
by (fast_tac (ZF_cs addEs [LeastI, ltE]) 2);
|
|
86 |
by (eresolve_tac [[subset_refl, UN_upper] MRS Vfrom_mono RS subsetD] 1);
|
|
87 |
by (assume_tac 1);
|
|
88 |
val fun_Vcsucc_lemma = result();
|
|
89 |
|
|
90 |
goal InfDatatype.thy
|
517
|
91 |
"!!K. [| W <= Vfrom(A,csucc(K)); |W| le K; InfCard(K) \
|
|
92 |
\ |] ==> EX j. W <= Vfrom(A,j) & j < csucc(K)";
|
|
93 |
by (asm_full_simp_tac (ZF_ss addsimps [subset_iff_id, fun_Vcsucc_lemma]) 1);
|
|
94 |
val subset_Vcsucc = result();
|
488
|
95 |
|
517
|
96 |
(*Version for arbitrary index sets*)
|
488
|
97 |
goal InfDatatype.thy
|
517
|
98 |
"!!K. [| |W| le K; W <= Vfrom(A,csucc(K)); InfCard(K) |] ==> \
|
|
99 |
\ W -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
|
|
100 |
by (safe_tac (ZF_cs addSDs [fun_Vcsucc_lemma, subset_Vcsucc]));
|
488
|
101 |
by (resolve_tac [Vfrom RS ssubst] 1);
|
|
102 |
by (eresolve_tac [PiE] 1);
|
|
103 |
(*This level includes the function, and is below csucc(K)*)
|
517
|
104 |
by (res_inst_tac [("a1", "succ(succ(j Un ja))")] (UN_I RS UnI2) 1);
|
488
|
105 |
by (eresolve_tac [subset_trans RS PowI] 2);
|
517
|
106 |
by (fast_tac (ZF_cs addIs [Pair_in_Vfrom, Vfrom_UnI1, Vfrom_UnI2]) 2);
|
|
107 |
|
488
|
108 |
by (REPEAT (ares_tac [ltD, InfCard_csucc, InfCard_is_Limit,
|
|
109 |
Limit_has_succ, Un_least_lt] 1));
|
516
|
110 |
val fun_Vcsucc = result();
|
488
|
111 |
|
|
112 |
goal InfDatatype.thy
|
517
|
113 |
"!!K. [| f: W -> Vfrom(A, csucc(K)); |W| le K; InfCard(K); \
|
|
114 |
\ W <= Vfrom(A,csucc(K)) \
|
|
115 |
\ |] ==> f: Vfrom(A,csucc(K))";
|
|
116 |
by (REPEAT (ares_tac [fun_Vcsucc RS subsetD] 1));
|
|
117 |
val fun_in_Vcsucc = result();
|
|
118 |
|
|
119 |
goal InfDatatype.thy
|
|
120 |
"!!K. [| W <= Vfrom(A,csucc(K)); B <= Vfrom(A,csucc(K)); \
|
|
121 |
\ |W| le K; InfCard(K) \
|
|
122 |
\ |] ==> W -> B <= Vfrom(A, csucc(K))";
|
|
123 |
by (REPEAT (ares_tac [[Pi_mono, fun_Vcsucc] MRS subset_trans] 1));
|
|
124 |
val fun_subset_Vcsucc = result();
|
|
125 |
|
|
126 |
goal InfDatatype.thy
|
|
127 |
"!!f. [| f: W -> B; W <= Vfrom(A,csucc(K)); B <= Vfrom(A,csucc(K)); \
|
|
128 |
\ |W| le K; InfCard(K) \
|
|
129 |
\ |] ==> f: Vfrom(A,csucc(K))";
|
|
130 |
by (DEPTH_SOLVE (ares_tac [fun_subset_Vcsucc RS subsetD] 1));
|
|
131 |
val fun_into_Vcsucc = result();
|
|
132 |
|
|
133 |
(*Version where K itself is the index set*)
|
|
134 |
goal InfDatatype.thy
|
|
135 |
"!!K. InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))";
|
|
136 |
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
|
|
137 |
by (REPEAT (ares_tac [fun_Vcsucc, Ord_cardinal_le,
|
|
138 |
i_subset_Vfrom,
|
|
139 |
lt_csucc RS leI RS le_imp_subset RS subset_trans] 1));
|
|
140 |
val Card_fun_Vcsucc = result();
|
|
141 |
|
|
142 |
goal InfDatatype.thy
|
488
|
143 |
"!!K. [| f: K -> Vfrom(A, csucc(K)); InfCard(K) \
|
|
144 |
\ |] ==> f: Vfrom(A,csucc(K))";
|
517
|
145 |
by (REPEAT (ares_tac [Card_fun_Vcsucc RS subsetD] 1));
|
|
146 |
val Card_fun_in_Vcsucc = result();
|
488
|
147 |
|
517
|
148 |
val Card_fun_subset_Vcsucc =
|
|
149 |
[Pi_mono, Card_fun_Vcsucc] MRS subset_trans |> standard;
|
488
|
150 |
|
|
151 |
goal InfDatatype.thy
|
|
152 |
"!!f. [| f: K -> B; B <= Vfrom(A,csucc(K)); InfCard(K) \
|
|
153 |
\ |] ==> f: Vfrom(A,csucc(K))";
|
517
|
154 |
by (REPEAT (ares_tac [Card_fun_subset_Vcsucc RS subsetD] 1));
|
|
155 |
val Card_fun_into_Vcsucc = result();
|
488
|
156 |
|
516
|
157 |
val Pair_in_Vcsucc = Limit_csucc RSN (3, Pair_in_VLimit) |> standard;
|
|
158 |
val Inl_in_Vcsucc = Limit_csucc RSN (2, Inl_in_VLimit) |> standard;
|
|
159 |
val Inr_in_Vcsucc = Limit_csucc RSN (2, Inr_in_VLimit) |> standard;
|
|
160 |
val zero_in_Vcsucc = Limit_csucc RS zero_in_VLimit |> standard;
|
|
161 |
val nat_into_Vcsucc = Limit_csucc RSN (2, nat_into_VLimit) |> standard;
|
488
|
162 |
|
|
163 |
(*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
|
|
164 |
val inf_datatype_intrs =
|
517
|
165 |
[Card_fun_in_Vcsucc, fun_in_Vcsucc, InfCard_nat, Pair_in_Vcsucc,
|
516
|
166 |
Inl_in_Vcsucc, Inr_in_Vcsucc,
|
|
167 |
zero_in_Vcsucc, A_into_Vfrom, nat_into_Vcsucc] @ datatype_intrs;
|
488
|
168 |
|