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