src/ZF/Constructible/Relative.thy
author paulson
Fri Jul 19 13:29:22 2002 +0200 (2002-07-19)
changeset 13397 6e5f4d911435
parent 13382 b37764a46b16
child 13418 7c0ba9dba978
permissions -rw-r--r--
Absoluteness of the function "nth"
     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{*Absoluteness for 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) ball_abs [simp]: 
   430      "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   431 by (blast intro: transM) 
   432 
   433 lemma (in M_triv_axioms) rall_abs [simp]: 
   434      "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   435 by (blast intro: transM) 
   436 
   437 lemma (in M_triv_axioms) bex_abs [simp]: 
   438      "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   439 by (blast intro: transM) 
   440 
   441 lemma (in M_triv_axioms) rex_abs [simp]: 
   442      "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   443 by (blast intro: transM) 
   444 
   445 lemma (in M_triv_axioms) ball_iff_equiv: 
   446      "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <-> 
   447                (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   448 by (blast intro: transM)
   449 
   450 text{*Simplifies proofs of equalities when there's an iff-equality
   451       available for rewriting, universally quantified over M. *}
   452 lemma (in M_triv_axioms) M_equalityI: 
   453      "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
   454 by (blast intro!: equalityI dest: transM) 
   455 
   456 lemma (in M_triv_axioms) empty_abs [simp]: 
   457      "M(z) ==> empty(M,z) <-> z=0"
   458 apply (simp add: empty_def)
   459 apply (blast intro: transM) 
   460 done
   461 
   462 lemma (in M_triv_axioms) subset_abs [simp]: 
   463      "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
   464 apply (simp add: subset_def) 
   465 apply (blast intro: transM) 
   466 done
   467 
   468 lemma (in M_triv_axioms) upair_abs [simp]: 
   469      "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
   470 apply (simp add: upair_def) 
   471 apply (blast intro: transM) 
   472 done
   473 
   474 lemma (in M_triv_axioms) upair_in_M_iff [iff]:
   475      "M({a,b}) <-> M(a) & M(b)"
   476 apply (insert upair_ax, simp add: upair_ax_def) 
   477 apply (blast intro: transM) 
   478 done
   479 
   480 lemma (in M_triv_axioms) singleton_in_M_iff [iff]:
   481      "M({a}) <-> M(a)"
   482 by (insert upair_in_M_iff [of a a], simp) 
   483 
   484 lemma (in M_triv_axioms) pair_abs [simp]: 
   485      "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   486 apply (simp add: pair_def ZF.Pair_def)
   487 apply (blast intro: transM) 
   488 done
   489 
   490 lemma (in M_triv_axioms) pair_in_M_iff [iff]:
   491      "M(<a,b>) <-> M(a) & M(b)"
   492 by (simp add: ZF.Pair_def)
   493 
   494 lemma (in M_triv_axioms) pair_components_in_M:
   495      "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   496 apply (simp add: Pair_def)
   497 apply (blast dest: transM) 
   498 done
   499 
   500 lemma (in M_triv_axioms) cartprod_abs [simp]: 
   501      "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   502 apply (simp add: cartprod_def)
   503 apply (rule iffI) 
   504  apply (blast intro!: equalityI intro: transM dest!: rspec) 
   505 apply (blast dest: transM) 
   506 done
   507 
   508 lemma (in M_triv_axioms) union_abs [simp]: 
   509      "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   510 apply (simp add: union_def) 
   511 apply (blast intro: transM) 
   512 done
   513 
   514 lemma (in M_triv_axioms) inter_abs [simp]: 
   515      "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   516 apply (simp add: inter_def) 
   517 apply (blast intro: transM) 
   518 done
   519 
   520 lemma (in M_triv_axioms) setdiff_abs [simp]: 
   521      "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   522 apply (simp add: setdiff_def) 
   523 apply (blast intro: transM) 
   524 done
   525 
   526 lemma (in M_triv_axioms) Union_abs [simp]: 
   527      "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   528 apply (simp add: big_union_def) 
   529 apply (blast intro!: equalityI dest: transM) 
   530 done
   531 
   532 lemma (in M_triv_axioms) Union_closed [intro,simp]:
   533      "M(A) ==> M(Union(A))"
   534 by (insert Union_ax, simp add: Union_ax_def) 
   535 
   536 lemma (in M_triv_axioms) Un_closed [intro,simp]:
   537      "[| M(A); M(B) |] ==> M(A Un B)"
   538 by (simp only: Un_eq_Union, blast) 
   539 
   540 lemma (in M_triv_axioms) cons_closed [intro,simp]:
   541      "[| M(a); M(A) |] ==> M(cons(a,A))"
   542 by (subst cons_eq [symmetric], blast) 
   543 
   544 lemma (in M_triv_axioms) cons_abs [simp]: 
   545      "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
   546 by (simp add: is_cons_def, blast intro: transM)  
   547 
   548 lemma (in M_triv_axioms) successor_abs [simp]: 
   549      "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
   550 by (simp add: successor_def, blast)  
   551 
   552 lemma (in M_triv_axioms) succ_in_M_iff [iff]:
   553      "M(succ(a)) <-> M(a)"
   554 apply (simp add: succ_def) 
   555 apply (blast intro: transM) 
   556 done
   557 
   558 lemma (in M_triv_axioms) separation_closed [intro,simp]:
   559      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   560 apply (insert separation, simp add: separation_def) 
   561 apply (drule rspec, assumption, clarify) 
   562 apply (subgoal_tac "y = Collect(A,P)", blast)
   563 apply (blast dest: transM) 
   564 done
   565 
   566 text{*Probably the premise and conclusion are equivalent*}
   567 lemma (in M_triv_axioms) strong_replacementI [rule_format]:
   568     "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
   569      ==> strong_replacement(M,P)"
   570 apply (simp add: strong_replacement_def, clarify) 
   571 apply (frule replacementD [OF replacement], assumption, clarify) 
   572 apply (drule_tac x=A in rspec, clarify)  
   573 apply (drule_tac z=Y in separationD, assumption, clarify) 
   574 apply (rule_tac x=y in rexI) 
   575 apply (blast dest: transM)+
   576 done
   577 
   578 
   579 (*The last premise expresses that P takes M to M*)
   580 lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:
   581      "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   582        !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   583 apply (simp add: strong_replacement_def) 
   584 apply (drule rspec, auto) 
   585 apply (subgoal_tac "Replace(A,P) = Y")
   586  apply simp 
   587 apply (rule equality_iffI) 
   588 apply (simp add: Replace_iff, safe)
   589  apply (blast dest: transM) 
   590 apply (frule transM, assumption) 
   591  apply (simp add: univalent_def)
   592  apply (drule rspec [THEN iffD1], assumption, assumption)
   593  apply (blast dest: transM) 
   594 done
   595 
   596 (*The first premise can't simply be assumed as a schema.
   597   It is essential to take care when asserting instances of Replacement.
   598   Let K be a nonconstructible subset of nat and define
   599   f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   600   nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   601   even for f : M -> M.
   602 *)
   603 lemma (in M_triv_axioms) RepFun_closed:
   604      "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   605       ==> M(RepFun(A,f))"
   606 apply (simp add: RepFun_def) 
   607 apply (rule strong_replacement_closed) 
   608 apply (auto dest: transM  simp add: univalent_def) 
   609 done
   610 
   611 lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
   612 by simp
   613 
   614 text{*Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
   615       makes relativization easier.*}
   616 lemma (in M_triv_axioms) RepFun_closed2:
   617      "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   618       ==> M(RepFun(A, %x. f(x)))"
   619 apply (simp add: RepFun_def)
   620 apply (frule strong_replacement_closed, assumption)
   621 apply (auto dest: transM  simp add: Replace_conj_eq univalent_def) 
   622 done
   623 
   624 lemma (in M_triv_axioms) lam_closed [intro,simp]:
   625      "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   626       ==> M(\<lambda>x\<in>A. b(x))"
   627 by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
   628 
   629 lemma (in M_triv_axioms) image_abs [simp]: 
   630      "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   631 apply (simp add: image_def)
   632 apply (rule iffI) 
   633  apply (blast intro!: equalityI dest: transM, blast) 
   634 done
   635 
   636 text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   637       This result is one direction of absoluteness.*}
   638 
   639 lemma (in M_triv_axioms) powerset_Pow: 
   640      "powerset(M, x, Pow(x))"
   641 by (simp add: powerset_def)
   642 
   643 text{*But we can't prove that the powerset in @{text M} includes the
   644       real powerset.*}
   645 lemma (in M_triv_axioms) powerset_imp_subset_Pow: 
   646      "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   647 apply (simp add: powerset_def) 
   648 apply (blast dest: transM) 
   649 done
   650 
   651 lemma (in M_triv_axioms) nat_into_M [intro]:
   652      "n \<in> nat ==> M(n)"
   653 by (induct n rule: nat_induct, simp_all)
   654 
   655 lemma (in M_triv_axioms) nat_case_closed [intro,simp]:
   656   "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   657 apply (case_tac "k=0", simp) 
   658 apply (case_tac "\<exists>m. k = succ(m)", force)
   659 apply (simp add: nat_case_def) 
   660 done
   661 
   662 lemma (in M_triv_axioms) quasinat_abs [simp]: 
   663      "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
   664 by (auto simp add: is_quasinat_def quasinat_def)
   665 
   666 lemma (in M_triv_axioms) nat_case_abs [simp]: 
   667      "[| relativize1(M,is_b,b); M(k); M(z) |] 
   668       ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
   669 apply (case_tac "quasinat(k)") 
   670  prefer 2 
   671  apply (simp add: is_nat_case_def non_nat_case) 
   672  apply (force simp add: quasinat_def) 
   673 apply (simp add: quasinat_def is_nat_case_def)
   674 apply (elim disjE exE) 
   675  apply (simp_all add: relativize1_def) 
   676 done
   677 
   678 (*NOT for the simplifier.  The assumption M(z') is apparently necessary, but 
   679   causes the error "Failed congruence proof!"  It may be better to replace
   680   is_nat_case by nat_case before attempting congruence reasoning.*)
   681 lemma (in M_triv_axioms) is_nat_case_cong:
   682      "[| a = a'; k = k';  z = z';  M(z');
   683        !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
   684       ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
   685 by (simp add: is_nat_case_def) 
   686 
   687 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
   688      "M(Inl(a)) <-> M(a)"
   689 by (simp add: Inl_def) 
   690 
   691 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
   692      "M(Inr(a)) <-> M(a)"
   693 by (simp add: Inr_def)
   694 
   695 
   696 subsection{*Absoluteness for ordinals*}
   697 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   698 
   699 lemma (in M_triv_axioms) lt_closed:
   700      "[| j<i; M(i) |] ==> M(j)" 
   701 by (blast dest: ltD intro: transM) 
   702 
   703 lemma (in M_triv_axioms) transitive_set_abs [simp]: 
   704      "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   705 by (simp add: transitive_set_def Transset_def)
   706 
   707 lemma (in M_triv_axioms) ordinal_abs [simp]: 
   708      "M(a) ==> ordinal(M,a) <-> Ord(a)"
   709 by (simp add: ordinal_def Ord_def)
   710 
   711 lemma (in M_triv_axioms) limit_ordinal_abs [simp]: 
   712      "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   713 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
   714 apply (simp add: lt_def, blast) 
   715 done
   716 
   717 lemma (in M_triv_axioms) successor_ordinal_abs [simp]: 
   718      "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   719 apply (simp add: successor_ordinal_def, safe)
   720 apply (drule Ord_cases_disj, auto) 
   721 done
   722 
   723 lemma finite_Ord_is_nat:
   724       "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   725 by (induct a rule: trans_induct3, simp_all)
   726 
   727 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   728 by (induct a rule: nat_induct, auto)
   729 
   730 lemma (in M_triv_axioms) finite_ordinal_abs [simp]: 
   731      "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   732 apply (simp add: finite_ordinal_def)
   733 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   734              dest: Ord_trans naturals_not_limit)
   735 done
   736 
   737 lemma Limit_non_Limit_implies_nat:
   738      "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   739 apply (rule le_anti_sym) 
   740 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   741  apply (simp add: lt_def)  
   742  apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   743 apply (erule nat_le_Limit)
   744 done
   745 
   746 lemma (in M_triv_axioms) omega_abs [simp]: 
   747      "M(a) ==> omega(M,a) <-> a = nat"
   748 apply (simp add: omega_def) 
   749 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   750 done
   751 
   752 lemma (in M_triv_axioms) number1_abs [simp]: 
   753      "M(a) ==> number1(M,a) <-> a = 1"
   754 by (simp add: number1_def) 
   755 
   756 lemma (in M_triv_axioms) number1_abs [simp]: 
   757      "M(a) ==> number2(M,a) <-> a = succ(1)"
   758 by (simp add: number2_def) 
   759 
   760 lemma (in M_triv_axioms) number3_abs [simp]: 
   761      "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   762 by (simp add: number3_def) 
   763 
   764 text{*Kunen continued to 20...*}
   765 
   766 (*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   767   but the recursion variable must stay unchanged.  But then the recursion
   768   equations only hold for x\<in>nat (or in some other set) and not for the 
   769   whole of the class M.
   770   consts
   771     natnumber_aux :: "[i=>o,i] => i"
   772 
   773   primrec
   774       "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   775       "natnumber_aux(M,succ(n)) = 
   776 	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   777 		     then 1 else 0)"
   778 
   779   constdefs
   780     natnumber :: "[i=>o,i,i] => o"
   781       "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   782 
   783   lemma (in M_triv_axioms) [simp]: 
   784        "natnumber(M,0,x) == x=0"
   785 *)
   786 
   787 subsection{*Some instances of separation and strong replacement*}
   788 
   789 locale (open) M_axioms = M_triv_axioms +
   790 assumes Inter_separation:
   791      "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
   792   and cartprod_separation:
   793      "[| M(A); M(B) |] 
   794       ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
   795   and image_separation:
   796      "[| M(A); M(r) |] 
   797       ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
   798   and converse_separation:
   799      "M(r) ==> separation(M, 
   800          \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
   801   and restrict_separation:
   802      "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
   803   and comp_separation:
   804      "[| M(r); M(s) |]
   805       ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   806 		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   807                   xy\<in>s & yz\<in>r)"
   808   and pred_separation:
   809      "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
   810   and Memrel_separation:
   811      "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
   812   and funspace_succ_replacement:
   813      "M(n) ==> 
   814       strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M]. 
   815                 pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
   816                 upair(M,cnbf,cnbf,z))"
   817   and well_ord_iso_separation:
   818      "[| M(A); M(f); M(r) |] 
   819       ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M]. 
   820 		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   821   and obase_separation:
   822      --{*part of the order type formalization*}
   823      "[| M(A); M(r) |] 
   824       ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   825 	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   826 	     order_isomorphism(M,par,r,x,mx,g))"
   827   and obase_equals_separation:
   828      "[| M(A); M(r) |] 
   829       ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
   830 			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
   831 			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   832 			      order_isomorphism(M,pxr,r,y,my,g))))"
   833   and omap_replacement:
   834      "[| M(A); M(r) |] 
   835       ==> strong_replacement(M,
   836              \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
   837 	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   838 	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   839   and is_recfun_separation:
   840      --{*for well-founded recursion*}
   841      "[| M(r); M(f); M(g); M(a); M(b) |] 
   842      ==> separation(M, 
   843             \<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
   844                 pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
   845                 (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
   846                                    fx \<noteq> gx))"
   847 
   848 lemma (in M_axioms) cartprod_iff_lemma:
   849      "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   850          powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   851        ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   852 apply (simp add: powerset_def) 
   853 apply (rule equalityI, clarify, simp)
   854  apply (frule transM, assumption) 
   855  apply (frule transM, assumption, simp) 
   856  apply blast 
   857 apply clarify
   858 apply (frule transM, assumption, force) 
   859 done
   860 
   861 lemma (in M_axioms) cartprod_iff:
   862      "[| M(A); M(B); M(C) |] 
   863       ==> cartprod(M,A,B,C) <-> 
   864           (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   865                    C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
   866 apply (simp add: Pair_def cartprod_def, safe)
   867 defer 1 
   868   apply (simp add: powerset_def) 
   869  apply blast 
   870 txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   871 apply (insert power_ax, simp add: power_ax_def) 
   872 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   873 apply (blast, clarify) 
   874 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
   875 apply assumption
   876 apply (blast intro: cartprod_iff_lemma) 
   877 done
   878 
   879 lemma (in M_axioms) cartprod_closed_lemma:
   880      "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
   881 apply (simp del: cartprod_abs add: cartprod_iff)
   882 apply (insert power_ax, simp add: power_ax_def) 
   883 apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   884 apply (blast, clarify) 
   885 apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   886 apply (blast, clarify)
   887 apply (intro rexI exI conjI) 
   888 prefer 5 apply (rule refl) 
   889 prefer 3 apply assumption
   890 prefer 3 apply assumption
   891 apply (insert cartprod_separation [of A B], auto)
   892 done
   893 
   894 text{*All the lemmas above are necessary because Powerset is not absolute.
   895       I should have used Replacement instead!*}
   896 lemma (in M_axioms) cartprod_closed [intro,simp]: 
   897      "[| M(A); M(B) |] ==> M(A*B)"
   898 by (frule cartprod_closed_lemma, assumption, force)
   899 
   900 lemma (in M_axioms) sum_closed [intro,simp]: 
   901      "[| M(A); M(B) |] ==> M(A+B)"
   902 by (simp add: sum_def)
   903 
   904 lemma (in M_axioms) sum_abs [simp]:
   905      "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
   906 by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
   907 
   908 lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
   909      "M(Inl(a)) <-> M(a)"
   910 by (simp add: Inl_def) 
   911 
   912 lemma (in M_triv_axioms) Inl_abs [simp]:
   913      "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
   914 by (simp add: is_Inl_def Inl_def)
   915 
   916 lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
   917      "M(Inr(a)) <-> M(a)"
   918 by (simp add: Inr_def) 
   919 
   920 lemma (in M_triv_axioms) Inr_abs [simp]:
   921      "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
   922 by (simp add: is_Inr_def Inr_def)
   923 
   924 
   925 subsubsection {*converse of a relation*}
   926 
   927 lemma (in M_axioms) M_converse_iff:
   928      "M(r) ==> 
   929       converse(r) = 
   930       {z \<in> Union(Union(r)) * Union(Union(r)). 
   931        \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
   932 apply (rule equalityI)
   933  prefer 2 apply (blast dest: transM, clarify, simp) 
   934 apply (simp add: Pair_def) 
   935 apply (blast dest: transM) 
   936 done
   937 
   938 lemma (in M_axioms) converse_closed [intro,simp]: 
   939      "M(r) ==> M(converse(r))"
   940 apply (simp add: M_converse_iff)
   941 apply (insert converse_separation [of r], simp)
   942 done
   943 
   944 lemma (in M_axioms) converse_abs [simp]: 
   945      "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   946 apply (simp add: is_converse_def)
   947 apply (rule iffI)
   948  prefer 2 apply blast 
   949 apply (rule M_equalityI)
   950   apply simp
   951   apply (blast dest: transM)+
   952 done
   953 
   954 
   955 subsubsection {*image, preimage, domain, range*}
   956 
   957 lemma (in M_axioms) image_closed [intro,simp]: 
   958      "[| M(A); M(r) |] ==> M(r``A)"
   959 apply (simp add: image_iff_Collect)
   960 apply (insert image_separation [of A r], simp) 
   961 done
   962 
   963 lemma (in M_axioms) vimage_abs [simp]: 
   964      "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
   965 apply (simp add: pre_image_def)
   966 apply (rule iffI) 
   967  apply (blast intro!: equalityI dest: transM, blast) 
   968 done
   969 
   970 lemma (in M_axioms) vimage_closed [intro,simp]: 
   971      "[| M(A); M(r) |] ==> M(r-``A)"
   972 by (simp add: vimage_def)
   973 
   974 
   975 subsubsection{*Domain, range and field*}
   976 
   977 lemma (in M_axioms) domain_abs [simp]: 
   978      "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
   979 apply (simp add: is_domain_def) 
   980 apply (blast intro!: equalityI dest: transM) 
   981 done
   982 
   983 lemma (in M_axioms) domain_closed [intro,simp]: 
   984      "M(r) ==> M(domain(r))"
   985 apply (simp add: domain_eq_vimage)
   986 done
   987 
   988 lemma (in M_axioms) range_abs [simp]: 
   989      "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
   990 apply (simp add: is_range_def)
   991 apply (blast intro!: equalityI dest: transM)
   992 done
   993 
   994 lemma (in M_axioms) range_closed [intro,simp]: 
   995      "M(r) ==> M(range(r))"
   996 apply (simp add: range_eq_image)
   997 done
   998 
   999 lemma (in M_axioms) field_abs [simp]: 
  1000      "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
  1001 by (simp add: domain_closed range_closed is_field_def field_def)
  1002 
  1003 lemma (in M_axioms) field_closed [intro,simp]: 
  1004      "M(r) ==> M(field(r))"
  1005 by (simp add: domain_closed range_closed Un_closed field_def) 
  1006 
  1007 
  1008 subsubsection{*Relations, functions and application*}
  1009 
  1010 lemma (in M_axioms) relation_abs [simp]: 
  1011      "M(r) ==> is_relation(M,r) <-> relation(r)"
  1012 apply (simp add: is_relation_def relation_def) 
  1013 apply (blast dest!: bspec dest: pair_components_in_M)+
  1014 done
  1015 
  1016 lemma (in M_axioms) function_abs [simp]: 
  1017      "M(r) ==> is_function(M,r) <-> function(r)"
  1018 apply (simp add: is_function_def function_def, safe) 
  1019    apply (frule transM, assumption) 
  1020   apply (blast dest: pair_components_in_M)+
  1021 done
  1022 
  1023 lemma (in M_axioms) apply_closed [intro,simp]: 
  1024      "[|M(f); M(a)|] ==> M(f`a)"
  1025 by (simp add: apply_def)
  1026 
  1027 lemma (in M_axioms) apply_abs [simp]: 
  1028      "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
  1029 apply (simp add: fun_apply_def apply_def, blast) 
  1030 done
  1031 
  1032 lemma (in M_axioms) typed_function_abs [simp]: 
  1033      "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
  1034 apply (auto simp add: typed_function_def relation_def Pi_iff) 
  1035 apply (blast dest: pair_components_in_M)+
  1036 done
  1037 
  1038 lemma (in M_axioms) injection_abs [simp]: 
  1039      "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
  1040 apply (simp add: injection_def apply_iff inj_def apply_closed)
  1041 apply (blast dest: transM [of _ A]) 
  1042 done
  1043 
  1044 lemma (in M_axioms) surjection_abs [simp]: 
  1045      "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
  1046 by (simp add: surjection_def surj_def)
  1047 
  1048 lemma (in M_axioms) bijection_abs [simp]: 
  1049      "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
  1050 by (simp add: bijection_def bij_def)
  1051 
  1052 
  1053 subsubsection{*Composition of relations*}
  1054 
  1055 lemma (in M_axioms) M_comp_iff:
  1056      "[| M(r); M(s) |] 
  1057       ==> r O s = 
  1058           {xz \<in> domain(s) * range(r).  
  1059             \<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}"
  1060 apply (simp add: comp_def)
  1061 apply (rule equalityI) 
  1062  apply clarify 
  1063  apply simp 
  1064  apply  (blast dest:  transM)+
  1065 done
  1066 
  1067 lemma (in M_axioms) comp_closed [intro,simp]: 
  1068      "[| M(r); M(s) |] ==> M(r O s)"
  1069 apply (simp add: M_comp_iff)
  1070 apply (insert comp_separation [of r s], simp) 
  1071 done
  1072 
  1073 lemma (in M_axioms) composition_abs [simp]: 
  1074      "[| M(r); M(s); M(t) |] 
  1075       ==> composition(M,r,s,t) <-> t = r O s"
  1076 apply safe
  1077  txt{*Proving @{term "composition(M, r, s, r O s)"}*}
  1078  prefer 2 
  1079  apply (simp add: composition_def comp_def)
  1080  apply (blast dest: transM) 
  1081 txt{*Opposite implication*}
  1082 apply (rule M_equalityI)
  1083   apply (simp add: composition_def comp_def)
  1084   apply (blast del: allE dest: transM)+
  1085 done
  1086 
  1087 text{*no longer needed*}
  1088 lemma (in M_axioms) restriction_is_function: 
  1089      "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
  1090       ==> function(z)"
  1091 apply (rotate_tac 1)
  1092 apply (simp add: restriction_def ball_iff_equiv) 
  1093 apply (unfold function_def, blast) 
  1094 done
  1095 
  1096 lemma (in M_axioms) restriction_abs [simp]: 
  1097      "[| M(f); M(A); M(z) |] 
  1098       ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  1099 apply (simp add: ball_iff_equiv restriction_def restrict_def)
  1100 apply (blast intro!: equalityI dest: transM) 
  1101 done
  1102 
  1103 
  1104 lemma (in M_axioms) M_restrict_iff:
  1105      "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  1106 by (simp add: restrict_def, blast dest: transM)
  1107 
  1108 lemma (in M_axioms) restrict_closed [intro,simp]: 
  1109      "[| M(A); M(r) |] ==> M(restrict(r,A))"
  1110 apply (simp add: M_restrict_iff)
  1111 apply (insert restrict_separation [of A], simp) 
  1112 done
  1113 
  1114 lemma (in M_axioms) Inter_abs [simp]: 
  1115      "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  1116 apply (simp add: big_inter_def Inter_def) 
  1117 apply (blast intro!: equalityI dest: transM) 
  1118 done
  1119 
  1120 lemma (in M_axioms) Inter_closed [intro,simp]:
  1121      "M(A) ==> M(Inter(A))"
  1122 by (insert Inter_separation, simp add: Inter_def)
  1123 
  1124 lemma (in M_axioms) Int_closed [intro,simp]:
  1125      "[| M(A); M(B) |] ==> M(A Int B)"
  1126 apply (subgoal_tac "M({A,B})")
  1127 apply (frule Inter_closed, force+) 
  1128 done
  1129 
  1130 subsubsection{*Functions and function space*}
  1131 
  1132 text{*M contains all finite functions*}
  1133 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
  1134      "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
  1135 apply (induct_tac n, simp)
  1136 apply (rule ballI)  
  1137 apply (simp add: succ_def) 
  1138 apply (frule fun_cons_restrict_eq)
  1139 apply (erule ssubst) 
  1140 apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
  1141  apply (simp add: cons_closed nat_into_M apply_closed) 
  1142 apply (blast intro: apply_funtype transM restrict_type2) 
  1143 done
  1144 
  1145 lemma (in M_axioms) finite_fun_closed [rule_format]: 
  1146      "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
  1147 by (blast intro: finite_fun_closed_lemma) 
  1148 
  1149 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
  1150 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  1151 lemma (in M_axioms) is_funspace_abs [simp]:
  1152      "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  1153 apply (simp add: is_funspace_def)
  1154 apply (rule iffI)
  1155  prefer 2 apply blast 
  1156 apply (rule M_equalityI)
  1157   apply simp_all
  1158 done
  1159 
  1160 lemma (in M_axioms) succ_fun_eq2:
  1161      "[|M(B); M(n->B)|] ==>
  1162       succ(n) -> B = 
  1163       \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  1164 apply (simp add: succ_fun_eq)
  1165 apply (blast dest: transM)  
  1166 done
  1167 
  1168 lemma (in M_axioms) funspace_succ:
  1169      "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  1170 apply (insert funspace_succ_replacement [of n], simp) 
  1171 apply (force simp add: succ_fun_eq2 univalent_def) 
  1172 done
  1173 
  1174 text{*@{term M} contains all finite function spaces.  Needed to prove the
  1175 absoluteness of transitive closure.*}
  1176 lemma (in M_axioms) finite_funspace_closed [intro,simp]:
  1177      "[|n\<in>nat; M(B)|] ==> M(n->B)"
  1178 apply (induct_tac n, simp)
  1179 apply (simp add: funspace_succ nat_into_M) 
  1180 done
  1181 
  1182 
  1183 subsection{*Relativization and Absoluteness for List Operators*}
  1184 
  1185 constdefs
  1186 
  1187   is_Nil :: "[i=>o, i] => o"
  1188      --{* because @{term "[] \<equiv> Inl(0)"}*}
  1189     "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
  1190 
  1191   is_Cons :: "[i=>o,i,i,i] => o"
  1192      --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
  1193     "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
  1194 
  1195 
  1196 lemma (in M_triv_axioms) Nil_in_M [intro,simp]: "M(Nil)"
  1197 by (simp add: Nil_def)
  1198 
  1199 lemma (in M_triv_axioms) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
  1200 by (simp add: is_Nil_def Nil_def)
  1201 
  1202 lemma (in M_triv_axioms) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
  1203 by (simp add: Cons_def) 
  1204 
  1205 lemma (in M_triv_axioms) Cons_abs [simp]:
  1206      "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
  1207 by (simp add: is_Cons_def Cons_def)
  1208 
  1209 
  1210 constdefs
  1211 
  1212   quasilist :: "i => o"
  1213     "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
  1214 
  1215   is_quasilist :: "[i=>o,i] => o"
  1216     "is_quasilist(M,z) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))"
  1217 
  1218   list_case' :: "[i, [i,i]=>i, i] => i"
  1219     --{*A version of @{term list_case} that's always defined.*}
  1220     "list_case'(a,b,xs) == 
  1221        if quasilist(xs) then list_case(a,b,xs) else 0"  
  1222 
  1223   is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
  1224     --{*Returns 0 for non-lists*}
  1225     "is_list_case(M, a, is_b, xs, z) == 
  1226        (is_Nil(M,xs) --> z=a) &
  1227        (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
  1228        (is_quasilist(M,xs) | empty(M,z))"
  1229 
  1230   hd' :: "i => i"
  1231     --{*A version of @{term hd} that's always defined.*}
  1232     "hd'(xs) == if quasilist(xs) then hd(xs) else 0"  
  1233 
  1234   tl' :: "i => i"
  1235     --{*A version of @{term tl} that's always defined.*}
  1236     "tl'(xs) == if quasilist(xs) then tl(xs) else 0"  
  1237 
  1238   is_hd :: "[i=>o,i,i] => o"
  1239      --{* @{term "hd([]) = 0"} no constraints if not a list.
  1240           Avoiding implication prevents the simplifier's looping.*}
  1241     "is_hd(M,xs,H) == 
  1242        (is_Nil(M,xs) --> empty(M,H)) &
  1243        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
  1244        (is_quasilist(M,xs) | empty(M,H))"
  1245 
  1246   is_tl :: "[i=>o,i,i] => o"
  1247      --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
  1248     "is_tl(M,xs,T) == 
  1249        (is_Nil(M,xs) --> T=xs) &
  1250        (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
  1251        (is_quasilist(M,xs) | empty(M,T))"
  1252 
  1253 subsubsection{*@{term quasilist}: For Case-Splitting with @{term list_case'}*}
  1254 
  1255 lemma [iff]: "quasilist(Nil)"
  1256 by (simp add: quasilist_def)
  1257 
  1258 lemma [iff]: "quasilist(Cons(x,l))"
  1259 by (simp add: quasilist_def)
  1260 
  1261 lemma list_imp_quasilist: "l \<in> list(A) ==> quasilist(l)"
  1262 by (erule list.cases, simp_all)
  1263 
  1264 subsubsection{*@{term list_case'}, the Modified Version of @{term list_case}*}
  1265 
  1266 lemma list_case'_Nil [simp]: "list_case'(a,b,Nil) = a"
  1267 by (simp add: list_case'_def quasilist_def)
  1268 
  1269 lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)"
  1270 by (simp add: list_case'_def quasilist_def)
  1271 
  1272 lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0" 
  1273 by (simp add: quasilist_def list_case'_def) 
  1274 
  1275 lemma list_case'_eq_list_case [simp]:
  1276      "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
  1277 by (erule list.cases, simp_all)
  1278 
  1279 lemma (in M_axioms) list_case'_closed [intro,simp]:
  1280   "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
  1281 apply (case_tac "quasilist(k)") 
  1282  apply (simp add: quasilist_def, force) 
  1283 apply (simp add: non_list_case) 
  1284 done
  1285 
  1286 lemma (in M_triv_axioms) quasilist_abs [simp]: 
  1287      "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
  1288 by (auto simp add: is_quasilist_def quasilist_def)
  1289 
  1290 lemma (in M_triv_axioms) list_case_abs [simp]: 
  1291      "[| relativize2(M,is_b,b); M(k); M(z) |] 
  1292       ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
  1293 apply (case_tac "quasilist(k)") 
  1294  prefer 2 
  1295  apply (simp add: is_list_case_def non_list_case) 
  1296  apply (force simp add: quasilist_def) 
  1297 apply (simp add: quasilist_def is_list_case_def)
  1298 apply (elim disjE exE) 
  1299  apply (simp_all add: relativize2_def) 
  1300 done
  1301 
  1302 
  1303 subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
  1304 
  1305 lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
  1306 by (simp add: is_hd_def )
  1307 
  1308 lemma (in M_triv_axioms) is_hd_Cons:
  1309      "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
  1310 by (force simp add: is_hd_def ) 
  1311 
  1312 lemma (in M_triv_axioms) hd_abs [simp]:
  1313      "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
  1314 apply (simp add: hd'_def)
  1315 apply (intro impI conjI)
  1316  prefer 2 apply (force simp add: is_hd_def) 
  1317 apply (simp add: quasilist_def is_hd_def )
  1318 apply (elim disjE exE, auto)
  1319 done 
  1320 
  1321 lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
  1322 by (simp add: is_tl_def )
  1323 
  1324 lemma (in M_triv_axioms) is_tl_Cons:
  1325      "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
  1326 by (force simp add: is_tl_def ) 
  1327 
  1328 lemma (in M_triv_axioms) tl_abs [simp]:
  1329      "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
  1330 apply (simp add: tl'_def)
  1331 apply (intro impI conjI)
  1332  prefer 2 apply (force simp add: is_tl_def) 
  1333 apply (simp add: quasilist_def is_tl_def )
  1334 apply (elim disjE exE, auto)
  1335 done 
  1336 
  1337 lemma (in M_triv_axioms) relativize1_tl: "relativize1(M, is_tl(M), tl')"  
  1338 by (simp add: relativize1_def)
  1339 
  1340 lemma hd'_Nil: "hd'([]) = 0"
  1341 by (simp add: hd'_def)
  1342 
  1343 lemma hd'_Cons: "hd'(Cons(a,l)) = a"
  1344 by (simp add: hd'_def)
  1345 
  1346 lemma tl'_Nil: "tl'([]) = []"
  1347 by (simp add: tl'_def)
  1348 
  1349 lemma tl'_Cons: "tl'(Cons(a,l)) = l"
  1350 by (simp add: tl'_def)
  1351 
  1352 lemma iterates_tl_Nil: "n \<in> nat ==> tl'^n ([]) = []"
  1353 apply (induct_tac n) 
  1354 apply (simp_all add: tl'_Nil) 
  1355 done
  1356 
  1357 lemma (in M_axioms) tl'_closed: "M(x) ==> M(tl'(x))"
  1358 apply (simp add: tl'_def)
  1359 apply (force simp add: quasilist_def)
  1360 done
  1361 
  1362 
  1363 end