src/ZF/Constructible/Relative.thy
 author paulson Fri Jun 28 11:25:46 2002 +0200 (2002-06-28) changeset 13254 5146ccaedf42 parent 13251 74cb2af8811e child 13268 240509babf00 permissions -rw-r--r--
class quantifiers (some)
absoluteness and closure for WFrec-defined functions
     1 header {*Relativization and Absoluteness*}

     2

     3 theory Relative = Main:

     4

     5 subsection{* Relativized versions of standard set-theoretic concepts *}

     6

     7 constdefs

     8   empty :: "[i=>o,i] => o"

     9     "empty(M,z) == \<forall>x[M]. x \<notin> z"

    10

    11   subset :: "[i=>o,i,i] => o"

    12     "subset(M,A,B) == \<forall>x\<in>A. M(x) --> x \<in> B"

    13

    14   upair :: "[i=>o,i,i,i] => o"

    15     "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x\<in>z. M(x) --> x = a | x = b)"

    16

    17   pair :: "[i=>o,i,i,i] => o"

    18     "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) &

    19                           (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"

    20

    21   union :: "[i=>o,i,i,i] => o"

    22     "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"

    23

    24   successor :: "[i=>o,i,i] => o"

    25     "successor(M,a,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,a,z)"

    26

    27   powerset :: "[i=>o,i,i] => o"

    28     "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"

    29

    30   inter :: "[i=>o,i,i,i] => o"

    31     "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"

    32

    33   setdiff :: "[i=>o,i,i,i] => o"

    34     "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"

    35

    36   big_union :: "[i=>o,i,i] => o"

    37     "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y)"

    38

    39   big_inter :: "[i=>o,i,i] => o"

    40     "big_inter(M,A,z) ==

    41              (A=0 --> z=0) &

    42 	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y)))"

    43

    44   cartprod :: "[i=>o,i,i,i] => o"

    45     "cartprod(M,A,B,z) ==

    46 	\<forall>u[M]. u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u)))"

    47

    48   is_converse :: "[i=>o,i,i] => o"

    49     "is_converse(M,r,z) ==

    50 	\<forall>x. M(x) -->

    51             (x \<in> z <->

    52              (\<exists>w\<in>r. M(w) &

    53               (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x))))"

    54

    55   pre_image :: "[i=>o,i,i,i] => o"

    56     "pre_image(M,r,A,z) ==

    57 	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y\<in>A. M(y) & pair(M,x,y,w))))"

    58

    59   is_domain :: "[i=>o,i,i] => o"

    60     "is_domain(M,r,z) ==

    61 	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y. M(y) & pair(M,x,y,w))))"

    62

    63   image :: "[i=>o,i,i,i] => o"

    64     "image(M,r,A,z) ==

    65         \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x\<in>A. M(x) & pair(M,x,y,w))))"

    66

    67   is_range :: "[i=>o,i,i] => o"

    68     --{*the cleaner

    69       @{term "\<exists>r'. M(r') & is_converse(M,r,r') & is_domain(M,r',z)"}

    70       unfortunately needs an instance of separation in order to prove

    71         @{term "M(converse(r))"}.*}

    72     "is_range(M,r,z) ==

    73 	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x. M(x) & pair(M,x,y,w))))"

    74

    75   is_field :: "[i=>o,i,i] => o"

    76     "is_field(M,r,z) ==

    77 	\<exists>dr. M(dr) & is_domain(M,r,dr) &

    78             (\<exists>rr. M(rr) & is_range(M,r,rr) & union(M,dr,rr,z))"

    79

    80   is_relation :: "[i=>o,i] => o"

    81     "is_relation(M,r) ==

    82         (\<forall>z\<in>r. M(z) --> (\<exists>x y. M(x) & M(y) & pair(M,x,y,z)))"

    83

    84   is_function :: "[i=>o,i] => o"

    85     "is_function(M,r) ==

    86 	(\<forall>x y y' p p'. M(x) --> M(y) --> M(y') --> M(p) --> M(p') -->

    87                       pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r -->

    88                       y=y')"

    89

    90   fun_apply :: "[i=>o,i,i,i] => o"

    91     "fun_apply(M,f,x,y) ==

    92 	(\<forall>y'. M(y') --> ((\<exists>u\<in>f. M(u) & pair(M,x,y',u)) <-> y=y'))"

    93

    94   typed_function :: "[i=>o,i,i,i] => o"

    95     "typed_function(M,A,B,r) ==

    96         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &

    97         (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"

    98

    99   composition :: "[i=>o,i,i,i] => o"

   100     "composition(M,r,s,t) ==

   101         \<forall>p. M(p) --> (p \<in> t <->

   102                       (\<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) &

   103                            p = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))))"

   104

   105

   106   injection :: "[i=>o,i,i,i] => o"

   107     "injection(M,A,B,f) ==

   108 	typed_function(M,A,B,f) &

   109         (\<forall>x x' y p p'. M(x) --> M(x') --> M(y) --> M(p) --> M(p') -->

   110                       pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f -->

   111                       x=x')"

   112

   113   surjection :: "[i=>o,i,i,i] => o"

   114     "surjection(M,A,B,f) ==

   115         typed_function(M,A,B,f) &

   116         (\<forall>y\<in>B. M(y) --> (\<exists>x\<in>A. M(x) & fun_apply(M,f,x,y)))"

   117

   118   bijection :: "[i=>o,i,i,i] => o"

   119     "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"

   120

   121   restriction :: "[i=>o,i,i,i] => o"

   122     "restriction(M,r,A,z) ==

   123 	\<forall>x. M(x) -->

   124             (x \<in> z <->

   125              (x \<in> r & (\<exists>u\<in>A. M(u) & (\<exists>v. M(v) & pair(M,u,v,x)))))"

   126

   127   transitive_set :: "[i=>o,i] => o"

   128     "transitive_set(M,a) == \<forall>x\<in>a. M(x) --> subset(M,x,a)"

   129

   130   ordinal :: "[i=>o,i] => o"

   131      --{*an ordinal is a transitive set of transitive sets*}

   132     "ordinal(M,a) == transitive_set(M,a) & (\<forall>x\<in>a. M(x) --> transitive_set(M,x))"

   133

   134   limit_ordinal :: "[i=>o,i] => o"

   135     --{*a limit ordinal is a non-empty, successor-closed ordinal*}

   136     "limit_ordinal(M,a) ==

   137 	ordinal(M,a) & ~ empty(M,a) &

   138         (\<forall>x\<in>a. M(x) --> (\<exists>y\<in>a. M(y) & successor(M,x,y)))"

   139

   140   successor_ordinal :: "[i=>o,i] => o"

   141     --{*a successor ordinal is any ordinal that is neither empty nor limit*}

   142     "successor_ordinal(M,a) ==

   143 	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"

   144

   145   finite_ordinal :: "[i=>o,i] => o"

   146     --{*an ordinal is finite if neither it nor any of its elements are limit*}

   147     "finite_ordinal(M,a) ==

   148 	ordinal(M,a) & ~ limit_ordinal(M,a) &

   149         (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"

   150

   151   omega :: "[i=>o,i] => o"

   152     --{*omega is a limit ordinal none of whose elements are limit*}

   153     "omega(M,a) == limit_ordinal(M,a) & (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"

   154

   155   number1 :: "[i=>o,i] => o"

   156     "number1(M,a) == (\<exists>x. M(x) & empty(M,x) & successor(M,x,a))"

   157

   158   number2 :: "[i=>o,i] => o"

   159     "number2(M,a) == (\<exists>x. M(x) & number1(M,x) & successor(M,x,a))"

   160

   161   number3 :: "[i=>o,i] => o"

   162     "number3(M,a) == (\<exists>x. M(x) & number2(M,x) & successor(M,x,a))"

   163

   164

   165 subsection {*The relativized ZF axioms*}

   166 constdefs

   167

   168   extensionality :: "(i=>o) => o"

   169     "extensionality(M) ==

   170 	\<forall>x y. M(x) --> M(y) --> (\<forall>z. M(z) --> (z \<in> x <-> z \<in> y)) --> x=y"

   171

   172   separation :: "[i=>o, i=>o] => o"

   173     --{*Big problem: the formula @{text P} should only involve parameters

   174         belonging to @{text M}.  Don't see how to enforce that.*}

   175     "separation(M,P) ==

   176 	\<forall>z. M(z) --> (\<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x))))"

   177

   178   upair_ax :: "(i=>o) => o"

   179     "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z. M(z) & upair(M,x,y,z))"

   180

   181   Union_ax :: "(i=>o) => o"

   182     "Union_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & big_union(M,x,z))"

   183

   184   power_ax :: "(i=>o) => o"

   185     "power_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & powerset(M,x,z))"

   186

   187   univalent :: "[i=>o, i, [i,i]=>o] => o"

   188     "univalent(M,A,P) ==

   189 	(\<forall>x\<in>A. M(x) --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"

   190

   191   replacement :: "[i=>o, [i,i]=>o] => o"

   192     "replacement(M,P) ==

   193       \<forall>A. M(A) --> univalent(M,A,P) -->

   194       (\<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y)))"

   195

   196   strong_replacement :: "[i=>o, [i,i]=>o] => o"

   197     "strong_replacement(M,P) ==

   198       \<forall>A. M(A) --> univalent(M,A,P) -->

   199       (\<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b)))))"

   200

   201   foundation_ax :: "(i=>o) => o"

   202     "foundation_ax(M) ==

   203 	\<forall>x. M(x) --> (\<exists>y\<in>x. M(y))

   204                  --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & z \<in> y))"

   205

   206

   207 subsection{*A trivial consistency proof for $V_\omega$ *}

   208

   209 text{*We prove that $V_\omega$

   210       (or @{text univ} in Isabelle) satisfies some ZF axioms.

   211      Kunen, Theorem IV 3.13, page 123.*}

   212

   213 lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"

   214 apply (insert Transset_univ [OF Transset_0])

   215 apply (simp add: Transset_def, blast)

   216 done

   217

   218 lemma univ0_Ball_abs [simp]:

   219      "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))"

   220 by (blast intro: univ0_downwards_mem)

   221

   222 lemma univ0_Bex_abs [simp]:

   223      "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))"

   224 by (blast intro: univ0_downwards_mem)

   225

   226 text{*Congruence rule for separation: can assume the variable is in @{text M}*}

   227 lemma separation_cong [cong]:

   228      "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"

   229 by (simp add: separation_def)

   230

   231 text{*Congruence rules for replacement*}

   232 lemma univalent_cong [cong]:

   233      "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]

   234       ==> univalent(M,A,P) <-> univalent(M,A',P')"

   235 by (simp add: univalent_def)

   236

   237 lemma strong_replacement_cong [cong]:

   238      "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]

   239       ==> strong_replacement(M,P) <-> strong_replacement(M,P')"

   240 by (simp add: strong_replacement_def)

   241

   242 text{*The extensionality axiom*}

   243 lemma "extensionality(\<lambda>x. x \<in> univ(0))"

   244 apply (simp add: extensionality_def)

   245 apply (blast intro: univ0_downwards_mem)

   246 done

   247

   248 text{*The separation axiom requires some lemmas*}

   249 lemma Collect_in_Vfrom:

   250      "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"

   251 apply (drule Transset_Vfrom)

   252 apply (rule subset_mem_Vfrom)

   253 apply (unfold Transset_def, blast)

   254 done

   255

   256 lemma Collect_in_VLimit:

   257      "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]

   258       ==> Collect(X,P) \<in> Vfrom(A,i)"

   259 apply (rule Limit_VfromE, assumption+)

   260 apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)

   261 done

   262

   263 lemma Collect_in_univ:

   264      "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"

   265 by (simp add: univ_def Collect_in_VLimit Limit_nat)

   266

   267 lemma "separation(\<lambda>x. x \<in> univ(0), P)"

   268 apply (simp add: separation_def)

   269 apply (blast intro: Collect_in_univ Transset_0)

   270 done

   271

   272 text{*Unordered pairing axiom*}

   273 lemma "upair_ax(\<lambda>x. x \<in> univ(0))"

   274 apply (simp add: upair_ax_def upair_def)

   275 apply (blast intro: doubleton_in_univ)

   276 done

   277

   278 text{*Union axiom*}

   279 lemma "Union_ax(\<lambda>x. x \<in> univ(0))"

   280 apply (simp add: Union_ax_def big_union_def)

   281 apply (blast intro: Union_in_univ Transset_0 univ0_downwards_mem)

   282 done

   283

   284 text{*Powerset axiom*}

   285

   286 lemma Pow_in_univ:

   287      "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"

   288 apply (simp add: univ_def Pow_in_VLimit Limit_nat)

   289 done

   290

   291 lemma "power_ax(\<lambda>x. x \<in> univ(0))"

   292 apply (simp add: power_ax_def powerset_def subset_def)

   293 apply (blast intro: Pow_in_univ Transset_0 univ0_downwards_mem)

   294 done

   295

   296 text{*Foundation axiom*}

   297 lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"

   298 apply (simp add: foundation_ax_def, clarify)

   299 apply (cut_tac A=x in foundation, blast)

   300 done

   301

   302 lemma "replacement(\<lambda>x. x \<in> univ(0), P)"

   303 apply (simp add: replacement_def, clarify)

   304 oops

   305 text{*no idea: maybe prove by induction on the rank of A?*}

   306

   307 text{*Still missing: Replacement, Choice*}

   308

   309 subsection{*lemmas needed to reduce some set constructions to instances

   310       of Separation*}

   311

   312 lemma image_iff_Collect: "r  A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"

   313 apply (rule equalityI, auto)

   314 apply (simp add: Pair_def, blast)

   315 done

   316

   317 lemma vimage_iff_Collect:

   318      "r - A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"

   319 apply (rule equalityI, auto)

   320 apply (simp add: Pair_def, blast)

   321 done

   322

   323 text{*These two lemmas lets us prove @{text domain_closed} and

   324       @{text range_closed} without new instances of separation*}

   325

   326 lemma domain_eq_vimage: "domain(r) = r - Union(Union(r))"

   327 apply (rule equalityI, auto)

   328 apply (rule vimageI, assumption)

   329 apply (simp add: Pair_def, blast)

   330 done

   331

   332 lemma range_eq_image: "range(r) = r  Union(Union(r))"

   333 apply (rule equalityI, auto)

   334 apply (rule imageI, assumption)

   335 apply (simp add: Pair_def, blast)

   336 done

   337

   338 lemma replacementD:

   339     "[| replacement(M,P); M(A);  univalent(M,A,P) |]

   340      ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y))"

   341 by (simp add: replacement_def)

   342

   343 lemma strong_replacementD:

   344     "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]

   345      ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b))))"

   346 by (simp add: strong_replacement_def)

   347

   348 lemma separationD:

   349     "[| separation(M,P); M(z) |]

   350      ==> \<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x)))"

   351 by (simp add: separation_def)

   352

   353

   354 text{*More constants, for order types*}

   355 constdefs

   356

   357   order_isomorphism :: "[i=>o,i,i,i,i,i] => o"

   358     "order_isomorphism(M,A,r,B,s,f) ==

   359         bijection(M,A,B,f) &

   360         (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>p fx fy q.

   361             M(x) --> M(y) --> M(p) --> M(fx) --> M(fy) --> M(q) -->

   362             pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->

   363             pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))"

   364

   365

   366   pred_set :: "[i=>o,i,i,i,i] => o"

   367     "pred_set(M,A,x,r,B) ==

   368 	\<forall>y. M(y) --> (y \<in> B <-> (\<exists>p\<in>r. M(p) & y \<in> A & pair(M,y,x,p)))"

   369

   370   membership :: "[i=>o,i,i] => o" --{*membership relation*}

   371     "membership(M,A,r) ==

   372 	\<forall>p. M(p) -->

   373              (p \<in> r <-> (\<exists>x\<in>A. \<exists>y\<in>A. M(x) & M(y) & x\<in>y & pair(M,x,y,p)))"

   374

   375

   376 subsection{*Absoluteness for a transitive class model*}

   377

   378 text{*The class M is assumed to be transitive and to satisfy some

   379       relativized ZF axioms*}

   380 locale M_axioms =

   381   fixes M

   382   assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"

   383       and nonempty [simp]:  "M(0)"

   384       and upair_ax:	    "upair_ax(M)"

   385       and Union_ax:	    "Union_ax(M)"

   386       and power_ax:         "power_ax(M)"

   387       and replacement:      "replacement(M,P)"

   388       and M_nat:            "M(nat)"   (*i.e. the axiom of infinity*)

   389   and Inter_separation:

   390      "M(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. M(y) --> x\<in>y)"

   391   and cartprod_separation:

   392      "[| M(A); M(B) |]

   393       ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. M(x) & M(y) & pair(M,x,y,z))"

   394   and image_separation:

   395      "[| M(A); M(r) |]

   396       ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & (\<exists>x\<in>A. M(x) & pair(M,x,y,p)))"

   397   and vimage_separation:

   398      "[| M(A); M(r) |]

   399       ==> separation(M, \<lambda>x. \<exists>p\<in>r. M(p) & (\<exists>y\<in>A. M(x) & pair(M,x,y,p)))"

   400   and converse_separation:

   401      "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r.

   402                     M(p) & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"

   403   and restrict_separation:

   404      "M(A)

   405       ==> separation(M, \<lambda>z. \<exists>x\<in>A. M(x) & (\<exists>y. M(y) & pair(M,x,y,z)))"

   406   and comp_separation:

   407      "[| M(r); M(s) |]

   408       ==> separation(M, \<lambda>xz. \<exists>x y z. M(x) & M(y) & M(z) &

   409 			   (\<exists>xy\<in>s. \<exists>yz\<in>r. M(xy) & M(yz) &

   410 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"

   411   and pred_separation:

   412      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"

   413   and Memrel_separation:

   414      "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) & x \<in> y)"

   415   and obase_separation:

   416      --{*part of the order type formalization*}

   417      "[| M(A); M(r) |]

   418       ==> separation(M, \<lambda>a. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &

   419 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &

   420 	     order_isomorphism(M,par,r,x,mx,g))"

   421   and well_ord_iso_separation:

   422      "[| M(A); M(f); M(r) |]

   423       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) & (\<exists>p. M(p) &

   424 		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"

   425   and obase_equals_separation:

   426      "[| M(A); M(r) |]

   427       ==> separation

   428       (M, \<lambda>x. x\<in>A --> ~(\<exists>y. M(y) & (\<exists>g. M(g) &

   429 	      ordinal(M,y) & (\<exists>my pxr. M(my) & M(pxr) &

   430 	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &

   431 	      order_isomorphism(M,pxr,r,y,my,g)))))"

   432   and is_recfun_separation:

   433      --{*for well-founded recursion.  NEEDS RELATIVIZATION*}

   434      "[| M(A); M(f); M(g); M(a); M(b) |]

   435      ==> separation(M, \<lambda>x. \<langle>x,a\<rangle> \<in> r & \<langle>x,b\<rangle> \<in> r & fx \<noteq> gx)"

   436   and omap_replacement:

   437      "[| M(A); M(r) |]

   438       ==> strong_replacement(M,

   439              \<lambda>a z. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &

   440 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &

   441 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"

   442

   443 lemma (in M_axioms) Ball_abs [simp]:

   444      "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))"

   445 by (blast intro: transM)

   446

   447 lemma (in M_axioms) Bex_abs [simp]:

   448      "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))"

   449 by (blast intro: transM)

   450

   451 lemma (in M_axioms) Ball_iff_equiv:

   452      "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <->

   453                (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)"

   454 by (blast intro: transM)

   455

   456 text{*Simplifies proofs of equalities when there's an iff-equality

   457       available for rewriting, universally quantified over M. *}

   458 lemma (in M_axioms) M_equalityI:

   459      "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"

   460 by (blast intro!: equalityI dest: transM)

   461

   462 lemma (in M_axioms) empty_abs [simp]:

   463      "M(z) ==> empty(M,z) <-> z=0"

   464 apply (simp add: empty_def)

   465 apply (blast intro: transM)

   466 done

   467

   468 lemma (in M_axioms) subset_abs [simp]:

   469      "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"

   470 apply (simp add: subset_def)

   471 apply (blast intro: transM)

   472 done

   473

   474 lemma (in M_axioms) upair_abs [simp]:

   475      "M(z) ==> upair(M,a,b,z) <-> z={a,b}"

   476 apply (simp add: upair_def)

   477 apply (blast intro: transM)

   478 done

   479

   480 lemma (in M_axioms) upair_in_M_iff [iff]:

   481      "M({a,b}) <-> M(a) & M(b)"

   482 apply (insert upair_ax, simp add: upair_ax_def)

   483 apply (blast intro: transM)

   484 done

   485

   486 lemma (in M_axioms) singleton_in_M_iff [iff]:

   487      "M({a}) <-> M(a)"

   488 by (insert upair_in_M_iff [of a a], simp)

   489

   490 lemma (in M_axioms) pair_abs [simp]:

   491      "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"

   492 apply (simp add: pair_def ZF.Pair_def)

   493 apply (blast intro: transM)

   494 done

   495

   496 lemma (in M_axioms) pair_in_M_iff [iff]:

   497      "M(<a,b>) <-> M(a) & M(b)"

   498 by (simp add: ZF.Pair_def)

   499

   500 lemma (in M_axioms) pair_components_in_M:

   501      "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"

   502 apply (simp add: Pair_def)

   503 apply (blast dest: transM)

   504 done

   505

   506 lemma (in M_axioms) cartprod_abs [simp]:

   507      "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"

   508 apply (simp add: cartprod_def)

   509 apply (rule iffI)

   510  apply (blast intro!: equalityI intro: transM dest!: rspec)

   511 apply (blast dest: transM)

   512 done

   513

   514 lemma (in M_axioms) union_abs [simp]:

   515      "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"

   516 apply (simp add: union_def)

   517 apply (blast intro: transM)

   518 done

   519

   520 lemma (in M_axioms) inter_abs [simp]:

   521      "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"

   522 apply (simp add: inter_def)

   523 apply (blast intro: transM)

   524 done

   525

   526 lemma (in M_axioms) setdiff_abs [simp]:

   527      "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"

   528 apply (simp add: setdiff_def)

   529 apply (blast intro: transM)

   530 done

   531

   532 lemma (in M_axioms) Union_abs [simp]:

   533      "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"

   534 apply (simp add: big_union_def)

   535 apply (blast intro!: equalityI dest: transM)

   536 done

   537

   538 lemma (in M_axioms) Union_closed [intro,simp]:

   539      "M(A) ==> M(Union(A))"

   540 by (insert Union_ax, simp add: Union_ax_def)

   541

   542 lemma (in M_axioms) Un_closed [intro,simp]:

   543      "[| M(A); M(B) |] ==> M(A Un B)"

   544 by (simp only: Un_eq_Union, blast)

   545

   546 lemma (in M_axioms) cons_closed [intro,simp]:

   547      "[| M(a); M(A) |] ==> M(cons(a,A))"

   548 by (subst cons_eq [symmetric], blast)

   549

   550 lemma (in M_axioms) successor_abs [simp]:

   551      "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)"

   552 by (simp add: successor_def, blast)

   553

   554 lemma (in M_axioms) succ_in_M_iff [iff]:

   555      "M(succ(a)) <-> M(a)"

   556 apply (simp add: succ_def)

   557 apply (blast intro: transM)

   558 done

   559

   560 lemma (in M_axioms) separation_closed [intro,simp]:

   561      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"

   562 apply (insert separation, simp add: separation_def)

   563 apply (drule spec [THEN mp], assumption, clarify)

   564 apply (subgoal_tac "y = Collect(A,P)", blast)

   565 apply (blast dest: transM)

   566 done

   567

   568 text{*Probably the premise and conclusion are equivalent*}

   569 lemma (in M_axioms) strong_replacementI [rule_format]:

   570     "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]

   571      ==> strong_replacement(M,P)"

   572 apply (simp add: strong_replacement_def, clarify)

   573 apply (frule replacementD [OF replacement], assumption)

   574 apply clarify

   575 apply (drule_tac x=A in spec, clarify)

   576 apply (drule_tac z=Y in separationD, assumption)

   577 apply clarify

   578 apply (blast dest: transM)

   579 done

   580

   581

   582 (*The last premise expresses that P takes M to M*)

   583 lemma (in M_axioms) strong_replacement_closed [intro,simp]:

   584      "[| strong_replacement(M,P); M(A); univalent(M,A,P);

   585        !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"

   586 apply (simp add: strong_replacement_def)

   587 apply (drule spec [THEN mp], auto)

   588 apply (subgoal_tac "Replace(A,P) = Y")

   589  apply simp

   590 apply (rule equality_iffI)

   591 apply (simp add: Replace_iff, safe)

   592  apply (blast dest: transM)

   593 apply (frule transM, assumption)

   594  apply (simp add: univalent_def)

   595  apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)

   596  apply (blast dest: transM)

   597 done

   598

   599 (*The first premise can't simply be assumed as a schema.

   600   It is essential to take care when asserting instances of Replacement.

   601   Let K be a nonconstructible subset of nat and define

   602   f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a

   603   nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))

   604   even for f : M -> M.

   605 *)

   606 lemma (in M_axioms) RepFun_closed [intro,simp]:

   607      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]

   608       ==> M(RepFun(A,f))"

   609 apply (simp add: RepFun_def)

   610 apply (rule strong_replacement_closed)

   611 apply (auto dest: transM  simp add: univalent_def)

   612 done

   613

   614 lemma (in M_axioms) lam_closed [intro,simp]:

   615      "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]

   616       ==> M(\<lambda>x\<in>A. b(x))"

   617 by (simp add: lam_def, blast dest: transM)

   618

   619 lemma (in M_axioms) image_abs [simp]:

   620      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = rA"

   621 apply (simp add: image_def)

   622 apply (rule iffI)

   623  apply (blast intro!: equalityI dest: transM, blast)

   624 done

   625

   626 text{*What about @{text Pow_abs}?  Powerset is NOT absolute!

   627       This result is one direction of absoluteness.*}

   628

   629 lemma (in M_axioms) powerset_Pow:

   630      "powerset(M, x, Pow(x))"

   631 by (simp add: powerset_def)

   632

   633 text{*But we can't prove that the powerset in @{text M} includes the

   634       real powerset.*}

   635 lemma (in M_axioms) powerset_imp_subset_Pow:

   636      "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"

   637 apply (simp add: powerset_def)

   638 apply (blast dest: transM)

   639 done

   640

   641 lemma (in M_axioms) cartprod_iff_lemma:

   642      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});

   643          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]

   644        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"

   645 apply (simp add: powerset_def)

   646 apply (rule equalityI, clarify, simp)

   647

   648  apply (frule transM, assumption)

   649

   650  apply (frule transM, assumption, simp)

   651  apply blast

   652 apply clarify

   653 apply (frule transM, assumption, force)

   654 done

   655

   656 lemma (in M_axioms) cartprod_iff:

   657      "[| M(A); M(B); M(C) |]

   658       ==> cartprod(M,A,B,C) <->

   659           (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &

   660                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"

   661 apply (simp add: Pair_def cartprod_def, safe)

   662 defer 1

   663   apply (simp add: powerset_def)

   664  apply blast

   665 txt{*Final, difficult case: the left-to-right direction of the theorem.*}

   666 apply (insert power_ax, simp add: power_ax_def)

   667 apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)

   668 apply (erule impE, blast, clarify)

   669 apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)

   670 apply (blast intro: cartprod_iff_lemma)

   671 done

   672

   673 lemma (in M_axioms) cartprod_closed_lemma:

   674      "[| M(A); M(B) |] ==> \<exists>C. M(C) & cartprod(M,A,B,C)"

   675 apply (simp del: cartprod_abs add: cartprod_iff)

   676 apply (insert power_ax, simp add: power_ax_def)

   677 apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)

   678 apply (erule impE, blast, clarify)

   679 apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)

   680 apply (erule impE, blast, clarify)

   681 apply (intro exI conjI)

   682 prefer 6 apply (rule refl)

   683 prefer 4 apply assumption

   684 prefer 4 apply assumption

   685 apply (insert cartprod_separation [of A B], auto)

   686 done

   687

   688

   689 text{*All the lemmas above are necessary because Powerset is not absolute.

   690       I should have used Replacement instead!*}

   691 lemma (in M_axioms) cartprod_closed [intro,simp]:

   692      "[| M(A); M(B) |] ==> M(A*B)"

   693 by (frule cartprod_closed_lemma, assumption, force)

   694

   695 lemma (in M_axioms) image_closed [intro,simp]:

   696      "[| M(A); M(r) |] ==> M(rA)"

   697 apply (simp add: image_iff_Collect)

   698 apply (insert image_separation [of A r], simp)

   699 done

   700

   701 lemma (in M_axioms) vimage_abs [simp]:

   702      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-A"

   703 apply (simp add: pre_image_def)

   704 apply (rule iffI)

   705  apply (blast intro!: equalityI dest: transM, blast)

   706 done

   707

   708 lemma (in M_axioms) vimage_closed [intro,simp]:

   709      "[| M(A); M(r) |] ==> M(r-A)"

   710 apply (simp add: vimage_iff_Collect)

   711 apply (insert vimage_separation [of A r], simp)

   712 done

   713

   714 lemma (in M_axioms) domain_abs [simp]:

   715      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"

   716 apply (simp add: is_domain_def)

   717 apply (blast intro!: equalityI dest: transM)

   718 done

   719

   720 lemma (in M_axioms) domain_closed [intro,simp]:

   721      "M(r) ==> M(domain(r))"

   722 apply (simp add: domain_eq_vimage)

   723 done

   724

   725 lemma (in M_axioms) range_abs [simp]:

   726      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"

   727 apply (simp add: is_range_def)

   728 apply (blast intro!: equalityI dest: transM)

   729 done

   730

   731 lemma (in M_axioms) range_closed [intro,simp]:

   732      "M(r) ==> M(range(r))"

   733 apply (simp add: range_eq_image)

   734 done

   735

   736 lemma (in M_axioms) field_abs [simp]:

   737      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"

   738 by (simp add: domain_closed range_closed is_field_def field_def)

   739

   740 lemma (in M_axioms) field_closed [intro,simp]:

   741      "M(r) ==> M(field(r))"

   742 by (simp add: domain_closed range_closed Un_closed field_def)

   743

   744

   745 lemma (in M_axioms) M_converse_iff:

   746      "M(r) ==>

   747       converse(r) =

   748       {z \<in> range(r) * domain(r). \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"

   749 by (blast dest: transM)

   750

   751 lemma (in M_axioms) converse_closed [intro,simp]:

   752      "M(r) ==> M(converse(r))"

   753 apply (simp add: M_converse_iff)

   754 apply (insert converse_separation [of r], simp)

   755 done

   756

   757 lemma (in M_axioms) converse_abs [simp]:

   758      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"

   759 apply (simp add: is_converse_def)

   760 apply (rule iffI)

   761  prefer 2 apply (blast intro: elim:);

   762 apply (rule M_equalityI)

   763   apply (simp add: )

   764   apply (blast dest: transM)+

   765 done

   766

   767 lemma (in M_axioms) relation_abs [simp]:

   768      "M(r) ==> is_relation(M,r) <-> relation(r)"

   769 apply (simp add: is_relation_def relation_def)

   770 apply (blast dest!: bspec dest: pair_components_in_M)+

   771 done

   772

   773 lemma (in M_axioms) function_abs [simp]:

   774      "M(r) ==> is_function(M,r) <-> function(r)"

   775 apply (simp add: is_function_def function_def, safe)

   776    apply (frule transM, assumption)

   777   apply (blast dest: pair_components_in_M)+

   778 done

   779

   780 lemma (in M_axioms) apply_closed [intro,simp]:

   781      "[|M(f); M(a)|] ==> M(fa)"

   782 apply (simp add: apply_def)

   783 done

   784

   785 lemma (in M_axioms) apply_abs:

   786      "[| function(f); M(f); M(y) |]

   787       ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & fx = y"

   788 apply (simp add: fun_apply_def)

   789 apply (blast intro: function_apply_equality function_apply_Pair)

   790 done

   791

   792 lemma (in M_axioms) typed_apply_abs:

   793      "[| f \<in> A -> B; M(f); M(y) |]

   794       ==> fun_apply(M,f,x,y) <-> x \<in> A & fx = y"

   795 by (simp add: apply_abs fun_is_function domain_of_fun)

   796

   797 lemma (in M_axioms) typed_function_abs [simp]:

   798      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"

   799 apply (auto simp add: typed_function_def relation_def Pi_iff)

   800 apply (blast dest: pair_components_in_M)+

   801 done

   802

   803 lemma (in M_axioms) injection_abs [simp]:

   804      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"

   805 apply (simp add: injection_def apply_iff inj_def apply_closed)

   806 apply (blast dest: transM [of _ A])

   807 done

   808

   809 lemma (in M_axioms) surjection_abs [simp]:

   810      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"

   811 by (simp add: typed_apply_abs surjection_def surj_def)

   812

   813 lemma (in M_axioms) bijection_abs [simp]:

   814      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"

   815 by (simp add: bijection_def bij_def)

   816

   817 text{*no longer needed*}

   818 lemma (in M_axioms) restriction_is_function:

   819      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]

   820       ==> function(z)"

   821 apply (rotate_tac 1)

   822 apply (simp add: restriction_def Ball_iff_equiv)

   823 apply (unfold function_def, blast)

   824 done

   825

   826 lemma (in M_axioms) restriction_abs [simp]:

   827      "[| M(f); M(A); M(z) |]

   828       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"

   829 apply (simp add: Ball_iff_equiv restriction_def restrict_def)

   830 apply (blast intro!: equalityI dest: transM)

   831 done

   832

   833

   834 lemma (in M_axioms) M_restrict_iff:

   835      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y. M(y) & z = \<langle>x, y\<rangle>}"

   836 by (simp add: restrict_def, blast dest: transM)

   837

   838 lemma (in M_axioms) restrict_closed [intro,simp]:

   839      "[| M(A); M(r) |] ==> M(restrict(r,A))"

   840 apply (simp add: M_restrict_iff)

   841 apply (insert restrict_separation [of A], simp)

   842 done

   843

   844 lemma (in M_axioms) M_comp_iff:

   845      "[| M(r); M(s) |]

   846       ==> r O s =

   847           {xz \<in> domain(s) * range(r).

   848             \<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) &

   849                 xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))}"

   850 apply (simp add: comp_def)

   851 apply (rule equalityI)

   852  apply clarify

   853  apply simp

   854  apply  (blast dest:  transM)+

   855 done

   856

   857 lemma (in M_axioms) comp_closed [intro,simp]:

   858      "[| M(r); M(s) |] ==> M(r O s)"

   859 apply (simp add: M_comp_iff)

   860 apply (insert comp_separation [of r s], simp)

   861 done

   862

   863 lemma (in M_axioms) composition_abs [simp]:

   864      "[| M(r); M(s); M(t) |]

   865       ==> composition(M,r,s,t) <-> t = r O s"

   866 apply safe

   867  txt{*Proving @{term "composition(M, r, s, r O s)"}*}

   868  prefer 2

   869  apply (simp add: composition_def comp_def)

   870  apply (blast dest: transM)

   871 txt{*Opposite implication*}

   872 apply (rule M_equalityI)

   873   apply (simp add: composition_def comp_def)

   874   apply (blast del: allE dest: transM)+

   875 done

   876

   877 lemma (in M_axioms) nat_into_M [intro]:

   878      "n \<in> nat ==> M(n)"

   879 by (induct n rule: nat_induct, simp_all)

   880

   881 lemma (in M_axioms) Inl_in_M_iff [iff]:

   882      "M(Inl(a)) <-> M(a)"

   883 by (simp add: Inl_def)

   884

   885 lemma (in M_axioms) Inr_in_M_iff [iff]:

   886      "M(Inr(a)) <-> M(a)"

   887 by (simp add: Inr_def)

   888

   889 lemma (in M_axioms) Inter_abs [simp]:

   890      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"

   891 apply (simp add: big_inter_def Inter_def)

   892 apply (blast intro!: equalityI dest: transM)

   893 done

   894

   895 lemma (in M_axioms) Inter_closed [intro,simp]:

   896      "M(A) ==> M(Inter(A))"

   897 by (insert Inter_separation, simp add: Inter_def)

   898

   899 lemma (in M_axioms) Int_closed [intro,simp]:

   900      "[| M(A); M(B) |] ==> M(A Int B)"

   901 apply (subgoal_tac "M({A,B})")

   902 apply (frule Inter_closed, force+)

   903 done

   904

   905 text{*M contains all finite functions*}

   906 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]:

   907      "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"

   908 apply (induct_tac n, simp)

   909 apply (rule ballI)

   910 apply (simp add: succ_def)

   911 apply (frule fun_cons_restrict_eq)

   912 apply (erule ssubst)

   913 apply (subgoal_tac "M(fx) & restrict(f,x) \<in> x -> A")

   914  apply (simp add: cons_closed nat_into_M apply_closed)

   915 apply (blast intro: apply_funtype transM restrict_type2)

   916 done

   917

   918 lemma (in M_axioms) finite_fun_closed [rule_format]:

   919      "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"

   920 by (blast intro: finite_fun_closed_lemma)

   921

   922

   923 subsection{*Absoluteness for ordinals*}

   924 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}

   925

   926 lemma (in M_axioms) lt_closed:

   927      "[| j<i; M(i) |] ==> M(j)"

   928 by (blast dest: ltD intro: transM)

   929

   930 lemma (in M_axioms) transitive_set_abs [simp]:

   931      "M(a) ==> transitive_set(M,a) <-> Transset(a)"

   932 by (simp add: transitive_set_def Transset_def)

   933

   934 lemma (in M_axioms) ordinal_abs [simp]:

   935      "M(a) ==> ordinal(M,a) <-> Ord(a)"

   936 by (simp add: ordinal_def Ord_def)

   937

   938 lemma (in M_axioms) limit_ordinal_abs [simp]:

   939      "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"

   940 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def)

   941 apply (simp add: lt_def, blast)

   942 done

   943

   944 lemma (in M_axioms) successor_ordinal_abs [simp]:

   945      "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b. M(b) & a = succ(b))"

   946 apply (simp add: successor_ordinal_def, safe)

   947 apply (drule Ord_cases_disj, auto)

   948 done

   949

   950 lemma finite_Ord_is_nat:

   951       "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"

   952 by (induct a rule: trans_induct3, simp_all)

   953

   954 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"

   955 by (induct a rule: nat_induct, auto)

   956

   957 lemma (in M_axioms) finite_ordinal_abs [simp]:

   958      "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"

   959 apply (simp add: finite_ordinal_def)

   960 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord

   961              dest: Ord_trans naturals_not_limit)

   962 done

   963

   964 lemma Limit_non_Limit_implies_nat: "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"

   965 apply (rule le_anti_sym)

   966 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)

   967  apply (simp add: lt_def)

   968  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat)

   969 apply (erule nat_le_Limit)

   970 done

   971

   972 lemma (in M_axioms) omega_abs [simp]:

   973      "M(a) ==> omega(M,a) <-> a = nat"

   974 apply (simp add: omega_def)

   975 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)

   976 done

   977

   978 lemma (in M_axioms) number1_abs [simp]:

   979      "M(a) ==> number1(M,a) <-> a = 1"

   980 by (simp add: number1_def)

   981

   982 lemma (in M_axioms) number1_abs [simp]:

   983      "M(a) ==> number2(M,a) <-> a = succ(1)"

   984 by (simp add: number2_def)

   985

   986 lemma (in M_axioms) number3_abs [simp]:

   987      "M(a) ==> number3(M,a) <-> a = succ(succ(1))"

   988 by (simp add: number3_def)

   989

   990 text{*Kunen continued to 20...*}

   991

   992 (*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything

   993   but the recursion variable must stay unchanged.  But then the recursion

   994   equations only hold for x\<in>nat (or in some other set) and not for the

   995   whole of the class M.

   996   consts

   997     natnumber_aux :: "[i=>o,i] => i"

   998

   999   primrec

  1000       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"

  1001       "natnumber_aux(M,succ(n)) =

  1002 	   (\<lambda>x\<in>nat. if (\<exists>y. M(y) & natnumber_aux(M,n)y=1 & successor(M,y,x))

  1003 		     then 1 else 0)"

  1004

  1005   constdefs

  1006     natnumber :: "[i=>o,i,i] => o"

  1007       "natnumber(M,n,x) == natnumber_aux(M,n)x = 1"

  1008

  1009   lemma (in M_axioms) [simp]:

  1010        "natnumber(M,0,x) == x=0"

  1011 *)

  1012

  1013

  1014 end