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