src/ZF/Constructible/Relative.thy
author wenzelm
Tue Aug 27 11:09:35 2002 +0200 (2002-08-27)
changeset 13535 007559e981c7
parent 13514 cc3bbaf1b8d3
child 13543 2b3c7e319d82
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      ZF/Constructible/Relative.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2002  University of Cambridge
     5 *)
     6 
     7 header {*Relativization and Absoluteness*}
     8 
     9 theory Relative = Main:
    10 
    11 subsection{* Relativized versions of standard set-theoretic concepts *}
    12 
    13 constdefs
    14   empty :: "[i=>o,i] => o"
    15     "empty(M,z) == \<forall>x[M]. x \<notin> z"
    16 
    17   subset :: "[i=>o,i,i] => o"
    18     "subset(M,A,B) == \<forall>x[M]. x\<in>A --> x \<in> B"
    19 
    20   upair :: "[i=>o,i,i,i] => o"
    21     "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z --> x = a | x = b)"
    22 
    23   pair :: "[i=>o,i,i,i] => o"
    24     "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & 
    25                           (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
    26 
    27 
    28   union :: "[i=>o,i,i,i] => o"
    29     "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"
    30 
    31   is_cons :: "[i=>o,i,i,i] => o"
    32     "is_cons(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,b,z)"
    33 
    34   successor :: "[i=>o,i,i] => o"
    35     "successor(M,a,z) == is_cons(M,a,a,z)"
    36 
    37   number1 :: "[i=>o,i] => o"
    38     "number1(M,a) == \<exists>x[M]. empty(M,x) & successor(M,x,a)"
    39 
    40   number2 :: "[i=>o,i] => o"
    41     "number2(M,a) == \<exists>x[M]. number1(M,x) & successor(M,x,a)"
    42 
    43   number3 :: "[i=>o,i] => o"
    44     "number3(M,a) == \<exists>x[M]. number2(M,x) & successor(M,x,a)"
    45 
    46   powerset :: "[i=>o,i,i] => o"
    47     "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
    48 
    49   is_Collect :: "[i=>o,i,i=>o,i] => o"
    50     "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)"
    51 
    52   is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
    53     "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))"
    54 
    55   inter :: "[i=>o,i,i,i] => o"
    56     "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
    57 
    58   setdiff :: "[i=>o,i,i,i] => o"
    59     "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
    60 
    61   big_union :: "[i=>o,i,i] => o"
    62     "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)"
    63 
    64   big_inter :: "[i=>o,i,i] => o"
    65     "big_inter(M,A,z) == 
    66              (A=0 --> z=0) &
    67 	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y[M]. y\<in>A --> x \<in> y)))"
    68 
    69   cartprod :: "[i=>o,i,i,i] => o"
    70     "cartprod(M,A,B,z) == 
    71 	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
    72 
    73   is_sum :: "[i=>o,i,i,i] => o"
    74     "is_sum(M,A,B,Z) == 
    75        \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
    76        number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
    77        cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
    78 
    79   is_Inl :: "[i=>o,i,i] => o"
    80     "is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z)"
    81 
    82   is_Inr :: "[i=>o,i,i] => o"
    83     "is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)"
    84 
    85   is_converse :: "[i=>o,i,i] => o"
    86     "is_converse(M,r,z) == 
    87 	\<forall>x[M]. x \<in> z <-> 
    88              (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
    89 
    90   pre_image :: "[i=>o,i,i,i] => o"
    91     "pre_image(M,r,A,z) == 
    92 	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
    93 
    94   is_domain :: "[i=>o,i,i] => o"
    95     "is_domain(M,r,z) == 
    96 	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
    97 
    98   image :: "[i=>o,i,i,i] => o"
    99     "image(M,r,A,z) == 
   100         \<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
   101 
   102   is_range :: "[i=>o,i,i] => o"
   103     --{*the cleaner 
   104       @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
   105       unfortunately needs an instance of separation in order to prove 
   106         @{term "M(converse(r))"}.*}
   107     "is_range(M,r,z) == 
   108 	\<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
   109 
   110   is_field :: "[i=>o,i,i] => o"
   111     "is_field(M,r,z) == 
   112 	\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) & 
   113                         union(M,dr,rr,z)"
   114 
   115   is_relation :: "[i=>o,i] => o"
   116     "is_relation(M,r) == 
   117         (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
   118 
   119   is_function :: "[i=>o,i] => o"
   120     "is_function(M,r) == 
   121 	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 
   122            pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
   123 
   124   fun_apply :: "[i=>o,i,i,i] => o"
   125     "fun_apply(M,f,x,y) == 
   126         (\<exists>xs[M]. \<exists>fxs[M]. 
   127          upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))"
   128 
   129   typed_function :: "[i=>o,i,i,i] => o"
   130     "typed_function(M,A,B,r) == 
   131         is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
   132         (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"
   133 
   134   is_funspace :: "[i=>o,i,i,i] => o"
   135     "is_funspace(M,A,B,F) == 
   136         \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
   137 
   138   composition :: "[i=>o,i,i,i] => o"
   139     "composition(M,r,s,t) == 
   140         \<forall>p[M]. p \<in> t <-> 
   141                (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   142                 pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   143                 xy \<in> s & yz \<in> r)"
   144 
   145   injection :: "[i=>o,i,i,i] => o"
   146     "injection(M,A,B,f) == 
   147 	typed_function(M,A,B,f) &
   148         (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M]. 
   149           pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')"
   150 
   151   surjection :: "[i=>o,i,i,i] => o"
   152     "surjection(M,A,B,f) == 
   153         typed_function(M,A,B,f) &
   154         (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
   155 
   156   bijection :: "[i=>o,i,i,i] => o"
   157     "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
   158 
   159   restriction :: "[i=>o,i,i,i] => o"
   160     "restriction(M,r,A,z) == 
   161 	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
   162 
   163   transitive_set :: "[i=>o,i] => o"
   164     "transitive_set(M,a) == \<forall>x[M]. x\<in>a --> subset(M,x,a)"
   165 
   166   ordinal :: "[i=>o,i] => o"
   167      --{*an ordinal is a transitive set of transitive sets*}
   168     "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a --> transitive_set(M,x))"
   169 
   170   limit_ordinal :: "[i=>o,i] => o"
   171     --{*a limit ordinal is a non-empty, successor-closed ordinal*}
   172     "limit_ordinal(M,a) == 
   173 	ordinal(M,a) & ~ empty(M,a) & 
   174         (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
   175 
   176   successor_ordinal :: "[i=>o,i] => o"
   177     --{*a successor ordinal is any ordinal that is neither empty nor limit*}
   178     "successor_ordinal(M,a) == 
   179 	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
   180 
   181   finite_ordinal :: "[i=>o,i] => o"
   182     --{*an ordinal is finite if neither it nor any of its elements are limit*}
   183     "finite_ordinal(M,a) == 
   184 	ordinal(M,a) & ~ limit_ordinal(M,a) & 
   185         (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   186 
   187   omega :: "[i=>o,i] => o"
   188     --{*omega is a limit ordinal none of whose elements are limit*}
   189     "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   190 
   191   is_quasinat :: "[i=>o,i] => o"
   192     "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
   193 
   194   is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
   195     "is_nat_case(M, a, is_b, k, z) == 
   196        (empty(M,k) --> z=a) &
   197        (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   198        (is_quasinat(M,k) | empty(M,z))"
   199 
   200   relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
   201     "relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
   202 
   203   Relativize1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
   204     --{*as above, but typed*}
   205     "Relativize1(M,A,is_f,f) == 
   206         \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
   207 
   208   relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
   209     "relativize2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
   210 
   211   Relativize2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o"
   212     "Relativize2(M,A,B,is_f,f) ==
   213         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A --> y\<in>B --> is_f(x,y,z) <-> z = f(x,y)"
   214 
   215   relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   216     "relativize3(M,is_f,f) == 
   217        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
   218 
   219   Relativize3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   220     "Relativize3(M,A,B,C,is_f,f) == 
   221        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. 
   222          x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
   223 
   224   relativize4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
   225     "relativize4(M,is_f,f) == 
   226        \<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) <-> a = f(u,x,y,z)"
   227 
   228 
   229 text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
   230 lemma triv_Relativize1:
   231      "Relativize1(M, A, \<lambda>x y. y = f(x), f)"
   232 by (simp add: Relativize1_def) 
   233 
   234 lemma triv_Relativize2:
   235      "Relativize2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
   236 by (simp add: Relativize2_def) 
   237 
   238 
   239 subsection {*The relativized ZF axioms*}
   240 constdefs
   241 
   242   extensionality :: "(i=>o) => o"
   243     "extensionality(M) == 
   244 	\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"
   245 
   246   separation :: "[i=>o, i=>o] => o"
   247     --{*Big problem: the formula @{text P} should only involve parameters
   248         belonging to @{text M}.  Don't see how to enforce that.*}
   249     "separation(M,P) == 
   250 	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   251 
   252   upair_ax :: "(i=>o) => o"
   253     "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z[M]. upair(M,x,y,z))"
   254 
   255   Union_ax :: "(i=>o) => o"
   256     "Union_ax(M) == \<forall>x[M]. \<exists>z[M]. big_union(M,x,z)"
   257 
   258   power_ax :: "(i=>o) => o"
   259     "power_ax(M) == \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)"
   260 
   261   univalent :: "[i=>o, i, [i,i]=>o] => o"
   262     "univalent(M,A,P) == 
   263 	(\<forall>x[M]. x\<in>A --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"
   264 
   265   replacement :: "[i=>o, [i,i]=>o] => o"
   266     "replacement(M,P) == 
   267       \<forall>A[M]. univalent(M,A,P) -->
   268       (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)"
   269 
   270   strong_replacement :: "[i=>o, [i,i]=>o] => o"
   271     "strong_replacement(M,P) == 
   272       \<forall>A[M]. univalent(M,A,P) -->
   273       (\<exists>Y[M]. \<forall>b[M]. b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))"
   274 
   275   foundation_ax :: "(i=>o) => o"
   276     "foundation_ax(M) == 
   277 	\<forall>x[M]. (\<exists>y\<in>x. M(y)) --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
   278 
   279 
   280 subsection{*A trivial consistency proof for $V_\omega$ *}
   281 
   282 text{*We prove that $V_\omega$ 
   283       (or @{text univ} in Isabelle) satisfies some ZF axioms.
   284      Kunen, Theorem IV 3.13, page 123.*}
   285 
   286 lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
   287 apply (insert Transset_univ [OF Transset_0])  
   288 apply (simp add: Transset_def, blast) 
   289 done
   290 
   291 lemma univ0_Ball_abs [simp]: 
   292      "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   293 by (blast intro: univ0_downwards_mem) 
   294 
   295 lemma univ0_Bex_abs [simp]: 
   296      "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   297 by (blast intro: univ0_downwards_mem) 
   298 
   299 text{*Congruence rule for separation: can assume the variable is in @{text M}*}
   300 lemma separation_cong [cong]:
   301      "(!!x. M(x) ==> P(x) <-> P'(x)) 
   302       ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
   303 by (simp add: separation_def) 
   304 
   305 lemma univalent_cong [cong]:
   306      "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   307       ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
   308 by (simp add: univalent_def) 
   309 
   310 lemma univalent_triv [intro,simp]:
   311      "univalent(M, A, \<lambda>x y. y = f(x))"
   312 by (simp add: univalent_def) 
   313 
   314 lemma univalent_conjI2 [intro,simp]:
   315      "univalent(M,A,Q) ==> univalent(M, A, \<lambda>x y. P(x,y) & Q(x,y))"
   316 by (simp add: univalent_def, blast) 
   317 
   318 text{*Congruence rule for replacement*}
   319 lemma strong_replacement_cong [cong]:
   320      "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   321       ==> strong_replacement(M, %x y. P(x,y)) <-> 
   322           strong_replacement(M, %x y. P'(x,y))" 
   323 by (simp add: strong_replacement_def) 
   324 
   325 text{*The extensionality axiom*}
   326 lemma "extensionality(\<lambda>x. x \<in> univ(0))"
   327 apply (simp add: extensionality_def)
   328 apply (blast intro: univ0_downwards_mem) 
   329 done
   330 
   331 text{*The separation axiom requires some lemmas*}
   332 lemma Collect_in_Vfrom:
   333      "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"
   334 apply (drule Transset_Vfrom)
   335 apply (rule subset_mem_Vfrom)
   336 apply (unfold Transset_def, blast)
   337 done
   338 
   339 lemma Collect_in_VLimit:
   340      "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] 
   341       ==> Collect(X,P) \<in> Vfrom(A,i)"
   342 apply (rule Limit_VfromE, assumption+)
   343 apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
   344 done
   345 
   346 lemma Collect_in_univ:
   347      "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
   348 by (simp add: univ_def Collect_in_VLimit Limit_nat)
   349 
   350 lemma "separation(\<lambda>x. x \<in> univ(0), P)"
   351 apply (simp add: separation_def, clarify) 
   352 apply (rule_tac x = "Collect(z,P)" in bexI) 
   353 apply (blast intro: Collect_in_univ Transset_0)+
   354 done
   355 
   356 text{*Unordered pairing axiom*}
   357 lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
   358 apply (simp add: upair_ax_def upair_def)  
   359 apply (blast intro: doubleton_in_univ) 
   360 done
   361 
   362 text{*Union axiom*}
   363 lemma "Union_ax(\<lambda>x. x \<in> univ(0))"  
   364 apply (simp add: Union_ax_def big_union_def, clarify) 
   365 apply (rule_tac x="\<Union>x" in bexI)  
   366  apply (blast intro: univ0_downwards_mem)
   367 apply (blast intro: Union_in_univ Transset_0) 
   368 done
   369 
   370 text{*Powerset axiom*}
   371 
   372 lemma Pow_in_univ:
   373      "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"
   374 apply (simp add: univ_def Pow_in_VLimit Limit_nat)
   375 done
   376 
   377 lemma "power_ax(\<lambda>x. x \<in> univ(0))"  
   378 apply (simp add: power_ax_def powerset_def subset_def, clarify) 
   379 apply (rule_tac x="Pow(x)" in bexI)
   380  apply (blast intro: univ0_downwards_mem)
   381 apply (blast intro: Pow_in_univ Transset_0) 
   382 done
   383 
   384 text{*Foundation axiom*}
   385 lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"  
   386 apply (simp add: foundation_ax_def, clarify)
   387 apply (cut_tac A=x in foundation) 
   388 apply (blast intro: univ0_downwards_mem)
   389 done
   390 
   391 lemma "replacement(\<lambda>x. x \<in> univ(0), P)"  
   392 apply (simp add: replacement_def, clarify) 
   393 oops
   394 text{*no idea: maybe prove by induction on the rank of A?*}
   395 
   396 text{*Still missing: Replacement, Choice*}
   397 
   398 subsection{*lemmas needed to reduce some set constructions to instances
   399       of Separation*}
   400 
   401 lemma image_iff_Collect: "r `` A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
   402 apply (rule equalityI, auto) 
   403 apply (simp add: Pair_def, blast) 
   404 done
   405 
   406 lemma vimage_iff_Collect:
   407      "r -`` A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
   408 apply (rule equalityI, auto) 
   409 apply (simp add: Pair_def, blast) 
   410 done
   411 
   412 text{*These two lemmas lets us prove @{text domain_closed} and 
   413       @{text range_closed} without new instances of separation*}
   414 
   415 lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
   416 apply (rule equalityI, auto)
   417 apply (rule vimageI, assumption)
   418 apply (simp add: Pair_def, blast) 
   419 done
   420 
   421 lemma range_eq_image: "range(r) = r `` Union(Union(r))"
   422 apply (rule equalityI, auto)
   423 apply (rule imageI, assumption)
   424 apply (simp add: Pair_def, blast) 
   425 done
   426 
   427 lemma replacementD:
   428     "[| replacement(M,P); M(A);  univalent(M,A,P) |]
   429      ==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y))"
   430 by (simp add: replacement_def) 
   431 
   432 lemma strong_replacementD:
   433     "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
   434      ==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b))))"
   435 by (simp add: strong_replacement_def) 
   436 
   437 lemma separationD:
   438     "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   439 by (simp add: separation_def) 
   440 
   441 
   442 text{*More constants, for order types*}
   443 constdefs
   444 
   445   order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
   446     "order_isomorphism(M,A,r,B,s,f) == 
   447         bijection(M,A,B,f) & 
   448         (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
   449           (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
   450             pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> 
   451             pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
   452 
   453   pred_set :: "[i=>o,i,i,i,i] => o"
   454     "pred_set(M,A,x,r,B) == 
   455 	\<forall>y[M]. y \<in> B <-> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
   456 
   457   membership :: "[i=>o,i,i] => o" --{*membership relation*}
   458     "membership(M,A,r) == 
   459 	\<forall>p[M]. p \<in> r <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
   460 
   461 
   462 subsection{*Introducing a Transitive Class Model*}
   463 
   464 text{*The class M is assumed to be transitive and to satisfy some
   465       relativized ZF axioms*}
   466 locale M_triv_axioms =
   467   fixes M
   468   assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
   469       and nonempty [simp]:  "M(0)"
   470       and upair_ax:	    "upair_ax(M)"
   471       and Union_ax:	    "Union_ax(M)"
   472       and power_ax:         "power_ax(M)"
   473       and replacement:      "replacement(M,P)"
   474       and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
   475 
   476 lemma (in M_triv_axioms) rall_abs [simp]: 
   477      "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   478 by (blast intro: transM) 
   479 
   480 lemma (in M_triv_axioms) rex_abs [simp]: 
   481      "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   482 by (blast intro: transM) 
   483 
   484 lemma (in M_triv_axioms) ball_iff_equiv: 
   485      "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <-> 
   486                (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   487 by (blast intro: transM)
   488 
   489 text{*Simplifies proofs of equalities when there's an iff-equality
   490       available for rewriting, universally quantified over M. *}
   491 lemma (in M_triv_axioms) M_equalityI: 
   492      "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
   493 by (blast intro!: equalityI dest: transM) 
   494 
   495 
   496 subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
   497 
   498 lemma (in M_triv_axioms) empty_abs [simp]: 
   499      "M(z) ==> empty(M,z) <-> z=0"
   500 apply (simp add: empty_def)
   501 apply (blast intro: transM) 
   502 done
   503 
   504 lemma (in M_triv_axioms) subset_abs [simp]: 
   505      "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
   506 apply (simp add: subset_def) 
   507 apply (blast intro: transM) 
   508 done
   509 
   510 lemma (in M_triv_axioms) upair_abs [simp]: 
   511      "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
   512 apply (simp add: upair_def) 
   513 apply (blast intro: transM) 
   514 done
   515 
   516 lemma (in M_triv_axioms) upair_in_M_iff [iff]:
   517      "M({a,b}) <-> M(a) & M(b)"
   518 apply (insert upair_ax, simp add: upair_ax_def) 
   519 apply (blast intro: transM) 
   520 done
   521 
   522 lemma (in M_triv_axioms) singleton_in_M_iff [iff]:
   523      "M({a}) <-> M(a)"
   524 by (insert upair_in_M_iff [of a a], simp) 
   525 
   526 lemma (in M_triv_axioms) pair_abs [simp]: 
   527      "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   528 apply (simp add: pair_def ZF.Pair_def)
   529 apply (blast intro: transM) 
   530 done
   531 
   532 lemma (in M_triv_axioms) pair_in_M_iff [iff]:
   533      "M(<a,b>) <-> M(a) & M(b)"
   534 by (simp add: ZF.Pair_def)
   535 
   536 lemma (in M_triv_axioms) pair_components_in_M:
   537      "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   538 apply (simp add: Pair_def)
   539 apply (blast dest: transM) 
   540 done
   541 
   542 lemma (in M_triv_axioms) cartprod_abs [simp]: 
   543      "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   544 apply (simp add: cartprod_def)
   545 apply (rule iffI) 
   546  apply (blast intro!: equalityI intro: transM dest!: rspec) 
   547 apply (blast dest: transM) 
   548 done
   549 
   550 subsubsection{*Absoluteness for Unions and Intersections*}
   551 
   552 lemma (in M_triv_axioms) union_abs [simp]: 
   553      "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   554 apply (simp add: union_def) 
   555 apply (blast intro: transM) 
   556 done
   557 
   558 lemma (in M_triv_axioms) inter_abs [simp]: 
   559      "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   560 apply (simp add: inter_def) 
   561 apply (blast intro: transM) 
   562 done
   563 
   564 lemma (in M_triv_axioms) setdiff_abs [simp]: 
   565      "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   566 apply (simp add: setdiff_def) 
   567 apply (blast intro: transM) 
   568 done
   569 
   570 lemma (in M_triv_axioms) Union_abs [simp]: 
   571      "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   572 apply (simp add: big_union_def) 
   573 apply (blast intro!: equalityI dest: transM) 
   574 done
   575 
   576 lemma (in M_triv_axioms) Union_closed [intro,simp]:
   577      "M(A) ==> M(Union(A))"
   578 by (insert Union_ax, simp add: Union_ax_def) 
   579 
   580 lemma (in M_triv_axioms) Un_closed [intro,simp]:
   581      "[| M(A); M(B) |] ==> M(A Un B)"
   582 by (simp only: Un_eq_Union, blast) 
   583 
   584 lemma (in M_triv_axioms) cons_closed [intro,simp]:
   585      "[| M(a); M(A) |] ==> M(cons(a,A))"
   586 by (subst cons_eq [symmetric], blast) 
   587 
   588 lemma (in M_triv_axioms) cons_abs [simp]: 
   589      "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
   590 by (simp add: is_cons_def, blast intro: transM)  
   591 
   592 lemma (in M_triv_axioms) successor_abs [simp]: 
   593      "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
   594 by (simp add: successor_def, blast)  
   595 
   596 lemma (in M_triv_axioms) succ_in_M_iff [iff]:
   597      "M(succ(a)) <-> M(a)"
   598 apply (simp add: succ_def) 
   599 apply (blast intro: transM) 
   600 done
   601 
   602 subsubsection{*Absoluteness for Separation and Replacement*}
   603 
   604 lemma (in M_triv_axioms) separation_closed [intro,simp]:
   605      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   606 apply (insert separation, simp add: separation_def) 
   607 apply (drule rspec, assumption, clarify) 
   608 apply (subgoal_tac "y = Collect(A,P)", blast)
   609 apply (blast dest: transM) 
   610 done
   611 
   612 lemma separation_iff:
   613      "separation(M,P) <-> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
   614 by (simp add: separation_def is_Collect_def) 
   615 
   616 lemma (in M_triv_axioms) Collect_abs [simp]: 
   617      "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)"
   618 apply (simp add: is_Collect_def)
   619 apply (blast intro!: equalityI dest: transM)
   620 done
   621 
   622 text{*Probably the premise and conclusion are equivalent*}
   623 lemma (in M_triv_axioms) strong_replacementI [rule_format]:
   624     "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
   625      ==> strong_replacement(M,P)"
   626 apply (simp add: strong_replacement_def, clarify) 
   627 apply (frule replacementD [OF replacement], assumption, clarify) 
   628 apply (drule_tac x=A in rspec, clarify)  
   629 apply (drule_tac z=Y in separationD, assumption, clarify) 
   630 apply (rule_tac x=y in rexI) 
   631 apply (blast dest: transM)+
   632 done
   633 
   634 
   635 subsubsection{*The Operator @{term is_Replace}*}
   636 
   637 
   638 lemma is_Replace_cong [cong]:
   639      "[| A=A'; 
   640          !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y);
   641          z=z' |] 
   642       ==> is_Replace(M, A, %x y. P(x,y), z) <-> 
   643           is_Replace(M, A', %x y. P'(x,y), z')" 
   644 by (simp add: is_Replace_def) 
   645 
   646 lemma (in M_triv_axioms) univalent_Replace_iff: 
   647      "[| M(A); univalent(M,A,P);
   648          !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] 
   649       ==> u \<in> Replace(A,P) <-> (\<exists>x. x\<in>A & P(x,u))"
   650 apply (simp add: Replace_iff univalent_def) 
   651 apply (blast dest: transM)
   652 done
   653 
   654 (*The last premise expresses that P takes M to M*)
   655 lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:
   656      "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   657          !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
   658 apply (simp add: strong_replacement_def) 
   659 apply (drule_tac x=A in rspec, safe) 
   660 apply (subgoal_tac "Replace(A,P) = Y")
   661  apply simp 
   662 apply (rule equality_iffI)
   663 apply (simp add: univalent_Replace_iff)
   664 apply (blast dest: transM) 
   665 done
   666 
   667 lemma (in M_triv_axioms) Replace_abs: 
   668      "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P);
   669          !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |] 
   670       ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
   671 apply (simp add: is_Replace_def)
   672 apply (rule iffI) 
   673 apply (rule M_equalityI) 
   674 apply (simp_all add: univalent_Replace_iff, blast, blast) 
   675 done
   676 
   677 (*The first premise can't simply be assumed as a schema.
   678   It is essential to take care when asserting instances of Replacement.
   679   Let K be a nonconstructible subset of nat and define
   680   f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   681   nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   682   even for f : M -> M.
   683 *)
   684 lemma (in M_triv_axioms) RepFun_closed:
   685      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   686       ==> M(RepFun(A,f))"
   687 apply (simp add: RepFun_def) 
   688 apply (rule strong_replacement_closed) 
   689 apply (auto dest: transM  simp add: univalent_def) 
   690 done
   691 
   692 lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
   693 by simp
   694 
   695 text{*Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
   696       makes relativization easier.*}
   697 lemma (in M_triv_axioms) RepFun_closed2:
   698      "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   699       ==> M(RepFun(A, %x. f(x)))"
   700 apply (simp add: RepFun_def)
   701 apply (frule strong_replacement_closed, assumption)
   702 apply (auto dest: transM  simp add: Replace_conj_eq univalent_def) 
   703 done
   704 
   705 subsubsection {*Absoluteness for @{term Lambda}*}
   706 
   707 constdefs
   708  is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
   709     "is_lambda(M, A, is_b, z) == 
   710        \<forall>p[M]. p \<in> z <->
   711         (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
   712 
   713 lemma (in M_triv_axioms) lam_closed:
   714      "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   715       ==> M(\<lambda>x\<in>A. b(x))"
   716 by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
   717 
   718 text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
   719 lemma (in M_triv_axioms) lam_closed2:
   720   "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   721      M(A); \<forall>m[M]. m\<in>A --> M(b(m))|] ==> M(Lambda(A,b))"
   722 apply (simp add: lam_def)
   723 apply (blast intro: RepFun_closed2 dest: transM)  
   724 done
   725 
   726 lemma (in M_triv_axioms) lambda_abs2 [simp]: 
   727      "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   728          Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |] 
   729       ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
   730 apply (simp add: Relativize1_def is_lambda_def)
   731 apply (rule iffI)
   732  prefer 2 apply (simp add: lam_def) 
   733 apply (rule M_equalityI)
   734   apply (simp add: lam_def) 
   735  apply (simp add: lam_closed2)+
   736 done
   737 
   738 lemma is_lambda_cong [cong]:
   739      "[| A=A';  z=z'; 
   740          !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] 
   741       ==> is_lambda(M, A, %x y. is_b(x,y), z) <-> 
   742           is_lambda(M, A', %x y. is_b'(x,y), z')" 
   743 by (simp add: is_lambda_def) 
   744 
   745 lemma (in M_triv_axioms) image_abs [simp]: 
   746      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   747 apply (simp add: image_def)
   748 apply (rule iffI) 
   749  apply (blast intro!: equalityI dest: transM, blast) 
   750 done
   751 
   752 text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   753       This result is one direction of absoluteness.*}
   754 
   755 lemma (in M_triv_axioms) powerset_Pow: 
   756      "powerset(M, x, Pow(x))"
   757 by (simp add: powerset_def)
   758 
   759 text{*But we can't prove that the powerset in @{text M} includes the
   760       real powerset.*}
   761 lemma (in M_triv_axioms) powerset_imp_subset_Pow: 
   762      "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   763 apply (simp add: powerset_def) 
   764 apply (blast dest: transM) 
   765 done
   766 
   767 subsubsection{*Absoluteness for the Natural Numbers*}
   768 
   769 lemma (in M_triv_axioms) nat_into_M [intro]:
   770      "n \<in> nat ==> M(n)"
   771 by (induct n rule: nat_induct, simp_all)
   772 
   773 lemma (in M_triv_axioms) nat_case_closed [intro,simp]:
   774   "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   775 apply (case_tac "k=0", simp) 
   776 apply (case_tac "\<exists>m. k = succ(m)", force)
   777 apply (simp add: nat_case_def) 
   778 done
   779 
   780 lemma (in M_triv_axioms) quasinat_abs [simp]: 
   781      "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
   782 by (auto simp add: is_quasinat_def quasinat_def)
   783 
   784 lemma (in M_triv_axioms) nat_case_abs [simp]: 
   785      "[| relativize1(M,is_b,b); M(k); M(z) |] 
   786       ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
   787 apply (case_tac "quasinat(k)") 
   788  prefer 2 
   789  apply (simp add: is_nat_case_def non_nat_case) 
   790  apply (force simp add: quasinat_def) 
   791 apply (simp add: quasinat_def is_nat_case_def)
   792 apply (elim disjE exE) 
   793  apply (simp_all add: relativize1_def) 
   794 done
   795 
   796 (*NOT for the simplifier.  The assumption M(z') is apparently necessary, but 
   797   causes the error "Failed congruence proof!"  It may be better to replace
   798   is_nat_case by nat_case before attempting congruence reasoning.*)
   799 lemma is_nat_case_cong:
   800      "[| a = a'; k = k';  z = z';  M(z');
   801        !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
   802       ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
   803 by (simp add: is_nat_case_def) 
   804 
   805 
   806 subsection{*Absoluteness for Ordinals*}
   807 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   808 
   809 lemma (in M_triv_axioms) lt_closed:
   810      "[| j<i; M(i) |] ==> M(j)" 
   811 by (blast dest: ltD intro: transM) 
   812 
   813 lemma (in M_triv_axioms) transitive_set_abs [simp]: 
   814      "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   815 by (simp add: transitive_set_def Transset_def)
   816 
   817 lemma (in M_triv_axioms) ordinal_abs [simp]: 
   818      "M(a) ==> ordinal(M,a) <-> Ord(a)"
   819 by (simp add: ordinal_def Ord_def)
   820 
   821 lemma (in M_triv_axioms) limit_ordinal_abs [simp]: 
   822      "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   823 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
   824 apply (simp add: lt_def, blast) 
   825 done
   826 
   827 lemma (in M_triv_axioms) successor_ordinal_abs [simp]: 
   828      "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   829 apply (simp add: successor_ordinal_def, safe)
   830 apply (drule Ord_cases_disj, auto) 
   831 done
   832 
   833 lemma finite_Ord_is_nat:
   834       "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   835 by (induct a rule: trans_induct3, simp_all)
   836 
   837 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   838 by (induct a rule: nat_induct, auto)
   839 
   840 lemma (in M_triv_axioms) finite_ordinal_abs [simp]: 
   841      "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   842 apply (simp add: finite_ordinal_def)
   843 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   844              dest: Ord_trans naturals_not_limit)
   845 done
   846 
   847 lemma Limit_non_Limit_implies_nat:
   848      "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   849 apply (rule le_anti_sym) 
   850 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   851  apply (simp add: lt_def)  
   852  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   853 apply (erule nat_le_Limit)
   854 done
   855 
   856 lemma (in M_triv_axioms) omega_abs [simp]: 
   857      "M(a) ==> omega(M,a) <-> a = nat"
   858 apply (simp add: omega_def) 
   859 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   860 done
   861 
   862 lemma (in M_triv_axioms) number1_abs [simp]: 
   863      "M(a) ==> number1(M,a) <-> a = 1"
   864 by (simp add: number1_def) 
   865 
   866 lemma (in M_triv_axioms) number2_abs [simp]: 
   867      "M(a) ==> number2(M,a) <-> a = succ(1)"
   868 by (simp add: number2_def) 
   869 
   870 lemma (in M_triv_axioms) number3_abs [simp]: 
   871      "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   872 by (simp add: number3_def) 
   873 
   874 text{*Kunen continued to 20...*}
   875 
   876 (*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   877   but the recursion variable must stay unchanged.  But then the recursion
   878   equations only hold for x\<in>nat (or in some other set) and not for the 
   879   whole of the class M.
   880   consts
   881     natnumber_aux :: "[i=>o,i] => i"
   882 
   883   primrec
   884       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   885       "natnumber_aux(M,succ(n)) = 
   886 	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   887 		     then 1 else 0)"
   888 
   889   constdefs
   890     natnumber :: "[i=>o,i,i] => o"
   891       "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   892 
   893   lemma (in M_triv_axioms) [simp]: 
   894        "natnumber(M,0,x) == x=0"
   895 *)
   896 
   897 subsection{*Some instances of separation and strong replacement*}
   898 
   899 locale M_axioms = M_triv_axioms +
   900 assumes Inter_separation:
   901      "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
   902   and Diff_separation:
   903      "M(B) ==> separation(M, \<lambda>x. x \<notin> B)"
   904   and cartprod_separation:
   905      "[| M(A); M(B) |] 
   906       ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
   907   and image_separation:
   908      "[| M(A); M(r) |] 
   909       ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
   910   and converse_separation:
   911      "M(r) ==> separation(M, 
   912          \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
   913   and restrict_separation:
   914      "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
   915   and comp_separation:
   916      "[| M(r); M(s) |]
   917       ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   918 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   919                   xy\<in>s & yz\<in>r)"
   920   and pred_separation:
   921      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
   922   and Memrel_separation:
   923      "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
   924   and funspace_succ_replacement:
   925      "M(n) ==> 
   926       strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M]. 
   927                 pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
   928                 upair(M,cnbf,cnbf,z))"
   929   and well_ord_iso_separation:
   930      "[| M(A); M(f); M(r) |] 
   931       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M]. 
   932 		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   933   and obase_separation:
   934      --{*part of the order type formalization*}
   935      "[| M(A); M(r) |] 
   936       ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   937 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   938 	     order_isomorphism(M,par,r,x,mx,g))"
   939   and obase_equals_separation:
   940      "[| M(A); M(r) |] 
   941       ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
   942 			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
   943 			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   944 			      order_isomorphism(M,pxr,r,y,my,g))))"
   945   and omap_replacement:
   946      "[| M(A); M(r) |] 
   947       ==> strong_replacement(M,
   948              \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   949 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   950 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   951   and is_recfun_separation:
   952      --{*for well-founded recursion*}
   953      "[| M(r); M(f); M(g); M(a); M(b) |] 
   954      ==> separation(M, 
   955             \<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
   956                 pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
   957                 (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
   958                                    fx \<noteq> gx))"
   959 
   960 lemma (in M_axioms) cartprod_iff_lemma:
   961      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   962          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   963        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   964 apply (simp add: powerset_def) 
   965 apply (rule equalityI, clarify, simp)
   966  apply (frule transM, assumption) 
   967  apply (frule transM, assumption, simp) 
   968  apply blast 
   969 apply clarify
   970 apply (frule transM, assumption, force) 
   971 done
   972 
   973 lemma (in M_axioms) cartprod_iff:
   974      "[| M(A); M(B); M(C) |] 
   975       ==> cartprod(M,A,B,C) <-> 
   976           (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   977                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
   978 apply (simp add: Pair_def cartprod_def, safe)
   979 defer 1 
   980   apply (simp add: powerset_def) 
   981  apply blast 
   982 txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   983 apply (insert power_ax, simp add: power_ax_def) 
   984 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   985 apply (blast, clarify) 
   986 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
   987 apply assumption
   988 apply (blast intro: cartprod_iff_lemma) 
   989 done
   990 
   991 lemma (in M_axioms) cartprod_closed_lemma:
   992      "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
   993 apply (simp del: cartprod_abs add: cartprod_iff)
   994 apply (insert power_ax, simp add: power_ax_def) 
   995 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   996 apply (blast, clarify) 
   997 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   998 apply (blast, clarify)
   999 apply (intro rexI exI conjI) 
  1000 prefer 5 apply (rule refl) 
  1001 prefer 3 apply assumption
  1002 prefer 3 apply assumption
  1003 apply (insert cartprod_separation [of A B], auto)
  1004 done
  1005 
  1006 text{*All the lemmas above are necessary because Powerset is not absolute.
  1007       I should have used Replacement instead!*}
  1008 lemma (in M_axioms) cartprod_closed [intro,simp]: 
  1009      "[| M(A); M(B) |] ==> M(A*B)"
  1010 by (frule cartprod_closed_lemma, assumption, force)
  1011 
  1012 lemma (in M_axioms) sum_closed [intro,simp]: 
  1013      "[| M(A); M(B) |] ==> M(A+B)"
  1014 by (simp add: sum_def)
  1015 
  1016 lemma (in M_axioms) sum_abs [simp]:
  1017      "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
  1018 by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
  1019 
  1020 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
  1021      "M(Inl(a)) <-> M(a)"
  1022 by (simp add: Inl_def) 
  1023 
  1024 lemma (in M_triv_axioms) Inl_abs [simp]:
  1025      "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
  1026 by (simp add: is_Inl_def Inl_def)
  1027 
  1028 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
  1029      "M(Inr(a)) <-> M(a)"
  1030 by (simp add: Inr_def) 
  1031 
  1032 lemma (in M_triv_axioms) Inr_abs [simp]:
  1033      "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
  1034 by (simp add: is_Inr_def Inr_def)
  1035 
  1036 
  1037 subsubsection {*converse of a relation*}
  1038 
  1039 lemma (in M_axioms) M_converse_iff:
  1040      "M(r) ==> 
  1041       converse(r) = 
  1042       {z \<in> Union(Union(r)) * Union(Union(r)). 
  1043        \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
  1044 apply (rule equalityI)
  1045  prefer 2 apply (blast dest: transM, clarify, simp) 
  1046 apply (simp add: Pair_def) 
  1047 apply (blast dest: transM) 
  1048 done
  1049 
  1050 lemma (in M_axioms) converse_closed [intro,simp]: 
  1051      "M(r) ==> M(converse(r))"
  1052 apply (simp add: M_converse_iff)
  1053 apply (insert converse_separation [of r], simp)
  1054 done
  1055 
  1056 lemma (in M_axioms) converse_abs [simp]: 
  1057      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
  1058 apply (simp add: is_converse_def)
  1059 apply (rule iffI)
  1060  prefer 2 apply blast 
  1061 apply (rule M_equalityI)
  1062   apply simp
  1063   apply (blast dest: transM)+
  1064 done
  1065 
  1066 
  1067 subsubsection {*image, preimage, domain, range*}
  1068 
  1069 lemma (in M_axioms) image_closed [intro,simp]: 
  1070      "[| M(A); M(r) |] ==> M(r``A)"
  1071 apply (simp add: image_iff_Collect)
  1072 apply (insert image_separation [of A r], simp) 
  1073 done
  1074 
  1075 lemma (in M_axioms) vimage_abs [simp]: 
  1076      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
  1077 apply (simp add: pre_image_def)
  1078 apply (rule iffI) 
  1079  apply (blast intro!: equalityI dest: transM, blast) 
  1080 done
  1081 
  1082 lemma (in M_axioms) vimage_closed [intro,simp]: 
  1083      "[| M(A); M(r) |] ==> M(r-``A)"
  1084 by (simp add: vimage_def)
  1085 
  1086 
  1087 subsubsection{*Domain, range and field*}
  1088 
  1089 lemma (in M_axioms) domain_abs [simp]: 
  1090      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
  1091 apply (simp add: is_domain_def) 
  1092 apply (blast intro!: equalityI dest: transM) 
  1093 done
  1094 
  1095 lemma (in M_axioms) domain_closed [intro,simp]: 
  1096      "M(r) ==> M(domain(r))"
  1097 apply (simp add: domain_eq_vimage)
  1098 done
  1099 
  1100 lemma (in M_axioms) range_abs [simp]: 
  1101      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
  1102 apply (simp add: is_range_def)
  1103 apply (blast intro!: equalityI dest: transM)
  1104 done
  1105 
  1106 lemma (in M_axioms) range_closed [intro,simp]: 
  1107      "M(r) ==> M(range(r))"
  1108 apply (simp add: range_eq_image)
  1109 done
  1110 
  1111 lemma (in M_axioms) field_abs [simp]: 
  1112      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
  1113 by (simp add: domain_closed range_closed is_field_def field_def)
  1114 
  1115 lemma (in M_axioms) field_closed [intro,simp]: 
  1116      "M(r) ==> M(field(r))"
  1117 by (simp add: domain_closed range_closed Un_closed field_def) 
  1118 
  1119 
  1120 subsubsection{*Relations, functions and application*}
  1121 
  1122 lemma (in M_axioms) relation_abs [simp]: 
  1123      "M(r) ==> is_relation(M,r) <-> relation(r)"
  1124 apply (simp add: is_relation_def relation_def) 
  1125 apply (blast dest!: bspec dest: pair_components_in_M)+
  1126 done
  1127 
  1128 lemma (in M_axioms) function_abs [simp]: 
  1129      "M(r) ==> is_function(M,r) <-> function(r)"
  1130 apply (simp add: is_function_def function_def, safe) 
  1131    apply (frule transM, assumption) 
  1132   apply (blast dest: pair_components_in_M)+
  1133 done
  1134 
  1135 lemma (in M_axioms) apply_closed [intro,simp]: 
  1136      "[|M(f); M(a)|] ==> M(f`a)"
  1137 by (simp add: apply_def)
  1138 
  1139 lemma (in M_axioms) apply_abs [simp]: 
  1140      "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
  1141 apply (simp add: fun_apply_def apply_def, blast) 
  1142 done
  1143 
  1144 lemma (in M_axioms) typed_function_abs [simp]: 
  1145      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
  1146 apply (auto simp add: typed_function_def relation_def Pi_iff) 
  1147 apply (blast dest: pair_components_in_M)+
  1148 done
  1149 
  1150 lemma (in M_axioms) injection_abs [simp]: 
  1151      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
  1152 apply (simp add: injection_def apply_iff inj_def apply_closed)
  1153 apply (blast dest: transM [of _ A]) 
  1154 done
  1155 
  1156 lemma (in M_axioms) surjection_abs [simp]: 
  1157      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
  1158 by (simp add: surjection_def surj_def)
  1159 
  1160 lemma (in M_axioms) bijection_abs [simp]: 
  1161      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
  1162 by (simp add: bijection_def bij_def)
  1163 
  1164 
  1165 subsubsection{*Composition of relations*}
  1166 
  1167 lemma (in M_axioms) M_comp_iff:
  1168      "[| M(r); M(s) |] 
  1169       ==> r O s = 
  1170           {xz \<in> domain(s) * range(r).  
  1171             \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r}"
  1172 apply (simp add: comp_def)
  1173 apply (rule equalityI) 
  1174  apply clarify 
  1175  apply simp 
  1176  apply  (blast dest:  transM)+
  1177 done
  1178 
  1179 lemma (in M_axioms) comp_closed [intro,simp]: 
  1180      "[| M(r); M(s) |] ==> M(r O s)"
  1181 apply (simp add: M_comp_iff)
  1182 apply (insert comp_separation [of r s], simp) 
  1183 done
  1184 
  1185 lemma (in M_axioms) composition_abs [simp]: 
  1186      "[| M(r); M(s); M(t) |] 
  1187       ==> composition(M,r,s,t) <-> t = r O s"
  1188 apply safe
  1189  txt{*Proving @{term "composition(M, r, s, r O s)"}*}
  1190  prefer 2 
  1191  apply (simp add: composition_def comp_def)
  1192  apply (blast dest: transM) 
  1193 txt{*Opposite implication*}
  1194 apply (rule M_equalityI)
  1195   apply (simp add: composition_def comp_def)
  1196   apply (blast del: allE dest: transM)+
  1197 done
  1198 
  1199 text{*no longer needed*}
  1200 lemma (in M_axioms) restriction_is_function: 
  1201      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
  1202       ==> function(z)"
  1203 apply (rotate_tac 1)
  1204 apply (simp add: restriction_def ball_iff_equiv) 
  1205 apply (unfold function_def, blast) 
  1206 done
  1207 
  1208 lemma (in M_axioms) restriction_abs [simp]: 
  1209      "[| M(f); M(A); M(z) |] 
  1210       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  1211 apply (simp add: ball_iff_equiv restriction_def restrict_def)
  1212 apply (blast intro!: equalityI dest: transM) 
  1213 done
  1214 
  1215 
  1216 lemma (in M_axioms) M_restrict_iff:
  1217      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  1218 by (simp add: restrict_def, blast dest: transM)
  1219 
  1220 lemma (in M_axioms) restrict_closed [intro,simp]: 
  1221      "[| M(A); M(r) |] ==> M(restrict(r,A))"
  1222 apply (simp add: M_restrict_iff)
  1223 apply (insert restrict_separation [of A], simp) 
  1224 done
  1225 
  1226 lemma (in M_axioms) Inter_abs [simp]: 
  1227      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  1228 apply (simp add: big_inter_def Inter_def) 
  1229 apply (blast intro!: equalityI dest: transM) 
  1230 done
  1231 
  1232 lemma (in M_axioms) Inter_closed [intro,simp]:
  1233      "M(A) ==> M(Inter(A))"
  1234 by (insert Inter_separation, simp add: Inter_def)
  1235 
  1236 lemma (in M_axioms) Int_closed [intro,simp]:
  1237      "[| M(A); M(B) |] ==> M(A Int B)"
  1238 apply (subgoal_tac "M({A,B})")
  1239 apply (frule Inter_closed, force+) 
  1240 done
  1241 
  1242 lemma (in M_axioms) Diff_closed [intro,simp]:
  1243      "[|M(A); M(B)|] ==> M(A-B)"
  1244 by (insert Diff_separation, simp add: Diff_def)
  1245 
  1246 subsubsection{*Some Facts About Separation Axioms*}
  1247 
  1248 lemma (in M_axioms) separation_conj:
  1249      "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
  1250 by (simp del: separation_closed
  1251          add: separation_iff Collect_Int_Collect_eq [symmetric]) 
  1252 
  1253 (*???equalities*)
  1254 lemma Collect_Un_Collect_eq:
  1255      "Collect(A,P) Un Collect(A,Q) = Collect(A, %x. P(x) | Q(x))"
  1256 by blast
  1257 
  1258 lemma Diff_Collect_eq:
  1259      "A - Collect(A,P) = Collect(A, %x. ~ P(x))"
  1260 by blast
  1261 
  1262 lemma (in M_triv_axioms) Collect_rall_eq:
  1263      "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) = 
  1264                (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
  1265 apply simp 
  1266 apply (blast intro!: equalityI dest: transM) 
  1267 done
  1268 
  1269 lemma (in M_axioms) separation_disj:
  1270      "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
  1271 by (simp del: separation_closed
  1272          add: separation_iff Collect_Un_Collect_eq [symmetric]) 
  1273 
  1274 lemma (in M_axioms) separation_neg:
  1275      "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
  1276 by (simp del: separation_closed
  1277          add: separation_iff Diff_Collect_eq [symmetric]) 
  1278 
  1279 lemma (in M_axioms) separation_imp:
  1280      "[|separation(M,P); separation(M,Q)|] 
  1281       ==> separation(M, \<lambda>z. P(z) --> Q(z))"
  1282 by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric]) 
  1283 
  1284 text{*This result is a hint of how little can be done without the Reflection 
  1285   Theorem.  The quantifier has to be bounded by a set.  We also need another
  1286   instance of Separation!*}
  1287 lemma (in M_axioms) separation_rall:
  1288      "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y)); 
  1289         \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
  1290       ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))" 
  1291 apply (simp del: separation_closed rall_abs
  1292          add: separation_iff Collect_rall_eq) 
  1293 apply (blast intro!: Inter_closed RepFun_closed dest: transM) 
  1294 done
  1295 
  1296 
  1297 subsubsection{*Functions and function space*}
  1298 
  1299 text{*M contains all finite functions*}
  1300 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
  1301      "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
  1302 apply (induct_tac n, simp)
  1303 apply (rule ballI)  
  1304 apply (simp add: succ_def) 
  1305 apply (frule fun_cons_restrict_eq)
  1306 apply (erule ssubst) 
  1307 apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
  1308  apply (simp add: cons_closed nat_into_M apply_closed) 
  1309 apply (blast intro: apply_funtype transM restrict_type2) 
  1310 done
  1311 
  1312 lemma (in M_axioms) finite_fun_closed [rule_format]: 
  1313      "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
  1314 by (blast intro: finite_fun_closed_lemma) 
  1315 
  1316 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
  1317 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  1318 lemma (in M_axioms) is_funspace_abs [simp]:
  1319      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  1320 apply (simp add: is_funspace_def)
  1321 apply (rule iffI)
  1322  prefer 2 apply blast 
  1323 apply (rule M_equalityI)
  1324   apply simp_all
  1325 done
  1326 
  1327 lemma (in M_axioms) succ_fun_eq2:
  1328      "[|M(B); M(n->B)|] ==>
  1329       succ(n) -> B = 
  1330       \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  1331 apply (simp add: succ_fun_eq)
  1332 apply (blast dest: transM)  
  1333 done
  1334 
  1335 lemma (in M_axioms) funspace_succ:
  1336      "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  1337 apply (insert funspace_succ_replacement [of n], simp) 
  1338 apply (force simp add: succ_fun_eq2 univalent_def) 
  1339 done
  1340 
  1341 text{*@{term M} contains all finite function spaces.  Needed to prove the
  1342 absoluteness of transitive closure.*}
  1343 lemma (in M_axioms) finite_funspace_closed [intro,simp]:
  1344      "[|n\<in>nat; M(B)|] ==> M(n->B)"
  1345 apply (induct_tac n, simp)
  1346 apply (simp add: funspace_succ nat_into_M) 
  1347 done
  1348 
  1349 
  1350 subsection{*Relativization and Absoluteness for Boolean Operators*}
  1351 
  1352 constdefs
  1353   is_bool_of_o :: "[i=>o, o, i] => o"
  1354    "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
  1355 
  1356   is_not :: "[i=>o, i, i] => o"
  1357    "is_not(M,a,z) == (number1(M,a)  & empty(M,z)) | 
  1358                      (~number1(M,a) & number1(M,z))"
  1359 
  1360   is_and :: "[i=>o, i, i, i] => o"
  1361    "is_and(M,a,b,z) == (number1(M,a)  & z=b) | 
  1362                        (~number1(M,a) & empty(M,z))"
  1363 
  1364   is_or :: "[i=>o, i, i, i] => o"
  1365    "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) | 
  1366                       (~number1(M,a) & z=b)"
  1367 
  1368 lemma (in M_triv_axioms) bool_of_o_abs [simp]: 
  1369      "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)" 
  1370 by (simp add: is_bool_of_o_def bool_of_o_def) 
  1371 
  1372 
  1373 lemma (in M_triv_axioms) not_abs [simp]: 
  1374      "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)"
  1375 by (simp add: Bool.not_def cond_def is_not_def) 
  1376 
  1377 lemma (in M_triv_axioms) and_abs [simp]: 
  1378      "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b"
  1379 by (simp add: Bool.and_def cond_def is_and_def) 
  1380 
  1381 lemma (in M_triv_axioms) or_abs [simp]: 
  1382      "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b"
  1383 by (simp add: Bool.or_def cond_def is_or_def)
  1384 
  1385 
  1386 lemma (in M_triv_axioms) bool_of_o_closed [intro,simp]:
  1387      "M(bool_of_o(P))"
  1388 by (simp add: bool_of_o_def) 
  1389 
  1390 lemma (in M_triv_axioms) and_closed [intro,simp]:
  1391      "[| M(p); M(q) |] ==> M(p and q)"
  1392 by (simp add: and_def cond_def) 
  1393 
  1394 lemma (in M_triv_axioms) or_closed [intro,simp]:
  1395      "[| M(p); M(q) |] ==> M(p or q)"
  1396 by (simp add: or_def cond_def) 
  1397 
  1398 lemma (in M_triv_axioms) not_closed [intro,simp]:
  1399      "M(p) ==> M(not(p))"
  1400 by (simp add: Bool.not_def cond_def) 
  1401 
  1402 
  1403 subsection{*Relativization and Absoluteness for List Operators*}
  1404 
  1405 constdefs
  1406 
  1407   is_Nil :: "[i=>o, i] => o"
  1408      --{* because @{term "[] \<equiv> Inl(0)"}*}
  1409     "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
  1410 
  1411   is_Cons :: "[i=>o,i,i,i] => o"
  1412      --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
  1413     "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
  1414 
  1415 
  1416 lemma (in M_triv_axioms) Nil_in_M [intro,simp]: "M(Nil)"
  1417 by (simp add: Nil_def)
  1418 
  1419 lemma (in M_triv_axioms) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
  1420 by (simp add: is_Nil_def Nil_def)
  1421 
  1422 lemma (in M_triv_axioms) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
  1423 by (simp add: Cons_def) 
  1424 
  1425 lemma (in M_triv_axioms) Cons_abs [simp]:
  1426      "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
  1427 by (simp add: is_Cons_def Cons_def)
  1428 
  1429 
  1430 constdefs
  1431 
  1432   quasilist :: "i => o"
  1433     "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
  1434 
  1435   is_quasilist :: "[i=>o,i] => o"
  1436     "is_quasilist(M,z) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))"
  1437 
  1438   list_case' :: "[i, [i,i]=>i, i] => i"
  1439     --{*A version of @{term list_case} that's always defined.*}
  1440     "list_case'(a,b,xs) == 
  1441        if quasilist(xs) then list_case(a,b,xs) else 0"  
  1442 
  1443   is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
  1444     --{*Returns 0 for non-lists*}
  1445     "is_list_case(M, a, is_b, xs, z) == 
  1446        (is_Nil(M,xs) --> z=a) &
  1447        (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
  1448        (is_quasilist(M,xs) | empty(M,z))"
  1449 
  1450   hd' :: "i => i"
  1451     --{*A version of @{term hd} that's always defined.*}
  1452     "hd'(xs) == if quasilist(xs) then hd(xs) else 0"  
  1453 
  1454   tl' :: "i => i"
  1455     --{*A version of @{term tl} that's always defined.*}
  1456     "tl'(xs) == if quasilist(xs) then tl(xs) else 0"  
  1457 
  1458   is_hd :: "[i=>o,i,i] => o"
  1459      --{* @{term "hd([]) = 0"} no constraints if not a list.
  1460           Avoiding implication prevents the simplifier's looping.*}
  1461     "is_hd(M,xs,H) == 
  1462        (is_Nil(M,xs) --> empty(M,H)) &
  1463        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
  1464        (is_quasilist(M,xs) | empty(M,H))"
  1465 
  1466   is_tl :: "[i=>o,i,i] => o"
  1467      --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
  1468     "is_tl(M,xs,T) == 
  1469        (is_Nil(M,xs) --> T=xs) &
  1470        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
  1471        (is_quasilist(M,xs) | empty(M,T))"
  1472 
  1473 subsubsection{*@{term quasilist}: For Case-Splitting with @{term list_case'}*}
  1474 
  1475 lemma [iff]: "quasilist(Nil)"
  1476 by (simp add: quasilist_def)
  1477 
  1478 lemma [iff]: "quasilist(Cons(x,l))"
  1479 by (simp add: quasilist_def)
  1480 
  1481 lemma list_imp_quasilist: "l \<in> list(A) ==> quasilist(l)"
  1482 by (erule list.cases, simp_all)
  1483 
  1484 subsubsection{*@{term list_case'}, the Modified Version of @{term list_case}*}
  1485 
  1486 lemma list_case'_Nil [simp]: "list_case'(a,b,Nil) = a"
  1487 by (simp add: list_case'_def quasilist_def)
  1488 
  1489 lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)"
  1490 by (simp add: list_case'_def quasilist_def)
  1491 
  1492 lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0" 
  1493 by (simp add: quasilist_def list_case'_def) 
  1494 
  1495 lemma list_case'_eq_list_case [simp]:
  1496      "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
  1497 by (erule list.cases, simp_all)
  1498 
  1499 lemma (in M_axioms) list_case'_closed [intro,simp]:
  1500   "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
  1501 apply (case_tac "quasilist(k)") 
  1502  apply (simp add: quasilist_def, force) 
  1503 apply (simp add: non_list_case) 
  1504 done
  1505 
  1506 lemma (in M_triv_axioms) quasilist_abs [simp]: 
  1507      "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
  1508 by (auto simp add: is_quasilist_def quasilist_def)
  1509 
  1510 lemma (in M_triv_axioms) list_case_abs [simp]: 
  1511      "[| relativize2(M,is_b,b); M(k); M(z) |] 
  1512       ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
  1513 apply (case_tac "quasilist(k)") 
  1514  prefer 2 
  1515  apply (simp add: is_list_case_def non_list_case) 
  1516  apply (force simp add: quasilist_def) 
  1517 apply (simp add: quasilist_def is_list_case_def)
  1518 apply (elim disjE exE) 
  1519  apply (simp_all add: relativize2_def) 
  1520 done
  1521 
  1522 
  1523 subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
  1524 
  1525 lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
  1526 by (simp add: is_hd_def)
  1527 
  1528 lemma (in M_triv_axioms) is_hd_Cons:
  1529      "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
  1530 by (force simp add: is_hd_def) 
  1531 
  1532 lemma (in M_triv_axioms) hd_abs [simp]:
  1533      "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
  1534 apply (simp add: hd'_def)
  1535 apply (intro impI conjI)
  1536  prefer 2 apply (force simp add: is_hd_def) 
  1537 apply (simp add: quasilist_def is_hd_def)
  1538 apply (elim disjE exE, auto)
  1539 done 
  1540 
  1541 lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
  1542 by (simp add: is_tl_def)
  1543 
  1544 lemma (in M_triv_axioms) is_tl_Cons:
  1545      "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
  1546 by (force simp add: is_tl_def) 
  1547 
  1548 lemma (in M_triv_axioms) tl_abs [simp]:
  1549      "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
  1550 apply (simp add: tl'_def)
  1551 apply (intro impI conjI)
  1552  prefer 2 apply (force simp add: is_tl_def) 
  1553 apply (simp add: quasilist_def is_tl_def)
  1554 apply (elim disjE exE, auto)
  1555 done 
  1556 
  1557 lemma (in M_triv_axioms) relativize1_tl: "relativize1(M, is_tl(M), tl')"  
  1558 by (simp add: relativize1_def)
  1559 
  1560 lemma hd'_Nil: "hd'([]) = 0"
  1561 by (simp add: hd'_def)
  1562 
  1563 lemma hd'_Cons: "hd'(Cons(a,l)) = a"
  1564 by (simp add: hd'_def)
  1565 
  1566 lemma tl'_Nil: "tl'([]) = []"
  1567 by (simp add: tl'_def)
  1568 
  1569 lemma tl'_Cons: "tl'(Cons(a,l)) = l"
  1570 by (simp add: tl'_def)
  1571 
  1572 lemma iterates_tl_Nil: "n \<in> nat ==> tl'^n ([]) = []"
  1573 apply (induct_tac n) 
  1574 apply (simp_all add: tl'_Nil) 
  1575 done
  1576 
  1577 lemma (in M_axioms) tl'_closed: "M(x) ==> M(tl'(x))"
  1578 apply (simp add: tl'_def)
  1579 apply (force simp add: quasilist_def)
  1580 done
  1581 
  1582 
  1583 end