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