src/ZF/Constructible/Formula.thy
 author paulson Tue Nov 19 10:41:20 2002 +0100 (2002-11-19) changeset 13721 2cf506c09946 parent 13687 22dce9134953 child 14171 0cab06e3bbd0 permissions -rw-r--r--
stylistic tweaks
1 (*  Title:      ZF/Constructible/Formula.thy
2     ID: \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4 *)
6 header {* First-Order Formulas and the Definition of the Class L *}
8 theory Formula = Main:
10 subsection{*Internalized formulas of FOL*}
12 text{*De Bruijn representation.
13   Unbound variables get their denotations from an environment.*}
15 consts   formula :: i
16 datatype
17   "formula" = Member ("x: nat", "y: nat")
18             | Equal  ("x: nat", "y: nat")
19             | Nand ("p: formula", "q: formula")
20             | Forall ("p: formula")
22 declare formula.intros [TC]
24 constdefs Neg :: "i=>i"
25     "Neg(p) == Nand(p,p)"
27 constdefs And :: "[i,i]=>i"
28     "And(p,q) == Neg(Nand(p,q))"
30 constdefs Or :: "[i,i]=>i"
31     "Or(p,q) == Nand(Neg(p),Neg(q))"
33 constdefs Implies :: "[i,i]=>i"
34     "Implies(p,q) == Nand(p,Neg(q))"
36 constdefs Iff :: "[i,i]=>i"
37     "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
39 constdefs Exists :: "i=>i"
40     "Exists(p) == Neg(Forall(Neg(p)))";
42 lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula"
45 lemma And_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> And(p,q) \<in> formula"
48 lemma Or_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> Or(p,q) \<in> formula"
51 lemma Implies_type [TC]:
52      "[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
55 lemma Iff_type [TC]:
56      "[| p \<in> formula; q \<in> formula |] ==> Iff(p,q) \<in> formula"
59 lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
63 consts   satisfies :: "[i,i]=>i"
64 primrec (*explicit lambda is required because the environment varies*)
65   "satisfies(A,Member(x,y)) =
66       (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env)))"
68   "satisfies(A,Equal(x,y)) =
69       (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))"
71   "satisfies(A,Nand(p,q)) =
72       (\<lambda>env \<in> list(A). not ((satisfies(A,p)`env) and (satisfies(A,q)`env)))"
74   "satisfies(A,Forall(p)) =
75       (\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))"
78 lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
79 by (induct_tac p, simp_all)
81 syntax sats :: "[i,i,i] => o"
82 translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"
84 lemma [simp]:
85   "env \<in> list(A)
86    ==> sats(A, Member(x,y), env) <-> nth(x,env) \<in> nth(y,env)"
87 by simp
89 lemma [simp]:
90   "env \<in> list(A)
91    ==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)"
92 by simp
94 lemma sats_Nand_iff [simp]:
95   "env \<in> list(A)
96    ==> (sats(A, Nand(p,q), env)) <-> ~ (sats(A,p,env) & sats(A,q,env))"
97 by (simp add: Bool.and_def Bool.not_def cond_def)
99 lemma sats_Forall_iff [simp]:
100   "env \<in> list(A)
101    ==> sats(A, Forall(p), env) <-> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
102 by simp
104 declare satisfies.simps [simp del];
106 subsection{*Dividing line between primitive and derived connectives*}
108 lemma sats_Neg_iff [simp]:
109   "env \<in> list(A)
110    ==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)"
113 lemma sats_And_iff [simp]:
114   "env \<in> list(A)
115    ==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)"
118 lemma sats_Or_iff [simp]:
119   "env \<in> list(A)
120    ==> (sats(A, Or(p,q), env)) <-> sats(A,p,env) | sats(A,q,env)"
123 lemma sats_Implies_iff [simp]:
124   "env \<in> list(A)
125    ==> (sats(A, Implies(p,q), env)) <-> (sats(A,p,env) --> sats(A,q,env))"
126 by (simp add: Implies_def, blast)
128 lemma sats_Iff_iff [simp]:
129   "env \<in> list(A)
130    ==> (sats(A, Iff(p,q), env)) <-> (sats(A,p,env) <-> sats(A,q,env))"
131 by (simp add: Iff_def, blast)
133 lemma sats_Exists_iff [simp]:
134   "env \<in> list(A)
135    ==> sats(A, Exists(p), env) <-> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))"
139 subsubsection{*Derived rules to help build up formulas*}
141 lemma mem_iff_sats:
142       "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
143        ==> (x\<in>y) <-> sats(A, Member(i,j), env)"
146 lemma equal_iff_sats:
147       "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
148        ==> (x=y) <-> sats(A, Equal(i,j), env)"
151 lemma not_iff_sats:
152       "[| P <-> sats(A,p,env); env \<in> list(A)|]
153        ==> (~P) <-> sats(A, Neg(p), env)"
154 by simp
156 lemma conj_iff_sats:
157       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
158        ==> (P & Q) <-> sats(A, And(p,q), env)"
161 lemma disj_iff_sats:
162       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
163        ==> (P | Q) <-> sats(A, Or(p,q), env)"
166 lemma iff_iff_sats:
167       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
168        ==> (P <-> Q) <-> sats(A, Iff(p,q), env)"
171 lemma imp_iff_sats:
172       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
173        ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
176 lemma ball_iff_sats:
177       "[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
178        ==> (\<forall>x\<in>A. P(x)) <-> sats(A, Forall(p), env)"
181 lemma bex_iff_sats:
182       "[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
183        ==> (\<exists>x\<in>A. P(x)) <-> sats(A, Exists(p), env)"
186 lemmas FOL_iff_sats =
187         mem_iff_sats equal_iff_sats not_iff_sats conj_iff_sats
188         disj_iff_sats imp_iff_sats iff_iff_sats imp_iff_sats ball_iff_sats
189         bex_iff_sats
192 subsection{*Arity of a Formula: Maximum Free de Bruijn Index*}
194 consts   arity :: "i=>i"
195 primrec
196   "arity(Member(x,y)) = succ(x) \<union> succ(y)"
198   "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
200   "arity(Nand(p,q)) = arity(p) \<union> arity(q)"
202   "arity(Forall(p)) = Arith.pred(arity(p))"
205 lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
206 by (induct_tac p, simp_all)
208 lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)"
211 lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)"
214 lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
217 lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
220 lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
221 by (simp add: Iff_def, blast)
223 lemma arity_Exists [simp]: "arity(Exists(p)) = Arith.pred(arity(p))"
227 lemma arity_sats_iff [rule_format]:
228   "[| p \<in> formula; extra \<in> list(A) |]
229    ==> \<forall>env \<in> list(A).
230            arity(p) \<le> length(env) -->
231            sats(A, p, env @ extra) <-> sats(A, p, env)"
232 apply (induct_tac p)
233 apply (simp_all add: Arith.pred_def nth_append Un_least_lt_iff nat_imp_quasinat
234                 split: split_nat_case, auto)
235 done
237 lemma arity_sats1_iff:
238   "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A);
239       extra \<in> list(A) |]
240    ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
241 apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
242 apply simp
243 done
246 subsection{*Renaming Some de Bruijn Variables*}
248 constdefs incr_var :: "[i,i]=>i"
249     "incr_var(x,nq) == if x<nq then x else succ(x)"
251 lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x"
254 lemma incr_var_le: "nq\<le>x ==> incr_var(x,nq) = succ(x)"
256 apply (blast dest: lt_trans1)
257 done
259 consts   incr_bv :: "i=>i"
260 primrec
261   "incr_bv(Member(x,y)) =
262       (\<lambda>nq \<in> nat. Member (incr_var(x,nq), incr_var(y,nq)))"
264   "incr_bv(Equal(x,y)) =
265       (\<lambda>nq \<in> nat. Equal (incr_var(x,nq), incr_var(y,nq)))"
267   "incr_bv(Nand(p,q)) =
268       (\<lambda>nq \<in> nat. Nand (incr_bv(p)`nq, incr_bv(q)`nq))"
270   "incr_bv(Forall(p)) =
271       (\<lambda>nq \<in> nat. Forall (incr_bv(p) ` succ(nq)))"
274 lemma [TC]: "x \<in> nat ==> incr_var(x,nq) \<in> nat"
277 lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
278 by (induct_tac p, simp_all)
280 text{*Obviously, @{term DPow} is closed under complements and finite
281 intersections and unions.  Needs an inductive lemma to allow two lists of
282 parameters to be combined.*}
284 lemma sats_incr_bv_iff [rule_format]:
285   "[| p \<in> formula; env \<in> list(A); x \<in> A |]
286    ==> \<forall>bvs \<in> list(A).
287            sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) <->
288            sats(A, p, bvs@env)"
289 apply (induct_tac p)
290 apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type)
291 apply (auto simp add: diff_succ not_lt_iff_le)
292 done
295 (*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
296 lemma incr_var_lemma:
297      "[| x \<in> nat; y \<in> nat; nq \<le> x |]
298       ==> succ(x) \<union> incr_var(y,nq) = succ(x \<union> y)"
299 apply (simp add: incr_var_def Ord_Un_if, auto)
300   apply (blast intro: leI)
302  apply (blast intro: le_anti_sym)
303 apply (blast dest: lt_trans2)
304 done
306 lemma incr_And_lemma:
307      "y < x ==> y \<union> succ(x) = succ(x \<union> y)"
308 apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff)
309 apply (blast dest: lt_asym)
310 done
312 lemma arity_incr_bv_lemma [rule_format]:
313   "p \<in> formula
314    ==> \<forall>n \<in> nat. arity (incr_bv(p) ` n) =
315                  (if n < arity(p) then succ(arity(p)) else arity(p))"
316 apply (induct_tac p)
317 apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
318                      succ_Un_distrib [symmetric] incr_var_lt incr_var_le
319                      Un_commute incr_var_lemma Arith.pred_def nat_imp_quasinat
320             split: split_nat_case)
321  txt{*the Forall case reduces to linear arithmetic*}
322  prefer 2
323  apply clarify
324  apply (blast dest: lt_trans1)
325 txt{*left with the And case*}
326 apply safe
327  apply (blast intro: incr_And_lemma lt_trans1)
328 apply (subst incr_And_lemma)
329  apply (blast intro: lt_trans1)
331 done
334 subsection{*Renaming all but the First de Bruijn Variable*}
336 constdefs incr_bv1 :: "i => i"
337     "incr_bv1(p) == incr_bv(p)`1"
340 lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula"
343 (*For renaming all but the bound variable at level 0*)
344 lemma sats_incr_bv1_iff:
345   "[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
346    ==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <->
347        sats(A, p, Cons(x,env))"
348 apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"])
350 done
353   "[| p \<in> formula; n \<in> nat; x \<in> A |]
354    ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
355           length(bvs) = n -->
356           sats(A, iterates(incr_bv1, n, p), Cons(x, bvs@env)) <->
357           sats(A, p, Cons(x,env))"
358 apply (induct_tac n, simp, clarify)
359 apply (erule list.cases)
361 done
364 lemma arity_incr_bv1_eq:
365   "p \<in> formula
366    ==> arity(incr_bv1(p)) =
367         (if 1 < arity(p) then succ(arity(p)) else arity(p))"
368 apply (insert arity_incr_bv_lemma [of p 1])
370 done
372 lemma arity_iterates_incr_bv1_eq:
373   "[| p \<in> formula; n \<in> nat |]
374    ==> arity(incr_bv1^n(p)) =
375          (if 1 < arity(p) then n #+ arity(p) else arity(p))"
376 apply (induct_tac n)
379 apply (blast intro: le_trans add_le_self2 arity_type)
380 done
384 subsection{*Definable Powerset*}
386 text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*}
387 constdefs DPow :: "i => i"
388   "DPow(A) == {X \<in> Pow(A).
389                \<exists>env \<in> list(A). \<exists>p \<in> formula.
390                  arity(p) \<le> succ(length(env)) &
391                  X = {x\<in>A. sats(A, p, Cons(x,env))}}"
393 lemma DPowI:
394   "[|env \<in> list(A);  p \<in> formula;  arity(p) \<le> succ(length(env))|]
395    ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
396 by (simp add: DPow_def, blast)
398 text{*With this rule we can specify @{term p} later.*}
399 lemma DPowI2 [rule_format]:
400   "[|\<forall>x\<in>A. P(x) <-> sats(A, p, Cons(x,env));
401      env \<in> list(A);  p \<in> formula;  arity(p) \<le> succ(length(env))|]
402    ==> {x\<in>A. P(x)} \<in> DPow(A)"
403 by (simp add: DPow_def, blast)
405 lemma DPowD:
406   "X \<in> DPow(A)
407    ==> X <= A &
408        (\<exists>env \<in> list(A).
409         \<exists>p \<in> formula. arity(p) \<le> succ(length(env)) &
410                       X = {x\<in>A. sats(A, p, Cons(x,env))})"
413 lemmas DPow_imp_subset = DPowD [THEN conjunct1]
415 (*Kunen's Lemma VI 1.2*)
416 lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |]
417        ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
418 by (blast intro: DPowI)
420 lemma DPow_subset_Pow: "DPow(A) <= Pow(A)"
421 by (simp add: DPow_def, blast)
423 lemma empty_in_DPow: "0 \<in> DPow(A)"
425 apply (rule_tac x=Nil in bexI)
426  apply (rule_tac x="Neg(Equal(0,0))" in bexI)
427   apply (auto simp add: Un_least_lt_iff)
428 done
430 lemma Compl_in_DPow: "X \<in> DPow(A) ==> (A-X) \<in> DPow(A)"
431 apply (simp add: DPow_def, clarify, auto)
432 apply (rule bexI)
433  apply (rule_tac x="Neg(p)" in bexI)
434   apply auto
435 done
437 lemma Int_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Int Y \<in> DPow(A)"
438 apply (simp add: DPow_def, auto)
439 apply (rename_tac envp p envq q)
440 apply (rule_tac x="envp@envq" in bexI)
441  apply (rule_tac x="And(p, iterates(incr_bv1,length(envp),q))" in bexI)
442   apply typecheck
443 apply (rule conjI)
444 (*finally check the arity!*)
445  apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)
446  apply (force intro: add_le_self le_trans)
448 done
450 lemma Un_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Un Y \<in> DPow(A)"
451 apply (subgoal_tac "X Un Y = A - ((A-X) Int (A-Y))")
452 apply (simp add: Int_in_DPow Compl_in_DPow)
453 apply (simp add: DPow_def, blast)
454 done
456 lemma singleton_in_DPow: "a \<in> A ==> {a} \<in> DPow(A)"
458 apply (rule_tac x="Cons(a,Nil)" in bexI)
459  apply (rule_tac x="Equal(0,1)" in bexI)
460   apply typecheck
461 apply (force simp add: succ_Un_distrib [symmetric])
462 done
464 lemma cons_in_DPow: "[| a \<in> A; X \<in> DPow(A) |] ==> cons(a,X) \<in> DPow(A)"
465 apply (rule cons_eq [THEN subst])
466 apply (blast intro: singleton_in_DPow Un_in_DPow)
467 done
469 (*Part of Lemma 1.3*)
470 lemma Fin_into_DPow: "X \<in> Fin(A) ==> X \<in> DPow(A)"
471 apply (erule Fin.induct)
472  apply (rule empty_in_DPow)
473 apply (blast intro: cons_in_DPow)
474 done
476 text{*@{term DPow} is not monotonic.  For example, let @{term A} be some
477 non-constructible set of natural numbers, and let @{term B} be @{term nat}.
478 Then @{term "A<=B"} and obviously @{term "A \<in> DPow(A)"} but @{term "A ~:
479 DPow(B)"}.*}
481 (*This may be true but the proof looks difficult, requiring relativization
482 lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
483 apply (rule equalityI, safe)
484 oops
485 *)
487 lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)"
488 by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)
490 lemma Finite_DPow_eq_Pow: "Finite(A) ==> DPow(A) = Pow(A)"
491 apply (rule equalityI)
492 apply (rule DPow_subset_Pow)
493 apply (erule Finite_Pow_subset_Pow)
494 done
497 subsection{*Internalized Formulas for the Ordinals*}
499 text{*The @{text sats} theorems below differ from the usual form in that they
500 include an element of absoluteness.  That is, they relate internalized
501 formulas to real concepts such as the subset relation, rather than to the
502 relativized concepts defined in theory @{text Relative}.  This lets us prove
503 the theorem as @{text Ords_in_DPow} without first having to instantiate the
504 locale @{text M_trivial}.  Note that the present theory does not even take
505 @{text Relative} as a parent.*}
507 subsubsection{*The subset relation*}
509 constdefs subset_fm :: "[i,i]=>i"
510     "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
512 lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
515 lemma arity_subset_fm [simp]:
516      "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
517 by (simp add: subset_fm_def succ_Un_distrib [symmetric])
519 lemma sats_subset_fm [simp]:
520    "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
521     ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
522 apply (frule lt_length_in_nat, assumption)
523 apply (simp add: subset_fm_def Transset_def)
524 apply (blast intro: nth_type)
525 done
527 subsubsection{*Transitive sets*}
529 constdefs transset_fm :: "i=>i"
530    "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
532 lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
535 lemma arity_transset_fm [simp]:
536      "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
537 by (simp add: transset_fm_def succ_Un_distrib [symmetric])
539 lemma sats_transset_fm [simp]:
540    "[|x < length(env); env \<in> list(A); Transset(A)|]
541     ==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
542 apply (frule lt_nat_in_nat, erule length_type)
543 apply (simp add: transset_fm_def Transset_def)
544 apply (blast intro: nth_type)
545 done
547 subsubsection{*Ordinals*}
549 constdefs ordinal_fm :: "i=>i"
550    "ordinal_fm(x) ==
551       And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
553 lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
556 lemma arity_ordinal_fm [simp]:
557      "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
558 by (simp add: ordinal_fm_def succ_Un_distrib [symmetric])
560 lemma sats_ordinal_fm:
561    "[|x < length(env); env \<in> list(A); Transset(A)|]
562     ==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
563 apply (frule lt_nat_in_nat, erule length_type)
564 apply (simp add: ordinal_fm_def Ord_def Transset_def)
565 apply (blast intro: nth_type)
566 done
568 text{*The subset consisting of the ordinals is definable.  Essential lemma for
569 @{text Ord_in_Lset}.  This result is the objective of the present subsection.*}
570 theorem Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
571 apply (simp add: DPow_def Collect_subset)
572 apply (rule_tac x=Nil in bexI)
573  apply (rule_tac x="ordinal_fm(0)" in bexI)
575 done
578 subsection{* Constant Lset: Levels of the Constructible Universe *}
580 constdefs
581   Lset :: "i=>i"
582     "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
584   L :: "i=>o" --{*Kunen's definition VI 1.5, page 167*}
585     "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
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)
591 lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)";
592 by (subst Lset, blast)
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
599 subsubsection{* Transitivity *}
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
608 lemma Transset_subset_DPow: "Transset(A) ==> A <= DPow(A)"
609 apply clarify
611 apply (blast intro: elem_subset_in_DPow)
612 done
614 lemma Transset_DPow: "Transset(A) ==> Transset(DPow(A))"
616 apply (blast intro: elem_subset_in_DPow dest: DPowD)
617 done
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
626 lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) ==> a \<subseteq> Lset(i)"
627 apply (insert Transset_Lset)
629 done
631 subsubsection{* Monotonicity *}
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
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
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])
656 subsubsection{* 0, successor and limit equations for Lset *}
658 lemma Lset_0 [simp]: "Lset(0) = 0"
659 by (subst Lset, blast)
661 lemma Lset_succ_subset1: "DPow(Lset(i)) <= Lset(succ(i))"
662 by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper])
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
675 lemma Lset_succ: "Lset(succ(i)) = DPow(Lset(i))"
676 by (intro equalityI Lset_succ_subset1 Lset_succ_subset2)
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
691 subsubsection{* Lset applied to Limit ordinals *}
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)
697 lemma lt_LsetI: "[| a: Lset(j);  j<i |] ==> a \<in> Lset(i)"
698 by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
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
711 subsubsection{* Basic closure properties *}
713 lemma zero_in_Lset: "y:x ==> 0 \<in> Lset(x)"
714 by (subst Lset, blast intro: empty_in_DPow)
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
723 subsection{*Constructible Ordinals: Kunen's VI 1.9 (b)*}
725 lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
726 apply (erule trans_induct3)
727   apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)
728 txt{*The successor case remains.*}
729 apply (rule equalityI)
730 txt{*First inclusion*}
731  apply clarify
732  apply (erule Ord_linear_lt, assumption)
733    apply (blast dest: DPow_imp_subset ltD notE [OF notin_Lset])
734   apply blast
735  apply (blast dest: ltD)
736 txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*}
737 apply auto
738 txt{*Key case: *}
739   apply (erule subst, rule Ords_in_DPow [OF Transset_Lset])
740  apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE)
741 apply (blast intro: Ord_in_Ord)
742 done
745 lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)"
746 by (subst Ords_of_Lset_eq [symmetric], assumption, fast)
748 lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))"
750 apply (subst Ords_of_Lset_eq [symmetric], assumption,
751        rule Ords_in_DPow [OF Transset_Lset])
752 done
754 lemma Ord_in_L: "Ord(i) ==> L(i)"
755 by (simp add: L_def, blast intro: Ord_in_Lset)
757 subsubsection{* Unions *}
759 lemma Union_in_Lset:
760      "X \<in> Lset(i) ==> Union(X) \<in> Lset(succ(i))"
761 apply (insert Transset_Lset)
762 apply (rule LsetI [OF succI1])
763 apply (simp add: Transset_def DPow_def)
764 apply (intro conjI, blast)
765 txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *}
766 apply (rule_tac x="Cons(X,Nil)" in bexI)
767  apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI)
768   apply typecheck
769 apply (simp add: succ_Un_distrib [symmetric], blast)
770 done
772 theorem Union_in_L: "L(X) ==> L(Union(X))"
773 by (simp add: L_def, blast dest: Union_in_Lset)
775 subsubsection{* Finite sets and ordered pairs *}
777 lemma singleton_in_Lset: "a: Lset(i) ==> {a} \<in> Lset(succ(i))"
778 by (simp add: Lset_succ singleton_in_DPow)
780 lemma doubleton_in_Lset:
781      "[| a: Lset(i);  b: Lset(i) |] ==> {a,b} \<in> Lset(succ(i))"
782 by (simp add: Lset_succ empty_in_DPow cons_in_DPow)
784 lemma Pair_in_Lset:
785     "[| a: Lset(i);  b: Lset(i); Ord(i) |] ==> <a,b> \<in> Lset(succ(succ(i)))"
786 apply (unfold Pair_def)
787 apply (blast intro: doubleton_in_Lset)
788 done
790 lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
791 lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
793 text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
794 lemma doubleton_in_LLimit:
795     "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> {a,b} \<in> Lset(i)"
796 apply (erule Limit_LsetE, assumption)
797 apply (erule Limit_LsetE, assumption)
798 apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
799                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
800 done
802 theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
803 apply (simp add: L_def, clarify)
804 apply (drule Ord2_imp_greater_Limit, assumption)
805 apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord)
806 done
808 lemma Pair_in_LLimit:
809     "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> <a,b> \<in> Lset(i)"
810 txt{*Infer that a, b occur at ordinals x,xa < i.*}
811 apply (erule Limit_LsetE, assumption)
812 apply (erule Limit_LsetE, assumption)
813 txt{*Infer that succ(succ(x Un xa)) < i *}
814 apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset]
815                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
816 done
820 text{*The rank function for the constructible universe*}
821 constdefs
822   lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
823     "lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
825 lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
826 by (simp add: L_def, blast)
828 lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)"
831 lemma Ord_lrank [simp]: "Ord(lrank(a))"
834 lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) --> lrank(x) < i"
835 apply (erule trans_induct3)
836   apply simp
837  apply (simp only: lrank_def)
838  apply (blast intro: Least_le)
840 apply (blast intro: ltI Limit_is_Ord lt_trans)
841 done
843 text{*Kunen's VI 1.8.  The proof is much harder than the text would
844 suggest.  For a start, it needs the previous lemma, which is proved by
845 induction.*}
846 lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i"
847 apply (simp add: L_def, auto)
848  apply (blast intro: Lset_lrank_lt)
849  apply (unfold lrank_def)
850 apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD])
851 apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption)
852 apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
853 done
855 lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)"
858 text{*Kunen's VI 1.9 (a)*}
859 lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
860 apply (unfold lrank_def)
861 apply (rule Least_equality)
862   apply (erule Ord_in_Lset)
863  apply assumption
864 apply (insert notin_Lset [of i])
865 apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
866 done
869 text{*This is lrank(lrank(a)) = lrank(a) *}
870 declare Ord_lrank [THEN lrank_of_Ord, simp]
872 text{*Kunen's VI 1.10 *}
873 lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
874 apply (simp add: Lset_succ DPow_def)
875 apply (rule_tac x=Nil in bexI)
876  apply (rule_tac x="Equal(0,0)" in bexI)
877 apply auto
878 done
880 lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i"
881 apply (unfold lrank_def)
882 apply (rule Least_equality)
883   apply (rule Lset_in_Lset_succ)
884  apply assumption
885 apply clarify
886 apply (subgoal_tac "Lset(succ(ia)) <= Lset(i)")
887  apply (blast dest: mem_irrefl)
888 apply (blast intro!: le_imp_subset Lset_mono)
889 done
891 text{*Kunen's VI 1.11 *}
892 lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
893 apply (erule trans_induct)
894 apply (subst Lset)
895 apply (subst Vset)
896 apply (rule UN_mono [OF subset_refl])
897 apply (rule subset_trans [OF DPow_subset_Pow])
898 apply (rule Pow_mono, blast)
899 done
901 text{*Kunen's VI 1.12 *}
902 lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
903 apply (erule nat_induct)
905 apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)
906 done
908 text{*Every set of constructible sets is included in some @{term Lset}*}
909 lemma subset_Lset:
910      "(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)"
911 by (rule_tac x = "\<Union>x\<in>A. succ(lrank(x))" in exI, force)
913 lemma subset_LsetE:
914      "[|\<forall>x\<in>A. L(x);
915         !!i. [|Ord(i); A \<subseteq> Lset(i)|] ==> P|]
916       ==> P"
917 by (blast dest: subset_Lset)
919 subsubsection{*For L to satisfy the Powerset axiom *}
921 lemma LPow_env_typing:
922     "[| y \<in> Lset(i); Ord(i); y \<subseteq> X |]
923      ==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))"
924 by (auto intro: L_I iff: Lset_succ_lrank_iff)
926 lemma LPow_in_Lset:
927      "[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"
928 apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI)
929 apply simp
930 apply (rule LsetI [OF succI1])
932 apply (intro conjI, clarify)
933  apply (rule_tac a=x in UN_I, simp+)
934 txt{*Now to create the formula @{term "y \<subseteq> X"} *}
935 apply (rule_tac x="Cons(X,Nil)" in bexI)
936  apply (rule_tac x="subset_fm(0,1)" in bexI)
937   apply typecheck
938  apply (rule conjI)
939 apply (simp add: succ_Un_distrib [symmetric])
940 apply (rule equality_iffI)
941 apply (simp add: Transset_UN [OF Transset_Lset] LPow_env_typing)
942 apply (auto intro: L_I iff: Lset_succ_lrank_iff)
943 done
945 theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
946 by (blast intro: L_I dest: L_D LPow_in_Lset)
949 subsection{*Eliminating @{term arity} from the Definition of @{term Lset}*}
951 lemma nth_zero_eq_0: "n \<in> nat ==> nth(n,[0]) = 0"
952 by (induct_tac n, auto)
954 lemma sats_app_0_iff [rule_format]:
955   "[| p \<in> formula; 0 \<in> A |]
956    ==> \<forall>env \<in> list(A). sats(A,p, env@[0]) <-> sats(A,p,env)"
957 apply (induct_tac p)
958 apply (simp_all del: app_Cons add: app_Cons [symmetric]
959 		add: nth_zero_eq_0 nth_append not_lt_iff_le nth_eq_0)
960 done
962 lemma sats_app_zeroes_iff:
963   "[| p \<in> formula; 0 \<in> A; env \<in> list(A); n \<in> nat |]
964    ==> sats(A,p,env @ repeat(0,n)) <-> sats(A,p,env)"
965 apply (induct_tac n, simp)
966 apply (simp del: repeat.simps
967             add: repeat_succ_app sats_app_0_iff app_assoc [symmetric])
968 done
970 lemma exists_bigger_env:
971   "[| p \<in> formula; 0 \<in> A; env \<in> list(A) |]
972    ==> \<exists>env' \<in> list(A). arity(p) \<le> succ(length(env')) &
973               (\<forall>a\<in>A. sats(A,p,Cons(a,env')) <-> sats(A,p,Cons(a,env)))"
974 apply (rule_tac x="env @ repeat(0,arity(p))" in bexI)
975 apply (simp del: app_Cons add: app_Cons [symmetric]
977 done
980 text{*A simpler version of @{term DPow}: no arity check!*}
981 constdefs DPow' :: "i => i"
982   "DPow'(A) == {X \<in> Pow(A).
983                 \<exists>env \<in> list(A). \<exists>p \<in> formula.
984                     X = {x\<in>A. sats(A, p, Cons(x,env))}}"
986 lemma DPow_subset_DPow': "DPow(A) <= DPow'(A)";
987 by (simp add: DPow_def DPow'_def, blast)
989 lemma DPow'_0: "DPow'(0) = {0}"
990 by (auto simp add: DPow'_def)
992 lemma DPow'_subset_DPow: "0 \<in> A ==> DPow'(A) \<subseteq> DPow(A)"
993 apply (auto simp add: DPow'_def DPow_def)
994 apply (frule exists_bigger_env, assumption+, force)
995 done
997 lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)"
998 apply (drule Transset_0_disj)
999 apply (erule disjE)
1000  apply (simp add: DPow'_0 Finite_DPow_eq_Pow)
1001 apply (rule equalityI)
1002  apply (rule DPow_subset_DPow')
1003 apply (erule DPow'_subset_DPow)
1004 done
1006 text{*And thus we can relativize @{term Lset} without bothering with
1007       @{term arity} and @{term length}*}
1008 lemma Lset_eq_transrec_DPow': "Lset(i) = transrec(i, %x f. \<Union>y\<in>x. DPow'(f`y))"
1009 apply (rule_tac a=i in eps_induct)
1010 apply (subst Lset)
1011 apply (subst transrec)
1012 apply (simp only: DPow_eq_DPow' [OF Transset_Lset], simp)
1013 done
1015 text{*With this rule we can specify @{term p} later and don't worry about
1016       arities at all!*}
1017 lemma DPow_LsetI [rule_format]:
1018   "[|\<forall>x\<in>Lset(i). P(x) <-> sats(Lset(i), p, Cons(x,env));
1019      env \<in> list(Lset(i));  p \<in> formula|]
1020    ==> {x\<in>Lset(i). P(x)} \<in> DPow(Lset(i))"
1021 by (simp add: DPow_eq_DPow' [OF Transset_Lset] DPow'_def, blast)
1023 end