6093
|
1 |
(* Title: ZF/QUniv.thy
|
0
|
2 |
ID: $Id$
|
1478
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
0
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
13285
|
6 |
A small universe for lazy recursive types
|
0
|
7 |
*)
|
|
8 |
|
13285
|
9 |
(** Properties involving Transset and Sum **)
|
|
10 |
|
|
11 |
theory QUniv = Univ + QPair + mono + equalities:
|
3923
|
12 |
|
6112
|
13 |
(*Disjoint sums as a datatype*)
|
|
14 |
rep_datatype
|
13285
|
15 |
elimination sumE
|
|
16 |
induction TrueI
|
|
17 |
case_eqns case_Inl case_Inr
|
6112
|
18 |
|
|
19 |
(*Variant disjoint sums as a datatype*)
|
|
20 |
rep_datatype
|
13285
|
21 |
elimination qsumE
|
|
22 |
induction TrueI
|
|
23 |
case_eqns qcase_QInl qcase_QInr
|
6112
|
24 |
|
6093
|
25 |
constdefs
|
13220
|
26 |
quniv :: "i => i"
|
6112
|
27 |
"quniv(A) == Pow(univ(eclose(A)))"
|
0
|
28 |
|
13285
|
29 |
|
|
30 |
lemma Transset_includes_summands:
|
|
31 |
"[| Transset(C); A+B <= C |] ==> A <= C & B <= C"
|
|
32 |
apply (simp add: sum_def Un_subset_iff)
|
|
33 |
apply (blast dest: Transset_includes_range)
|
|
34 |
done
|
|
35 |
|
|
36 |
lemma Transset_sum_Int_subset:
|
|
37 |
"Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"
|
|
38 |
apply (simp add: sum_def Int_Un_distrib2)
|
|
39 |
apply (blast dest: Transset_Pair_D)
|
|
40 |
done
|
|
41 |
|
|
42 |
(** Introduction and elimination rules avoid tiresome folding/unfolding **)
|
|
43 |
|
|
44 |
lemma qunivI: "X <= univ(eclose(A)) ==> X : quniv(A)"
|
|
45 |
by (simp add: quniv_def)
|
|
46 |
|
|
47 |
lemma qunivD: "X : quniv(A) ==> X <= univ(eclose(A))"
|
|
48 |
by (simp add: quniv_def)
|
|
49 |
|
|
50 |
lemma quniv_mono: "A<=B ==> quniv(A) <= quniv(B)"
|
|
51 |
apply (unfold quniv_def)
|
|
52 |
apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
|
|
53 |
done
|
|
54 |
|
|
55 |
(*** Closure properties ***)
|
|
56 |
|
|
57 |
lemma univ_eclose_subset_quniv: "univ(eclose(A)) <= quniv(A)"
|
|
58 |
apply (simp add: quniv_def Transset_iff_Pow [symmetric])
|
|
59 |
apply (rule Transset_eclose [THEN Transset_univ])
|
|
60 |
done
|
|
61 |
|
|
62 |
(*Key property for proving A_subset_quniv; requires eclose in def of quniv*)
|
|
63 |
lemma univ_subset_quniv: "univ(A) <= quniv(A)"
|
|
64 |
apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans])
|
|
65 |
apply (rule univ_eclose_subset_quniv)
|
|
66 |
done
|
|
67 |
|
|
68 |
lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD, standard]
|
|
69 |
|
|
70 |
lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)"
|
|
71 |
apply (unfold quniv_def)
|
|
72 |
apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono])
|
|
73 |
done
|
|
74 |
|
|
75 |
lemmas univ_subset_into_quniv =
|
|
76 |
PowI [THEN Pow_univ_subset_quniv [THEN subsetD], standard]
|
|
77 |
|
|
78 |
lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv, standard]
|
|
79 |
lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv, standard]
|
|
80 |
lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv, standard]
|
|
81 |
|
|
82 |
lemmas A_subset_quniv = subset_trans [OF A_subset_univ univ_subset_quniv]
|
|
83 |
|
|
84 |
lemmas A_into_quniv = A_subset_quniv [THEN subsetD, standard]
|
|
85 |
|
|
86 |
(*** univ(A) closure for Quine-inspired pairs and injections ***)
|
|
87 |
|
|
88 |
(*Quine ordered pairs*)
|
|
89 |
lemma QPair_subset_univ:
|
|
90 |
"[| a <= univ(A); b <= univ(A) |] ==> <a;b> <= univ(A)"
|
|
91 |
by (simp add: QPair_def sum_subset_univ)
|
|
92 |
|
|
93 |
(** Quine disjoint sum **)
|
|
94 |
|
|
95 |
lemma QInl_subset_univ: "a <= univ(A) ==> QInl(a) <= univ(A)"
|
|
96 |
apply (unfold QInl_def)
|
|
97 |
apply (erule empty_subsetI [THEN QPair_subset_univ])
|
|
98 |
done
|
|
99 |
|
|
100 |
lemmas naturals_subset_nat =
|
|
101 |
Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec, standard]
|
|
102 |
|
|
103 |
lemmas naturals_subset_univ =
|
|
104 |
subset_trans [OF naturals_subset_nat nat_subset_univ]
|
|
105 |
|
|
106 |
lemma QInr_subset_univ: "a <= univ(A) ==> QInr(a) <= univ(A)"
|
|
107 |
apply (unfold QInr_def)
|
|
108 |
apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ])
|
|
109 |
done
|
|
110 |
|
|
111 |
(*** Closure for Quine-inspired products and sums ***)
|
|
112 |
|
|
113 |
(*Quine ordered pairs*)
|
|
114 |
lemma QPair_in_quniv:
|
|
115 |
"[| a: quniv(A); b: quniv(A) |] ==> <a;b> : quniv(A)"
|
|
116 |
by (simp add: quniv_def QPair_def sum_subset_univ)
|
|
117 |
|
|
118 |
lemma QSigma_quniv: "quniv(A) <*> quniv(A) <= quniv(A)"
|
|
119 |
by (blast intro: QPair_in_quniv)
|
|
120 |
|
|
121 |
lemmas QSigma_subset_quniv = subset_trans [OF QSigma_mono QSigma_quniv]
|
|
122 |
|
|
123 |
(*The opposite inclusion*)
|
|
124 |
lemma quniv_QPair_D:
|
|
125 |
"<a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)"
|
|
126 |
apply (unfold quniv_def QPair_def)
|
|
127 |
apply (rule Transset_includes_summands [THEN conjE])
|
|
128 |
apply (rule Transset_eclose [THEN Transset_univ])
|
|
129 |
apply (erule PowD, blast)
|
|
130 |
done
|
|
131 |
|
|
132 |
lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE, standard]
|
|
133 |
|
|
134 |
lemma quniv_QPair_iff: "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"
|
|
135 |
by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
|
|
136 |
|
|
137 |
|
|
138 |
(** Quine disjoint sum **)
|
|
139 |
|
|
140 |
lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) : quniv(A)"
|
|
141 |
by (simp add: QInl_def zero_in_quniv QPair_in_quniv)
|
|
142 |
|
|
143 |
lemma QInr_in_quniv: "b: quniv(A) ==> QInr(b) : quniv(A)"
|
|
144 |
by (simp add: QInr_def one_in_quniv QPair_in_quniv)
|
|
145 |
|
|
146 |
lemma qsum_quniv: "quniv(C) <+> quniv(C) <= quniv(C)"
|
|
147 |
by (blast intro: QInl_in_quniv QInr_in_quniv)
|
|
148 |
|
|
149 |
lemmas qsum_subset_quniv = subset_trans [OF qsum_mono qsum_quniv]
|
|
150 |
|
|
151 |
|
|
152 |
(*** The natural numbers ***)
|
|
153 |
|
|
154 |
lemmas nat_subset_quniv = subset_trans [OF nat_subset_univ univ_subset_quniv]
|
|
155 |
|
|
156 |
(* n:nat ==> n:quniv(A) *)
|
|
157 |
lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD, standard]
|
|
158 |
|
|
159 |
lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv]
|
|
160 |
|
|
161 |
lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard]
|
|
162 |
|
|
163 |
|
|
164 |
(*** Intersecting <a;b> with Vfrom... ***)
|
|
165 |
|
|
166 |
lemma QPair_Int_Vfrom_succ_subset:
|
|
167 |
"Transset(X) ==>
|
|
168 |
<a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"
|
|
169 |
by (simp add: QPair_def sum_def Int_Un_distrib2 Un_mono
|
|
170 |
product_Int_Vfrom_subset [THEN subset_trans]
|
|
171 |
Sigma_mono [OF Int_lower1 subset_refl])
|
|
172 |
|
|
173 |
(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****)
|
|
174 |
|
|
175 |
(*Rule for level i -- preserving the level, not decreasing it*)
|
|
176 |
|
|
177 |
lemma QPair_Int_Vfrom_subset:
|
|
178 |
"Transset(X) ==>
|
|
179 |
<a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"
|
|
180 |
apply (unfold QPair_def)
|
|
181 |
apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset])
|
|
182 |
done
|
|
183 |
|
|
184 |
(*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*)
|
|
185 |
lemmas QPair_Int_Vset_subset_trans =
|
|
186 |
subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono]
|
|
187 |
|
|
188 |
lemma QPair_Int_Vset_subset_UN:
|
|
189 |
"Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"
|
|
190 |
apply (erule Ord_cases)
|
|
191 |
(*0 case*)
|
|
192 |
apply (simp add: Vfrom_0)
|
|
193 |
(*succ(j) case*)
|
|
194 |
apply (erule ssubst)
|
|
195 |
apply (rule Transset_0 [THEN QPair_Int_Vfrom_succ_subset, THEN subset_trans])
|
|
196 |
apply (rule succI1 [THEN UN_upper])
|
|
197 |
(*Limit(i) case*)
|
|
198 |
apply (simp del: UN_simps
|
|
199 |
add: Limit_Vfrom_eq Int_UN_distrib UN_mono QPair_Int_Vset_subset_trans)
|
|
200 |
done
|
|
201 |
|
|
202 |
ML
|
|
203 |
{*
|
|
204 |
val Transset_includes_summands = thm "Transset_includes_summands";
|
|
205 |
val Transset_sum_Int_subset = thm "Transset_sum_Int_subset";
|
|
206 |
val qunivI = thm "qunivI";
|
|
207 |
val qunivD = thm "qunivD";
|
|
208 |
val quniv_mono = thm "quniv_mono";
|
|
209 |
val univ_eclose_subset_quniv = thm "univ_eclose_subset_quniv";
|
|
210 |
val univ_subset_quniv = thm "univ_subset_quniv";
|
|
211 |
val univ_into_quniv = thm "univ_into_quniv";
|
|
212 |
val Pow_univ_subset_quniv = thm "Pow_univ_subset_quniv";
|
|
213 |
val univ_subset_into_quniv = thm "univ_subset_into_quniv";
|
|
214 |
val zero_in_quniv = thm "zero_in_quniv";
|
|
215 |
val one_in_quniv = thm "one_in_quniv";
|
|
216 |
val two_in_quniv = thm "two_in_quniv";
|
|
217 |
val A_subset_quniv = thm "A_subset_quniv";
|
|
218 |
val A_into_quniv = thm "A_into_quniv";
|
|
219 |
val QPair_subset_univ = thm "QPair_subset_univ";
|
|
220 |
val QInl_subset_univ = thm "QInl_subset_univ";
|
|
221 |
val naturals_subset_nat = thm "naturals_subset_nat";
|
|
222 |
val naturals_subset_univ = thm "naturals_subset_univ";
|
|
223 |
val QInr_subset_univ = thm "QInr_subset_univ";
|
|
224 |
val QPair_in_quniv = thm "QPair_in_quniv";
|
|
225 |
val QSigma_quniv = thm "QSigma_quniv";
|
|
226 |
val QSigma_subset_quniv = thm "QSigma_subset_quniv";
|
|
227 |
val quniv_QPair_D = thm "quniv_QPair_D";
|
|
228 |
val quniv_QPair_E = thm "quniv_QPair_E";
|
|
229 |
val quniv_QPair_iff = thm "quniv_QPair_iff";
|
|
230 |
val QInl_in_quniv = thm "QInl_in_quniv";
|
|
231 |
val QInr_in_quniv = thm "QInr_in_quniv";
|
|
232 |
val qsum_quniv = thm "qsum_quniv";
|
|
233 |
val qsum_subset_quniv = thm "qsum_subset_quniv";
|
|
234 |
val nat_subset_quniv = thm "nat_subset_quniv";
|
|
235 |
val nat_into_quniv = thm "nat_into_quniv";
|
|
236 |
val bool_subset_quniv = thm "bool_subset_quniv";
|
|
237 |
val bool_into_quniv = thm "bool_into_quniv";
|
|
238 |
val QPair_Int_Vfrom_succ_subset = thm "QPair_Int_Vfrom_succ_subset";
|
|
239 |
val QPair_Int_Vfrom_subset = thm "QPair_Int_Vfrom_subset";
|
|
240 |
val QPair_Int_Vset_subset_trans = thm "QPair_Int_Vset_subset_trans";
|
|
241 |
val QPair_Int_Vset_subset_UN = thm "QPair_Int_Vset_subset_UN";
|
|
242 |
*}
|
|
243 |
|
0
|
244 |
end
|