src/ZF/Constructible/Relative.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
     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) --> 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(x) & upair(M,a,a,x) &

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

    20

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

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

    23

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

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

    26

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

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

    29

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

    31     "inter(M,a,b,z) == \<forall>x. M(x) --> (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) --> (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) --> (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) --> (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) --> (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 v. M(u) & M(v) & 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_relation :: "[i=>o,i] => o"

    76     "is_relation(M,r) ==

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

    78

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

    80     "is_function(M,r) ==

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

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

    83                       y=y')"

    84

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

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

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

    88

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

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

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

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

    93

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

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

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

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

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

    99                       x=x')"

   100

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

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

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

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

   105

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

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

   108

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

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

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

   112             (x \<in> z <->

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

   114

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

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

   117

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

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

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

   121

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

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

   124     "limit_ordinal(M,a) ==

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

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

   127

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

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

   130     "successor_ordinal(M,a) ==

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

   132

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

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

   135     "finite_ordinal(M,a) ==

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

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

   138

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

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

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

   142

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

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

   145

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

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

   148

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

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

   151

   152

   153 subsection {*The relativized ZF axioms*}

   154 constdefs

   155

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

   157     "extensionality(M) ==

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

   159

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

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

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

   163     "separation(M,P) ==

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

   165

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

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

   168

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

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

   171

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

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

   174

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

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

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

   178

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

   180     "replacement(M,P) ==

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

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

   183

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

   185     "strong_replacement(M,P) ==

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

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

   188

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

   190     "foundation_ax(M) ==

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

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

   193

   194

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

   196

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

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

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

   200

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

   202 apply (insert Transset_univ [OF Transset_0])

   203 apply (simp add: Transset_def, blast)

   204 done

   205

   206 lemma univ0_Ball_abs [simp]:

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

   208 by (blast intro: univ0_downwards_mem)

   209

   210 lemma univ0_Bex_abs [simp]:

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

   212 by (blast intro: univ0_downwards_mem)

   213

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

   215 lemma [cong]:

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

   217 by (simp add: separation_def)

   218

   219 text{*Congruence rules for replacement*}

   220 lemma [cong]:

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

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

   223 by (simp add: univalent_def)

   224

   225 lemma [cong]:

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

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

   228 by (simp add: strong_replacement_def)

   229

   230 text{*The extensionality axiom*}

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

   232 apply (simp add: extensionality_def)

   233 apply (blast intro: univ0_downwards_mem)

   234 done

   235

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

   237 lemma Collect_in_Vfrom:

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

   239 apply (drule Transset_Vfrom)

   240 apply (rule subset_mem_Vfrom)

   241 apply (unfold Transset_def, blast)

   242 done

   243

   244 lemma Collect_in_VLimit:

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

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

   247 apply (rule Limit_VfromE, assumption+)

   248 apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)

   249 done

   250

   251 lemma Collect_in_univ:

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

   253 by (simp add: univ_def Collect_in_VLimit Limit_nat)

   254

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

   256 apply (simp add: separation_def)

   257 apply (blast intro: Collect_in_univ Transset_0)

   258 done

   259

   260 text{*Unordered pairing axiom*}

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

   262 apply (simp add: upair_ax_def upair_def)

   263 apply (blast intro: doubleton_in_univ)

   264 done

   265

   266 text{*Union axiom*}

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

   268 apply (simp add: Union_ax_def big_union_def)

   269 apply (blast intro: Union_in_univ Transset_0 univ0_downwards_mem)

   270 done

   271

   272 text{*Powerset axiom*}

   273

   274 lemma Pow_in_univ:

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

   276 apply (simp add: univ_def Pow_in_VLimit Limit_nat)

   277 done

   278

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

   280 apply (simp add: power_ax_def powerset_def subset_def)

   281 apply (blast intro: Pow_in_univ Transset_0 univ0_downwards_mem)

   282 done

   283

   284 text{*Foundation axiom*}

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

   286 apply (simp add: foundation_ax_def, clarify)

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

   288 done

   289

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

   291 apply (simp add: replacement_def, clarify)

   292 oops

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

   294

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

   296

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

   298       of Separation*}

   299

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

   301 apply (rule equalityI, auto)

   302 apply (simp add: Pair_def, blast)

   303 done

   304

   305 lemma vimage_iff_Collect:

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

   307 apply (rule equalityI, auto)

   308 apply (simp add: Pair_def, blast)

   309 done

   310

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

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

   313

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

   315 apply (rule equalityI, auto)

   316 apply (rule vimageI, assumption)

   317 apply (simp add: Pair_def, blast)

   318 done

   319

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

   321 apply (rule equalityI, auto)

   322 apply (rule imageI, assumption)

   323 apply (simp add: Pair_def, blast)

   324 done

   325

   326 lemma replacementD:

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

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

   329 by (simp add: replacement_def)

   330

   331 lemma strong_replacementD:

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

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

   334 by (simp add: strong_replacement_def)

   335

   336 lemma separationD:

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

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

   339 by (simp add: separation_def)

   340

   341

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

   343 constdefs

   344

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

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

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

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

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

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

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

   352

   353

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

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

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

   357

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

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

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

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

   362

   363

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

   365

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

   367       relativized ZF axioms*}

   368 locale M_axioms =

   369   fixes M

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

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

   372       and upair_ax:	    "upair_ax(M)"

   373       and Union_ax:	    "Union_ax(M)"

   374       and power_ax:         "power_ax(M)"

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

   376   and Inter_separation:

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

   378   and cartprod_separation:

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

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

   381   and image_separation:

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

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

   384   and vimage_separation:

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

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

   387   and converse_separation:

   388      "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. M(p) & (\<exists>x y. M(x) & M(y) &

   389 				     pair(M,x,y,p) & pair(M,y,x,z)))"

   390   and restrict_separation:

   391      "M(A)

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

   393   and comp_separation:

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

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

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

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

   398   and pred_separation:

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

   400   and Memrel_separation:

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

   402   and obase_separation:

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

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

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

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

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

   408   and well_ord_iso_separation:

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

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

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

   412   and obase_equals_separation:

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

   414       ==> separation

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

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

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

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

   419   and is_recfun_separation:

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

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

   422      ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> fx \<noteq> gx)"

   423   and omap_replacement:

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

   425       ==> strong_replacement(M,

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

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

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

   429

   430 lemma (in M_axioms) Ball_abs [simp]:

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

   432 by (blast intro: transM)

   433

   434 lemma (in M_axioms) Bex_abs [simp]:

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

   436 by (blast intro: transM)

   437

   438 lemma (in M_axioms) Ball_iff_equiv:

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

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

   441 by (blast intro: transM)

   442

   443 lemma (in M_axioms) empty_abs [simp]:

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

   445 apply (simp add: empty_def)

   446 apply (blast intro: transM)

   447 done

   448

   449 lemma (in M_axioms) subset_abs [simp]:

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

   451 apply (simp add: subset_def)

   452 apply (blast intro: transM)

   453 done

   454

   455 lemma (in M_axioms) upair_abs [simp]:

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

   457 apply (simp add: upair_def)

   458 apply (blast intro: transM)

   459 done

   460

   461 lemma (in M_axioms) upair_in_M_iff [iff]:

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

   463 apply (insert upair_ax, simp add: upair_ax_def)

   464 apply (blast intro: transM)

   465 done

   466

   467 lemma (in M_axioms) singleton_in_M_iff [iff]:

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

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

   470

   471 lemma (in M_axioms) pair_abs [simp]:

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

   473 apply (simp add: pair_def ZF.Pair_def)

   474 apply (blast intro: transM)

   475 done

   476

   477 lemma (in M_axioms) pair_in_M_iff [iff]:

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

   479 by (simp add: ZF.Pair_def)

   480

   481 lemma (in M_axioms) pair_components_in_M:

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

   483 apply (simp add: Pair_def)

   484 apply (blast dest: transM)

   485 done

   486

   487 lemma (in M_axioms) cartprod_abs [simp]:

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

   489 apply (simp add: cartprod_def)

   490 apply (rule iffI)

   491 apply (blast intro!: equalityI intro: transM dest!: spec)

   492 apply (blast dest: transM)

   493 done

   494

   495 lemma (in M_axioms) union_abs [simp]:

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

   497 apply (simp add: union_def)

   498 apply (blast intro: transM)

   499 done

   500

   501 lemma (in M_axioms) inter_abs [simp]:

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

   503 apply (simp add: inter_def)

   504 apply (blast intro: transM)

   505 done

   506

   507 lemma (in M_axioms) setdiff_abs [simp]:

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

   509 apply (simp add: setdiff_def)

   510 apply (blast intro: transM)

   511 done

   512

   513 lemma (in M_axioms) Union_abs [simp]:

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

   515 apply (simp add: big_union_def)

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

   517 done

   518

   519 lemma (in M_axioms) Union_closed [intro]:

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

   521 by (insert Union_ax, simp add: Union_ax_def)

   522

   523 lemma (in M_axioms) Un_closed [intro]:

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

   525 by (simp only: Un_eq_Union, blast)

   526

   527 lemma (in M_axioms) cons_closed [intro]:

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

   529 by (subst cons_eq [symmetric], blast)

   530

   531 lemma (in M_axioms) successor_abs [simp]:

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

   533 by (simp add: successor_def, blast)

   534

   535 lemma (in M_axioms) succ_in_M_iff [iff]:

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

   537 apply (simp add: succ_def)

   538 apply (blast intro: transM)

   539 done

   540

   541 lemma (in M_axioms) separation_closed [intro]:

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

   543 apply (insert separation, simp add: separation_def)

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

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

   546 apply (blast dest: transM)

   547 done

   548

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

   550 lemma (in M_axioms) strong_replacementI [rule_format]:

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

   552      ==> strong_replacement(M,P)"

   553 apply (simp add: strong_replacement_def)

   554 apply (clarify );

   555 apply (frule replacementD [OF replacement])

   556 apply assumption

   557 apply (clarify );

   558 apply (drule_tac x=A in spec)

   559 apply (clarify );

   560 apply (drule_tac z=Y in separationD)

   561 apply assumption;

   562 apply (clarify );

   563 apply (blast dest: transM)

   564 done

   565

   566

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

   568 lemma (in M_axioms) strong_replacement_closed [intro]:

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

   570        !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"

   571 apply (simp add: strong_replacement_def)

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

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

   574  apply (simp add: );

   575 apply (rule equality_iffI)

   576 apply (simp add: Replace_iff)

   577 apply safe;

   578  apply (blast dest: transM)

   579 apply (frule transM, assumption)

   580  apply (simp add: univalent_def);

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

   582  apply (blast dest: transM)

   583 done

   584

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

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

   587   Let K be a nonconstructible subset of nat and define

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

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

   590   even for f : M -> M.

   591 *)

   592 lemma (in M_axioms) RepFun_closed [intro]:

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

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

   595 apply (simp add: RepFun_def)

   596 apply (rule strong_replacement_closed)

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

   598 done

   599

   600 lemma (in M_axioms) converse_abs [simp]:

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

   602 apply (simp add: is_converse_def)

   603 apply (rule iffI)

   604  apply (rule equalityI)

   605   apply (blast dest: transM)

   606  apply (clarify, frule transM, assumption, simp, blast)

   607 done

   608

   609 lemma (in M_axioms) image_abs [simp]:

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

   611 apply (simp add: image_def)

   612 apply (rule iffI)

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

   614 done

   615

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

   617       This result is one direction of absoluteness.*}

   618

   619 lemma (in M_axioms) powerset_Pow:

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

   621 by (simp add: powerset_def)

   622

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

   624       real powerset.*}

   625 lemma (in M_axioms) powerset_imp_subset_Pow:

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

   627 apply (simp add: powerset_def)

   628 apply (blast dest: transM)

   629 done

   630

   631 lemma (in M_axioms) cartprod_iff_lemma:

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

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

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

   635 apply (simp add: powerset_def)

   636 apply (rule equalityI, clarify, simp)

   637  apply (frule transM, assumption, simp)

   638  apply blast

   639 apply clarify

   640 apply (frule transM, assumption, force)

   641 done

   642

   643 lemma (in M_axioms) cartprod_iff:

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

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

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

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

   648 apply (simp add: Pair_def cartprod_def, safe)

   649 defer 1

   650   apply (simp add: powerset_def)

   651  apply blast

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

   653 apply (insert power_ax, simp add: power_ax_def)

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

   655 apply (erule impE, blast, clarify)

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

   657 apply (blast intro: cartprod_iff_lemma)

   658 done

   659

   660 lemma (in M_axioms) cartprod_closed_lemma:

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

   662 apply (simp del: cartprod_abs add: cartprod_iff)

   663 apply (insert power_ax, simp add: power_ax_def)

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

   665 apply (erule impE, blast, clarify)

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

   667 apply (erule impE, blast, clarify)

   668 apply (intro exI conjI)

   669 prefer 6 apply (rule refl)

   670 prefer 4 apply assumption

   671 prefer 4 apply assumption

   672 apply (insert cartprod_separation [of A B], simp, blast+)

   673 done

   674

   675

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

   677       I should have used Replacement instead!*}

   678 lemma (in M_axioms) cartprod_closed [intro]:

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

   680 by (frule cartprod_closed_lemma, assumption, force)

   681

   682 lemma (in M_axioms) image_closed [intro]:

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

   684 apply (simp add: image_iff_Collect)

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

   686 done

   687

   688 lemma (in M_axioms) vimage_abs [simp]:

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

   690 apply (simp add: pre_image_def)

   691 apply (rule iffI)

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

   693 done

   694

   695 lemma (in M_axioms) vimage_closed [intro]:

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

   697 apply (simp add: vimage_iff_Collect)

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

   699 done

   700

   701 lemma (in M_axioms) domain_abs [simp]:

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

   703 apply (simp add: is_domain_def)

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

   705 done

   706

   707 lemma (in M_axioms) domain_closed [intro]:

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

   709 apply (simp add: domain_eq_vimage)

   710 apply (blast intro: vimage_closed)

   711 done

   712

   713 lemma (in M_axioms) range_abs [simp]:

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

   715 apply (simp add: is_range_def)

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

   717 done

   718

   719 lemma (in M_axioms) range_closed [intro]:

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

   721 apply (simp add: range_eq_image)

   722 apply (blast intro: image_closed)

   723 done

   724

   725 lemma (in M_axioms) M_converse_iff:

   726      "M(r) ==>

   727       converse(r) =

   728       {z \<in> range(r) * domain(r).

   729         \<exists>p\<in>r. \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> p = \<langle>x,y\<rangle> \<and> z = \<langle>y,x\<rangle>)}"

   730 by (blast dest: transM)

   731

   732 lemma (in M_axioms) converse_closed [intro]:

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

   734 apply (simp add: M_converse_iff)

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

   736 apply (blast intro: image_closed)

   737 done

   738

   739 lemma (in M_axioms) relation_abs [simp]:

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

   741 apply (simp add: is_relation_def relation_def)

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

   743 done

   744

   745 lemma (in M_axioms) function_abs [simp]:

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

   747 apply (simp add: is_function_def function_def, safe)

   748    apply (frule transM, assumption)

   749   apply (blast dest: pair_components_in_M)+

   750 done

   751

   752 lemma (in M_axioms) apply_closed [intro]:

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

   754 apply (simp add: apply_def)

   755 apply (blast intro: elim:);

   756 done

   757

   758 lemma (in M_axioms) apply_abs:

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

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

   761 apply (simp add: fun_apply_def)

   762 apply (blast intro: function_apply_equality function_apply_Pair)

   763 done

   764

   765 lemma (in M_axioms) typed_apply_abs:

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

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

   768 by (simp add: apply_abs fun_is_function domain_of_fun)

   769

   770 lemma (in M_axioms) typed_function_abs [simp]:

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

   772 apply (auto simp add: typed_function_def relation_def Pi_iff)

   773 apply (blast dest: pair_components_in_M)+

   774 done

   775

   776 lemma (in M_axioms) injection_abs [simp]:

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

   778 apply (simp add: injection_def apply_iff inj_def apply_closed)

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

   780 done

   781

   782 lemma (in M_axioms) surjection_abs [simp]:

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

   784 by (simp add: typed_apply_abs surjection_def surj_def)

   785

   786 lemma (in M_axioms) bijection_abs [simp]:

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

   788 by (simp add: bijection_def bij_def)

   789

   790 text{*no longer needed*}

   791 lemma (in M_axioms) restriction_is_function:

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

   793       ==> function(z)"

   794 apply (rotate_tac 1)

   795 apply (simp add: restriction_def Ball_iff_equiv)

   796 apply (unfold function_def, blast)

   797 done

   798

   799 lemma (in M_axioms) restriction_abs [simp]:

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

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

   802 apply (simp add: Ball_iff_equiv restriction_def restrict_def)

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

   804 done

   805

   806

   807 lemma (in M_axioms) M_restrict_iff:

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

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

   810

   811 lemma (in M_axioms) restrict_closed [intro]:

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

   813 apply (simp add: M_restrict_iff)

   814 apply (insert restrict_separation [of A], simp, blast)

   815 done

   816

   817

   818 lemma (in M_axioms) M_comp_iff:

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

   820       ==> r O s =

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

   822             \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> (\<exists>z. M(z) \<and>

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

   824 apply (simp add: comp_def)

   825 apply (rule equalityI)

   826  apply (clarify );

   827  apply (simp add: );

   828  apply  (blast dest:  transM)+

   829 done

   830

   831 lemma (in M_axioms) comp_closed [intro]:

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

   833 apply (simp add: M_comp_iff)

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

   835 done

   836

   837 lemma (in M_axioms) nat_into_M [intro]:

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

   839 by (induct n rule: nat_induct, simp_all)

   840

   841 lemma (in M_axioms) Inl_in_M_iff [iff]:

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

   843 by (simp add: Inl_def)

   844

   845 lemma (in M_axioms) Inr_in_M_iff [iff]:

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

   847 by (simp add: Inr_def)

   848

   849 lemma (in M_axioms) Inter_abs [simp]:

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

   851 apply (simp add: big_inter_def Inter_def)

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

   853 done

   854

   855 lemma (in M_axioms) Inter_closed [intro]:

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

   857 by (insert Inter_separation, simp add: Inter_def, blast)

   858

   859 lemma (in M_axioms) Int_closed [intro]:

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

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

   862 apply (frule Inter_closed, force+);

   863 done

   864

   865 subsection{*Absoluteness for ordinals*}

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

   867

   868 lemma (in M_axioms) lt_closed:

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

   870 by (blast dest: ltD intro: transM)

   871

   872 lemma (in M_axioms) transitive_set_abs [simp]:

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

   874 by (simp add: transitive_set_def Transset_def)

   875

   876 lemma (in M_axioms) ordinal_abs [simp]:

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

   878 by (simp add: ordinal_def Ord_def)

   879

   880 lemma (in M_axioms) limit_ordinal_abs [simp]:

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

   882 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def)

   883 apply (simp add: lt_def, blast)

   884 done

   885

   886 lemma (in M_axioms) successor_ordinal_abs [simp]:

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

   888 apply (simp add: successor_ordinal_def, safe)

   889 apply (drule Ord_cases_disj, auto)

   890 done

   891

   892 lemma finite_Ord_is_nat:

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

   894 by (induct a rule: trans_induct3, simp_all)

   895

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

   897 by (induct a rule: nat_induct, auto)

   898

   899 lemma (in M_axioms) finite_ordinal_abs [simp]:

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

   901 apply (simp add: finite_ordinal_def)

   902 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord

   903              dest: Ord_trans naturals_not_limit)

   904 done

   905

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

   907 apply (rule le_anti_sym)

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

   909  apply (simp add: lt_def)

   910  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat)

   911 apply (erule nat_le_Limit)

   912 done

   913

   914 lemma (in M_axioms) omega_abs [simp]:

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

   916 apply (simp add: omega_def)

   917 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)

   918 done

   919

   920 lemma (in M_axioms) number1_abs [simp]:

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

   922 by (simp add: number1_def)

   923

   924 lemma (in M_axioms) number1_abs [simp]:

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

   926 by (simp add: number2_def)

   927

   928 lemma (in M_axioms) number3_abs [simp]:

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

   930 by (simp add: number3_def)

   931

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

   933

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

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

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

   937   whole of the class M.

   938   consts

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

   940

   941   primrec

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

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

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

   945 		     then 1 else 0)"

   946

   947   constdefs

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

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

   950

   951   lemma (in M_axioms) [simp]:

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

   953 *)

   954

   955

   956 end
`