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