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