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