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