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