Various simplifications of the Constructible theories
authorpaulson
Fri Oct 04 15:57:32 2002 +0200 (2002-10-04)
changeset 1362887482b5e3f2e
parent 13627 67b0b7500a9d
child 13629 a46362d2b19b
Various simplifications of the Constructible theories
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/Wellorderings.thy
src/ZF/Nat.thy
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Fri Oct 04 15:23:58 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Fri Oct 04 15:57:32 2002 +0200
     1.3 @@ -95,8 +95,7 @@
     1.4  
     1.5  theorem M_trivial_L: "PROP M_trivial(L)"
     1.6    apply (rule M_trivial.intro)
     1.7 -        apply (erule (1) transL)
     1.8 -       apply (rule nonempty)
     1.9 +       apply (erule (1) transL)
    1.10        apply (rule upair_ax)
    1.11       apply (rule Union_ax)
    1.12      apply (rule power_ax)
     2.1 --- a/src/ZF/Constructible/Relative.thy	Fri Oct 04 15:23:58 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Oct 04 15:57:32 2002 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4      "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z --> x = a | x = b)"
     2.5  
     2.6    pair :: "[i=>o,i,i,i] => o"
     2.7 -    "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & 
     2.8 +    "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) &
     2.9                            (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
    2.10  
    2.11  
    2.12 @@ -62,17 +62,17 @@
    2.13      "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)"
    2.14  
    2.15    big_inter :: "[i=>o,i,i] => o"
    2.16 -    "big_inter(M,A,z) == 
    2.17 +    "big_inter(M,A,z) ==
    2.18               (A=0 --> z=0) &
    2.19  	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y[M]. y\<in>A --> x \<in> y)))"
    2.20  
    2.21    cartprod :: "[i=>o,i,i,i] => o"
    2.22 -    "cartprod(M,A,B,z) == 
    2.23 +    "cartprod(M,A,B,z) ==
    2.24  	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
    2.25  
    2.26    is_sum :: "[i=>o,i,i,i] => o"
    2.27 -    "is_sum(M,A,B,Z) == 
    2.28 -       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
    2.29 +    "is_sum(M,A,B,Z) ==
    2.30 +       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
    2.31         number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
    2.32         cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
    2.33  
    2.34 @@ -83,73 +83,73 @@
    2.35      "is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)"
    2.36  
    2.37    is_converse :: "[i=>o,i,i] => o"
    2.38 -    "is_converse(M,r,z) == 
    2.39 -	\<forall>x[M]. x \<in> z <-> 
    2.40 +    "is_converse(M,r,z) ==
    2.41 +	\<forall>x[M]. x \<in> z <->
    2.42               (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
    2.43  
    2.44    pre_image :: "[i=>o,i,i,i] => o"
    2.45 -    "pre_image(M,r,A,z) == 
    2.46 +    "pre_image(M,r,A,z) ==
    2.47  	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
    2.48  
    2.49    is_domain :: "[i=>o,i,i] => o"
    2.50 -    "is_domain(M,r,z) == 
    2.51 +    "is_domain(M,r,z) ==
    2.52  	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
    2.53  
    2.54    image :: "[i=>o,i,i,i] => o"
    2.55 -    "image(M,r,A,z) == 
    2.56 +    "image(M,r,A,z) ==
    2.57          \<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
    2.58  
    2.59    is_range :: "[i=>o,i,i] => o"
    2.60 -    --{*the cleaner 
    2.61 +    --{*the cleaner
    2.62        @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
    2.63 -      unfortunately needs an instance of separation in order to prove 
    2.64 +      unfortunately needs an instance of separation in order to prove
    2.65          @{term "M(converse(r))"}.*}
    2.66 -    "is_range(M,r,z) == 
    2.67 +    "is_range(M,r,z) ==
    2.68  	\<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
    2.69  
    2.70    is_field :: "[i=>o,i,i] => o"
    2.71 -    "is_field(M,r,z) == 
    2.72 -	\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) & 
    2.73 +    "is_field(M,r,z) ==
    2.74 +	\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) &
    2.75                          union(M,dr,rr,z)"
    2.76  
    2.77    is_relation :: "[i=>o,i] => o"
    2.78 -    "is_relation(M,r) == 
    2.79 +    "is_relation(M,r) ==
    2.80          (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
    2.81  
    2.82    is_function :: "[i=>o,i] => o"
    2.83 -    "is_function(M,r) == 
    2.84 -	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 
    2.85 +    "is_function(M,r) ==
    2.86 +	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
    2.87             pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
    2.88  
    2.89    fun_apply :: "[i=>o,i,i,i] => o"
    2.90 -    "fun_apply(M,f,x,y) == 
    2.91 -        (\<exists>xs[M]. \<exists>fxs[M]. 
    2.92 +    "fun_apply(M,f,x,y) ==
    2.93 +        (\<exists>xs[M]. \<exists>fxs[M].
    2.94           upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))"
    2.95  
    2.96    typed_function :: "[i=>o,i,i,i] => o"
    2.97 -    "typed_function(M,A,B,r) == 
    2.98 +    "typed_function(M,A,B,r) ==
    2.99          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
   2.100          (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"
   2.101  
   2.102    is_funspace :: "[i=>o,i,i,i] => o"
   2.103 -    "is_funspace(M,A,B,F) == 
   2.104 +    "is_funspace(M,A,B,F) ==
   2.105          \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
   2.106  
   2.107    composition :: "[i=>o,i,i,i] => o"
   2.108 -    "composition(M,r,s,t) == 
   2.109 -        \<forall>p[M]. p \<in> t <-> 
   2.110 -               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   2.111 -                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   2.112 +    "composition(M,r,s,t) ==
   2.113 +        \<forall>p[M]. p \<in> t <->
   2.114 +               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
   2.115 +                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
   2.116                  xy \<in> s & yz \<in> r)"
   2.117  
   2.118    injection :: "[i=>o,i,i,i] => o"
   2.119 -    "injection(M,A,B,f) == 
   2.120 +    "injection(M,A,B,f) ==
   2.121  	typed_function(M,A,B,f) &
   2.122 -        (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M]. 
   2.123 +        (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
   2.124            pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')"
   2.125  
   2.126    surjection :: "[i=>o,i,i,i] => o"
   2.127 -    "surjection(M,A,B,f) == 
   2.128 +    "surjection(M,A,B,f) ==
   2.129          typed_function(M,A,B,f) &
   2.130          (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
   2.131  
   2.132 @@ -157,7 +157,7 @@
   2.133      "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
   2.134  
   2.135    restriction :: "[i=>o,i,i,i] => o"
   2.136 -    "restriction(M,r,A,z) == 
   2.137 +    "restriction(M,r,A,z) ==
   2.138  	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
   2.139  
   2.140    transitive_set :: "[i=>o,i] => o"
   2.141 @@ -169,19 +169,19 @@
   2.142  
   2.143    limit_ordinal :: "[i=>o,i] => o"
   2.144      --{*a limit ordinal is a non-empty, successor-closed ordinal*}
   2.145 -    "limit_ordinal(M,a) == 
   2.146 -	ordinal(M,a) & ~ empty(M,a) & 
   2.147 +    "limit_ordinal(M,a) ==
   2.148 +	ordinal(M,a) & ~ empty(M,a) &
   2.149          (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
   2.150  
   2.151    successor_ordinal :: "[i=>o,i] => o"
   2.152      --{*a successor ordinal is any ordinal that is neither empty nor limit*}
   2.153 -    "successor_ordinal(M,a) == 
   2.154 +    "successor_ordinal(M,a) ==
   2.155  	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
   2.156  
   2.157    finite_ordinal :: "[i=>o,i] => o"
   2.158      --{*an ordinal is finite if neither it nor any of its elements are limit*}
   2.159 -    "finite_ordinal(M,a) == 
   2.160 -	ordinal(M,a) & ~ limit_ordinal(M,a) & 
   2.161 +    "finite_ordinal(M,a) ==
   2.162 +	ordinal(M,a) & ~ limit_ordinal(M,a) &
   2.163          (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   2.164  
   2.165    omega :: "[i=>o,i] => o"
   2.166 @@ -192,7 +192,7 @@
   2.167      "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
   2.168  
   2.169    is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
   2.170 -    "is_nat_case(M, a, is_b, k, z) == 
   2.171 +    "is_nat_case(M, a, is_b, k, z) ==
   2.172         (empty(M,k) --> z=a) &
   2.173         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   2.174         (is_quasinat(M,k) | empty(M,z))"
   2.175 @@ -202,7 +202,7 @@
   2.176  
   2.177    Relativize1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
   2.178      --{*as above, but typed*}
   2.179 -    "Relativize1(M,A,is_f,f) == 
   2.180 +    "Relativize1(M,A,is_f,f) ==
   2.181          \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
   2.182  
   2.183    relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
   2.184 @@ -213,42 +213,42 @@
   2.185          \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A --> y\<in>B --> is_f(x,y,z) <-> z = f(x,y)"
   2.186  
   2.187    relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   2.188 -    "relativize3(M,is_f,f) == 
   2.189 +    "relativize3(M,is_f,f) ==
   2.190         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
   2.191  
   2.192    Relativize3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   2.193 -    "Relativize3(M,A,B,C,is_f,f) == 
   2.194 -       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. 
   2.195 +    "Relativize3(M,A,B,C,is_f,f) ==
   2.196 +       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
   2.197           x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
   2.198  
   2.199    relativize4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
   2.200 -    "relativize4(M,is_f,f) == 
   2.201 +    "relativize4(M,is_f,f) ==
   2.202         \<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) <-> a = f(u,x,y,z)"
   2.203  
   2.204  
   2.205  text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
   2.206  lemma triv_Relativize1:
   2.207       "Relativize1(M, A, \<lambda>x y. y = f(x), f)"
   2.208 -by (simp add: Relativize1_def) 
   2.209 +by (simp add: Relativize1_def)
   2.210  
   2.211  lemma triv_Relativize2:
   2.212       "Relativize2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
   2.213 -by (simp add: Relativize2_def) 
   2.214 +by (simp add: Relativize2_def)
   2.215  
   2.216  
   2.217  subsection {*The relativized ZF axioms*}
   2.218  constdefs
   2.219  
   2.220    extensionality :: "(i=>o) => o"
   2.221 -    "extensionality(M) == 
   2.222 +    "extensionality(M) ==
   2.223  	\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"
   2.224  
   2.225    separation :: "[i=>o, i=>o] => o"
   2.226      --{*The formula @{text P} should only involve parameters
   2.227 -        belonging to @{text M}.  But we can't prove separation as a scheme
   2.228 -        anyway.  Every instance that we need must individually be assumed
   2.229 -        and later proved.*}
   2.230 -    "separation(M,P) == 
   2.231 +        belonging to @{text M} and all its quantifiers must be relativized
   2.232 +        to @{text M}.  We do not have separation as a scheme; every instance
   2.233 +        that we need must be assumed (and later proved) separately.*}
   2.234 +    "separation(M,P) ==
   2.235  	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   2.236  
   2.237    upair_ax :: "(i=>o) => o"
   2.238 @@ -261,73 +261,73 @@
   2.239      "power_ax(M) == \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)"
   2.240  
   2.241    univalent :: "[i=>o, i, [i,i]=>o] => o"
   2.242 -    "univalent(M,A,P) == 
   2.243 -	(\<forall>x[M]. x\<in>A --> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) --> y=z))"
   2.244 +    "univalent(M,A,P) ==
   2.245 +	\<forall>x[M]. x\<in>A --> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) --> y=z)"
   2.246  
   2.247    replacement :: "[i=>o, [i,i]=>o] => o"
   2.248 -    "replacement(M,P) == 
   2.249 +    "replacement(M,P) ==
   2.250        \<forall>A[M]. univalent(M,A,P) -->
   2.251        (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)"
   2.252  
   2.253    strong_replacement :: "[i=>o, [i,i]=>o] => o"
   2.254 -    "strong_replacement(M,P) == 
   2.255 +    "strong_replacement(M,P) ==
   2.256        \<forall>A[M]. univalent(M,A,P) -->
   2.257        (\<exists>Y[M]. \<forall>b[M]. b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))"
   2.258  
   2.259    foundation_ax :: "(i=>o) => o"
   2.260 -    "foundation_ax(M) == 
   2.261 +    "foundation_ax(M) ==
   2.262  	\<forall>x[M]. (\<exists>y[M]. y\<in>x) --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
   2.263  
   2.264  
   2.265  subsection{*A trivial consistency proof for $V_\omega$ *}
   2.266  
   2.267 -text{*We prove that $V_\omega$ 
   2.268 +text{*We prove that $V_\omega$
   2.269        (or @{text univ} in Isabelle) satisfies some ZF axioms.
   2.270       Kunen, Theorem IV 3.13, page 123.*}
   2.271  
   2.272  lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
   2.273 -apply (insert Transset_univ [OF Transset_0])  
   2.274 -apply (simp add: Transset_def, blast) 
   2.275 +apply (insert Transset_univ [OF Transset_0])
   2.276 +apply (simp add: Transset_def, blast)
   2.277  done
   2.278  
   2.279 -lemma univ0_Ball_abs [simp]: 
   2.280 -     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   2.281 -by (blast intro: univ0_downwards_mem) 
   2.282 +lemma univ0_Ball_abs [simp]:
   2.283 +     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))"
   2.284 +by (blast intro: univ0_downwards_mem)
   2.285  
   2.286 -lemma univ0_Bex_abs [simp]: 
   2.287 -     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   2.288 -by (blast intro: univ0_downwards_mem) 
   2.289 +lemma univ0_Bex_abs [simp]:
   2.290 +     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))"
   2.291 +by (blast intro: univ0_downwards_mem)
   2.292  
   2.293  text{*Congruence rule for separation: can assume the variable is in @{text M}*}
   2.294  lemma separation_cong [cong]:
   2.295 -     "(!!x. M(x) ==> P(x) <-> P'(x)) 
   2.296 +     "(!!x. M(x) ==> P(x) <-> P'(x))
   2.297        ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
   2.298 -by (simp add: separation_def) 
   2.299 +by (simp add: separation_def)
   2.300  
   2.301  lemma univalent_cong [cong]:
   2.302 -     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   2.303 +     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
   2.304        ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
   2.305 -by (simp add: univalent_def) 
   2.306 +by (simp add: univalent_def)
   2.307  
   2.308  lemma univalent_triv [intro,simp]:
   2.309       "univalent(M, A, \<lambda>x y. y = f(x))"
   2.310 -by (simp add: univalent_def) 
   2.311 +by (simp add: univalent_def)
   2.312  
   2.313  lemma univalent_conjI2 [intro,simp]:
   2.314       "univalent(M,A,Q) ==> univalent(M, A, \<lambda>x y. P(x,y) & Q(x,y))"
   2.315 -by (simp add: univalent_def, blast) 
   2.316 +by (simp add: univalent_def, blast)
   2.317  
   2.318  text{*Congruence rule for replacement*}
   2.319  lemma strong_replacement_cong [cong]:
   2.320 -     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   2.321 -      ==> strong_replacement(M, %x y. P(x,y)) <-> 
   2.322 -          strong_replacement(M, %x y. P'(x,y))" 
   2.323 -by (simp add: strong_replacement_def) 
   2.324 +     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
   2.325 +      ==> strong_replacement(M, %x y. P(x,y)) <->
   2.326 +          strong_replacement(M, %x y. P'(x,y))"
   2.327 +by (simp add: strong_replacement_def)
   2.328  
   2.329  text{*The extensionality axiom*}
   2.330  lemma "extensionality(\<lambda>x. x \<in> univ(0))"
   2.331  apply (simp add: extensionality_def)
   2.332 -apply (blast intro: univ0_downwards_mem) 
   2.333 +apply (blast intro: univ0_downwards_mem)
   2.334  done
   2.335  
   2.336  text{*The separation axiom requires some lemmas*}
   2.337 @@ -339,7 +339,7 @@
   2.338  done
   2.339  
   2.340  lemma Collect_in_VLimit:
   2.341 -     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] 
   2.342 +     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
   2.343        ==> Collect(X,P) \<in> Vfrom(A,i)"
   2.344  apply (rule Limit_VfromE, assumption+)
   2.345  apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
   2.346 @@ -350,23 +350,23 @@
   2.347  by (simp add: univ_def Collect_in_VLimit Limit_nat)
   2.348  
   2.349  lemma "separation(\<lambda>x. x \<in> univ(0), P)"
   2.350 -apply (simp add: separation_def, clarify) 
   2.351 -apply (rule_tac x = "Collect(z,P)" in bexI) 
   2.352 +apply (simp add: separation_def, clarify)
   2.353 +apply (rule_tac x = "Collect(z,P)" in bexI)
   2.354  apply (blast intro: Collect_in_univ Transset_0)+
   2.355  done
   2.356  
   2.357  text{*Unordered pairing axiom*}
   2.358  lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
   2.359 -apply (simp add: upair_ax_def upair_def)  
   2.360 -apply (blast intro: doubleton_in_univ) 
   2.361 +apply (simp add: upair_ax_def upair_def)
   2.362 +apply (blast intro: doubleton_in_univ)
   2.363  done
   2.364  
   2.365  text{*Union axiom*}
   2.366 -lemma "Union_ax(\<lambda>x. x \<in> univ(0))"  
   2.367 -apply (simp add: Union_ax_def big_union_def, clarify) 
   2.368 -apply (rule_tac x="\<Union>x" in bexI)  
   2.369 +lemma "Union_ax(\<lambda>x. x \<in> univ(0))"
   2.370 +apply (simp add: Union_ax_def big_union_def, clarify)
   2.371 +apply (rule_tac x="\<Union>x" in bexI)
   2.372   apply (blast intro: univ0_downwards_mem)
   2.373 -apply (blast intro: Union_in_univ Transset_0) 
   2.374 +apply (blast intro: Union_in_univ Transset_0)
   2.375  done
   2.376  
   2.377  text{*Powerset axiom*}
   2.378 @@ -376,88 +376,88 @@
   2.379  apply (simp add: univ_def Pow_in_VLimit Limit_nat)
   2.380  done
   2.381  
   2.382 -lemma "power_ax(\<lambda>x. x \<in> univ(0))"  
   2.383 -apply (simp add: power_ax_def powerset_def subset_def, clarify) 
   2.384 +lemma "power_ax(\<lambda>x. x \<in> univ(0))"
   2.385 +apply (simp add: power_ax_def powerset_def subset_def, clarify)
   2.386  apply (rule_tac x="Pow(x)" in bexI)
   2.387   apply (blast intro: univ0_downwards_mem)
   2.388 -apply (blast intro: Pow_in_univ Transset_0) 
   2.389 +apply (blast intro: Pow_in_univ Transset_0)
   2.390  done
   2.391  
   2.392  text{*Foundation axiom*}
   2.393 -lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"  
   2.394 +lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"
   2.395  apply (simp add: foundation_ax_def, clarify)
   2.396 -apply (cut_tac A=x in foundation) 
   2.397 +apply (cut_tac A=x in foundation)
   2.398  apply (blast intro: univ0_downwards_mem)
   2.399  done
   2.400  
   2.401 -lemma "replacement(\<lambda>x. x \<in> univ(0), P)"  
   2.402 -apply (simp add: replacement_def, clarify) 
   2.403 +lemma "replacement(\<lambda>x. x \<in> univ(0), P)"
   2.404 +apply (simp add: replacement_def, clarify)
   2.405  oops
   2.406  text{*no idea: maybe prove by induction on the rank of A?*}
   2.407  
   2.408  text{*Still missing: Replacement, Choice*}
   2.409  
   2.410 -subsection{*lemmas needed to reduce some set constructions to instances
   2.411 +subsection{*Lemmas Needed to Reduce Some Set Constructions to Instances
   2.412        of Separation*}
   2.413  
   2.414  lemma image_iff_Collect: "r `` A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
   2.415 -apply (rule equalityI, auto) 
   2.416 -apply (simp add: Pair_def, blast) 
   2.417 +apply (rule equalityI, auto)
   2.418 +apply (simp add: Pair_def, blast)
   2.419  done
   2.420  
   2.421  lemma vimage_iff_Collect:
   2.422       "r -`` A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
   2.423 -apply (rule equalityI, auto) 
   2.424 -apply (simp add: Pair_def, blast) 
   2.425 +apply (rule equalityI, auto)
   2.426 +apply (simp add: Pair_def, blast)
   2.427  done
   2.428  
   2.429 -text{*These two lemmas lets us prove @{text domain_closed} and 
   2.430 +text{*These two lemmas lets us prove @{text domain_closed} and
   2.431        @{text range_closed} without new instances of separation*}
   2.432  
   2.433  lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
   2.434  apply (rule equalityI, auto)
   2.435  apply (rule vimageI, assumption)
   2.436 -apply (simp add: Pair_def, blast) 
   2.437 +apply (simp add: Pair_def, blast)
   2.438  done
   2.439  
   2.440  lemma range_eq_image: "range(r) = r `` Union(Union(r))"
   2.441  apply (rule equalityI, auto)
   2.442  apply (rule imageI, assumption)
   2.443 -apply (simp add: Pair_def, blast) 
   2.444 +apply (simp add: Pair_def, blast)
   2.445  done
   2.446  
   2.447  lemma replacementD:
   2.448      "[| replacement(M,P); M(A);  univalent(M,A,P) |]
   2.449       ==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y))"
   2.450 -by (simp add: replacement_def) 
   2.451 +by (simp add: replacement_def)
   2.452  
   2.453  lemma strong_replacementD:
   2.454      "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
   2.455       ==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b))))"
   2.456 -by (simp add: strong_replacement_def) 
   2.457 +by (simp add: strong_replacement_def)
   2.458  
   2.459  lemma separationD:
   2.460      "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   2.461 -by (simp add: separation_def) 
   2.462 +by (simp add: separation_def)
   2.463  
   2.464  
   2.465  text{*More constants, for order types*}
   2.466  constdefs
   2.467  
   2.468    order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
   2.469 -    "order_isomorphism(M,A,r,B,s,f) == 
   2.470 -        bijection(M,A,B,f) & 
   2.471 +    "order_isomorphism(M,A,r,B,s,f) ==
   2.472 +        bijection(M,A,B,f) &
   2.473          (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
   2.474            (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
   2.475 -            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> 
   2.476 +            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
   2.477              pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
   2.478  
   2.479    pred_set :: "[i=>o,i,i,i,i] => o"
   2.480 -    "pred_set(M,A,x,r,B) == 
   2.481 +    "pred_set(M,A,x,r,B) ==
   2.482  	\<forall>y[M]. y \<in> B <-> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
   2.483  
   2.484    membership :: "[i=>o,i,i] => o" --{*membership relation*}
   2.485 -    "membership(M,A,r) == 
   2.486 +    "membership(M,A,r) ==
   2.487  	\<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)))"
   2.488  
   2.489  
   2.490 @@ -468,67 +468,72 @@
   2.491  locale M_trivial =
   2.492    fixes M
   2.493    assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
   2.494 -      and nonempty [simp]:  "M(0)"
   2.495        and upair_ax:	    "upair_ax(M)"
   2.496        and Union_ax:	    "Union_ax(M)"
   2.497        and power_ax:         "power_ax(M)"
   2.498        and replacement:      "replacement(M,P)"
   2.499        and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
   2.500  
   2.501 -lemma (in M_trivial) rall_abs [simp]: 
   2.502 -     "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   2.503 -by (blast intro: transM) 
   2.504 +
   2.505 +text{*Automatically discovers the proof using @{text transM}, @{text nat_0I}
   2.506 +and @{text M_nat}.*}
   2.507 +lemma (in M_trivial) nonempty [simp]: "M(0)"
   2.508 +by (blast intro: transM)
   2.509  
   2.510 -lemma (in M_trivial) rex_abs [simp]: 
   2.511 -     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   2.512 -by (blast intro: transM) 
   2.513 +lemma (in M_trivial) rall_abs [simp]:
   2.514 +     "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))"
   2.515 +by (blast intro: transM)
   2.516  
   2.517 -lemma (in M_trivial) ball_iff_equiv: 
   2.518 -     "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <-> 
   2.519 -               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   2.520 +lemma (in M_trivial) rex_abs [simp]:
   2.521 +     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))"
   2.522 +by (blast intro: transM)
   2.523 +
   2.524 +lemma (in M_trivial) ball_iff_equiv:
   2.525 +     "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <->
   2.526 +               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)"
   2.527  by (blast intro: transM)
   2.528  
   2.529  text{*Simplifies proofs of equalities when there's an iff-equality
   2.530        available for rewriting, universally quantified over M. *}
   2.531 -lemma (in M_trivial) M_equalityI: 
   2.532 +lemma (in M_trivial) M_equalityI:
   2.533       "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
   2.534 -by (blast intro!: equalityI dest: transM) 
   2.535 +by (blast intro!: equalityI dest: transM)
   2.536  
   2.537  
   2.538  subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
   2.539  
   2.540 -lemma (in M_trivial) empty_abs [simp]: 
   2.541 +lemma (in M_trivial) empty_abs [simp]:
   2.542       "M(z) ==> empty(M,z) <-> z=0"
   2.543  apply (simp add: empty_def)
   2.544 -apply (blast intro: transM) 
   2.545 +apply (blast intro: transM)
   2.546  done
   2.547  
   2.548 -lemma (in M_trivial) subset_abs [simp]: 
   2.549 +lemma (in M_trivial) subset_abs [simp]:
   2.550       "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
   2.551 -apply (simp add: subset_def) 
   2.552 -apply (blast intro: transM) 
   2.553 +apply (simp add: subset_def)
   2.554 +apply (blast intro: transM)
   2.555  done
   2.556  
   2.557 -lemma (in M_trivial) upair_abs [simp]: 
   2.558 +lemma (in M_trivial) upair_abs [simp]:
   2.559       "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
   2.560 -apply (simp add: upair_def) 
   2.561 -apply (blast intro: transM) 
   2.562 +apply (simp add: upair_def)
   2.563 +apply (blast intro: transM)
   2.564  done
   2.565  
   2.566  lemma (in M_trivial) upair_in_M_iff [iff]:
   2.567       "M({a,b}) <-> M(a) & M(b)"
   2.568 -apply (insert upair_ax, simp add: upair_ax_def) 
   2.569 -apply (blast intro: transM) 
   2.570 +apply (insert upair_ax, simp add: upair_ax_def)
   2.571 +apply (blast intro: transM)
   2.572  done
   2.573  
   2.574  lemma (in M_trivial) singleton_in_M_iff [iff]:
   2.575       "M({a}) <-> M(a)"
   2.576 -by (insert upair_in_M_iff [of a a], simp) 
   2.577 +by (insert upair_in_M_iff [of a a], simp)
   2.578  
   2.579 -lemma (in M_trivial) pair_abs [simp]: 
   2.580 +lemma (in M_trivial) pair_abs [simp]:
   2.581       "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   2.582  apply (simp add: pair_def ZF.Pair_def)
   2.583 -apply (blast intro: transM) 
   2.584 +apply (blast intro: transM)
   2.585  done
   2.586  
   2.587  lemma (in M_trivial) pair_in_M_iff [iff]:
   2.588 @@ -538,84 +543,84 @@
   2.589  lemma (in M_trivial) pair_components_in_M:
   2.590       "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   2.591  apply (simp add: Pair_def)
   2.592 -apply (blast dest: transM) 
   2.593 +apply (blast dest: transM)
   2.594  done
   2.595  
   2.596 -lemma (in M_trivial) cartprod_abs [simp]: 
   2.597 +lemma (in M_trivial) cartprod_abs [simp]:
   2.598       "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   2.599  apply (simp add: cartprod_def)
   2.600 -apply (rule iffI) 
   2.601 - apply (blast intro!: equalityI intro: transM dest!: rspec) 
   2.602 -apply (blast dest: transM) 
   2.603 +apply (rule iffI)
   2.604 + apply (blast intro!: equalityI intro: transM dest!: rspec)
   2.605 +apply (blast dest: transM)
   2.606  done
   2.607  
   2.608  subsubsection{*Absoluteness for Unions and Intersections*}
   2.609  
   2.610 -lemma (in M_trivial) union_abs [simp]: 
   2.611 +lemma (in M_trivial) union_abs [simp]:
   2.612       "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   2.613 -apply (simp add: union_def) 
   2.614 -apply (blast intro: transM) 
   2.615 +apply (simp add: union_def)
   2.616 +apply (blast intro: transM)
   2.617  done
   2.618  
   2.619 -lemma (in M_trivial) inter_abs [simp]: 
   2.620 +lemma (in M_trivial) inter_abs [simp]:
   2.621       "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   2.622 -apply (simp add: inter_def) 
   2.623 -apply (blast intro: transM) 
   2.624 +apply (simp add: inter_def)
   2.625 +apply (blast intro: transM)
   2.626  done
   2.627  
   2.628 -lemma (in M_trivial) setdiff_abs [simp]: 
   2.629 +lemma (in M_trivial) setdiff_abs [simp]:
   2.630       "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   2.631 -apply (simp add: setdiff_def) 
   2.632 -apply (blast intro: transM) 
   2.633 +apply (simp add: setdiff_def)
   2.634 +apply (blast intro: transM)
   2.635  done
   2.636  
   2.637 -lemma (in M_trivial) Union_abs [simp]: 
   2.638 +lemma (in M_trivial) Union_abs [simp]:
   2.639       "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   2.640 -apply (simp add: big_union_def) 
   2.641 -apply (blast intro!: equalityI dest: transM) 
   2.642 +apply (simp add: big_union_def)
   2.643 +apply (blast intro!: equalityI dest: transM)
   2.644  done
   2.645  
   2.646  lemma (in M_trivial) Union_closed [intro,simp]:
   2.647       "M(A) ==> M(Union(A))"
   2.648 -by (insert Union_ax, simp add: Union_ax_def) 
   2.649 +by (insert Union_ax, simp add: Union_ax_def)
   2.650  
   2.651  lemma (in M_trivial) Un_closed [intro,simp]:
   2.652       "[| M(A); M(B) |] ==> M(A Un B)"
   2.653 -by (simp only: Un_eq_Union, blast) 
   2.654 +by (simp only: Un_eq_Union, blast)
   2.655  
   2.656  lemma (in M_trivial) cons_closed [intro,simp]:
   2.657       "[| M(a); M(A) |] ==> M(cons(a,A))"
   2.658 -by (subst cons_eq [symmetric], blast) 
   2.659 +by (subst cons_eq [symmetric], blast)
   2.660  
   2.661 -lemma (in M_trivial) cons_abs [simp]: 
   2.662 +lemma (in M_trivial) cons_abs [simp]:
   2.663       "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
   2.664 -by (simp add: is_cons_def, blast intro: transM)  
   2.665 +by (simp add: is_cons_def, blast intro: transM)
   2.666  
   2.667 -lemma (in M_trivial) successor_abs [simp]: 
   2.668 +lemma (in M_trivial) successor_abs [simp]:
   2.669       "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
   2.670 -by (simp add: successor_def, blast)  
   2.671 +by (simp add: successor_def, blast)
   2.672  
   2.673  lemma (in M_trivial) succ_in_M_iff [iff]:
   2.674       "M(succ(a)) <-> M(a)"
   2.675 -apply (simp add: succ_def) 
   2.676 -apply (blast intro: transM) 
   2.677 +apply (simp add: succ_def)
   2.678 +apply (blast intro: transM)
   2.679  done
   2.680  
   2.681  subsubsection{*Absoluteness for Separation and Replacement*}
   2.682  
   2.683  lemma (in M_trivial) separation_closed [intro,simp]:
   2.684       "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   2.685 -apply (insert separation, simp add: separation_def) 
   2.686 -apply (drule rspec, assumption, clarify) 
   2.687 +apply (insert separation, simp add: separation_def)
   2.688 +apply (drule rspec, assumption, clarify)
   2.689  apply (subgoal_tac "y = Collect(A,P)", blast)
   2.690 -apply (blast dest: transM) 
   2.691 +apply (blast dest: transM)
   2.692  done
   2.693  
   2.694  lemma separation_iff:
   2.695       "separation(M,P) <-> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
   2.696 -by (simp add: separation_def is_Collect_def) 
   2.697 +by (simp add: separation_def is_Collect_def)
   2.698  
   2.699 -lemma (in M_trivial) Collect_abs [simp]: 
   2.700 +lemma (in M_trivial) Collect_abs [simp]:
   2.701       "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)"
   2.702  apply (simp add: is_Collect_def)
   2.703  apply (blast intro!: equalityI dest: transM)
   2.704 @@ -625,70 +630,68 @@
   2.705  lemma (in M_trivial) strong_replacementI [rule_format]:
   2.706      "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
   2.707       ==> strong_replacement(M,P)"
   2.708 -apply (simp add: strong_replacement_def, clarify) 
   2.709 -apply (frule replacementD [OF replacement], assumption, clarify) 
   2.710 -apply (drule_tac x=A in rspec, clarify)  
   2.711 -apply (drule_tac z=Y in separationD, assumption, clarify) 
   2.712 -apply (rule_tac x=y in rexI) 
   2.713 -apply (blast dest: transM)+
   2.714 +apply (simp add: strong_replacement_def, clarify)
   2.715 +apply (frule replacementD [OF replacement], assumption, clarify)
   2.716 +apply (drule_tac x=A in rspec, clarify)
   2.717 +apply (drule_tac z=Y in separationD, assumption, clarify)
   2.718 +apply (rule_tac x=y in rexI, force, assumption)
   2.719  done
   2.720  
   2.721 -
   2.722  subsubsection{*The Operator @{term is_Replace}*}
   2.723  
   2.724  
   2.725  lemma is_Replace_cong [cong]:
   2.726 -     "[| A=A'; 
   2.727 +     "[| A=A';
   2.728           !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y);
   2.729 -         z=z' |] 
   2.730 -      ==> is_Replace(M, A, %x y. P(x,y), z) <-> 
   2.731 -          is_Replace(M, A', %x y. P'(x,y), z')" 
   2.732 -by (simp add: is_Replace_def) 
   2.733 +         z=z' |]
   2.734 +      ==> is_Replace(M, A, %x y. P(x,y), z) <->
   2.735 +          is_Replace(M, A', %x y. P'(x,y), z')"
   2.736 +by (simp add: is_Replace_def)
   2.737  
   2.738 -lemma (in M_trivial) univalent_Replace_iff: 
   2.739 +lemma (in M_trivial) univalent_Replace_iff:
   2.740       "[| M(A); univalent(M,A,P);
   2.741 -         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] 
   2.742 +         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
   2.743        ==> u \<in> Replace(A,P) <-> (\<exists>x. x\<in>A & P(x,u))"
   2.744 -apply (simp add: Replace_iff univalent_def) 
   2.745 +apply (simp add: Replace_iff univalent_def)
   2.746  apply (blast dest: transM)
   2.747  done
   2.748  
   2.749  (*The last premise expresses that P takes M to M*)
   2.750  lemma (in M_trivial) strong_replacement_closed [intro,simp]:
   2.751 -     "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   2.752 +     "[| strong_replacement(M,P); M(A); univalent(M,A,P);
   2.753           !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
   2.754 -apply (simp add: strong_replacement_def) 
   2.755 -apply (drule_tac x=A in rspec, safe) 
   2.756 +apply (simp add: strong_replacement_def)
   2.757 +apply (drule_tac x=A in rspec, safe)
   2.758  apply (subgoal_tac "Replace(A,P) = Y")
   2.759 - apply simp 
   2.760 + apply simp
   2.761  apply (rule equality_iffI)
   2.762  apply (simp add: univalent_Replace_iff)
   2.763 -apply (blast dest: transM) 
   2.764 +apply (blast dest: transM)
   2.765  done
   2.766  
   2.767 -lemma (in M_trivial) Replace_abs: 
   2.768 +lemma (in M_trivial) Replace_abs:
   2.769       "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P);
   2.770 -         !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |] 
   2.771 +         !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |]
   2.772        ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
   2.773  apply (simp add: is_Replace_def)
   2.774 -apply (rule iffI) 
   2.775 -apply (rule M_equalityI) 
   2.776 -apply (simp_all add: univalent_Replace_iff, blast, blast) 
   2.777 +apply (rule iffI)
   2.778 +apply (rule M_equalityI)
   2.779 +apply (simp_all add: univalent_Replace_iff, blast, blast)
   2.780  done
   2.781  
   2.782  (*The first premise can't simply be assumed as a schema.
   2.783    It is essential to take care when asserting instances of Replacement.
   2.784    Let K be a nonconstructible subset of nat and define
   2.785 -  f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   2.786 +  f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a
   2.787    nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   2.788    even for f : M -> M.
   2.789  *)
   2.790  lemma (in M_trivial) RepFun_closed:
   2.791       "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   2.792        ==> M(RepFun(A,f))"
   2.793 -apply (simp add: RepFun_def) 
   2.794 -apply (rule strong_replacement_closed) 
   2.795 -apply (auto dest: transM  simp add: univalent_def) 
   2.796 +apply (simp add: RepFun_def)
   2.797 +apply (rule strong_replacement_closed)
   2.798 +apply (auto dest: transM  simp add: univalent_def)
   2.799  done
   2.800  
   2.801  lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
   2.802 @@ -701,69 +704,69 @@
   2.803        ==> M(RepFun(A, %x. f(x)))"
   2.804  apply (simp add: RepFun_def)
   2.805  apply (frule strong_replacement_closed, assumption)
   2.806 -apply (auto dest: transM  simp add: Replace_conj_eq univalent_def) 
   2.807 +apply (auto dest: transM  simp add: Replace_conj_eq univalent_def)
   2.808  done
   2.809  
   2.810  subsubsection {*Absoluteness for @{term Lambda}*}
   2.811  
   2.812  constdefs
   2.813   is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
   2.814 -    "is_lambda(M, A, is_b, z) == 
   2.815 +    "is_lambda(M, A, is_b, z) ==
   2.816         \<forall>p[M]. p \<in> z <->
   2.817          (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
   2.818  
   2.819  lemma (in M_trivial) lam_closed:
   2.820       "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   2.821        ==> M(\<lambda>x\<in>A. b(x))"
   2.822 -by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
   2.823 +by (simp add: lam_def, blast intro: RepFun_closed dest: transM)
   2.824  
   2.825  text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
   2.826  lemma (in M_trivial) lam_closed2:
   2.827    "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   2.828       M(A); \<forall>m[M]. m\<in>A --> M(b(m))|] ==> M(Lambda(A,b))"
   2.829  apply (simp add: lam_def)
   2.830 -apply (blast intro: RepFun_closed2 dest: transM)  
   2.831 +apply (blast intro: RepFun_closed2 dest: transM)
   2.832  done
   2.833  
   2.834 -lemma (in M_trivial) lambda_abs2 [simp]: 
   2.835 +lemma (in M_trivial) lambda_abs2 [simp]:
   2.836       "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   2.837 -         Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |] 
   2.838 +         Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
   2.839        ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
   2.840  apply (simp add: Relativize1_def is_lambda_def)
   2.841  apply (rule iffI)
   2.842 - prefer 2 apply (simp add: lam_def) 
   2.843 + prefer 2 apply (simp add: lam_def)
   2.844  apply (rule M_equalityI)
   2.845 -  apply (simp add: lam_def) 
   2.846 +  apply (simp add: lam_def)
   2.847   apply (simp add: lam_closed2)+
   2.848  done
   2.849  
   2.850  lemma is_lambda_cong [cong]:
   2.851 -     "[| A=A';  z=z'; 
   2.852 -         !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] 
   2.853 -      ==> is_lambda(M, A, %x y. is_b(x,y), z) <-> 
   2.854 -          is_lambda(M, A', %x y. is_b'(x,y), z')" 
   2.855 -by (simp add: is_lambda_def) 
   2.856 +     "[| A=A';  z=z';
   2.857 +         !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
   2.858 +      ==> is_lambda(M, A, %x y. is_b(x,y), z) <->
   2.859 +          is_lambda(M, A', %x y. is_b'(x,y), z')"
   2.860 +by (simp add: is_lambda_def)
   2.861  
   2.862 -lemma (in M_trivial) image_abs [simp]: 
   2.863 +lemma (in M_trivial) image_abs [simp]:
   2.864       "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   2.865  apply (simp add: image_def)
   2.866 -apply (rule iffI) 
   2.867 - apply (blast intro!: equalityI dest: transM, blast) 
   2.868 +apply (rule iffI)
   2.869 + apply (blast intro!: equalityI dest: transM, blast)
   2.870  done
   2.871  
   2.872  text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   2.873        This result is one direction of absoluteness.*}
   2.874  
   2.875 -lemma (in M_trivial) powerset_Pow: 
   2.876 +lemma (in M_trivial) powerset_Pow:
   2.877       "powerset(M, x, Pow(x))"
   2.878  by (simp add: powerset_def)
   2.879  
   2.880  text{*But we can't prove that the powerset in @{text M} includes the
   2.881        real powerset.*}
   2.882 -lemma (in M_trivial) powerset_imp_subset_Pow: 
   2.883 +lemma (in M_trivial) powerset_imp_subset_Pow:
   2.884       "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   2.885 -apply (simp add: powerset_def) 
   2.886 -apply (blast dest: transM) 
   2.887 +apply (simp add: powerset_def)
   2.888 +apply (blast dest: transM)
   2.889  done
   2.890  
   2.891  subsubsection{*Absoluteness for the Natural Numbers*}
   2.892 @@ -774,126 +777,123 @@
   2.893  
   2.894  lemma (in M_trivial) nat_case_closed [intro,simp]:
   2.895    "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   2.896 -apply (case_tac "k=0", simp) 
   2.897 +apply (case_tac "k=0", simp)
   2.898  apply (case_tac "\<exists>m. k = succ(m)", force)
   2.899 -apply (simp add: nat_case_def) 
   2.900 +apply (simp add: nat_case_def)
   2.901  done
   2.902  
   2.903 -lemma (in M_trivial) quasinat_abs [simp]: 
   2.904 +lemma (in M_trivial) quasinat_abs [simp]:
   2.905       "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
   2.906  by (auto simp add: is_quasinat_def quasinat_def)
   2.907  
   2.908 -lemma (in M_trivial) nat_case_abs [simp]: 
   2.909 -     "[| relativize1(M,is_b,b); M(k); M(z) |] 
   2.910 +lemma (in M_trivial) nat_case_abs [simp]:
   2.911 +     "[| relativize1(M,is_b,b); M(k); M(z) |]
   2.912        ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
   2.913 -apply (case_tac "quasinat(k)") 
   2.914 - prefer 2 
   2.915 - apply (simp add: is_nat_case_def non_nat_case) 
   2.916 - apply (force simp add: quasinat_def) 
   2.917 +apply (case_tac "quasinat(k)")
   2.918 + prefer 2
   2.919 + apply (simp add: is_nat_case_def non_nat_case)
   2.920 + apply (force simp add: quasinat_def)
   2.921  apply (simp add: quasinat_def is_nat_case_def)
   2.922 -apply (elim disjE exE) 
   2.923 - apply (simp_all add: relativize1_def) 
   2.924 +apply (elim disjE exE)
   2.925 + apply (simp_all add: relativize1_def)
   2.926  done
   2.927  
   2.928 -(*NOT for the simplifier.  The assumption M(z') is apparently necessary, but 
   2.929 +(*NOT for the simplifier.  The assumption M(z') is apparently necessary, but
   2.930    causes the error "Failed congruence proof!"  It may be better to replace
   2.931    is_nat_case by nat_case before attempting congruence reasoning.*)
   2.932  lemma is_nat_case_cong:
   2.933       "[| a = a'; k = k';  z = z';  M(z');
   2.934         !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
   2.935        ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
   2.936 -by (simp add: is_nat_case_def) 
   2.937 +by (simp add: is_nat_case_def)
   2.938  
   2.939  
   2.940  subsection{*Absoluteness for Ordinals*}
   2.941  text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   2.942  
   2.943  lemma (in M_trivial) lt_closed:
   2.944 -     "[| j<i; M(i) |] ==> M(j)" 
   2.945 -by (blast dest: ltD intro: transM) 
   2.946 +     "[| j<i; M(i) |] ==> M(j)"
   2.947 +by (blast dest: ltD intro: transM)
   2.948  
   2.949 -lemma (in M_trivial) transitive_set_abs [simp]: 
   2.950 +lemma (in M_trivial) transitive_set_abs [simp]:
   2.951       "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   2.952  by (simp add: transitive_set_def Transset_def)
   2.953  
   2.954 -lemma (in M_trivial) ordinal_abs [simp]: 
   2.955 +lemma (in M_trivial) ordinal_abs [simp]:
   2.956       "M(a) ==> ordinal(M,a) <-> Ord(a)"
   2.957  by (simp add: ordinal_def Ord_def)
   2.958  
   2.959 -lemma (in M_trivial) limit_ordinal_abs [simp]: 
   2.960 -     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)" 
   2.961 -apply (unfold Limit_def limit_ordinal_def) 
   2.962 -apply (simp add: Ord_0_lt_iff) 
   2.963 -apply (simp add: lt_def, blast) 
   2.964 +lemma (in M_trivial) limit_ordinal_abs [simp]:
   2.965 +     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   2.966 +apply (unfold Limit_def limit_ordinal_def)
   2.967 +apply (simp add: Ord_0_lt_iff)
   2.968 +apply (simp add: lt_def, blast)
   2.969  done
   2.970  
   2.971 -lemma (in M_trivial) successor_ordinal_abs [simp]: 
   2.972 +lemma (in M_trivial) successor_ordinal_abs [simp]:
   2.973       "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   2.974  apply (simp add: successor_ordinal_def, safe)
   2.975 -apply (drule Ord_cases_disj, auto) 
   2.976 +apply (drule Ord_cases_disj, auto)
   2.977  done
   2.978  
   2.979  lemma finite_Ord_is_nat:
   2.980        "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   2.981  by (induct a rule: trans_induct3, simp_all)
   2.982  
   2.983 -lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   2.984 -by (induct a rule: nat_induct, auto)
   2.985 -
   2.986 -lemma (in M_trivial) finite_ordinal_abs [simp]: 
   2.987 +lemma (in M_trivial) finite_ordinal_abs [simp]:
   2.988       "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   2.989  apply (simp add: finite_ordinal_def)
   2.990 -apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   2.991 +apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord
   2.992               dest: Ord_trans naturals_not_limit)
   2.993  done
   2.994  
   2.995  lemma Limit_non_Limit_implies_nat:
   2.996       "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   2.997 -apply (rule le_anti_sym) 
   2.998 -apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   2.999 - apply (simp add: lt_def)  
  2.1000 - apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
  2.1001 +apply (rule le_anti_sym)
  2.1002 +apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)
  2.1003 + apply (simp add: lt_def)
  2.1004 + apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat)
  2.1005  apply (erule nat_le_Limit)
  2.1006  done
  2.1007  
  2.1008 -lemma (in M_trivial) omega_abs [simp]: 
  2.1009 +lemma (in M_trivial) omega_abs [simp]:
  2.1010       "M(a) ==> omega(M,a) <-> a = nat"
  2.1011 -apply (simp add: omega_def) 
  2.1012 +apply (simp add: omega_def)
  2.1013  apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
  2.1014  done
  2.1015  
  2.1016 -lemma (in M_trivial) number1_abs [simp]: 
  2.1017 +lemma (in M_trivial) number1_abs [simp]:
  2.1018       "M(a) ==> number1(M,a) <-> a = 1"
  2.1019 -by (simp add: number1_def) 
  2.1020 +by (simp add: number1_def)
  2.1021  
  2.1022 -lemma (in M_trivial) number2_abs [simp]: 
  2.1023 +lemma (in M_trivial) number2_abs [simp]:
  2.1024       "M(a) ==> number2(M,a) <-> a = succ(1)"
  2.1025 -by (simp add: number2_def) 
  2.1026 +by (simp add: number2_def)
  2.1027  
  2.1028 -lemma (in M_trivial) number3_abs [simp]: 
  2.1029 +lemma (in M_trivial) number3_abs [simp]:
  2.1030       "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
  2.1031 -by (simp add: number3_def) 
  2.1032 +by (simp add: number3_def)
  2.1033  
  2.1034  text{*Kunen continued to 20...*}
  2.1035  
  2.1036 -(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
  2.1037 +(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything
  2.1038    but the recursion variable must stay unchanged.  But then the recursion
  2.1039 -  equations only hold for x\<in>nat (or in some other set) and not for the 
  2.1040 +  equations only hold for x\<in>nat (or in some other set) and not for the
  2.1041    whole of the class M.
  2.1042    consts
  2.1043      natnumber_aux :: "[i=>o,i] => i"
  2.1044  
  2.1045    primrec
  2.1046        "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
  2.1047 -      "natnumber_aux(M,succ(n)) = 
  2.1048 -	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
  2.1049 +      "natnumber_aux(M,succ(n)) =
  2.1050 +	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x))
  2.1051  		     then 1 else 0)"
  2.1052  
  2.1053    constdefs
  2.1054      natnumber :: "[i=>o,i,i] => o"
  2.1055        "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
  2.1056  
  2.1057 -  lemma (in M_trivial) [simp]: 
  2.1058 +  lemma (in M_trivial) [simp]:
  2.1059         "natnumber(M,0,x) == x=0"
  2.1060  *)
  2.1061  
  2.1062 @@ -905,114 +905,110 @@
  2.1063    and Diff_separation:
  2.1064       "M(B) ==> separation(M, \<lambda>x. x \<notin> B)"
  2.1065    and cartprod_separation:
  2.1066 -     "[| M(A); M(B) |] 
  2.1067 +     "[| M(A); M(B) |]
  2.1068        ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
  2.1069    and image_separation:
  2.1070 -     "[| M(A); M(r) |] 
  2.1071 +     "[| M(A); M(r) |]
  2.1072        ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
  2.1073    and converse_separation:
  2.1074 -     "M(r) ==> separation(M, 
  2.1075 +     "M(r) ==> separation(M,
  2.1076           \<lambda>z. \<exists>p[M]. p\<in>r & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
  2.1077    and restrict_separation:
  2.1078       "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
  2.1079    and comp_separation:
  2.1080       "[| M(r); M(s) |]
  2.1081 -      ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
  2.1082 -		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
  2.1083 +      ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
  2.1084 +		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) &
  2.1085                    xy\<in>s & yz\<in>r)"
  2.1086    and pred_separation:
  2.1087       "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
  2.1088    and Memrel_separation:
  2.1089       "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
  2.1090    and funspace_succ_replacement:
  2.1091 -     "M(n) ==> 
  2.1092 -      strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M]. 
  2.1093 +     "M(n) ==>
  2.1094 +      strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M].
  2.1095                  pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
  2.1096                  upair(M,cnbf,cnbf,z))"
  2.1097    and well_ord_iso_separation:
  2.1098 -     "[| M(A); M(f); M(r) |] 
  2.1099 -      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M]. 
  2.1100 +     "[| M(A); M(f); M(r) |]
  2.1101 +      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M].
  2.1102  		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
  2.1103    and obase_separation:
  2.1104       --{*part of the order type formalization*}
  2.1105 -     "[| M(A); M(r) |] 
  2.1106 -      ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
  2.1107 +     "[| M(A); M(r) |]
  2.1108 +      ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
  2.1109  	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
  2.1110  	     order_isomorphism(M,par,r,x,mx,g))"
  2.1111    and obase_equals_separation:
  2.1112 -     "[| M(A); M(r) |] 
  2.1113 -      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
  2.1114 -			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
  2.1115 +     "[| M(A); M(r) |]
  2.1116 +      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].
  2.1117 +			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].
  2.1118  			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
  2.1119  			      order_isomorphism(M,pxr,r,y,my,g))))"
  2.1120    and omap_replacement:
  2.1121 -     "[| M(A); M(r) |] 
  2.1122 +     "[| M(A); M(r) |]
  2.1123        ==> strong_replacement(M,
  2.1124 -             \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
  2.1125 -	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
  2.1126 +             \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
  2.1127 +	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
  2.1128  	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
  2.1129    and is_recfun_separation:
  2.1130       --{*for well-founded recursion*}
  2.1131 -     "[| M(r); M(f); M(g); M(a); M(b) |] 
  2.1132 -     ==> separation(M, 
  2.1133 -            \<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
  2.1134 -                pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
  2.1135 -                (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
  2.1136 +     "[| M(r); M(f); M(g); M(a); M(b) |]
  2.1137 +     ==> separation(M,
  2.1138 +            \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
  2.1139 +                pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r &
  2.1140 +                (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
  2.1141                                     fx \<noteq> gx))"
  2.1142  
  2.1143  lemma (in M_basic) cartprod_iff_lemma:
  2.1144 -     "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
  2.1145 +     "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
  2.1146           powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
  2.1147         ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
  2.1148 -apply (simp add: powerset_def) 
  2.1149 +apply (simp add: powerset_def)
  2.1150  apply (rule equalityI, clarify, simp)
  2.1151 - apply (frule transM, assumption) 
  2.1152 + apply (frule transM, assumption)
  2.1153   apply (frule transM, assumption, simp (no_asm_simp))
  2.1154 - apply blast 
  2.1155 + apply blast
  2.1156  apply clarify
  2.1157 -apply (frule transM, assumption, force) 
  2.1158 +apply (frule transM, assumption, force)
  2.1159  done
  2.1160  
  2.1161  lemma (in M_basic) cartprod_iff:
  2.1162 -     "[| M(A); M(B); M(C) |] 
  2.1163 -      ==> cartprod(M,A,B,C) <-> 
  2.1164 -          (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
  2.1165 +     "[| M(A); M(B); M(C) |]
  2.1166 +      ==> cartprod(M,A,B,C) <->
  2.1167 +          (\<exists>p1[M]. \<exists>p2[M]. powerset(M,A Un B,p1) & powerset(M,p1,p2) &
  2.1168                     C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
  2.1169  apply (simp add: Pair_def cartprod_def, safe)
  2.1170 -defer 1 
  2.1171 -  apply (simp add: powerset_def) 
  2.1172 - apply blast 
  2.1173 +defer 1
  2.1174 +  apply (simp add: powerset_def)
  2.1175 + apply blast
  2.1176  txt{*Final, difficult case: the left-to-right direction of the theorem.*}
  2.1177 -apply (insert power_ax, simp add: power_ax_def) 
  2.1178 -apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
  2.1179 -apply (blast, clarify) 
  2.1180 +apply (insert power_ax, simp add: power_ax_def)
  2.1181 +apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
  2.1182 +apply (blast, clarify)
  2.1183  apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
  2.1184  apply assumption
  2.1185 -apply (blast intro: cartprod_iff_lemma) 
  2.1186 +apply (blast intro: cartprod_iff_lemma)
  2.1187  done
  2.1188  
  2.1189  lemma (in M_basic) cartprod_closed_lemma:
  2.1190       "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
  2.1191  apply (simp del: cartprod_abs add: cartprod_iff)
  2.1192 -apply (insert power_ax, simp add: power_ax_def) 
  2.1193 -apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
  2.1194 -apply (blast, clarify) 
  2.1195 -apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
  2.1196 +apply (insert power_ax, simp add: power_ax_def)
  2.1197 +apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
  2.1198  apply (blast, clarify)
  2.1199 -apply (intro rexI exI conjI) 
  2.1200 -prefer 5 apply (rule refl) 
  2.1201 -prefer 3 apply assumption
  2.1202 -prefer 3 apply assumption
  2.1203 -apply (insert cartprod_separation [of A B], auto)
  2.1204 +apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec, auto)
  2.1205 +apply (intro rexI conjI, simp+)
  2.1206 +apply (insert cartprod_separation [of A B], simp)
  2.1207  done
  2.1208  
  2.1209  text{*All the lemmas above are necessary because Powerset is not absolute.
  2.1210        I should have used Replacement instead!*}
  2.1211 -lemma (in M_basic) cartprod_closed [intro,simp]: 
  2.1212 +lemma (in M_basic) cartprod_closed [intro,simp]:
  2.1213       "[| M(A); M(B) |] ==> M(A*B)"
  2.1214  by (frule cartprod_closed_lemma, assumption, force)
  2.1215  
  2.1216 -lemma (in M_basic) sum_closed [intro,simp]: 
  2.1217 +lemma (in M_basic) sum_closed [intro,simp]:
  2.1218       "[| M(A); M(B) |] ==> M(A+B)"
  2.1219  by (simp add: sum_def)
  2.1220  
  2.1221 @@ -1022,7 +1018,7 @@
  2.1222  
  2.1223  lemma (in M_trivial) Inl_in_M_iff [iff]:
  2.1224       "M(Inl(a)) <-> M(a)"
  2.1225 -by (simp add: Inl_def) 
  2.1226 +by (simp add: Inl_def)
  2.1227  
  2.1228  lemma (in M_trivial) Inl_abs [simp]:
  2.1229       "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
  2.1230 @@ -1030,7 +1026,7 @@
  2.1231  
  2.1232  lemma (in M_trivial) Inr_in_M_iff [iff]:
  2.1233       "M(Inr(a)) <-> M(a)"
  2.1234 -by (simp add: Inr_def) 
  2.1235 +by (simp add: Inr_def)
  2.1236  
  2.1237  lemma (in M_trivial) Inr_abs [simp]:
  2.1238       "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
  2.1239 @@ -1040,27 +1036,27 @@
  2.1240  subsubsection {*converse of a relation*}
  2.1241  
  2.1242  lemma (in M_basic) M_converse_iff:
  2.1243 -     "M(r) ==> 
  2.1244 -      converse(r) = 
  2.1245 -      {z \<in> Union(Union(r)) * Union(Union(r)). 
  2.1246 +     "M(r) ==>
  2.1247 +      converse(r) =
  2.1248 +      {z \<in> Union(Union(r)) * Union(Union(r)).
  2.1249         \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
  2.1250  apply (rule equalityI)
  2.1251 - prefer 2 apply (blast dest: transM, clarify, simp) 
  2.1252 -apply (simp add: Pair_def) 
  2.1253 -apply (blast dest: transM) 
  2.1254 + prefer 2 apply (blast dest: transM, clarify, simp)
  2.1255 +apply (simp add: Pair_def)
  2.1256 +apply (blast dest: transM)
  2.1257  done
  2.1258  
  2.1259 -lemma (in M_basic) converse_closed [intro,simp]: 
  2.1260 +lemma (in M_basic) converse_closed [intro,simp]:
  2.1261       "M(r) ==> M(converse(r))"
  2.1262  apply (simp add: M_converse_iff)
  2.1263  apply (insert converse_separation [of r], simp)
  2.1264  done
  2.1265  
  2.1266 -lemma (in M_basic) converse_abs [simp]: 
  2.1267 +lemma (in M_basic) converse_abs [simp]:
  2.1268       "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
  2.1269  apply (simp add: is_converse_def)
  2.1270  apply (rule iffI)
  2.1271 - prefer 2 apply blast 
  2.1272 + prefer 2 apply blast
  2.1273  apply (rule M_equalityI)
  2.1274    apply simp
  2.1275    apply (blast dest: transM)+
  2.1276 @@ -1069,98 +1065,98 @@
  2.1277  
  2.1278  subsubsection {*image, preimage, domain, range*}
  2.1279  
  2.1280 -lemma (in M_basic) image_closed [intro,simp]: 
  2.1281 +lemma (in M_basic) image_closed [intro,simp]:
  2.1282       "[| M(A); M(r) |] ==> M(r``A)"
  2.1283  apply (simp add: image_iff_Collect)
  2.1284 -apply (insert image_separation [of A r], simp) 
  2.1285 +apply (insert image_separation [of A r], simp)
  2.1286  done
  2.1287  
  2.1288 -lemma (in M_basic) vimage_abs [simp]: 
  2.1289 +lemma (in M_basic) vimage_abs [simp]:
  2.1290       "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
  2.1291  apply (simp add: pre_image_def)
  2.1292 -apply (rule iffI) 
  2.1293 - apply (blast intro!: equalityI dest: transM, blast) 
  2.1294 +apply (rule iffI)
  2.1295 + apply (blast intro!: equalityI dest: transM, blast)
  2.1296  done
  2.1297  
  2.1298 -lemma (in M_basic) vimage_closed [intro,simp]: 
  2.1299 +lemma (in M_basic) vimage_closed [intro,simp]:
  2.1300       "[| M(A); M(r) |] ==> M(r-``A)"
  2.1301  by (simp add: vimage_def)
  2.1302  
  2.1303  
  2.1304  subsubsection{*Domain, range and field*}
  2.1305  
  2.1306 -lemma (in M_basic) domain_abs [simp]: 
  2.1307 +lemma (in M_basic) domain_abs [simp]:
  2.1308       "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
  2.1309 -apply (simp add: is_domain_def) 
  2.1310 -apply (blast intro!: equalityI dest: transM) 
  2.1311 +apply (simp add: is_domain_def)
  2.1312 +apply (blast intro!: equalityI dest: transM)
  2.1313  done
  2.1314  
  2.1315 -lemma (in M_basic) domain_closed [intro,simp]: 
  2.1316 +lemma (in M_basic) domain_closed [intro,simp]:
  2.1317       "M(r) ==> M(domain(r))"
  2.1318  apply (simp add: domain_eq_vimage)
  2.1319  done
  2.1320  
  2.1321 -lemma (in M_basic) range_abs [simp]: 
  2.1322 +lemma (in M_basic) range_abs [simp]:
  2.1323       "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
  2.1324  apply (simp add: is_range_def)
  2.1325  apply (blast intro!: equalityI dest: transM)
  2.1326  done
  2.1327  
  2.1328 -lemma (in M_basic) range_closed [intro,simp]: 
  2.1329 +lemma (in M_basic) range_closed [intro,simp]:
  2.1330       "M(r) ==> M(range(r))"
  2.1331  apply (simp add: range_eq_image)
  2.1332  done
  2.1333  
  2.1334 -lemma (in M_basic) field_abs [simp]: 
  2.1335 +lemma (in M_basic) field_abs [simp]:
  2.1336       "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
  2.1337  by (simp add: domain_closed range_closed is_field_def field_def)
  2.1338  
  2.1339 -lemma (in M_basic) field_closed [intro,simp]: 
  2.1340 +lemma (in M_basic) field_closed [intro,simp]:
  2.1341       "M(r) ==> M(field(r))"
  2.1342 -by (simp add: domain_closed range_closed Un_closed field_def) 
  2.1343 +by (simp add: domain_closed range_closed Un_closed field_def)
  2.1344  
  2.1345  
  2.1346  subsubsection{*Relations, functions and application*}
  2.1347  
  2.1348 -lemma (in M_basic) relation_abs [simp]: 
  2.1349 +lemma (in M_basic) relation_abs [simp]:
  2.1350       "M(r) ==> is_relation(M,r) <-> relation(r)"
  2.1351 -apply (simp add: is_relation_def relation_def) 
  2.1352 +apply (simp add: is_relation_def relation_def)
  2.1353  apply (blast dest!: bspec dest: pair_components_in_M)+
  2.1354  done
  2.1355  
  2.1356 -lemma (in M_basic) function_abs [simp]: 
  2.1357 +lemma (in M_basic) function_abs [simp]:
  2.1358       "M(r) ==> is_function(M,r) <-> function(r)"
  2.1359 -apply (simp add: is_function_def function_def, safe) 
  2.1360 -   apply (frule transM, assumption) 
  2.1361 +apply (simp add: is_function_def function_def, safe)
  2.1362 +   apply (frule transM, assumption)
  2.1363    apply (blast dest: pair_components_in_M)+
  2.1364  done
  2.1365  
  2.1366 -lemma (in M_basic) apply_closed [intro,simp]: 
  2.1367 +lemma (in M_basic) apply_closed [intro,simp]:
  2.1368       "[|M(f); M(a)|] ==> M(f`a)"
  2.1369  by (simp add: apply_def)
  2.1370  
  2.1371 -lemma (in M_basic) apply_abs [simp]: 
  2.1372 +lemma (in M_basic) apply_abs [simp]:
  2.1373       "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
  2.1374 -apply (simp add: fun_apply_def apply_def, blast) 
  2.1375 +apply (simp add: fun_apply_def apply_def, blast)
  2.1376  done
  2.1377  
  2.1378 -lemma (in M_basic) typed_function_abs [simp]: 
  2.1379 +lemma (in M_basic) typed_function_abs [simp]:
  2.1380       "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
  2.1381 -apply (auto simp add: typed_function_def relation_def Pi_iff) 
  2.1382 +apply (auto simp add: typed_function_def relation_def Pi_iff)
  2.1383  apply (blast dest: pair_components_in_M)+
  2.1384  done
  2.1385  
  2.1386 -lemma (in M_basic) injection_abs [simp]: 
  2.1387 +lemma (in M_basic) injection_abs [simp]:
  2.1388       "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
  2.1389  apply (simp add: injection_def apply_iff inj_def apply_closed)
  2.1390 -apply (blast dest: transM [of _ A]) 
  2.1391 +apply (blast dest: transM [of _ A])
  2.1392  done
  2.1393  
  2.1394 -lemma (in M_basic) surjection_abs [simp]: 
  2.1395 +lemma (in M_basic) surjection_abs [simp]:
  2.1396       "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
  2.1397  by (simp add: surjection_def surj_def)
  2.1398  
  2.1399 -lemma (in M_basic) bijection_abs [simp]: 
  2.1400 +lemma (in M_basic) bijection_abs [simp]:
  2.1401       "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
  2.1402  by (simp add: bijection_def bij_def)
  2.1403  
  2.1404 @@ -1168,31 +1164,31 @@
  2.1405  subsubsection{*Composition of relations*}
  2.1406  
  2.1407  lemma (in M_basic) M_comp_iff:
  2.1408 -     "[| M(r); M(s) |] 
  2.1409 -      ==> r O s = 
  2.1410 -          {xz \<in> domain(s) * range(r).  
  2.1411 +     "[| M(r); M(s) |]
  2.1412 +      ==> r O s =
  2.1413 +          {xz \<in> domain(s) * range(r).
  2.1414              \<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}"
  2.1415  apply (simp add: comp_def)
  2.1416 -apply (rule equalityI) 
  2.1417 - apply clarify 
  2.1418 - apply simp 
  2.1419 +apply (rule equalityI)
  2.1420 + apply clarify
  2.1421 + apply simp
  2.1422   apply  (blast dest:  transM)+
  2.1423  done
  2.1424  
  2.1425 -lemma (in M_basic) comp_closed [intro,simp]: 
  2.1426 +lemma (in M_basic) comp_closed [intro,simp]:
  2.1427       "[| M(r); M(s) |] ==> M(r O s)"
  2.1428  apply (simp add: M_comp_iff)
  2.1429 -apply (insert comp_separation [of r s], simp) 
  2.1430 +apply (insert comp_separation [of r s], simp)
  2.1431  done
  2.1432  
  2.1433 -lemma (in M_basic) composition_abs [simp]: 
  2.1434 -     "[| M(r); M(s); M(t) |] 
  2.1435 +lemma (in M_basic) composition_abs [simp]:
  2.1436 +     "[| M(r); M(s); M(t) |]
  2.1437        ==> composition(M,r,s,t) <-> t = r O s"
  2.1438  apply safe
  2.1439   txt{*Proving @{term "composition(M, r, s, r O s)"}*}
  2.1440 - prefer 2 
  2.1441 + prefer 2
  2.1442   apply (simp add: composition_def comp_def)
  2.1443 - apply (blast dest: transM) 
  2.1444 + apply (blast dest: transM)
  2.1445  txt{*Opposite implication*}
  2.1446  apply (rule M_equalityI)
  2.1447    apply (simp add: composition_def comp_def)
  2.1448 @@ -1200,18 +1196,18 @@
  2.1449  done
  2.1450  
  2.1451  text{*no longer needed*}
  2.1452 -lemma (in M_basic) restriction_is_function: 
  2.1453 -     "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
  2.1454 +lemma (in M_basic) restriction_is_function:
  2.1455 +     "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]
  2.1456        ==> function(z)"
  2.1457 -apply (simp add: restriction_def ball_iff_equiv) 
  2.1458 -apply (unfold function_def, blast) 
  2.1459 +apply (simp add: restriction_def ball_iff_equiv)
  2.1460 +apply (unfold function_def, blast)
  2.1461  done
  2.1462  
  2.1463 -lemma (in M_basic) restriction_abs [simp]: 
  2.1464 -     "[| M(f); M(A); M(z) |] 
  2.1465 +lemma (in M_basic) restriction_abs [simp]:
  2.1466 +     "[| M(f); M(A); M(z) |]
  2.1467        ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  2.1468  apply (simp add: ball_iff_equiv restriction_def restrict_def)
  2.1469 -apply (blast intro!: equalityI dest: transM) 
  2.1470 +apply (blast intro!: equalityI dest: transM)
  2.1471  done
  2.1472  
  2.1473  
  2.1474 @@ -1219,16 +1215,16 @@
  2.1475       "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  2.1476  by (simp add: restrict_def, blast dest: transM)
  2.1477  
  2.1478 -lemma (in M_basic) restrict_closed [intro,simp]: 
  2.1479 +lemma (in M_basic) restrict_closed [intro,simp]:
  2.1480       "[| M(A); M(r) |] ==> M(restrict(r,A))"
  2.1481  apply (simp add: M_restrict_iff)
  2.1482 -apply (insert restrict_separation [of A], simp) 
  2.1483 +apply (insert restrict_separation [of A], simp)
  2.1484  done
  2.1485  
  2.1486 -lemma (in M_basic) Inter_abs [simp]: 
  2.1487 +lemma (in M_basic) Inter_abs [simp]:
  2.1488       "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  2.1489 -apply (simp add: big_inter_def Inter_def) 
  2.1490 -apply (blast intro!: equalityI dest: transM) 
  2.1491 +apply (simp add: big_inter_def Inter_def)
  2.1492 +apply (blast intro!: equalityI dest: transM)
  2.1493  done
  2.1494  
  2.1495  lemma (in M_basic) Inter_closed [intro,simp]:
  2.1496 @@ -1238,7 +1234,7 @@
  2.1497  lemma (in M_basic) Int_closed [intro,simp]:
  2.1498       "[| M(A); M(B) |] ==> M(A Int B)"
  2.1499  apply (subgoal_tac "M({A,B})")
  2.1500 -apply (frule Inter_closed, force+) 
  2.1501 +apply (frule Inter_closed, force+)
  2.1502  done
  2.1503  
  2.1504  lemma (in M_basic) Diff_closed [intro,simp]:
  2.1505 @@ -1250,7 +1246,7 @@
  2.1506  lemma (in M_basic) separation_conj:
  2.1507       "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
  2.1508  by (simp del: separation_closed
  2.1509 -         add: separation_iff Collect_Int_Collect_eq [symmetric]) 
  2.1510 +         add: separation_iff Collect_Int_Collect_eq [symmetric])
  2.1511  
  2.1512  (*???equalities*)
  2.1513  lemma Collect_Un_Collect_eq:
  2.1514 @@ -1262,90 +1258,74 @@
  2.1515  by blast
  2.1516  
  2.1517  lemma (in M_trivial) Collect_rall_eq:
  2.1518 -     "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) = 
  2.1519 +     "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) =
  2.1520                 (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
  2.1521 -apply simp 
  2.1522 -apply (blast intro!: equalityI dest: transM) 
  2.1523 +apply simp
  2.1524 +apply (blast intro!: equalityI dest: transM)
  2.1525  done
  2.1526  
  2.1527  lemma (in M_basic) separation_disj:
  2.1528       "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
  2.1529  by (simp del: separation_closed
  2.1530 -         add: separation_iff Collect_Un_Collect_eq [symmetric]) 
  2.1531 +         add: separation_iff Collect_Un_Collect_eq [symmetric])
  2.1532  
  2.1533  lemma (in M_basic) separation_neg:
  2.1534       "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
  2.1535  by (simp del: separation_closed
  2.1536 -         add: separation_iff Diff_Collect_eq [symmetric]) 
  2.1537 +         add: separation_iff Diff_Collect_eq [symmetric])
  2.1538  
  2.1539  lemma (in M_basic) separation_imp:
  2.1540 -     "[|separation(M,P); separation(M,Q)|] 
  2.1541 +     "[|separation(M,P); separation(M,Q)|]
  2.1542        ==> separation(M, \<lambda>z. P(z) --> Q(z))"
  2.1543 -by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric]) 
  2.1544 +by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric])
  2.1545  
  2.1546 -text{*This result is a hint of how little can be done without the Reflection 
  2.1547 +text{*This result is a hint of how little can be done without the Reflection
  2.1548    Theorem.  The quantifier has to be bounded by a set.  We also need another
  2.1549    instance of Separation!*}
  2.1550  lemma (in M_basic) separation_rall:
  2.1551 -     "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y)); 
  2.1552 +     "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y));
  2.1553          \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
  2.1554 -      ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))" 
  2.1555 +      ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))"
  2.1556  apply (simp del: separation_closed rall_abs
  2.1557 -         add: separation_iff Collect_rall_eq) 
  2.1558 -apply (blast intro!: Inter_closed RepFun_closed dest: transM) 
  2.1559 +         add: separation_iff Collect_rall_eq)
  2.1560 +apply (blast intro!: Inter_closed RepFun_closed dest: transM)
  2.1561  done
  2.1562  
  2.1563  
  2.1564  subsubsection{*Functions and function space*}
  2.1565  
  2.1566 -text{*M contains all finite functions*}
  2.1567 -lemma (in M_basic) finite_fun_closed_lemma [rule_format]: 
  2.1568 -     "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
  2.1569 -apply (induct_tac n, simp)
  2.1570 -apply (rule ballI)  
  2.1571 -apply (simp add: succ_def) 
  2.1572 -apply (frule fun_cons_restrict_eq)
  2.1573 -apply (erule ssubst) 
  2.1574 -apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
  2.1575 - apply (simp add: cons_closed nat_into_M apply_closed) 
  2.1576 -apply (blast intro: apply_funtype transM restrict_type2) 
  2.1577 -done
  2.1578 -
  2.1579 -lemma (in M_basic) finite_fun_closed [rule_format]: 
  2.1580 -     "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
  2.1581 -by (blast intro: finite_fun_closed_lemma) 
  2.1582 -
  2.1583 -text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
  2.1584 +text{*The assumption @{term "M(A->B)"} is unusual, but essential: in
  2.1585  all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  2.1586  lemma (in M_basic) is_funspace_abs [simp]:
  2.1587       "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  2.1588  apply (simp add: is_funspace_def)
  2.1589  apply (rule iffI)
  2.1590 - prefer 2 apply blast 
  2.1591 + prefer 2 apply blast
  2.1592  apply (rule M_equalityI)
  2.1593    apply simp_all
  2.1594  done
  2.1595  
  2.1596  lemma (in M_basic) succ_fun_eq2:
  2.1597       "[|M(B); M(n->B)|] ==>
  2.1598 -      succ(n) -> B = 
  2.1599 +      succ(n) -> B =
  2.1600        \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  2.1601  apply (simp add: succ_fun_eq)
  2.1602 -apply (blast dest: transM)  
  2.1603 +apply (blast dest: transM)
  2.1604  done
  2.1605  
  2.1606  lemma (in M_basic) funspace_succ:
  2.1607       "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  2.1608 -apply (insert funspace_succ_replacement [of n], simp) 
  2.1609 -apply (force simp add: succ_fun_eq2 univalent_def) 
  2.1610 +apply (insert funspace_succ_replacement [of n], simp)
  2.1611 +apply (force simp add: succ_fun_eq2 univalent_def)
  2.1612  done
  2.1613  
  2.1614  text{*@{term M} contains all finite function spaces.  Needed to prove the
  2.1615 -absoluteness of transitive closure.*}
  2.1616 +absoluteness of transitive closure.  See the definition of
  2.1617 +@{text rtrancl_alt} in in @{text WF_absolute.thy}.*}
  2.1618  lemma (in M_basic) finite_funspace_closed [intro,simp]:
  2.1619       "[|n\<in>nat; M(B)|] ==> M(n->B)"
  2.1620  apply (induct_tac n, simp)
  2.1621 -apply (simp add: funspace_succ nat_into_M) 
  2.1622 +apply (simp add: funspace_succ nat_into_M)
  2.1623  done
  2.1624  
  2.1625  
  2.1626 @@ -1356,50 +1336,50 @@
  2.1627     "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
  2.1628  
  2.1629    is_not :: "[i=>o, i, i] => o"
  2.1630 -   "is_not(M,a,z) == (number1(M,a)  & empty(M,z)) | 
  2.1631 +   "is_not(M,a,z) == (number1(M,a)  & empty(M,z)) |
  2.1632                       (~number1(M,a) & number1(M,z))"
  2.1633  
  2.1634    is_and :: "[i=>o, i, i, i] => o"
  2.1635 -   "is_and(M,a,b,z) == (number1(M,a)  & z=b) | 
  2.1636 +   "is_and(M,a,b,z) == (number1(M,a)  & z=b) |
  2.1637                         (~number1(M,a) & empty(M,z))"
  2.1638  
  2.1639    is_or :: "[i=>o, i, i, i] => o"
  2.1640 -   "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) | 
  2.1641 +   "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) |
  2.1642                        (~number1(M,a) & z=b)"
  2.1643  
  2.1644 -lemma (in M_trivial) bool_of_o_abs [simp]: 
  2.1645 -     "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)" 
  2.1646 -by (simp add: is_bool_of_o_def bool_of_o_def) 
  2.1647 +lemma (in M_trivial) bool_of_o_abs [simp]:
  2.1648 +     "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)"
  2.1649 +by (simp add: is_bool_of_o_def bool_of_o_def)
  2.1650  
  2.1651  
  2.1652 -lemma (in M_trivial) not_abs [simp]: 
  2.1653 +lemma (in M_trivial) not_abs [simp]:
  2.1654       "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)"
  2.1655 -by (simp add: Bool.not_def cond_def is_not_def) 
  2.1656 +by (simp add: Bool.not_def cond_def is_not_def)
  2.1657  
  2.1658 -lemma (in M_trivial) and_abs [simp]: 
  2.1659 +lemma (in M_trivial) and_abs [simp]:
  2.1660       "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b"
  2.1661 -by (simp add: Bool.and_def cond_def is_and_def) 
  2.1662 +by (simp add: Bool.and_def cond_def is_and_def)
  2.1663  
  2.1664 -lemma (in M_trivial) or_abs [simp]: 
  2.1665 +lemma (in M_trivial) or_abs [simp]:
  2.1666       "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b"
  2.1667  by (simp add: Bool.or_def cond_def is_or_def)
  2.1668  
  2.1669  
  2.1670  lemma (in M_trivial) bool_of_o_closed [intro,simp]:
  2.1671       "M(bool_of_o(P))"
  2.1672 -by (simp add: bool_of_o_def) 
  2.1673 +by (simp add: bool_of_o_def)
  2.1674  
  2.1675  lemma (in M_trivial) and_closed [intro,simp]:
  2.1676       "[| M(p); M(q) |] ==> M(p and q)"
  2.1677 -by (simp add: and_def cond_def) 
  2.1678 +by (simp add: and_def cond_def)
  2.1679  
  2.1680  lemma (in M_trivial) or_closed [intro,simp]:
  2.1681       "[| M(p); M(q) |] ==> M(p or q)"
  2.1682 -by (simp add: or_def cond_def) 
  2.1683 +by (simp add: or_def cond_def)
  2.1684  
  2.1685  lemma (in M_trivial) not_closed [intro,simp]:
  2.1686       "M(p) ==> M(not(p))"
  2.1687 -by (simp add: Bool.not_def cond_def) 
  2.1688 +by (simp add: Bool.not_def cond_def)
  2.1689  
  2.1690  
  2.1691  subsection{*Relativization and Absoluteness for List Operators*}
  2.1692 @@ -1422,7 +1402,7 @@
  2.1693  by (simp add: is_Nil_def Nil_def)
  2.1694  
  2.1695  lemma (in M_trivial) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
  2.1696 -by (simp add: Cons_def) 
  2.1697 +by (simp add: Cons_def)
  2.1698  
  2.1699  lemma (in M_trivial) Cons_abs [simp]:
  2.1700       "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
  2.1701 @@ -1439,35 +1419,35 @@
  2.1702  
  2.1703    list_case' :: "[i, [i,i]=>i, i] => i"
  2.1704      --{*A version of @{term list_case} that's always defined.*}
  2.1705 -    "list_case'(a,b,xs) == 
  2.1706 -       if quasilist(xs) then list_case(a,b,xs) else 0"  
  2.1707 +    "list_case'(a,b,xs) ==
  2.1708 +       if quasilist(xs) then list_case(a,b,xs) else 0"
  2.1709  
  2.1710    is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
  2.1711      --{*Returns 0 for non-lists*}
  2.1712 -    "is_list_case(M, a, is_b, xs, z) == 
  2.1713 +    "is_list_case(M, a, is_b, xs, z) ==
  2.1714         (is_Nil(M,xs) --> z=a) &
  2.1715         (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
  2.1716         (is_quasilist(M,xs) | empty(M,z))"
  2.1717  
  2.1718    hd' :: "i => i"
  2.1719      --{*A version of @{term hd} that's always defined.*}
  2.1720 -    "hd'(xs) == if quasilist(xs) then hd(xs) else 0"  
  2.1721 +    "hd'(xs) == if quasilist(xs) then hd(xs) else 0"
  2.1722  
  2.1723    tl' :: "i => i"
  2.1724      --{*A version of @{term tl} that's always defined.*}
  2.1725 -    "tl'(xs) == if quasilist(xs) then tl(xs) else 0"  
  2.1726 +    "tl'(xs) == if quasilist(xs) then tl(xs) else 0"
  2.1727  
  2.1728    is_hd :: "[i=>o,i,i] => o"
  2.1729       --{* @{term "hd([]) = 0"} no constraints if not a list.
  2.1730            Avoiding implication prevents the simplifier's looping.*}
  2.1731 -    "is_hd(M,xs,H) == 
  2.1732 +    "is_hd(M,xs,H) ==
  2.1733         (is_Nil(M,xs) --> empty(M,H)) &
  2.1734         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
  2.1735         (is_quasilist(M,xs) | empty(M,H))"
  2.1736  
  2.1737    is_tl :: "[i=>o,i,i] => o"
  2.1738       --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
  2.1739 -    "is_tl(M,xs,T) == 
  2.1740 +    "is_tl(M,xs,T) ==
  2.1741         (is_Nil(M,xs) --> T=xs) &
  2.1742         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
  2.1743         (is_quasilist(M,xs) | empty(M,T))"
  2.1744 @@ -1491,8 +1471,8 @@
  2.1745  lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)"
  2.1746  by (simp add: list_case'_def quasilist_def)
  2.1747  
  2.1748 -lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0" 
  2.1749 -by (simp add: quasilist_def list_case'_def) 
  2.1750 +lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0"
  2.1751 +by (simp add: quasilist_def list_case'_def)
  2.1752  
  2.1753  lemma list_case'_eq_list_case [simp]:
  2.1754       "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
  2.1755 @@ -1500,25 +1480,25 @@
  2.1756  
  2.1757  lemma (in M_basic) list_case'_closed [intro,simp]:
  2.1758    "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
  2.1759 -apply (case_tac "quasilist(k)") 
  2.1760 - apply (simp add: quasilist_def, force) 
  2.1761 -apply (simp add: non_list_case) 
  2.1762 +apply (case_tac "quasilist(k)")
  2.1763 + apply (simp add: quasilist_def, force)
  2.1764 +apply (simp add: non_list_case)
  2.1765  done
  2.1766  
  2.1767 -lemma (in M_trivial) quasilist_abs [simp]: 
  2.1768 +lemma (in M_trivial) quasilist_abs [simp]:
  2.1769       "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
  2.1770  by (auto simp add: is_quasilist_def quasilist_def)
  2.1771  
  2.1772 -lemma (in M_trivial) list_case_abs [simp]: 
  2.1773 -     "[| relativize2(M,is_b,b); M(k); M(z) |] 
  2.1774 +lemma (in M_trivial) list_case_abs [simp]:
  2.1775 +     "[| relativize2(M,is_b,b); M(k); M(z) |]
  2.1776        ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
  2.1777 -apply (case_tac "quasilist(k)") 
  2.1778 - prefer 2 
  2.1779 - apply (simp add: is_list_case_def non_list_case) 
  2.1780 - apply (force simp add: quasilist_def) 
  2.1781 +apply (case_tac "quasilist(k)")
  2.1782 + prefer 2
  2.1783 + apply (simp add: is_list_case_def non_list_case)
  2.1784 + apply (force simp add: quasilist_def)
  2.1785  apply (simp add: quasilist_def is_list_case_def)
  2.1786 -apply (elim disjE exE) 
  2.1787 - apply (simp_all add: relativize2_def) 
  2.1788 +apply (elim disjE exE)
  2.1789 + apply (simp_all add: relativize2_def)
  2.1790  done
  2.1791  
  2.1792  
  2.1793 @@ -1529,34 +1509,34 @@
  2.1794  
  2.1795  lemma (in M_trivial) is_hd_Cons:
  2.1796       "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
  2.1797 -by (force simp add: is_hd_def) 
  2.1798 +by (force simp add: is_hd_def)
  2.1799  
  2.1800  lemma (in M_trivial) hd_abs [simp]:
  2.1801       "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
  2.1802  apply (simp add: hd'_def)
  2.1803  apply (intro impI conjI)
  2.1804 - prefer 2 apply (force simp add: is_hd_def) 
  2.1805 + prefer 2 apply (force simp add: is_hd_def)
  2.1806  apply (simp add: quasilist_def is_hd_def)
  2.1807  apply (elim disjE exE, auto)
  2.1808 -done 
  2.1809 +done
  2.1810  
  2.1811  lemma (in M_trivial) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
  2.1812  by (simp add: is_tl_def)
  2.1813  
  2.1814  lemma (in M_trivial) is_tl_Cons:
  2.1815       "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
  2.1816 -by (force simp add: is_tl_def) 
  2.1817 +by (force simp add: is_tl_def)
  2.1818  
  2.1819  lemma (in M_trivial) tl_abs [simp]:
  2.1820       "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
  2.1821  apply (simp add: tl'_def)
  2.1822  apply (intro impI conjI)
  2.1823 - prefer 2 apply (force simp add: is_tl_def) 
  2.1824 + prefer 2 apply (force simp add: is_tl_def)
  2.1825  apply (simp add: quasilist_def is_tl_def)
  2.1826  apply (elim disjE exE, auto)
  2.1827 -done 
  2.1828 +done
  2.1829  
  2.1830 -lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')"  
  2.1831 +lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')"
  2.1832  by (simp add: relativize1_def)
  2.1833  
  2.1834  lemma hd'_Nil: "hd'([]) = 0"
  2.1835 @@ -1572,8 +1552,8 @@
  2.1836  by (simp add: tl'_def)
  2.1837  
  2.1838  lemma iterates_tl_Nil: "n \<in> nat ==> tl'^n ([]) = []"
  2.1839 -apply (induct_tac n) 
  2.1840 -apply (simp_all add: tl'_Nil) 
  2.1841 +apply (induct_tac n)
  2.1842 +apply (simp_all add: tl'_Nil)
  2.1843  done
  2.1844  
  2.1845  lemma (in M_basic) tl'_closed: "M(x) ==> M(tl'(x))"
     3.1 --- a/src/ZF/Constructible/Separation.thy	Fri Oct 04 15:23:58 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Separation.thy	Fri Oct 04 15:57:32 2002 +0200
     3.3 @@ -458,7 +458,6 @@
     3.4    and Inter_abs = M_basic.Inter_abs [OF M_basic_L]
     3.5    and Inter_closed = M_basic.Inter_closed [OF M_basic_L]
     3.6    and Int_closed = M_basic.Int_closed [OF M_basic_L]
     3.7 -  and finite_fun_closed = M_basic.finite_fun_closed [OF M_basic_L]
     3.8    and is_funspace_abs = M_basic.is_funspace_abs [OF M_basic_L]
     3.9    and succ_fun_eq2 = M_basic.succ_fun_eq2 [OF M_basic_L]
    3.10    and funspace_succ = M_basic.funspace_succ [OF M_basic_L]
    3.11 @@ -488,7 +487,6 @@
    3.12    and wellfounded_iff_wellfounded_on_field = M_basic.wellfounded_iff_wellfounded_on_field [OF M_basic_L]
    3.13    and wellfounded_induct = M_basic.wellfounded_induct [OF M_basic_L]
    3.14    and wellfounded_on_induct = M_basic.wellfounded_on_induct [OF M_basic_L]
    3.15 -  and wellfounded_on_induct2 = M_basic.wellfounded_on_induct2 [OF M_basic_L]
    3.16    and linear_imp_relativized = M_basic.linear_imp_relativized [OF M_basic_L]
    3.17    and trans_on_imp_relativized = M_basic.trans_on_imp_relativized [OF M_basic_L]
    3.18    and wf_on_imp_relativized = M_basic.wf_on_imp_relativized [OF M_basic_L]
     4.1 --- a/src/ZF/Constructible/Wellorderings.thy	Fri Oct 04 15:23:58 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Fri Oct 04 15:57:32 2002 +0200
     4.3 @@ -33,13 +33,11 @@
     4.4    wellfounded :: "[i=>o,i]=>o"
     4.5      --{*EVERY non-empty set has an @{text r}-minimal element*}
     4.6      "wellfounded(M,r) == 
     4.7 -	\<forall>x[M]. ~ empty(M,x) 
     4.8 -                 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
     4.9 +	\<forall>x[M]. x\<noteq>0 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
    4.10    wellfounded_on :: "[i=>o,i,i]=>o"
    4.11      --{*every non-empty SUBSET OF @{text A} has an @{text r}-minimal element*}
    4.12      "wellfounded_on(M,A,r) == 
    4.13 -	\<forall>x[M]. ~ empty(M,x) --> subset(M,x,A)
    4.14 -                 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
    4.15 +	\<forall>x[M]. x\<noteq>0 --> x\<subseteq>A --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))"
    4.16  
    4.17    wellordered :: "[i=>o,i,i]=>o"
    4.18      --{*linear and wellfounded on @{text A}*}
    4.19 @@ -124,15 +122,6 @@
    4.20  apply (blast intro: transM)+
    4.21  done
    4.22  
    4.23 -text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
    4.24 -      hypothesis by removing the restriction to @{term A}.*}
    4.25 -lemma (in M_basic) wellfounded_on_induct2: 
    4.26 -     "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  r \<subseteq> A*A;  
    4.27 -       separation(M, \<lambda>x. x\<in>A --> ~P(x));  
    4.28 -       \<forall>x\<in>A. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
    4.29 -      ==> P(a)";
    4.30 -by (rule wellfounded_on_induct, assumption+, blast)
    4.31 -
    4.32  
    4.33  subsubsection {*Kunen's lemma IV 3.14, page 123*}
    4.34  
    4.35 @@ -297,13 +286,13 @@
    4.36  by (simp add: wellordered_def, blast dest: wellfounded_on_asym)
    4.37  
    4.38  
    4.39 -text{*Surely a shorter proof using lemmas in @{text Order}?
    4.40 -     Like @{text well_ord_iso_preserving}?*}
    4.41 +text{*Can't use @{text well_ord_iso_preserving} because it needs the
    4.42 +strong premise @{term "well_ord(A,r)"}*}
    4.43  lemma (in M_basic) ord_iso_pred_imp_lt:
    4.44       "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
    4.45 -       g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
    4.46 -       wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
    4.47 -       Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
    4.48 +         g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
    4.49 +         wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
    4.50 +         Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
    4.51        ==> i < j"
    4.52  apply (frule wellordered_is_trans_on, assumption)
    4.53  apply (frule_tac y=y in transM, assumption) 
    4.54 @@ -351,9 +340,8 @@
    4.55     "obase(M,A,r,z) == 
    4.56  	\<forall>a[M]. 
    4.57           a \<in> z <-> 
    4.58 -          (a\<in>A & (\<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
    4.59 -                   ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
    4.60 -                   order_isomorphism(M,par,r,x,mx,g)))"
    4.61 +          (a\<in>A & (\<exists>x[M]. \<exists>g[M]. Ord(x) & 
    4.62 +                   order_isomorphism(M,Order.pred(A,a,r),r,x,Memrel(x),g)))"
    4.63  
    4.64  
    4.65    omap :: "[i=>o,i,i,i] => o"  
     5.1 --- a/src/ZF/Nat.thy	Fri Oct 04 15:23:58 2002 +0200
     5.2 +++ b/src/ZF/Nat.thy	Fri Oct 04 15:57:32 2002 +0200
     5.3 @@ -110,6 +110,9 @@
     5.4  apply (erule ltD)
     5.5  done
     5.6  
     5.7 +lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
     5.8 +by (induct a rule: nat_induct, auto)
     5.9 +
    5.10  lemma succ_natD [dest!]: "succ(i): nat ==> i: nat"
    5.11  by (rule Ord_trans [OF succI1], auto)
    5.12