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