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