13223
|
1 |
header {* First-Order Formulas and the Definition of the Class L *}
|
|
2 |
|
|
3 |
theory Formula = Main:
|
|
4 |
|
13291
|
5 |
subsection{*Internalized formulas of FOL*}
|
|
6 |
|
|
7 |
text{*De Bruijn representation.
|
|
8 |
Unbound variables get their denotations from an environment.*}
|
13223
|
9 |
|
|
10 |
consts formula :: i
|
|
11 |
datatype
|
|
12 |
"formula" = Member ("x: nat", "y: nat")
|
|
13 |
| Equal ("x: nat", "y: nat")
|
|
14 |
| Neg ("p: formula")
|
|
15 |
| And ("p: formula", "q: formula")
|
|
16 |
| Forall ("p: formula")
|
|
17 |
|
|
18 |
declare formula.intros [TC]
|
|
19 |
|
|
20 |
constdefs Or :: "[i,i]=>i"
|
|
21 |
"Or(p,q) == Neg(And(Neg(p),Neg(q)))"
|
|
22 |
|
|
23 |
constdefs Implies :: "[i,i]=>i"
|
|
24 |
"Implies(p,q) == Neg(And(p,Neg(q)))"
|
|
25 |
|
13291
|
26 |
constdefs Iff :: "[i,i]=>i"
|
|
27 |
"Iff(p,q) == And(Implies(p,q), Implies(q,p))"
|
|
28 |
|
13223
|
29 |
constdefs Exists :: "i=>i"
|
|
30 |
"Exists(p) == Neg(Forall(Neg(p)))";
|
|
31 |
|
|
32 |
lemma Or_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> Or(p,q) \<in> formula"
|
|
33 |
by (simp add: Or_def)
|
|
34 |
|
|
35 |
lemma Implies_type [TC]:
|
|
36 |
"[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
|
|
37 |
by (simp add: Implies_def)
|
|
38 |
|
13291
|
39 |
lemma Iff_type [TC]:
|
|
40 |
"[| p \<in> formula; q \<in> formula |] ==> Iff(p,q) \<in> formula"
|
|
41 |
by (simp add: Iff_def)
|
|
42 |
|
13223
|
43 |
lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
|
|
44 |
by (simp add: Exists_def)
|
|
45 |
|
|
46 |
|
|
47 |
consts satisfies :: "[i,i]=>i"
|
|
48 |
primrec (*explicit lambda is required because the environment varies*)
|
|
49 |
"satisfies(A,Member(x,y)) =
|
|
50 |
(\<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env)))"
|
|
51 |
|
|
52 |
"satisfies(A,Equal(x,y)) =
|
|
53 |
(\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))"
|
|
54 |
|
|
55 |
"satisfies(A,Neg(p)) =
|
|
56 |
(\<lambda>env \<in> list(A). not(satisfies(A,p)`env))"
|
|
57 |
|
|
58 |
"satisfies(A,And(p,q)) =
|
|
59 |
(\<lambda>env \<in> list(A). (satisfies(A,p)`env) and (satisfies(A,q)`env))"
|
|
60 |
|
|
61 |
"satisfies(A,Forall(p)) =
|
|
62 |
(\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))"
|
|
63 |
|
|
64 |
|
|
65 |
lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
|
|
66 |
by (induct_tac p, simp_all)
|
|
67 |
|
|
68 |
syntax sats :: "[i,i,i] => o"
|
|
69 |
translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"
|
|
70 |
|
|
71 |
lemma [simp]:
|
|
72 |
"env \<in> list(A)
|
|
73 |
==> sats(A, Member(x,y), env) <-> nth(x,env) \<in> nth(y,env)"
|
|
74 |
by simp
|
|
75 |
|
|
76 |
lemma [simp]:
|
|
77 |
"env \<in> list(A)
|
|
78 |
==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)"
|
|
79 |
by simp
|
|
80 |
|
|
81 |
lemma sats_Neg_iff [simp]:
|
|
82 |
"env \<in> list(A)
|
|
83 |
==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)"
|
|
84 |
by (simp add: Bool.not_def cond_def)
|
|
85 |
|
|
86 |
lemma sats_And_iff [simp]:
|
|
87 |
"env \<in> list(A)
|
|
88 |
==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)"
|
|
89 |
by (simp add: Bool.and_def cond_def)
|
|
90 |
|
|
91 |
lemma sats_Forall_iff [simp]:
|
|
92 |
"env \<in> list(A)
|
|
93 |
==> sats(A, Forall(p), env) <-> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
|
|
94 |
by simp
|
|
95 |
|
|
96 |
declare satisfies.simps [simp del];
|
|
97 |
|
13298
|
98 |
subsection{*Dividing line between primitive and derived connectives*}
|
13223
|
99 |
|
|
100 |
lemma sats_Or_iff [simp]:
|
|
101 |
"env \<in> list(A)
|
|
102 |
==> (sats(A, Or(p,q), env)) <-> sats(A,p,env) | sats(A,q,env)"
|
|
103 |
by (simp add: Or_def)
|
|
104 |
|
|
105 |
lemma sats_Implies_iff [simp]:
|
|
106 |
"env \<in> list(A)
|
|
107 |
==> (sats(A, Implies(p,q), env)) <-> (sats(A,p,env) --> sats(A,q,env))"
|
13291
|
108 |
by (simp add: Implies_def, blast)
|
|
109 |
|
|
110 |
lemma sats_Iff_iff [simp]:
|
|
111 |
"env \<in> list(A)
|
|
112 |
==> (sats(A, Iff(p,q), env)) <-> (sats(A,p,env) <-> sats(A,q,env))"
|
|
113 |
by (simp add: Iff_def, blast)
|
13223
|
114 |
|
|
115 |
lemma sats_Exists_iff [simp]:
|
|
116 |
"env \<in> list(A)
|
|
117 |
==> sats(A, Exists(p), env) <-> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))"
|
|
118 |
by (simp add: Exists_def)
|
|
119 |
|
|
120 |
|
13291
|
121 |
subsubsection{*Derived rules to help build up formulas*}
|
|
122 |
|
|
123 |
lemma mem_iff_sats:
|
|
124 |
"[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
|
|
125 |
==> (x\<in>y) <-> sats(A, Member(i,j), env)"
|
|
126 |
by (simp add: satisfies.simps)
|
|
127 |
|
13298
|
128 |
lemma equal_iff_sats:
|
|
129 |
"[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
|
|
130 |
==> (x=y) <-> sats(A, Equal(i,j), env)"
|
|
131 |
by (simp add: satisfies.simps)
|
|
132 |
|
13291
|
133 |
lemma conj_iff_sats:
|
|
134 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
|
|
135 |
==> (P & Q) <-> sats(A, And(p,q), env)"
|
|
136 |
by (simp add: sats_And_iff)
|
|
137 |
|
|
138 |
lemma disj_iff_sats:
|
|
139 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
|
|
140 |
==> (P | Q) <-> sats(A, Or(p,q), env)"
|
|
141 |
by (simp add: sats_Or_iff)
|
|
142 |
|
|
143 |
lemma imp_iff_sats:
|
|
144 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
|
|
145 |
==> (P --> Q) <-> sats(A, Implies(p,q), env)"
|
|
146 |
by (simp add: sats_Forall_iff)
|
|
147 |
|
|
148 |
lemma iff_iff_sats:
|
|
149 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
|
|
150 |
==> (P <-> Q) <-> sats(A, Iff(p,q), env)"
|
|
151 |
by (simp add: sats_Forall_iff)
|
|
152 |
|
|
153 |
lemma imp_iff_sats:
|
|
154 |
"[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
|
|
155 |
==> (P --> Q) <-> sats(A, Implies(p,q), env)"
|
|
156 |
by (simp add: sats_Forall_iff)
|
|
157 |
|
|
158 |
lemma ball_iff_sats:
|
|
159 |
"[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
|
|
160 |
==> (\<forall>x\<in>A. P(x)) <-> sats(A, Forall(p), env)"
|
|
161 |
by (simp add: sats_Forall_iff)
|
|
162 |
|
|
163 |
lemma bex_iff_sats:
|
|
164 |
"[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
|
|
165 |
==> (\<exists>x\<in>A. P(x)) <-> sats(A, Exists(p), env)"
|
|
166 |
by (simp add: sats_Exists_iff)
|
|
167 |
|
13223
|
168 |
|
|
169 |
constdefs incr_var :: "[i,i]=>i"
|
|
170 |
"incr_var(x,lev) == if x<lev then x else succ(x)"
|
|
171 |
|
|
172 |
lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x"
|
|
173 |
by (simp add: incr_var_def)
|
|
174 |
|
|
175 |
lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"
|
|
176 |
apply (simp add: incr_var_def)
|
|
177 |
apply (blast dest: lt_trans1)
|
|
178 |
done
|
|
179 |
|
|
180 |
consts incr_bv :: "i=>i"
|
|
181 |
primrec
|
|
182 |
"incr_bv(Member(x,y)) =
|
|
183 |
(\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))"
|
|
184 |
|
|
185 |
"incr_bv(Equal(x,y)) =
|
|
186 |
(\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"
|
|
187 |
|
|
188 |
"incr_bv(Neg(p)) =
|
|
189 |
(\<lambda>lev \<in> nat. Neg(incr_bv(p)`lev))"
|
|
190 |
|
|
191 |
"incr_bv(And(p,q)) =
|
|
192 |
(\<lambda>lev \<in> nat. And (incr_bv(p)`lev, incr_bv(q)`lev))"
|
|
193 |
|
|
194 |
"incr_bv(Forall(p)) =
|
|
195 |
(\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
|
|
196 |
|
|
197 |
|
|
198 |
constdefs incr_boundvars :: "i => i"
|
|
199 |
"incr_boundvars(p) == incr_bv(p)`0"
|
|
200 |
|
|
201 |
|
|
202 |
lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
|
|
203 |
by (simp add: incr_var_def)
|
|
204 |
|
|
205 |
lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
|
|
206 |
by (induct_tac p, simp_all)
|
|
207 |
|
|
208 |
lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula"
|
|
209 |
by (simp add: incr_boundvars_def)
|
|
210 |
|
|
211 |
(*Obviously DPow is closed under complements and finite intersections and
|
|
212 |
unions. Needs an inductive lemma to allow two lists of parameters to
|
|
213 |
be combined.*)
|
|
214 |
|
|
215 |
lemma sats_incr_bv_iff [rule_format]:
|
|
216 |
"[| p \<in> formula; env \<in> list(A); x \<in> A |]
|
|
217 |
==> \<forall>bvs \<in> list(A).
|
|
218 |
sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) <->
|
|
219 |
sats(A, p, bvs@env)"
|
|
220 |
apply (induct_tac p)
|
|
221 |
apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type)
|
|
222 |
apply (auto simp add: diff_succ not_lt_iff_le)
|
|
223 |
done
|
|
224 |
|
|
225 |
(*UNUSED*)
|
|
226 |
lemma sats_incr_boundvars_iff:
|
|
227 |
"[| p \<in> formula; env \<in> list(A); x \<in> A |]
|
|
228 |
==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)"
|
|
229 |
apply (insert sats_incr_bv_iff [of p env A x Nil])
|
|
230 |
apply (simp add: incr_boundvars_def)
|
|
231 |
done
|
|
232 |
|
|
233 |
(*UNUSED
|
|
234 |
lemma formula_add_params [rule_format]:
|
|
235 |
"[| p \<in> formula; n \<in> nat |]
|
|
236 |
==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
|
|
237 |
length(bvs) = n -->
|
|
238 |
sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)"
|
|
239 |
apply (induct_tac n, simp, clarify)
|
|
240 |
apply (erule list.cases)
|
|
241 |
apply (auto simp add: sats_incr_boundvars_iff)
|
|
242 |
done
|
|
243 |
*)
|
|
244 |
|
|
245 |
consts arity :: "i=>i"
|
|
246 |
primrec
|
|
247 |
"arity(Member(x,y)) = succ(x) \<union> succ(y)"
|
|
248 |
|
|
249 |
"arity(Equal(x,y)) = succ(x) \<union> succ(y)"
|
|
250 |
|
|
251 |
"arity(Neg(p)) = arity(p)"
|
|
252 |
|
|
253 |
"arity(And(p,q)) = arity(p) \<union> arity(q)"
|
|
254 |
|
13269
|
255 |
"arity(Forall(p)) = nat_case(0, %x. x, arity(p))"
|
13223
|
256 |
|
|
257 |
|
|
258 |
lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
|
|
259 |
by (induct_tac p, simp_all)
|
|
260 |
|
|
261 |
lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
|
|
262 |
by (simp add: Or_def)
|
|
263 |
|
|
264 |
lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
|
|
265 |
by (simp add: Implies_def)
|
|
266 |
|
13291
|
267 |
lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
|
|
268 |
by (simp add: Iff_def, blast)
|
|
269 |
|
13269
|
270 |
lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
|
13223
|
271 |
by (simp add: Exists_def)
|
|
272 |
|
|
273 |
|
|
274 |
lemma arity_sats_iff [rule_format]:
|
|
275 |
"[| p \<in> formula; extra \<in> list(A) |]
|
|
276 |
==> \<forall>env \<in> list(A).
|
|
277 |
arity(p) \<le> length(env) -->
|
|
278 |
sats(A, p, env @ extra) <-> sats(A, p, env)"
|
|
279 |
apply (induct_tac p)
|
13269
|
280 |
apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat
|
|
281 |
split: split_nat_case, auto)
|
13223
|
282 |
done
|
|
283 |
|
|
284 |
lemma arity_sats1_iff:
|
|
285 |
"[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A);
|
|
286 |
extra \<in> list(A) |]
|
|
287 |
==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
|
|
288 |
apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
|
|
289 |
apply simp
|
|
290 |
done
|
|
291 |
|
|
292 |
(*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
|
|
293 |
lemma incr_var_lemma:
|
|
294 |
"[| x \<in> nat; y \<in> nat; lev \<le> x |]
|
|
295 |
==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)"
|
|
296 |
apply (simp add: incr_var_def Ord_Un_if, auto)
|
|
297 |
apply (blast intro: leI)
|
|
298 |
apply (simp add: not_lt_iff_le)
|
|
299 |
apply (blast intro: le_anti_sym)
|
|
300 |
apply (blast dest: lt_trans2)
|
|
301 |
done
|
|
302 |
|
|
303 |
lemma incr_And_lemma:
|
|
304 |
"y < x ==> y \<union> succ(x) = succ(x \<union> y)"
|
|
305 |
apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff)
|
|
306 |
apply (blast dest: lt_asym)
|
|
307 |
done
|
|
308 |
|
|
309 |
lemma arity_incr_bv_lemma [rule_format]:
|
|
310 |
"p \<in> formula
|
|
311 |
==> \<forall>n \<in> nat. arity (incr_bv(p) ` n) =
|
|
312 |
(if n < arity(p) then succ(arity(p)) else arity(p))"
|
|
313 |
apply (induct_tac p)
|
|
314 |
apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
|
|
315 |
succ_Un_distrib [symmetric] incr_var_lt incr_var_le
|
13269
|
316 |
Un_commute incr_var_lemma arity_type nat_imp_quasinat
|
|
317 |
split: split_nat_case)
|
|
318 |
txt{*the Forall case reduces to linear arithmetic*}
|
|
319 |
prefer 2
|
|
320 |
apply clarify
|
|
321 |
apply (blast dest: lt_trans1)
|
|
322 |
txt{*left with the And case*}
|
13223
|
323 |
apply safe
|
|
324 |
apply (blast intro: incr_And_lemma lt_trans1)
|
|
325 |
apply (subst incr_And_lemma)
|
13269
|
326 |
apply (blast intro: lt_trans1)
|
|
327 |
apply (simp add: Un_commute)
|
13223
|
328 |
done
|
|
329 |
|
|
330 |
lemma arity_incr_boundvars_eq:
|
|
331 |
"p \<in> formula
|
|
332 |
==> arity(incr_boundvars(p)) =
|
|
333 |
(if 0 < arity(p) then succ(arity(p)) else arity(p))"
|
|
334 |
apply (insert arity_incr_bv_lemma [of p 0])
|
|
335 |
apply (simp add: incr_boundvars_def)
|
|
336 |
done
|
|
337 |
|
|
338 |
lemma arity_iterates_incr_boundvars_eq:
|
|
339 |
"[| p \<in> formula; n \<in> nat |]
|
|
340 |
==> arity(incr_boundvars^n(p)) =
|
|
341 |
(if 0 < arity(p) then n #+ arity(p) else arity(p))"
|
|
342 |
apply (induct_tac n)
|
|
343 |
apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le)
|
|
344 |
done
|
|
345 |
|
|
346 |
|
13298
|
347 |
subsection{*Renaming all but the first bound variable*}
|
13223
|
348 |
|
|
349 |
constdefs incr_bv1 :: "i => i"
|
|
350 |
"incr_bv1(p) == incr_bv(p)`1"
|
|
351 |
|
|
352 |
|
|
353 |
lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula"
|
|
354 |
by (simp add: incr_bv1_def)
|
|
355 |
|
|
356 |
(*For renaming all but the bound variable at level 0*)
|
|
357 |
lemma sats_incr_bv1_iff [rule_format]:
|
|
358 |
"[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
|
|
359 |
==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <->
|
|
360 |
sats(A, p, Cons(x,env))"
|
|
361 |
apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"])
|
|
362 |
apply (simp add: incr_bv1_def)
|
|
363 |
done
|
|
364 |
|
|
365 |
lemma formula_add_params1 [rule_format]:
|
|
366 |
"[| p \<in> formula; n \<in> nat; x \<in> A |]
|
|
367 |
==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
|
|
368 |
length(bvs) = n -->
|
|
369 |
sats(A, iterates(incr_bv1, n, p), Cons(x, bvs@env)) <->
|
|
370 |
sats(A, p, Cons(x,env))"
|
|
371 |
apply (induct_tac n, simp, clarify)
|
|
372 |
apply (erule list.cases)
|
|
373 |
apply (simp_all add: sats_incr_bv1_iff)
|
|
374 |
done
|
|
375 |
|
|
376 |
|
|
377 |
lemma arity_incr_bv1_eq:
|
|
378 |
"p \<in> formula
|
|
379 |
==> arity(incr_bv1(p)) =
|
|
380 |
(if 1 < arity(p) then succ(arity(p)) else arity(p))"
|
|
381 |
apply (insert arity_incr_bv_lemma [of p 1])
|
|
382 |
apply (simp add: incr_bv1_def)
|
|
383 |
done
|
|
384 |
|
|
385 |
lemma arity_iterates_incr_bv1_eq:
|
|
386 |
"[| p \<in> formula; n \<in> nat |]
|
|
387 |
==> arity(incr_bv1^n(p)) =
|
|
388 |
(if 1 < arity(p) then n #+ arity(p) else arity(p))"
|
|
389 |
apply (induct_tac n)
|
13298
|
390 |
apply (simp_all add: arity_incr_bv1_eq)
|
13223
|
391 |
apply (simp add: not_lt_iff_le)
|
|
392 |
apply (blast intro: le_trans add_le_self2 arity_type)
|
|
393 |
done
|
|
394 |
|
|
395 |
|
|
396 |
(*Definable powerset operation: Kunen's definition 1.1, page 165.*)
|
|
397 |
constdefs DPow :: "i => i"
|
|
398 |
"DPow(A) == {X \<in> Pow(A).
|
|
399 |
\<exists>env \<in> list(A). \<exists>p \<in> formula.
|
|
400 |
arity(p) \<le> succ(length(env)) &
|
|
401 |
X = {x\<in>A. sats(A, p, Cons(x,env))}}"
|
|
402 |
|
|
403 |
lemma DPowI:
|
13291
|
404 |
"[|env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))|]
|
13223
|
405 |
==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
|
|
406 |
by (simp add: DPow_def, blast)
|
|
407 |
|
13291
|
408 |
text{*With this rule we can specify @{term p} later.*}
|
|
409 |
lemma DPowI2 [rule_format]:
|
|
410 |
"[|\<forall>x\<in>A. P(x) <-> sats(A, p, Cons(x,env));
|
|
411 |
env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))|]
|
|
412 |
==> {x\<in>A. P(x)} \<in> DPow(A)"
|
|
413 |
by (simp add: DPow_def, blast)
|
|
414 |
|
13223
|
415 |
lemma DPowD:
|
|
416 |
"X \<in> DPow(A)
|
|
417 |
==> X <= A &
|
|
418 |
(\<exists>env \<in> list(A).
|
|
419 |
\<exists>p \<in> formula. arity(p) \<le> succ(length(env)) &
|
|
420 |
X = {x\<in>A. sats(A, p, Cons(x,env))})"
|
|
421 |
by (simp add: DPow_def)
|
|
422 |
|
|
423 |
lemmas DPow_imp_subset = DPowD [THEN conjunct1]
|
|
424 |
|
|
425 |
(*Lemma 1.2*)
|
|
426 |
lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |]
|
|
427 |
==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
|
|
428 |
by (blast intro: DPowI)
|
|
429 |
|
|
430 |
lemma DPow_subset_Pow: "DPow(A) <= Pow(A)"
|
|
431 |
by (simp add: DPow_def, blast)
|
|
432 |
|
|
433 |
lemma empty_in_DPow: "0 \<in> DPow(A)"
|
|
434 |
apply (simp add: DPow_def)
|
|
435 |
apply (rule_tac x="Nil" in bexI)
|
|
436 |
apply (rule_tac x="Neg(Equal(0,0))" in bexI)
|
|
437 |
apply (auto simp add: Un_least_lt_iff)
|
|
438 |
done
|
|
439 |
|
|
440 |
lemma Compl_in_DPow: "X \<in> DPow(A) ==> (A-X) \<in> DPow(A)"
|
|
441 |
apply (simp add: DPow_def, clarify, auto)
|
|
442 |
apply (rule bexI)
|
|
443 |
apply (rule_tac x="Neg(p)" in bexI)
|
|
444 |
apply auto
|
|
445 |
done
|
|
446 |
|
|
447 |
lemma Int_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Int Y \<in> DPow(A)"
|
|
448 |
apply (simp add: DPow_def, auto)
|
|
449 |
apply (rename_tac envp p envq q)
|
|
450 |
apply (rule_tac x="envp@envq" in bexI)
|
|
451 |
apply (rule_tac x="And(p, iterates(incr_bv1,length(envp),q))" in bexI)
|
|
452 |
apply typecheck
|
|
453 |
apply (rule conjI)
|
|
454 |
(*finally check the arity!*)
|
|
455 |
apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)
|
|
456 |
apply (force intro: add_le_self le_trans)
|
|
457 |
apply (simp add: arity_sats1_iff formula_add_params1, blast)
|
|
458 |
done
|
|
459 |
|
|
460 |
lemma Un_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Un Y \<in> DPow(A)"
|
|
461 |
apply (subgoal_tac "X Un Y = A - ((A-X) Int (A-Y))")
|
|
462 |
apply (simp add: Int_in_DPow Compl_in_DPow)
|
|
463 |
apply (simp add: DPow_def, blast)
|
|
464 |
done
|
|
465 |
|
|
466 |
lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)"
|
|
467 |
apply (simp add: DPow_def)
|
|
468 |
apply (rule_tac x="Cons(x,Nil)" in bexI)
|
|
469 |
apply (rule_tac x="Equal(0,1)" in bexI)
|
|
470 |
apply typecheck
|
|
471 |
apply (force simp add: succ_Un_distrib [symmetric])
|
|
472 |
done
|
|
473 |
|
|
474 |
lemma cons_in_DPow: "[| a \<in> A; X \<in> DPow(A) |] ==> cons(a,X) \<in> DPow(A)"
|
|
475 |
apply (rule cons_eq [THEN subst])
|
|
476 |
apply (blast intro: singleton_in_DPow Un_in_DPow)
|
|
477 |
done
|
|
478 |
|
|
479 |
(*Part of Lemma 1.3*)
|
|
480 |
lemma Fin_into_DPow: "X \<in> Fin(A) ==> X \<in> DPow(A)"
|
|
481 |
apply (erule Fin.induct)
|
|
482 |
apply (rule empty_in_DPow)
|
|
483 |
apply (blast intro: cons_in_DPow)
|
|
484 |
done
|
|
485 |
|
|
486 |
(*DPow is not monotonic. For example, let A be some non-constructible set
|
|
487 |
of natural numbers, and let B be nat. Then A<=B and obviously A : DPow(A)
|
|
488 |
but A ~: DPow(B).*)
|
|
489 |
lemma DPow_mono: "A : DPow(B) ==> DPow(A) <= DPow(B)"
|
|
490 |
apply (simp add: DPow_def, auto)
|
|
491 |
(*must use the formula defining A in B to relativize the new formula...*)
|
|
492 |
oops
|
|
493 |
|
|
494 |
lemma DPow_0: "DPow(0) = {0}"
|
|
495 |
by (blast intro: empty_in_DPow dest: DPow_imp_subset)
|
|
496 |
|
|
497 |
lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)"
|
|
498 |
by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)
|
|
499 |
|
|
500 |
lemma Finite_DPow_eq_Pow: "Finite(A) ==> DPow(A) = Pow(A)"
|
|
501 |
apply (rule equalityI)
|
|
502 |
apply (rule DPow_subset_Pow)
|
|
503 |
apply (erule Finite_Pow_subset_Pow)
|
|
504 |
done
|
|
505 |
|
|
506 |
(*This may be true but the proof looks difficult, requiring relativization
|
|
507 |
lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
|
|
508 |
apply (rule equalityI, safe)
|
|
509 |
oops
|
|
510 |
*)
|
|
511 |
|
13298
|
512 |
|
|
513 |
subsection{*Internalized formulas for basic concepts*}
|
|
514 |
|
|
515 |
subsubsection{*The subset relation*}
|
|
516 |
|
|
517 |
lemma lt_length_in_nat:
|
|
518 |
"[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
|
|
519 |
apply (frule lt_nat_in_nat, typecheck)
|
|
520 |
done
|
|
521 |
|
|
522 |
constdefs subset_fm :: "[i,i]=>i"
|
|
523 |
"subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
|
|
524 |
|
|
525 |
lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
|
|
526 |
by (simp add: subset_fm_def)
|
|
527 |
|
|
528 |
lemma arity_subset_fm [simp]:
|
|
529 |
"[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
|
|
530 |
by (simp add: subset_fm_def succ_Un_distrib [symmetric])
|
|
531 |
|
|
532 |
lemma sats_subset_fm [simp]:
|
|
533 |
"[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
|
|
534 |
==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
|
|
535 |
apply (frule lt_length_in_nat, assumption)
|
|
536 |
apply (simp add: subset_fm_def Transset_def)
|
|
537 |
apply (blast intro: nth_type)
|
|
538 |
done
|
|
539 |
|
|
540 |
subsubsection{*Transitive sets*}
|
|
541 |
|
|
542 |
constdefs transset_fm :: "i=>i"
|
|
543 |
"transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
|
|
544 |
|
|
545 |
lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
|
|
546 |
by (simp add: transset_fm_def)
|
|
547 |
|
|
548 |
lemma arity_transset_fm [simp]:
|
|
549 |
"x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
|
|
550 |
by (simp add: transset_fm_def succ_Un_distrib [symmetric])
|
|
551 |
|
|
552 |
lemma sats_transset_fm [simp]:
|
|
553 |
"[|x < length(env); env \<in> list(A); Transset(A)|]
|
|
554 |
==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
|
|
555 |
apply (frule lt_nat_in_nat, erule length_type)
|
|
556 |
apply (simp add: transset_fm_def Transset_def)
|
|
557 |
apply (blast intro: nth_type)
|
|
558 |
done
|
|
559 |
|
|
560 |
subsubsection{*Ordinals*}
|
|
561 |
|
|
562 |
constdefs ordinal_fm :: "i=>i"
|
|
563 |
"ordinal_fm(x) ==
|
|
564 |
And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
|
|
565 |
|
|
566 |
lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
|
|
567 |
by (simp add: ordinal_fm_def)
|
|
568 |
|
|
569 |
lemma arity_ordinal_fm [simp]:
|
|
570 |
"x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
|
|
571 |
by (simp add: ordinal_fm_def succ_Un_distrib [symmetric])
|
|
572 |
|
|
573 |
lemma sats_ordinal_fm [simp]:
|
|
574 |
"[|x < length(env); env \<in> list(A); Transset(A)|]
|
|
575 |
==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
|
|
576 |
apply (frule lt_nat_in_nat, erule length_type)
|
|
577 |
apply (simp add: ordinal_fm_def Ord_def Transset_def)
|
|
578 |
apply (blast intro: nth_type)
|
|
579 |
done
|
|
580 |
|
|
581 |
|
13223
|
582 |
subsection{* Constant Lset: Levels of the Constructible Universe *}
|
|
583 |
|
|
584 |
constdefs Lset :: "i=>i"
|
|
585 |
"Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
|
|
586 |
|
|
587 |
text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
|
|
588 |
lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"
|
|
589 |
by (subst Lset_def [THEN def_transrec], simp)
|
|
590 |
|
|
591 |
lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)";
|
|
592 |
by (subst Lset, blast)
|
|
593 |
|
|
594 |
lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))";
|
|
595 |
apply (insert Lset [of x])
|
|
596 |
apply (blast intro: elim: equalityE)
|
|
597 |
done
|
|
598 |
|
|
599 |
subsubsection{* Transitivity *}
|
|
600 |
|
|
601 |
lemma elem_subset_in_DPow: "[|X \<in> A; X \<subseteq> A|] ==> X \<in> DPow(A)"
|
|
602 |
apply (simp add: Transset_def DPow_def)
|
|
603 |
apply (rule_tac x="[X]" in bexI)
|
|
604 |
apply (rule_tac x="Member(0,1)" in bexI)
|
|
605 |
apply (auto simp add: Un_least_lt_iff)
|
|
606 |
done
|
|
607 |
|
|
608 |
lemma Transset_subset_DPow: "Transset(A) ==> A <= DPow(A)"
|
|
609 |
apply clarify
|
|
610 |
apply (simp add: Transset_def)
|
|
611 |
apply (blast intro: elem_subset_in_DPow)
|
|
612 |
done
|
|
613 |
|
|
614 |
lemma Transset_DPow: "Transset(A) ==> Transset(DPow(A))"
|
|
615 |
apply (simp add: Transset_def)
|
|
616 |
apply (blast intro: elem_subset_in_DPow dest: DPowD)
|
|
617 |
done
|
|
618 |
|
|
619 |
text{*Kunen's VI, 1.6 (a)*}
|
|
620 |
lemma Transset_Lset: "Transset(Lset(i))"
|
|
621 |
apply (rule_tac a=i in eps_induct)
|
|
622 |
apply (subst Lset)
|
|
623 |
apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)
|
|
624 |
done
|
|
625 |
|
13291
|
626 |
lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) ==> a \<subseteq> Lset(i)"
|
|
627 |
apply (insert Transset_Lset)
|
|
628 |
apply (simp add: Transset_def)
|
|
629 |
done
|
|
630 |
|
13223
|
631 |
subsubsection{* Monotonicity *}
|
|
632 |
|
|
633 |
text{*Kunen's VI, 1.6 (b)*}
|
|
634 |
lemma Lset_mono [rule_format]:
|
|
635 |
"ALL j. i<=j --> Lset(i) <= Lset(j)"
|
|
636 |
apply (rule_tac a=i in eps_induct)
|
|
637 |
apply (rule impI [THEN allI])
|
|
638 |
apply (subst Lset)
|
|
639 |
apply (subst Lset, blast)
|
|
640 |
done
|
|
641 |
|
|
642 |
text{*This version lets us remove the premise @{term "Ord(i)"} sometimes.*}
|
|
643 |
lemma Lset_mono_mem [rule_format]:
|
|
644 |
"ALL j. i:j --> Lset(i) <= Lset(j)"
|
|
645 |
apply (rule_tac a=i in eps_induct)
|
|
646 |
apply (rule impI [THEN allI])
|
|
647 |
apply (subst Lset, auto)
|
|
648 |
apply (rule rev_bexI, assumption)
|
|
649 |
apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD)
|
|
650 |
done
|
|
651 |
|
13291
|
652 |
text{*Useful with Reflection to bump up the ordinal*}
|
|
653 |
lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"
|
|
654 |
by (blast dest: ltD [THEN Lset_mono_mem])
|
|
655 |
|
13223
|
656 |
subsubsection{* 0, successor and limit equations fof Lset *}
|
|
657 |
|
|
658 |
lemma Lset_0 [simp]: "Lset(0) = 0"
|
|
659 |
by (subst Lset, blast)
|
|
660 |
|
|
661 |
lemma Lset_succ_subset1: "DPow(Lset(i)) <= Lset(succ(i))"
|
|
662 |
by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper])
|
|
663 |
|
|
664 |
lemma Lset_succ_subset2: "Lset(succ(i)) <= DPow(Lset(i))"
|
|
665 |
apply (subst Lset, rule UN_least)
|
|
666 |
apply (erule succE)
|
|
667 |
apply blast
|
|
668 |
apply clarify
|
|
669 |
apply (rule elem_subset_in_DPow)
|
|
670 |
apply (subst Lset)
|
|
671 |
apply blast
|
|
672 |
apply (blast intro: dest: DPowD Lset_mono_mem)
|
|
673 |
done
|
|
674 |
|
|
675 |
lemma Lset_succ: "Lset(succ(i)) = DPow(Lset(i))"
|
|
676 |
by (intro equalityI Lset_succ_subset1 Lset_succ_subset2)
|
|
677 |
|
|
678 |
lemma Lset_Union [simp]: "Lset(\<Union>(X)) = (\<Union>y\<in>X. Lset(y))"
|
|
679 |
apply (subst Lset)
|
|
680 |
apply (rule equalityI)
|
|
681 |
txt{*first inclusion*}
|
|
682 |
apply (rule UN_least)
|
|
683 |
apply (erule UnionE)
|
|
684 |
apply (rule subset_trans)
|
|
685 |
apply (erule_tac [2] UN_upper, subst Lset, erule UN_upper)
|
|
686 |
txt{*opposite inclusion*}
|
|
687 |
apply (rule UN_least)
|
|
688 |
apply (subst Lset, blast)
|
|
689 |
done
|
|
690 |
|
|
691 |
subsubsection{* Lset applied to Limit ordinals *}
|
|
692 |
|
|
693 |
lemma Limit_Lset_eq:
|
|
694 |
"Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"
|
|
695 |
by (simp add: Lset_Union [symmetric] Limit_Union_eq)
|
|
696 |
|
|
697 |
lemma lt_LsetI: "[| a: Lset(j); j<i |] ==> a : Lset(i)"
|
|
698 |
by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
|
|
699 |
|
|
700 |
lemma Limit_LsetE:
|
|
701 |
"[| a: Lset(i); ~R ==> Limit(i);
|
|
702 |
!!x. [| x<i; a: Lset(x) |] ==> R
|
|
703 |
|] ==> R"
|
|
704 |
apply (rule classical)
|
|
705 |
apply (rule Limit_Lset_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
|
|
706 |
prefer 2 apply assumption
|
|
707 |
apply blast
|
|
708 |
apply (blast intro: ltI Limit_is_Ord)
|
|
709 |
done
|
|
710 |
|
|
711 |
subsubsection{* Basic closure properties *}
|
|
712 |
|
|
713 |
lemma zero_in_Lset: "y:x ==> 0 : Lset(x)"
|
|
714 |
by (subst Lset, blast intro: empty_in_DPow)
|
|
715 |
|
|
716 |
lemma notin_Lset: "x \<notin> Lset(x)"
|
|
717 |
apply (rule_tac a=x in eps_induct)
|
|
718 |
apply (subst Lset)
|
|
719 |
apply (blast dest: DPowD)
|
|
720 |
done
|
|
721 |
|
|
722 |
|
13298
|
723 |
subsection{*Constructible Ordinals: Kunen's VI, 1.9 (b)*}
|
13223
|
724 |
|
|
725 |
text{*The subset consisting of the ordinals is definable.*}
|
|
726 |
lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
|
|
727 |
apply (simp add: DPow_def Collect_subset)
|
|
728 |
apply (rule_tac x="Nil" in bexI)
|
|
729 |
apply (rule_tac x="ordinal_fm(0)" in bexI)
|
|
730 |
apply (simp_all add: sats_ordinal_fm)
|
|
731 |
done
|
|
732 |
|
|
733 |
lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
|
|
734 |
apply (erule trans_induct3)
|
|
735 |
apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)
|
|
736 |
txt{*The successor case remains.*}
|
|
737 |
apply (rule equalityI)
|
|
738 |
txt{*First inclusion*}
|
|
739 |
apply clarify
|
|
740 |
apply (erule Ord_linear_lt, assumption)
|
|
741 |
apply (blast dest: DPow_imp_subset ltD notE [OF notin_Lset])
|
|
742 |
apply blast
|
|
743 |
apply (blast dest: ltD)
|
|
744 |
txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*}
|
|
745 |
apply auto
|
|
746 |
txt{*Key case: *}
|
|
747 |
apply (erule subst, rule Ords_in_DPow [OF Transset_Lset])
|
|
748 |
apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE)
|
|
749 |
apply (blast intro: Ord_in_Ord)
|
|
750 |
done
|
|
751 |
|
|
752 |
|
|
753 |
lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)"
|
|
754 |
by (subst Ords_of_Lset_eq [symmetric], assumption, fast)
|
|
755 |
|
|
756 |
lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))"
|
|
757 |
apply (simp add: Lset_succ)
|
|
758 |
apply (subst Ords_of_Lset_eq [symmetric], assumption,
|
|
759 |
rule Ords_in_DPow [OF Transset_Lset])
|
|
760 |
done
|
|
761 |
|
|
762 |
subsubsection{* Unions *}
|
|
763 |
|
|
764 |
lemma Union_in_Lset:
|
|
765 |
"X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))"
|
|
766 |
apply (insert Transset_Lset)
|
|
767 |
apply (rule LsetI [OF succI1])
|
|
768 |
apply (simp add: Transset_def DPow_def)
|
|
769 |
apply (intro conjI, blast)
|
|
770 |
txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *}
|
|
771 |
apply (rule_tac x="Cons(X,Nil)" in bexI)
|
|
772 |
apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI)
|
|
773 |
apply typecheck
|
|
774 |
apply (simp add: succ_Un_distrib [symmetric], blast)
|
|
775 |
done
|
|
776 |
|
|
777 |
lemma Union_in_LLimit:
|
|
778 |
"[| X: Lset(i); Limit(i) |] ==> Union(X) : Lset(i)"
|
|
779 |
apply (rule Limit_LsetE, assumption+)
|
|
780 |
apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
|
|
781 |
done
|
|
782 |
|
|
783 |
subsubsection{* Finite sets and ordered pairs *}
|
|
784 |
|
|
785 |
lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
|
|
786 |
by (simp add: Lset_succ singleton_in_DPow)
|
|
787 |
|
|
788 |
lemma doubleton_in_Lset:
|
|
789 |
"[| a: Lset(i); b: Lset(i) |] ==> {a,b} : Lset(succ(i))"
|
|
790 |
by (simp add: Lset_succ empty_in_DPow cons_in_DPow)
|
|
791 |
|
|
792 |
lemma Pair_in_Lset:
|
|
793 |
"[| a: Lset(i); b: Lset(i); Ord(i) |] ==> <a,b> : Lset(succ(succ(i)))"
|
|
794 |
apply (unfold Pair_def)
|
|
795 |
apply (blast intro: doubleton_in_Lset)
|
|
796 |
done
|
|
797 |
|
|
798 |
lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
|
|
799 |
|
|
800 |
lemma singleton_in_LLimit:
|
|
801 |
"[| a: Lset(i); Limit(i) |] ==> {a} : Lset(i)"
|
|
802 |
apply (erule Limit_LsetE, assumption)
|
|
803 |
apply (erule singleton_in_Lset [THEN lt_LsetI])
|
|
804 |
apply (blast intro: Limit_has_succ)
|
|
805 |
done
|
|
806 |
|
|
807 |
lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
|
|
808 |
lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
|
|
809 |
|
|
810 |
text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
|
|
811 |
lemma doubleton_in_LLimit:
|
|
812 |
"[| a: Lset(i); b: Lset(i); Limit(i) |] ==> {a,b} : Lset(i)"
|
|
813 |
apply (erule Limit_LsetE, assumption)
|
|
814 |
apply (erule Limit_LsetE, assumption)
|
13269
|
815 |
apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
|
|
816 |
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
|
13223
|
817 |
done
|
|
818 |
|
|
819 |
lemma Pair_in_LLimit:
|
|
820 |
"[| a: Lset(i); b: Lset(i); Limit(i) |] ==> <a,b> : Lset(i)"
|
|
821 |
txt{*Infer that a, b occur at ordinals x,xa < i.*}
|
|
822 |
apply (erule Limit_LsetE, assumption)
|
|
823 |
apply (erule Limit_LsetE, assumption)
|
|
824 |
txt{*Infer that succ(succ(x Un xa)) < i *}
|
|
825 |
apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset]
|
|
826 |
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
|
|
827 |
done
|
|
828 |
|
|
829 |
lemma product_LLimit: "Limit(i) ==> Lset(i) * Lset(i) <= Lset(i)"
|
|
830 |
by (blast intro: Pair_in_LLimit)
|
|
831 |
|
|
832 |
lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit]
|
|
833 |
|
|
834 |
lemma nat_subset_LLimit: "Limit(i) ==> nat \<subseteq> Lset(i)"
|
|
835 |
by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord)
|
|
836 |
|
|
837 |
lemma nat_into_LLimit: "[| n: nat; Limit(i) |] ==> n : Lset(i)"
|
|
838 |
by (blast intro: nat_subset_LLimit [THEN subsetD])
|
|
839 |
|
|
840 |
|
|
841 |
subsubsection{* Closure under disjoint union *}
|
|
842 |
|
|
843 |
lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
|
|
844 |
|
|
845 |
lemma one_in_LLimit: "Limit(i) ==> 1 : Lset(i)"
|
|
846 |
by (blast intro: nat_into_LLimit)
|
|
847 |
|
|
848 |
lemma Inl_in_LLimit:
|
|
849 |
"[| a: Lset(i); Limit(i) |] ==> Inl(a) : Lset(i)"
|
|
850 |
apply (unfold Inl_def)
|
|
851 |
apply (blast intro: zero_in_LLimit Pair_in_LLimit)
|
|
852 |
done
|
|
853 |
|
|
854 |
lemma Inr_in_LLimit:
|
|
855 |
"[| b: Lset(i); Limit(i) |] ==> Inr(b) : Lset(i)"
|
|
856 |
apply (unfold Inr_def)
|
|
857 |
apply (blast intro: one_in_LLimit Pair_in_LLimit)
|
|
858 |
done
|
|
859 |
|
|
860 |
lemma sum_LLimit: "Limit(i) ==> Lset(i) + Lset(i) <= Lset(i)"
|
|
861 |
by (blast intro!: Inl_in_LLimit Inr_in_LLimit)
|
|
862 |
|
|
863 |
lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit]
|
|
864 |
|
|
865 |
|
|
866 |
text{*The constructible universe and its rank function*}
|
|
867 |
constdefs
|
|
868 |
L :: "i=>o" --{*Kunen's definition VI, 1.5, page 167*}
|
|
869 |
"L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
|
|
870 |
|
|
871 |
lrank :: "i=>i" --{*Kunen's definition VI, 1.7*}
|
|
872 |
"lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
|
|
873 |
|
|
874 |
lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
|
|
875 |
by (simp add: L_def, blast)
|
|
876 |
|
|
877 |
lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)"
|
|
878 |
by (simp add: L_def)
|
|
879 |
|
|
880 |
lemma Ord_lrank [simp]: "Ord(lrank(a))"
|
|
881 |
by (simp add: lrank_def)
|
|
882 |
|
|
883 |
lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) --> lrank(x) < i"
|
|
884 |
apply (erule trans_induct3)
|
|
885 |
apply simp
|
|
886 |
apply (simp only: lrank_def)
|
|
887 |
apply (blast intro: Least_le)
|
|
888 |
apply (simp_all add: Limit_Lset_eq)
|
|
889 |
apply (blast intro: ltI Limit_is_Ord lt_trans)
|
|
890 |
done
|
|
891 |
|
|
892 |
text{*Kunen's VI, 1.8, and the proof is much less trivial than the text
|
|
893 |
would suggest. For a start it need the previous lemma, proved by induction.*}
|
|
894 |
lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i"
|
|
895 |
apply (simp add: L_def, auto)
|
|
896 |
apply (blast intro: Lset_lrank_lt)
|
|
897 |
apply (unfold lrank_def)
|
|
898 |
apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD])
|
|
899 |
apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption)
|
|
900 |
apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
|
|
901 |
done
|
|
902 |
|
|
903 |
lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)"
|
|
904 |
by (simp add: Lset_iff_lrank_lt)
|
|
905 |
|
|
906 |
text{*Kunen's VI, 1.9 (a)*}
|
|
907 |
lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
|
|
908 |
apply (unfold lrank_def)
|
|
909 |
apply (rule Least_equality)
|
|
910 |
apply (erule Ord_in_Lset)
|
|
911 |
apply assumption
|
|
912 |
apply (insert notin_Lset [of i])
|
|
913 |
apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
|
|
914 |
done
|
|
915 |
|
13245
|
916 |
|
|
917 |
lemma Ord_in_L: "Ord(i) ==> L(i)"
|
|
918 |
by (blast intro: Ord_in_Lset L_I)
|
|
919 |
|
13223
|
920 |
text{*This is lrank(lrank(a)) = lrank(a) *}
|
|
921 |
declare Ord_lrank [THEN lrank_of_Ord, simp]
|
|
922 |
|
|
923 |
text{*Kunen's VI, 1.10 *}
|
|
924 |
lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
|
|
925 |
apply (simp add: Lset_succ DPow_def)
|
|
926 |
apply (rule_tac x="Nil" in bexI)
|
|
927 |
apply (rule_tac x="Equal(0,0)" in bexI)
|
|
928 |
apply auto
|
|
929 |
done
|
|
930 |
|
|
931 |
lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i"
|
|
932 |
apply (unfold lrank_def)
|
|
933 |
apply (rule Least_equality)
|
|
934 |
apply (rule Lset_in_Lset_succ)
|
|
935 |
apply assumption
|
|
936 |
apply clarify
|
|
937 |
apply (subgoal_tac "Lset(succ(ia)) <= Lset(i)")
|
|
938 |
apply (blast dest: mem_irrefl)
|
|
939 |
apply (blast intro!: le_imp_subset Lset_mono)
|
|
940 |
done
|
|
941 |
|
|
942 |
text{*Kunen's VI, 1.11 *}
|
|
943 |
lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
|
|
944 |
apply (erule trans_induct)
|
|
945 |
apply (subst Lset)
|
|
946 |
apply (subst Vset)
|
|
947 |
apply (rule UN_mono [OF subset_refl])
|
|
948 |
apply (rule subset_trans [OF DPow_subset_Pow])
|
|
949 |
apply (rule Pow_mono, blast)
|
|
950 |
done
|
|
951 |
|
|
952 |
text{*Kunen's VI, 1.12 *}
|
|
953 |
lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";
|
|
954 |
apply (erule nat_induct)
|
|
955 |
apply (simp add: Vfrom_0)
|
|
956 |
apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)
|
|
957 |
done
|
|
958 |
|
13291
|
959 |
text{*Every set of constructible sets is included in some @{term Lset}*}
|
|
960 |
lemma subset_Lset:
|
|
961 |
"(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)"
|
|
962 |
by (rule_tac x = "\<Union>x\<in>A. succ(lrank(x))" in exI, force)
|
|
963 |
|
|
964 |
lemma subset_LsetE:
|
|
965 |
"[|\<forall>x\<in>A. L(x);
|
|
966 |
!!i. [|Ord(i); A \<subseteq> Lset(i)|] ==> P|]
|
|
967 |
==> P"
|
|
968 |
by (blast dest: subset_Lset)
|
|
969 |
|
13223
|
970 |
subsection{*For L to satisfy the ZF axioms*}
|
|
971 |
|
13245
|
972 |
theorem Union_in_L: "L(X) ==> L(Union(X))"
|
13223
|
973 |
apply (simp add: L_def, clarify)
|
|
974 |
apply (drule Ord_imp_greater_Limit)
|
|
975 |
apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord)
|
|
976 |
done
|
|
977 |
|
13245
|
978 |
theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
|
13223
|
979 |
apply (simp add: L_def, clarify)
|
|
980 |
apply (drule Ord2_imp_greater_Limit, assumption)
|
|
981 |
apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord)
|
|
982 |
done
|
|
983 |
|
|
984 |
subsubsection{*For L to satisfy Powerset *}
|
|
985 |
|
|
986 |
lemma LPow_env_typing:
|
|
987 |
"[| y : Lset(i); Ord(i); y \<subseteq> X |] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))"
|
|
988 |
by (auto intro: L_I iff: Lset_succ_lrank_iff)
|
|
989 |
|
|
990 |
lemma LPow_in_Lset:
|
|
991 |
"[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"
|
|
992 |
apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI)
|
|
993 |
apply simp
|
|
994 |
apply (rule LsetI [OF succI1])
|
|
995 |
apply (simp add: DPow_def)
|
|
996 |
apply (intro conjI, clarify)
|
|
997 |
apply (rule_tac a="x" in UN_I, simp+)
|
|
998 |
txt{*Now to create the formula @{term "y \<subseteq> X"} *}
|
|
999 |
apply (rule_tac x="Cons(X,Nil)" in bexI)
|
|
1000 |
apply (rule_tac x="subset_fm(0,1)" in bexI)
|
|
1001 |
apply typecheck
|
|
1002 |
apply (rule conjI)
|
|
1003 |
apply (simp add: succ_Un_distrib [symmetric])
|
|
1004 |
apply (rule equality_iffI)
|
|
1005 |
apply (simp add: Transset_UN [OF Transset_Lset] list.Cons [OF LPow_env_typing])
|
|
1006 |
apply (auto intro: L_I iff: Lset_succ_lrank_iff)
|
|
1007 |
done
|
|
1008 |
|
13245
|
1009 |
theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
|
13223
|
1010 |
by (blast intro: L_I dest: L_D LPow_in_Lset)
|
|
1011 |
|
|
1012 |
end
|