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