src/ZF/Constructible/Relative.thy
author paulson
Wed Aug 28 13:08:34 2002 +0200 (2002-08-28)
changeset 13543 2b3c7e319d82
parent 13535 007559e981c7
child 13563 7d6c9817c432
permissions -rw-r--r--
completion of the consistency proof for AC
     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 (unfold Limit_def limit_ordinal_def) 
   824 apply (simp add: Ord_0_lt_iff) 
   825 apply (simp add: lt_def, blast) 
   826 done
   827 
   828 lemma (in M_triv_axioms) successor_ordinal_abs [simp]: 
   829      "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   830 apply (simp add: successor_ordinal_def, safe)
   831 apply (drule Ord_cases_disj, auto) 
   832 done
   833 
   834 lemma finite_Ord_is_nat:
   835       "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   836 by (induct a rule: trans_induct3, simp_all)
   837 
   838 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   839 by (induct a rule: nat_induct, auto)
   840 
   841 lemma (in M_triv_axioms) finite_ordinal_abs [simp]: 
   842      "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   843 apply (simp add: finite_ordinal_def)
   844 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   845              dest: Ord_trans naturals_not_limit)
   846 done
   847 
   848 lemma Limit_non_Limit_implies_nat:
   849      "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   850 apply (rule le_anti_sym) 
   851 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   852  apply (simp add: lt_def)  
   853  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   854 apply (erule nat_le_Limit)
   855 done
   856 
   857 lemma (in M_triv_axioms) omega_abs [simp]: 
   858      "M(a) ==> omega(M,a) <-> a = nat"
   859 apply (simp add: omega_def) 
   860 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   861 done
   862 
   863 lemma (in M_triv_axioms) number1_abs [simp]: 
   864      "M(a) ==> number1(M,a) <-> a = 1"
   865 by (simp add: number1_def) 
   866 
   867 lemma (in M_triv_axioms) number2_abs [simp]: 
   868      "M(a) ==> number2(M,a) <-> a = succ(1)"
   869 by (simp add: number2_def) 
   870 
   871 lemma (in M_triv_axioms) number3_abs [simp]: 
   872      "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   873 by (simp add: number3_def) 
   874 
   875 text{*Kunen continued to 20...*}
   876 
   877 (*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   878   but the recursion variable must stay unchanged.  But then the recursion
   879   equations only hold for x\<in>nat (or in some other set) and not for the 
   880   whole of the class M.
   881   consts
   882     natnumber_aux :: "[i=>o,i] => i"
   883 
   884   primrec
   885       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   886       "natnumber_aux(M,succ(n)) = 
   887 	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   888 		     then 1 else 0)"
   889 
   890   constdefs
   891     natnumber :: "[i=>o,i,i] => o"
   892       "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   893 
   894   lemma (in M_triv_axioms) [simp]: 
   895        "natnumber(M,0,x) == x=0"
   896 *)
   897 
   898 subsection{*Some instances of separation and strong replacement*}
   899 
   900 locale M_axioms = M_triv_axioms +
   901 assumes Inter_separation:
   902      "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
   903   and Diff_separation:
   904      "M(B) ==> separation(M, \<lambda>x. x \<notin> B)"
   905   and cartprod_separation:
   906      "[| M(A); M(B) |] 
   907       ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
   908   and image_separation:
   909      "[| M(A); M(r) |] 
   910       ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
   911   and converse_separation:
   912      "M(r) ==> separation(M, 
   913          \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
   914   and restrict_separation:
   915      "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
   916   and comp_separation:
   917      "[| M(r); M(s) |]
   918       ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   919 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   920                   xy\<in>s & yz\<in>r)"
   921   and pred_separation:
   922      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
   923   and Memrel_separation:
   924      "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
   925   and funspace_succ_replacement:
   926      "M(n) ==> 
   927       strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M]. 
   928                 pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
   929                 upair(M,cnbf,cnbf,z))"
   930   and well_ord_iso_separation:
   931      "[| M(A); M(f); M(r) |] 
   932       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M]. 
   933 		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   934   and obase_separation:
   935      --{*part of the order type formalization*}
   936      "[| M(A); M(r) |] 
   937       ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   938 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   939 	     order_isomorphism(M,par,r,x,mx,g))"
   940   and obase_equals_separation:
   941      "[| M(A); M(r) |] 
   942       ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
   943 			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
   944 			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   945 			      order_isomorphism(M,pxr,r,y,my,g))))"
   946   and omap_replacement:
   947      "[| M(A); M(r) |] 
   948       ==> strong_replacement(M,
   949              \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   950 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   951 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   952   and is_recfun_separation:
   953      --{*for well-founded recursion*}
   954      "[| M(r); M(f); M(g); M(a); M(b) |] 
   955      ==> separation(M, 
   956             \<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
   957                 pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
   958                 (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
   959                                    fx \<noteq> gx))"
   960 
   961 lemma (in M_axioms) cartprod_iff_lemma:
   962      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   963          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   964        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   965 apply (simp add: powerset_def) 
   966 apply (rule equalityI, clarify, simp)
   967  apply (frule transM, assumption) 
   968  apply (frule transM, assumption, simp) 
   969  apply blast 
   970 apply clarify
   971 apply (frule transM, assumption, force) 
   972 done
   973 
   974 lemma (in M_axioms) cartprod_iff:
   975      "[| M(A); M(B); M(C) |] 
   976       ==> cartprod(M,A,B,C) <-> 
   977           (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   978                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
   979 apply (simp add: Pair_def cartprod_def, safe)
   980 defer 1 
   981   apply (simp add: powerset_def) 
   982  apply blast 
   983 txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   984 apply (insert power_ax, simp add: power_ax_def) 
   985 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   986 apply (blast, clarify) 
   987 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
   988 apply assumption
   989 apply (blast intro: cartprod_iff_lemma) 
   990 done
   991 
   992 lemma (in M_axioms) cartprod_closed_lemma:
   993      "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
   994 apply (simp del: cartprod_abs add: cartprod_iff)
   995 apply (insert power_ax, simp add: power_ax_def) 
   996 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   997 apply (blast, clarify) 
   998 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   999 apply (blast, clarify)
  1000 apply (intro rexI exI conjI) 
  1001 prefer 5 apply (rule refl) 
  1002 prefer 3 apply assumption
  1003 prefer 3 apply assumption
  1004 apply (insert cartprod_separation [of A B], auto)
  1005 done
  1006 
  1007 text{*All the lemmas above are necessary because Powerset is not absolute.
  1008       I should have used Replacement instead!*}
  1009 lemma (in M_axioms) cartprod_closed [intro,simp]: 
  1010      "[| M(A); M(B) |] ==> M(A*B)"
  1011 by (frule cartprod_closed_lemma, assumption, force)
  1012 
  1013 lemma (in M_axioms) sum_closed [intro,simp]: 
  1014      "[| M(A); M(B) |] ==> M(A+B)"
  1015 by (simp add: sum_def)
  1016 
  1017 lemma (in M_axioms) sum_abs [simp]:
  1018      "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
  1019 by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
  1020 
  1021 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
  1022      "M(Inl(a)) <-> M(a)"
  1023 by (simp add: Inl_def) 
  1024 
  1025 lemma (in M_triv_axioms) Inl_abs [simp]:
  1026      "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
  1027 by (simp add: is_Inl_def Inl_def)
  1028 
  1029 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
  1030      "M(Inr(a)) <-> M(a)"
  1031 by (simp add: Inr_def) 
  1032 
  1033 lemma (in M_triv_axioms) Inr_abs [simp]:
  1034      "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
  1035 by (simp add: is_Inr_def Inr_def)
  1036 
  1037 
  1038 subsubsection {*converse of a relation*}
  1039 
  1040 lemma (in M_axioms) M_converse_iff:
  1041      "M(r) ==> 
  1042       converse(r) = 
  1043       {z \<in> Union(Union(r)) * Union(Union(r)). 
  1044        \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
  1045 apply (rule equalityI)
  1046  prefer 2 apply (blast dest: transM, clarify, simp) 
  1047 apply (simp add: Pair_def) 
  1048 apply (blast dest: transM) 
  1049 done
  1050 
  1051 lemma (in M_axioms) converse_closed [intro,simp]: 
  1052      "M(r) ==> M(converse(r))"
  1053 apply (simp add: M_converse_iff)
  1054 apply (insert converse_separation [of r], simp)
  1055 done
  1056 
  1057 lemma (in M_axioms) converse_abs [simp]: 
  1058      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
  1059 apply (simp add: is_converse_def)
  1060 apply (rule iffI)
  1061  prefer 2 apply blast 
  1062 apply (rule M_equalityI)
  1063   apply simp
  1064   apply (blast dest: transM)+
  1065 done
  1066 
  1067 
  1068 subsubsection {*image, preimage, domain, range*}
  1069 
  1070 lemma (in M_axioms) image_closed [intro,simp]: 
  1071      "[| M(A); M(r) |] ==> M(r``A)"
  1072 apply (simp add: image_iff_Collect)
  1073 apply (insert image_separation [of A r], simp) 
  1074 done
  1075 
  1076 lemma (in M_axioms) vimage_abs [simp]: 
  1077      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
  1078 apply (simp add: pre_image_def)
  1079 apply (rule iffI) 
  1080  apply (blast intro!: equalityI dest: transM, blast) 
  1081 done
  1082 
  1083 lemma (in M_axioms) vimage_closed [intro,simp]: 
  1084      "[| M(A); M(r) |] ==> M(r-``A)"
  1085 by (simp add: vimage_def)
  1086 
  1087 
  1088 subsubsection{*Domain, range and field*}
  1089 
  1090 lemma (in M_axioms) domain_abs [simp]: 
  1091      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
  1092 apply (simp add: is_domain_def) 
  1093 apply (blast intro!: equalityI dest: transM) 
  1094 done
  1095 
  1096 lemma (in M_axioms) domain_closed [intro,simp]: 
  1097      "M(r) ==> M(domain(r))"
  1098 apply (simp add: domain_eq_vimage)
  1099 done
  1100 
  1101 lemma (in M_axioms) range_abs [simp]: 
  1102      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
  1103 apply (simp add: is_range_def)
  1104 apply (blast intro!: equalityI dest: transM)
  1105 done
  1106 
  1107 lemma (in M_axioms) range_closed [intro,simp]: 
  1108      "M(r) ==> M(range(r))"
  1109 apply (simp add: range_eq_image)
  1110 done
  1111 
  1112 lemma (in M_axioms) field_abs [simp]: 
  1113      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
  1114 by (simp add: domain_closed range_closed is_field_def field_def)
  1115 
  1116 lemma (in M_axioms) field_closed [intro,simp]: 
  1117      "M(r) ==> M(field(r))"
  1118 by (simp add: domain_closed range_closed Un_closed field_def) 
  1119 
  1120 
  1121 subsubsection{*Relations, functions and application*}
  1122 
  1123 lemma (in M_axioms) relation_abs [simp]: 
  1124      "M(r) ==> is_relation(M,r) <-> relation(r)"
  1125 apply (simp add: is_relation_def relation_def) 
  1126 apply (blast dest!: bspec dest: pair_components_in_M)+
  1127 done
  1128 
  1129 lemma (in M_axioms) function_abs [simp]: 
  1130      "M(r) ==> is_function(M,r) <-> function(r)"
  1131 apply (simp add: is_function_def function_def, safe) 
  1132    apply (frule transM, assumption) 
  1133   apply (blast dest: pair_components_in_M)+
  1134 done
  1135 
  1136 lemma (in M_axioms) apply_closed [intro,simp]: 
  1137      "[|M(f); M(a)|] ==> M(f`a)"
  1138 by (simp add: apply_def)
  1139 
  1140 lemma (in M_axioms) apply_abs [simp]: 
  1141      "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
  1142 apply (simp add: fun_apply_def apply_def, blast) 
  1143 done
  1144 
  1145 lemma (in M_axioms) typed_function_abs [simp]: 
  1146      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
  1147 apply (auto simp add: typed_function_def relation_def Pi_iff) 
  1148 apply (blast dest: pair_components_in_M)+
  1149 done
  1150 
  1151 lemma (in M_axioms) injection_abs [simp]: 
  1152      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
  1153 apply (simp add: injection_def apply_iff inj_def apply_closed)
  1154 apply (blast dest: transM [of _ A]) 
  1155 done
  1156 
  1157 lemma (in M_axioms) surjection_abs [simp]: 
  1158      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
  1159 by (simp add: surjection_def surj_def)
  1160 
  1161 lemma (in M_axioms) bijection_abs [simp]: 
  1162      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
  1163 by (simp add: bijection_def bij_def)
  1164 
  1165 
  1166 subsubsection{*Composition of relations*}
  1167 
  1168 lemma (in M_axioms) M_comp_iff:
  1169      "[| M(r); M(s) |] 
  1170       ==> r O s = 
  1171           {xz \<in> domain(s) * range(r).  
  1172             \<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}"
  1173 apply (simp add: comp_def)
  1174 apply (rule equalityI) 
  1175  apply clarify 
  1176  apply simp 
  1177  apply  (blast dest:  transM)+
  1178 done
  1179 
  1180 lemma (in M_axioms) comp_closed [intro,simp]: 
  1181      "[| M(r); M(s) |] ==> M(r O s)"
  1182 apply (simp add: M_comp_iff)
  1183 apply (insert comp_separation [of r s], simp) 
  1184 done
  1185 
  1186 lemma (in M_axioms) composition_abs [simp]: 
  1187      "[| M(r); M(s); M(t) |] 
  1188       ==> composition(M,r,s,t) <-> t = r O s"
  1189 apply safe
  1190  txt{*Proving @{term "composition(M, r, s, r O s)"}*}
  1191  prefer 2 
  1192  apply (simp add: composition_def comp_def)
  1193  apply (blast dest: transM) 
  1194 txt{*Opposite implication*}
  1195 apply (rule M_equalityI)
  1196   apply (simp add: composition_def comp_def)
  1197   apply (blast del: allE dest: transM)+
  1198 done
  1199 
  1200 text{*no longer needed*}
  1201 lemma (in M_axioms) restriction_is_function: 
  1202      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
  1203       ==> function(z)"
  1204 apply (rotate_tac 1)
  1205 apply (simp add: restriction_def ball_iff_equiv) 
  1206 apply (unfold function_def, blast) 
  1207 done
  1208 
  1209 lemma (in M_axioms) restriction_abs [simp]: 
  1210      "[| M(f); M(A); M(z) |] 
  1211       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  1212 apply (simp add: ball_iff_equiv restriction_def restrict_def)
  1213 apply (blast intro!: equalityI dest: transM) 
  1214 done
  1215 
  1216 
  1217 lemma (in M_axioms) M_restrict_iff:
  1218      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  1219 by (simp add: restrict_def, blast dest: transM)
  1220 
  1221 lemma (in M_axioms) restrict_closed [intro,simp]: 
  1222      "[| M(A); M(r) |] ==> M(restrict(r,A))"
  1223 apply (simp add: M_restrict_iff)
  1224 apply (insert restrict_separation [of A], simp) 
  1225 done
  1226 
  1227 lemma (in M_axioms) Inter_abs [simp]: 
  1228      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  1229 apply (simp add: big_inter_def Inter_def) 
  1230 apply (blast intro!: equalityI dest: transM) 
  1231 done
  1232 
  1233 lemma (in M_axioms) Inter_closed [intro,simp]:
  1234      "M(A) ==> M(Inter(A))"
  1235 by (insert Inter_separation, simp add: Inter_def)
  1236 
  1237 lemma (in M_axioms) Int_closed [intro,simp]:
  1238      "[| M(A); M(B) |] ==> M(A Int B)"
  1239 apply (subgoal_tac "M({A,B})")
  1240 apply (frule Inter_closed, force+) 
  1241 done
  1242 
  1243 lemma (in M_axioms) Diff_closed [intro,simp]:
  1244      "[|M(A); M(B)|] ==> M(A-B)"
  1245 by (insert Diff_separation, simp add: Diff_def)
  1246 
  1247 subsubsection{*Some Facts About Separation Axioms*}
  1248 
  1249 lemma (in M_axioms) separation_conj:
  1250      "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
  1251 by (simp del: separation_closed
  1252          add: separation_iff Collect_Int_Collect_eq [symmetric]) 
  1253 
  1254 (*???equalities*)
  1255 lemma Collect_Un_Collect_eq:
  1256      "Collect(A,P) Un Collect(A,Q) = Collect(A, %x. P(x) | Q(x))"
  1257 by blast
  1258 
  1259 lemma Diff_Collect_eq:
  1260      "A - Collect(A,P) = Collect(A, %x. ~ P(x))"
  1261 by blast
  1262 
  1263 lemma (in M_triv_axioms) Collect_rall_eq:
  1264      "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) = 
  1265                (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
  1266 apply simp 
  1267 apply (blast intro!: equalityI dest: transM) 
  1268 done
  1269 
  1270 lemma (in M_axioms) separation_disj:
  1271      "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
  1272 by (simp del: separation_closed
  1273          add: separation_iff Collect_Un_Collect_eq [symmetric]) 
  1274 
  1275 lemma (in M_axioms) separation_neg:
  1276      "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
  1277 by (simp del: separation_closed
  1278          add: separation_iff Diff_Collect_eq [symmetric]) 
  1279 
  1280 lemma (in M_axioms) separation_imp:
  1281      "[|separation(M,P); separation(M,Q)|] 
  1282       ==> separation(M, \<lambda>z. P(z) --> Q(z))"
  1283 by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric]) 
  1284 
  1285 text{*This result is a hint of how little can be done without the Reflection 
  1286   Theorem.  The quantifier has to be bounded by a set.  We also need another
  1287   instance of Separation!*}
  1288 lemma (in M_axioms) separation_rall:
  1289      "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y)); 
  1290         \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
  1291       ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))" 
  1292 apply (simp del: separation_closed rall_abs
  1293          add: separation_iff Collect_rall_eq) 
  1294 apply (blast intro!: Inter_closed RepFun_closed dest: transM) 
  1295 done
  1296 
  1297 
  1298 subsubsection{*Functions and function space*}
  1299 
  1300 text{*M contains all finite functions*}
  1301 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
  1302      "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
  1303 apply (induct_tac n, simp)
  1304 apply (rule ballI)  
  1305 apply (simp add: succ_def) 
  1306 apply (frule fun_cons_restrict_eq)
  1307 apply (erule ssubst) 
  1308 apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
  1309  apply (simp add: cons_closed nat_into_M apply_closed) 
  1310 apply (blast intro: apply_funtype transM restrict_type2) 
  1311 done
  1312 
  1313 lemma (in M_axioms) finite_fun_closed [rule_format]: 
  1314      "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
  1315 by (blast intro: finite_fun_closed_lemma) 
  1316 
  1317 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
  1318 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  1319 lemma (in M_axioms) is_funspace_abs [simp]:
  1320      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  1321 apply (simp add: is_funspace_def)
  1322 apply (rule iffI)
  1323  prefer 2 apply blast 
  1324 apply (rule M_equalityI)
  1325   apply simp_all
  1326 done
  1327 
  1328 lemma (in M_axioms) succ_fun_eq2:
  1329      "[|M(B); M(n->B)|] ==>
  1330       succ(n) -> B = 
  1331       \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  1332 apply (simp add: succ_fun_eq)
  1333 apply (blast dest: transM)  
  1334 done
  1335 
  1336 lemma (in M_axioms) funspace_succ:
  1337      "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  1338 apply (insert funspace_succ_replacement [of n], simp) 
  1339 apply (force simp add: succ_fun_eq2 univalent_def) 
  1340 done
  1341 
  1342 text{*@{term M} contains all finite function spaces.  Needed to prove the
  1343 absoluteness of transitive closure.*}
  1344 lemma (in M_axioms) finite_funspace_closed [intro,simp]:
  1345      "[|n\<in>nat; M(B)|] ==> M(n->B)"
  1346 apply (induct_tac n, simp)
  1347 apply (simp add: funspace_succ nat_into_M) 
  1348 done
  1349 
  1350 
  1351 subsection{*Relativization and Absoluteness for Boolean Operators*}
  1352 
  1353 constdefs
  1354   is_bool_of_o :: "[i=>o, o, i] => o"
  1355    "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
  1356 
  1357   is_not :: "[i=>o, i, i] => o"
  1358    "is_not(M,a,z) == (number1(M,a)  & empty(M,z)) | 
  1359                      (~number1(M,a) & number1(M,z))"
  1360 
  1361   is_and :: "[i=>o, i, i, i] => o"
  1362    "is_and(M,a,b,z) == (number1(M,a)  & z=b) | 
  1363                        (~number1(M,a) & empty(M,z))"
  1364 
  1365   is_or :: "[i=>o, i, i, i] => o"
  1366    "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) | 
  1367                       (~number1(M,a) & z=b)"
  1368 
  1369 lemma (in M_triv_axioms) bool_of_o_abs [simp]: 
  1370      "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)" 
  1371 by (simp add: is_bool_of_o_def bool_of_o_def) 
  1372 
  1373 
  1374 lemma (in M_triv_axioms) not_abs [simp]: 
  1375      "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)"
  1376 by (simp add: Bool.not_def cond_def is_not_def) 
  1377 
  1378 lemma (in M_triv_axioms) and_abs [simp]: 
  1379      "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b"
  1380 by (simp add: Bool.and_def cond_def is_and_def) 
  1381 
  1382 lemma (in M_triv_axioms) or_abs [simp]: 
  1383      "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b"
  1384 by (simp add: Bool.or_def cond_def is_or_def)
  1385 
  1386 
  1387 lemma (in M_triv_axioms) bool_of_o_closed [intro,simp]:
  1388      "M(bool_of_o(P))"
  1389 by (simp add: bool_of_o_def) 
  1390 
  1391 lemma (in M_triv_axioms) and_closed [intro,simp]:
  1392      "[| M(p); M(q) |] ==> M(p and q)"
  1393 by (simp add: and_def cond_def) 
  1394 
  1395 lemma (in M_triv_axioms) or_closed [intro,simp]:
  1396      "[| M(p); M(q) |] ==> M(p or q)"
  1397 by (simp add: or_def cond_def) 
  1398 
  1399 lemma (in M_triv_axioms) not_closed [intro,simp]:
  1400      "M(p) ==> M(not(p))"
  1401 by (simp add: Bool.not_def cond_def) 
  1402 
  1403 
  1404 subsection{*Relativization and Absoluteness for List Operators*}
  1405 
  1406 constdefs
  1407 
  1408   is_Nil :: "[i=>o, i] => o"
  1409      --{* because @{term "[] \<equiv> Inl(0)"}*}
  1410     "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
  1411 
  1412   is_Cons :: "[i=>o,i,i,i] => o"
  1413      --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
  1414     "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
  1415 
  1416 
  1417 lemma (in M_triv_axioms) Nil_in_M [intro,simp]: "M(Nil)"
  1418 by (simp add: Nil_def)
  1419 
  1420 lemma (in M_triv_axioms) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
  1421 by (simp add: is_Nil_def Nil_def)
  1422 
  1423 lemma (in M_triv_axioms) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
  1424 by (simp add: Cons_def) 
  1425 
  1426 lemma (in M_triv_axioms) Cons_abs [simp]:
  1427      "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
  1428 by (simp add: is_Cons_def Cons_def)
  1429 
  1430 
  1431 constdefs
  1432 
  1433   quasilist :: "i => o"
  1434     "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
  1435 
  1436   is_quasilist :: "[i=>o,i] => o"
  1437     "is_quasilist(M,z) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))"
  1438 
  1439   list_case' :: "[i, [i,i]=>i, i] => i"
  1440     --{*A version of @{term list_case} that's always defined.*}
  1441     "list_case'(a,b,xs) == 
  1442        if quasilist(xs) then list_case(a,b,xs) else 0"  
  1443 
  1444   is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
  1445     --{*Returns 0 for non-lists*}
  1446     "is_list_case(M, a, is_b, xs, z) == 
  1447        (is_Nil(M,xs) --> z=a) &
  1448        (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
  1449        (is_quasilist(M,xs) | empty(M,z))"
  1450 
  1451   hd' :: "i => i"
  1452     --{*A version of @{term hd} that's always defined.*}
  1453     "hd'(xs) == if quasilist(xs) then hd(xs) else 0"  
  1454 
  1455   tl' :: "i => i"
  1456     --{*A version of @{term tl} that's always defined.*}
  1457     "tl'(xs) == if quasilist(xs) then tl(xs) else 0"  
  1458 
  1459   is_hd :: "[i=>o,i,i] => o"
  1460      --{* @{term "hd([]) = 0"} no constraints if not a list.
  1461           Avoiding implication prevents the simplifier's looping.*}
  1462     "is_hd(M,xs,H) == 
  1463        (is_Nil(M,xs) --> empty(M,H)) &
  1464        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
  1465        (is_quasilist(M,xs) | empty(M,H))"
  1466 
  1467   is_tl :: "[i=>o,i,i] => o"
  1468      --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
  1469     "is_tl(M,xs,T) == 
  1470        (is_Nil(M,xs) --> T=xs) &
  1471        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
  1472        (is_quasilist(M,xs) | empty(M,T))"
  1473 
  1474 subsubsection{*@{term quasilist}: For Case-Splitting with @{term list_case'}*}
  1475 
  1476 lemma [iff]: "quasilist(Nil)"
  1477 by (simp add: quasilist_def)
  1478 
  1479 lemma [iff]: "quasilist(Cons(x,l))"
  1480 by (simp add: quasilist_def)
  1481 
  1482 lemma list_imp_quasilist: "l \<in> list(A) ==> quasilist(l)"
  1483 by (erule list.cases, simp_all)
  1484 
  1485 subsubsection{*@{term list_case'}, the Modified Version of @{term list_case}*}
  1486 
  1487 lemma list_case'_Nil [simp]: "list_case'(a,b,Nil) = a"
  1488 by (simp add: list_case'_def quasilist_def)
  1489 
  1490 lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)"
  1491 by (simp add: list_case'_def quasilist_def)
  1492 
  1493 lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0" 
  1494 by (simp add: quasilist_def list_case'_def) 
  1495 
  1496 lemma list_case'_eq_list_case [simp]:
  1497      "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
  1498 by (erule list.cases, simp_all)
  1499 
  1500 lemma (in M_axioms) list_case'_closed [intro,simp]:
  1501   "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
  1502 apply (case_tac "quasilist(k)") 
  1503  apply (simp add: quasilist_def, force) 
  1504 apply (simp add: non_list_case) 
  1505 done
  1506 
  1507 lemma (in M_triv_axioms) quasilist_abs [simp]: 
  1508      "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
  1509 by (auto simp add: is_quasilist_def quasilist_def)
  1510 
  1511 lemma (in M_triv_axioms) list_case_abs [simp]: 
  1512      "[| relativize2(M,is_b,b); M(k); M(z) |] 
  1513       ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
  1514 apply (case_tac "quasilist(k)") 
  1515  prefer 2 
  1516  apply (simp add: is_list_case_def non_list_case) 
  1517  apply (force simp add: quasilist_def) 
  1518 apply (simp add: quasilist_def is_list_case_def)
  1519 apply (elim disjE exE) 
  1520  apply (simp_all add: relativize2_def) 
  1521 done
  1522 
  1523 
  1524 subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
  1525 
  1526 lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
  1527 by (simp add: is_hd_def)
  1528 
  1529 lemma (in M_triv_axioms) is_hd_Cons:
  1530      "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
  1531 by (force simp add: is_hd_def) 
  1532 
  1533 lemma (in M_triv_axioms) hd_abs [simp]:
  1534      "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
  1535 apply (simp add: hd'_def)
  1536 apply (intro impI conjI)
  1537  prefer 2 apply (force simp add: is_hd_def) 
  1538 apply (simp add: quasilist_def is_hd_def)
  1539 apply (elim disjE exE, auto)
  1540 done 
  1541 
  1542 lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
  1543 by (simp add: is_tl_def)
  1544 
  1545 lemma (in M_triv_axioms) is_tl_Cons:
  1546      "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
  1547 by (force simp add: is_tl_def) 
  1548 
  1549 lemma (in M_triv_axioms) tl_abs [simp]:
  1550      "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
  1551 apply (simp add: tl'_def)
  1552 apply (intro impI conjI)
  1553  prefer 2 apply (force simp add: is_tl_def) 
  1554 apply (simp add: quasilist_def is_tl_def)
  1555 apply (elim disjE exE, auto)
  1556 done 
  1557 
  1558 lemma (in M_triv_axioms) relativize1_tl: "relativize1(M, is_tl(M), tl')"  
  1559 by (simp add: relativize1_def)
  1560 
  1561 lemma hd'_Nil: "hd'([]) = 0"
  1562 by (simp add: hd'_def)
  1563 
  1564 lemma hd'_Cons: "hd'(Cons(a,l)) = a"
  1565 by (simp add: hd'_def)
  1566 
  1567 lemma tl'_Nil: "tl'([]) = []"
  1568 by (simp add: tl'_def)
  1569 
  1570 lemma tl'_Cons: "tl'(Cons(a,l)) = l"
  1571 by (simp add: tl'_def)
  1572 
  1573 lemma iterates_tl_Nil: "n \<in> nat ==> tl'^n ([]) = []"
  1574 apply (induct_tac n) 
  1575 apply (simp_all add: tl'_Nil) 
  1576 done
  1577 
  1578 lemma (in M_axioms) tl'_closed: "M(x) ==> M(tl'(x))"
  1579 apply (simp add: tl'_def)
  1580 apply (force simp add: quasilist_def)
  1581 done
  1582 
  1583 
  1584 end