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