src/ZF/Constructible/Relative.thy
changeset 13628 87482b5e3f2e
parent 13615 449a70d88b38
child 13634 99a593b49b04
     1.1 --- a/src/ZF/Constructible/Relative.thy	Fri Oct 04 15:23:58 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Oct 04 15:57:32 2002 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4      "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z --> x = a | x = b)"
     1.5  
     1.6    pair :: "[i=>o,i,i,i] => o"
     1.7 -    "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & 
     1.8 +    "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) &
     1.9                            (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
    1.10  
    1.11  
    1.12 @@ -62,17 +62,17 @@
    1.13      "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)"
    1.14  
    1.15    big_inter :: "[i=>o,i,i] => o"
    1.16 -    "big_inter(M,A,z) == 
    1.17 +    "big_inter(M,A,z) ==
    1.18               (A=0 --> z=0) &
    1.19  	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y[M]. y\<in>A --> x \<in> y)))"
    1.20  
    1.21    cartprod :: "[i=>o,i,i,i] => o"
    1.22 -    "cartprod(M,A,B,z) == 
    1.23 +    "cartprod(M,A,B,z) ==
    1.24  	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
    1.25  
    1.26    is_sum :: "[i=>o,i,i,i] => o"
    1.27 -    "is_sum(M,A,B,Z) == 
    1.28 -       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M]. 
    1.29 +    "is_sum(M,A,B,Z) ==
    1.30 +       \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
    1.31         number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
    1.32         cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
    1.33  
    1.34 @@ -83,73 +83,73 @@
    1.35      "is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)"
    1.36  
    1.37    is_converse :: "[i=>o,i,i] => o"
    1.38 -    "is_converse(M,r,z) == 
    1.39 -	\<forall>x[M]. x \<in> z <-> 
    1.40 +    "is_converse(M,r,z) ==
    1.41 +	\<forall>x[M]. x \<in> z <->
    1.42               (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
    1.43  
    1.44    pre_image :: "[i=>o,i,i,i] => o"
    1.45 -    "pre_image(M,r,A,z) == 
    1.46 +    "pre_image(M,r,A,z) ==
    1.47  	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
    1.48  
    1.49    is_domain :: "[i=>o,i,i] => o"
    1.50 -    "is_domain(M,r,z) == 
    1.51 +    "is_domain(M,r,z) ==
    1.52  	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
    1.53  
    1.54    image :: "[i=>o,i,i,i] => o"
    1.55 -    "image(M,r,A,z) == 
    1.56 +    "image(M,r,A,z) ==
    1.57          \<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
    1.58  
    1.59    is_range :: "[i=>o,i,i] => o"
    1.60 -    --{*the cleaner 
    1.61 +    --{*the cleaner
    1.62        @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
    1.63 -      unfortunately needs an instance of separation in order to prove 
    1.64 +      unfortunately needs an instance of separation in order to prove
    1.65          @{term "M(converse(r))"}.*}
    1.66 -    "is_range(M,r,z) == 
    1.67 +    "is_range(M,r,z) ==
    1.68  	\<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
    1.69  
    1.70    is_field :: "[i=>o,i,i] => o"
    1.71 -    "is_field(M,r,z) == 
    1.72 -	\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) & 
    1.73 +    "is_field(M,r,z) ==
    1.74 +	\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) &
    1.75                          union(M,dr,rr,z)"
    1.76  
    1.77    is_relation :: "[i=>o,i] => o"
    1.78 -    "is_relation(M,r) == 
    1.79 +    "is_relation(M,r) ==
    1.80          (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
    1.81  
    1.82    is_function :: "[i=>o,i] => o"
    1.83 -    "is_function(M,r) == 
    1.84 -	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 
    1.85 +    "is_function(M,r) ==
    1.86 +	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
    1.87             pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
    1.88  
    1.89    fun_apply :: "[i=>o,i,i,i] => o"
    1.90 -    "fun_apply(M,f,x,y) == 
    1.91 -        (\<exists>xs[M]. \<exists>fxs[M]. 
    1.92 +    "fun_apply(M,f,x,y) ==
    1.93 +        (\<exists>xs[M]. \<exists>fxs[M].
    1.94           upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))"
    1.95  
    1.96    typed_function :: "[i=>o,i,i,i] => o"
    1.97 -    "typed_function(M,A,B,r) == 
    1.98 +    "typed_function(M,A,B,r) ==
    1.99          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
   1.100          (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"
   1.101  
   1.102    is_funspace :: "[i=>o,i,i,i] => o"
   1.103 -    "is_funspace(M,A,B,F) == 
   1.104 +    "is_funspace(M,A,B,F) ==
   1.105          \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
   1.106  
   1.107    composition :: "[i=>o,i,i,i] => o"
   1.108 -    "composition(M,r,s,t) == 
   1.109 -        \<forall>p[M]. p \<in> t <-> 
   1.110 -               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
   1.111 -                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
   1.112 +    "composition(M,r,s,t) ==
   1.113 +        \<forall>p[M]. p \<in> t <->
   1.114 +               (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
   1.115 +                pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
   1.116                  xy \<in> s & yz \<in> r)"
   1.117  
   1.118    injection :: "[i=>o,i,i,i] => o"
   1.119 -    "injection(M,A,B,f) == 
   1.120 +    "injection(M,A,B,f) ==
   1.121  	typed_function(M,A,B,f) &
   1.122 -        (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M]. 
   1.123 +        (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
   1.124            pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')"
   1.125  
   1.126    surjection :: "[i=>o,i,i,i] => o"
   1.127 -    "surjection(M,A,B,f) == 
   1.128 +    "surjection(M,A,B,f) ==
   1.129          typed_function(M,A,B,f) &
   1.130          (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
   1.131  
   1.132 @@ -157,7 +157,7 @@
   1.133      "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
   1.134  
   1.135    restriction :: "[i=>o,i,i,i] => o"
   1.136 -    "restriction(M,r,A,z) == 
   1.137 +    "restriction(M,r,A,z) ==
   1.138  	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
   1.139  
   1.140    transitive_set :: "[i=>o,i] => o"
   1.141 @@ -169,19 +169,19 @@
   1.142  
   1.143    limit_ordinal :: "[i=>o,i] => o"
   1.144      --{*a limit ordinal is a non-empty, successor-closed ordinal*}
   1.145 -    "limit_ordinal(M,a) == 
   1.146 -	ordinal(M,a) & ~ empty(M,a) & 
   1.147 +    "limit_ordinal(M,a) ==
   1.148 +	ordinal(M,a) & ~ empty(M,a) &
   1.149          (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
   1.150  
   1.151    successor_ordinal :: "[i=>o,i] => o"
   1.152      --{*a successor ordinal is any ordinal that is neither empty nor limit*}
   1.153 -    "successor_ordinal(M,a) == 
   1.154 +    "successor_ordinal(M,a) ==
   1.155  	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
   1.156  
   1.157    finite_ordinal :: "[i=>o,i] => o"
   1.158      --{*an ordinal is finite if neither it nor any of its elements are limit*}
   1.159 -    "finite_ordinal(M,a) == 
   1.160 -	ordinal(M,a) & ~ limit_ordinal(M,a) & 
   1.161 +    "finite_ordinal(M,a) ==
   1.162 +	ordinal(M,a) & ~ limit_ordinal(M,a) &
   1.163          (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   1.164  
   1.165    omega :: "[i=>o,i] => o"
   1.166 @@ -192,7 +192,7 @@
   1.167      "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
   1.168  
   1.169    is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
   1.170 -    "is_nat_case(M, a, is_b, k, z) == 
   1.171 +    "is_nat_case(M, a, is_b, k, z) ==
   1.172         (empty(M,k) --> z=a) &
   1.173         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   1.174         (is_quasinat(M,k) | empty(M,z))"
   1.175 @@ -202,7 +202,7 @@
   1.176  
   1.177    Relativize1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
   1.178      --{*as above, but typed*}
   1.179 -    "Relativize1(M,A,is_f,f) == 
   1.180 +    "Relativize1(M,A,is_f,f) ==
   1.181          \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
   1.182  
   1.183    relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
   1.184 @@ -213,42 +213,42 @@
   1.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)"
   1.186  
   1.187    relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   1.188 -    "relativize3(M,is_f,f) == 
   1.189 +    "relativize3(M,is_f,f) ==
   1.190         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
   1.191  
   1.192    Relativize3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
   1.193 -    "Relativize3(M,A,B,C,is_f,f) == 
   1.194 -       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. 
   1.195 +    "Relativize3(M,A,B,C,is_f,f) ==
   1.196 +       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
   1.197           x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
   1.198  
   1.199    relativize4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
   1.200 -    "relativize4(M,is_f,f) == 
   1.201 +    "relativize4(M,is_f,f) ==
   1.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)"
   1.203  
   1.204  
   1.205  text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
   1.206  lemma triv_Relativize1:
   1.207       "Relativize1(M, A, \<lambda>x y. y = f(x), f)"
   1.208 -by (simp add: Relativize1_def) 
   1.209 +by (simp add: Relativize1_def)
   1.210  
   1.211  lemma triv_Relativize2:
   1.212       "Relativize2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
   1.213 -by (simp add: Relativize2_def) 
   1.214 +by (simp add: Relativize2_def)
   1.215  
   1.216  
   1.217  subsection {*The relativized ZF axioms*}
   1.218  constdefs
   1.219  
   1.220    extensionality :: "(i=>o) => o"
   1.221 -    "extensionality(M) == 
   1.222 +    "extensionality(M) ==
   1.223  	\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"
   1.224  
   1.225    separation :: "[i=>o, i=>o] => o"
   1.226      --{*The formula @{text P} should only involve parameters
   1.227 -        belonging to @{text M}.  But we can't prove separation as a scheme
   1.228 -        anyway.  Every instance that we need must individually be assumed
   1.229 -        and later proved.*}
   1.230 -    "separation(M,P) == 
   1.231 +        belonging to @{text M} and all its quantifiers must be relativized
   1.232 +        to @{text M}.  We do not have separation as a scheme; every instance
   1.233 +        that we need must be assumed (and later proved) separately.*}
   1.234 +    "separation(M,P) ==
   1.235  	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   1.236  
   1.237    upair_ax :: "(i=>o) => o"
   1.238 @@ -261,73 +261,73 @@
   1.239      "power_ax(M) == \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)"
   1.240  
   1.241    univalent :: "[i=>o, i, [i,i]=>o] => o"
   1.242 -    "univalent(M,A,P) == 
   1.243 -	(\<forall>x[M]. x\<in>A --> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) --> y=z))"
   1.244 +    "univalent(M,A,P) ==
   1.245 +	\<forall>x[M]. x\<in>A --> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) --> y=z)"
   1.246  
   1.247    replacement :: "[i=>o, [i,i]=>o] => o"
   1.248 -    "replacement(M,P) == 
   1.249 +    "replacement(M,P) ==
   1.250        \<forall>A[M]. univalent(M,A,P) -->
   1.251        (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)"
   1.252  
   1.253    strong_replacement :: "[i=>o, [i,i]=>o] => o"
   1.254 -    "strong_replacement(M,P) == 
   1.255 +    "strong_replacement(M,P) ==
   1.256        \<forall>A[M]. univalent(M,A,P) -->
   1.257        (\<exists>Y[M]. \<forall>b[M]. b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))"
   1.258  
   1.259    foundation_ax :: "(i=>o) => o"
   1.260 -    "foundation_ax(M) == 
   1.261 +    "foundation_ax(M) ==
   1.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))"
   1.263  
   1.264  
   1.265  subsection{*A trivial consistency proof for $V_\omega$ *}
   1.266  
   1.267 -text{*We prove that $V_\omega$ 
   1.268 +text{*We prove that $V_\omega$
   1.269        (or @{text univ} in Isabelle) satisfies some ZF axioms.
   1.270       Kunen, Theorem IV 3.13, page 123.*}
   1.271  
   1.272  lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
   1.273 -apply (insert Transset_univ [OF Transset_0])  
   1.274 -apply (simp add: Transset_def, blast) 
   1.275 +apply (insert Transset_univ [OF Transset_0])
   1.276 +apply (simp add: Transset_def, blast)
   1.277  done
   1.278  
   1.279 -lemma univ0_Ball_abs [simp]: 
   1.280 -     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   1.281 -by (blast intro: univ0_downwards_mem) 
   1.282 +lemma univ0_Ball_abs [simp]:
   1.283 +     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))"
   1.284 +by (blast intro: univ0_downwards_mem)
   1.285  
   1.286 -lemma univ0_Bex_abs [simp]: 
   1.287 -     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   1.288 -by (blast intro: univ0_downwards_mem) 
   1.289 +lemma univ0_Bex_abs [simp]:
   1.290 +     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))"
   1.291 +by (blast intro: univ0_downwards_mem)
   1.292  
   1.293  text{*Congruence rule for separation: can assume the variable is in @{text M}*}
   1.294  lemma separation_cong [cong]:
   1.295 -     "(!!x. M(x) ==> P(x) <-> P'(x)) 
   1.296 +     "(!!x. M(x) ==> P(x) <-> P'(x))
   1.297        ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
   1.298 -by (simp add: separation_def) 
   1.299 +by (simp add: separation_def)
   1.300  
   1.301  lemma univalent_cong [cong]:
   1.302 -     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   1.303 +     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
   1.304        ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
   1.305 -by (simp add: univalent_def) 
   1.306 +by (simp add: univalent_def)
   1.307  
   1.308  lemma univalent_triv [intro,simp]:
   1.309       "univalent(M, A, \<lambda>x y. y = f(x))"
   1.310 -by (simp add: univalent_def) 
   1.311 +by (simp add: univalent_def)
   1.312  
   1.313  lemma univalent_conjI2 [intro,simp]:
   1.314       "univalent(M,A,Q) ==> univalent(M, A, \<lambda>x y. P(x,y) & Q(x,y))"
   1.315 -by (simp add: univalent_def, blast) 
   1.316 +by (simp add: univalent_def, blast)
   1.317  
   1.318  text{*Congruence rule for replacement*}
   1.319  lemma strong_replacement_cong [cong]:
   1.320 -     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   1.321 -      ==> strong_replacement(M, %x y. P(x,y)) <-> 
   1.322 -          strong_replacement(M, %x y. P'(x,y))" 
   1.323 -by (simp add: strong_replacement_def) 
   1.324 +     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
   1.325 +      ==> strong_replacement(M, %x y. P(x,y)) <->
   1.326 +          strong_replacement(M, %x y. P'(x,y))"
   1.327 +by (simp add: strong_replacement_def)
   1.328  
   1.329  text{*The extensionality axiom*}
   1.330  lemma "extensionality(\<lambda>x. x \<in> univ(0))"
   1.331  apply (simp add: extensionality_def)
   1.332 -apply (blast intro: univ0_downwards_mem) 
   1.333 +apply (blast intro: univ0_downwards_mem)
   1.334  done
   1.335  
   1.336  text{*The separation axiom requires some lemmas*}
   1.337 @@ -339,7 +339,7 @@
   1.338  done
   1.339  
   1.340  lemma Collect_in_VLimit:
   1.341 -     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] 
   1.342 +     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
   1.343        ==> Collect(X,P) \<in> Vfrom(A,i)"
   1.344  apply (rule Limit_VfromE, assumption+)
   1.345  apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
   1.346 @@ -350,23 +350,23 @@
   1.347  by (simp add: univ_def Collect_in_VLimit Limit_nat)
   1.348  
   1.349  lemma "separation(\<lambda>x. x \<in> univ(0), P)"
   1.350 -apply (simp add: separation_def, clarify) 
   1.351 -apply (rule_tac x = "Collect(z,P)" in bexI) 
   1.352 +apply (simp add: separation_def, clarify)
   1.353 +apply (rule_tac x = "Collect(z,P)" in bexI)
   1.354  apply (blast intro: Collect_in_univ Transset_0)+
   1.355  done
   1.356  
   1.357  text{*Unordered pairing axiom*}
   1.358  lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
   1.359 -apply (simp add: upair_ax_def upair_def)  
   1.360 -apply (blast intro: doubleton_in_univ) 
   1.361 +apply (simp add: upair_ax_def upair_def)
   1.362 +apply (blast intro: doubleton_in_univ)
   1.363  done
   1.364  
   1.365  text{*Union axiom*}
   1.366 -lemma "Union_ax(\<lambda>x. x \<in> univ(0))"  
   1.367 -apply (simp add: Union_ax_def big_union_def, clarify) 
   1.368 -apply (rule_tac x="\<Union>x" in bexI)  
   1.369 +lemma "Union_ax(\<lambda>x. x \<in> univ(0))"
   1.370 +apply (simp add: Union_ax_def big_union_def, clarify)
   1.371 +apply (rule_tac x="\<Union>x" in bexI)
   1.372   apply (blast intro: univ0_downwards_mem)
   1.373 -apply (blast intro: Union_in_univ Transset_0) 
   1.374 +apply (blast intro: Union_in_univ Transset_0)
   1.375  done
   1.376  
   1.377  text{*Powerset axiom*}
   1.378 @@ -376,88 +376,88 @@
   1.379  apply (simp add: univ_def Pow_in_VLimit Limit_nat)
   1.380  done
   1.381  
   1.382 -lemma "power_ax(\<lambda>x. x \<in> univ(0))"  
   1.383 -apply (simp add: power_ax_def powerset_def subset_def, clarify) 
   1.384 +lemma "power_ax(\<lambda>x. x \<in> univ(0))"
   1.385 +apply (simp add: power_ax_def powerset_def subset_def, clarify)
   1.386  apply (rule_tac x="Pow(x)" in bexI)
   1.387   apply (blast intro: univ0_downwards_mem)
   1.388 -apply (blast intro: Pow_in_univ Transset_0) 
   1.389 +apply (blast intro: Pow_in_univ Transset_0)
   1.390  done
   1.391  
   1.392  text{*Foundation axiom*}
   1.393 -lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"  
   1.394 +lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"
   1.395  apply (simp add: foundation_ax_def, clarify)
   1.396 -apply (cut_tac A=x in foundation) 
   1.397 +apply (cut_tac A=x in foundation)
   1.398  apply (blast intro: univ0_downwards_mem)
   1.399  done
   1.400  
   1.401 -lemma "replacement(\<lambda>x. x \<in> univ(0), P)"  
   1.402 -apply (simp add: replacement_def, clarify) 
   1.403 +lemma "replacement(\<lambda>x. x \<in> univ(0), P)"
   1.404 +apply (simp add: replacement_def, clarify)
   1.405  oops
   1.406  text{*no idea: maybe prove by induction on the rank of A?*}
   1.407  
   1.408  text{*Still missing: Replacement, Choice*}
   1.409  
   1.410 -subsection{*lemmas needed to reduce some set constructions to instances
   1.411 +subsection{*Lemmas Needed to Reduce Some Set Constructions to Instances
   1.412        of Separation*}
   1.413  
   1.414  lemma image_iff_Collect: "r `` A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
   1.415 -apply (rule equalityI, auto) 
   1.416 -apply (simp add: Pair_def, blast) 
   1.417 +apply (rule equalityI, auto)
   1.418 +apply (simp add: Pair_def, blast)
   1.419  done
   1.420  
   1.421  lemma vimage_iff_Collect:
   1.422       "r -`` A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
   1.423 -apply (rule equalityI, auto) 
   1.424 -apply (simp add: Pair_def, blast) 
   1.425 +apply (rule equalityI, auto)
   1.426 +apply (simp add: Pair_def, blast)
   1.427  done
   1.428  
   1.429 -text{*These two lemmas lets us prove @{text domain_closed} and 
   1.430 +text{*These two lemmas lets us prove @{text domain_closed} and
   1.431        @{text range_closed} without new instances of separation*}
   1.432  
   1.433  lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
   1.434  apply (rule equalityI, auto)
   1.435  apply (rule vimageI, assumption)
   1.436 -apply (simp add: Pair_def, blast) 
   1.437 +apply (simp add: Pair_def, blast)
   1.438  done
   1.439  
   1.440  lemma range_eq_image: "range(r) = r `` Union(Union(r))"
   1.441  apply (rule equalityI, auto)
   1.442  apply (rule imageI, assumption)
   1.443 -apply (simp add: Pair_def, blast) 
   1.444 +apply (simp add: Pair_def, blast)
   1.445  done
   1.446  
   1.447  lemma replacementD:
   1.448      "[| replacement(M,P); M(A);  univalent(M,A,P) |]
   1.449       ==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y))"
   1.450 -by (simp add: replacement_def) 
   1.451 +by (simp add: replacement_def)
   1.452  
   1.453  lemma strong_replacementD:
   1.454      "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
   1.455       ==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b))))"
   1.456 -by (simp add: strong_replacement_def) 
   1.457 +by (simp add: strong_replacement_def)
   1.458  
   1.459  lemma separationD:
   1.460      "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   1.461 -by (simp add: separation_def) 
   1.462 +by (simp add: separation_def)
   1.463  
   1.464  
   1.465  text{*More constants, for order types*}
   1.466  constdefs
   1.467  
   1.468    order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
   1.469 -    "order_isomorphism(M,A,r,B,s,f) == 
   1.470 -        bijection(M,A,B,f) & 
   1.471 +    "order_isomorphism(M,A,r,B,s,f) ==
   1.472 +        bijection(M,A,B,f) &
   1.473          (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
   1.474            (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
   1.475 -            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> 
   1.476 +            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
   1.477              pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
   1.478  
   1.479    pred_set :: "[i=>o,i,i,i,i] => o"
   1.480 -    "pred_set(M,A,x,r,B) == 
   1.481 +    "pred_set(M,A,x,r,B) ==
   1.482  	\<forall>y[M]. y \<in> B <-> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
   1.483  
   1.484    membership :: "[i=>o,i,i] => o" --{*membership relation*}
   1.485 -    "membership(M,A,r) == 
   1.486 +    "membership(M,A,r) ==
   1.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)))"
   1.488  
   1.489  
   1.490 @@ -468,67 +468,72 @@
   1.491  locale M_trivial =
   1.492    fixes M
   1.493    assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
   1.494 -      and nonempty [simp]:  "M(0)"
   1.495        and upair_ax:	    "upair_ax(M)"
   1.496        and Union_ax:	    "Union_ax(M)"
   1.497        and power_ax:         "power_ax(M)"
   1.498        and replacement:      "replacement(M,P)"
   1.499        and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
   1.500  
   1.501 -lemma (in M_trivial) rall_abs [simp]: 
   1.502 -     "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   1.503 -by (blast intro: transM) 
   1.504 +
   1.505 +text{*Automatically discovers the proof using @{text transM}, @{text nat_0I}
   1.506 +and @{text M_nat}.*}
   1.507 +lemma (in M_trivial) nonempty [simp]: "M(0)"
   1.508 +by (blast intro: transM)
   1.509  
   1.510 -lemma (in M_trivial) rex_abs [simp]: 
   1.511 -     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   1.512 -by (blast intro: transM) 
   1.513 +lemma (in M_trivial) rall_abs [simp]:
   1.514 +     "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))"
   1.515 +by (blast intro: transM)
   1.516  
   1.517 -lemma (in M_trivial) ball_iff_equiv: 
   1.518 -     "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <-> 
   1.519 -               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   1.520 +lemma (in M_trivial) rex_abs [simp]:
   1.521 +     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))"
   1.522 +by (blast intro: transM)
   1.523 +
   1.524 +lemma (in M_trivial) ball_iff_equiv:
   1.525 +     "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <->
   1.526 +               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)"
   1.527  by (blast intro: transM)
   1.528  
   1.529  text{*Simplifies proofs of equalities when there's an iff-equality
   1.530        available for rewriting, universally quantified over M. *}
   1.531 -lemma (in M_trivial) M_equalityI: 
   1.532 +lemma (in M_trivial) M_equalityI:
   1.533       "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
   1.534 -by (blast intro!: equalityI dest: transM) 
   1.535 +by (blast intro!: equalityI dest: transM)
   1.536  
   1.537  
   1.538  subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
   1.539  
   1.540 -lemma (in M_trivial) empty_abs [simp]: 
   1.541 +lemma (in M_trivial) empty_abs [simp]:
   1.542       "M(z) ==> empty(M,z) <-> z=0"
   1.543  apply (simp add: empty_def)
   1.544 -apply (blast intro: transM) 
   1.545 +apply (blast intro: transM)
   1.546  done
   1.547  
   1.548 -lemma (in M_trivial) subset_abs [simp]: 
   1.549 +lemma (in M_trivial) subset_abs [simp]:
   1.550       "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
   1.551 -apply (simp add: subset_def) 
   1.552 -apply (blast intro: transM) 
   1.553 +apply (simp add: subset_def)
   1.554 +apply (blast intro: transM)
   1.555  done
   1.556  
   1.557 -lemma (in M_trivial) upair_abs [simp]: 
   1.558 +lemma (in M_trivial) upair_abs [simp]:
   1.559       "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
   1.560 -apply (simp add: upair_def) 
   1.561 -apply (blast intro: transM) 
   1.562 +apply (simp add: upair_def)
   1.563 +apply (blast intro: transM)
   1.564  done
   1.565  
   1.566  lemma (in M_trivial) upair_in_M_iff [iff]:
   1.567       "M({a,b}) <-> M(a) & M(b)"
   1.568 -apply (insert upair_ax, simp add: upair_ax_def) 
   1.569 -apply (blast intro: transM) 
   1.570 +apply (insert upair_ax, simp add: upair_ax_def)
   1.571 +apply (blast intro: transM)
   1.572  done
   1.573  
   1.574  lemma (in M_trivial) singleton_in_M_iff [iff]:
   1.575       "M({a}) <-> M(a)"
   1.576 -by (insert upair_in_M_iff [of a a], simp) 
   1.577 +by (insert upair_in_M_iff [of a a], simp)
   1.578  
   1.579 -lemma (in M_trivial) pair_abs [simp]: 
   1.580 +lemma (in M_trivial) pair_abs [simp]:
   1.581       "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   1.582  apply (simp add: pair_def ZF.Pair_def)
   1.583 -apply (blast intro: transM) 
   1.584 +apply (blast intro: transM)
   1.585  done
   1.586  
   1.587  lemma (in M_trivial) pair_in_M_iff [iff]:
   1.588 @@ -538,84 +543,84 @@
   1.589  lemma (in M_trivial) pair_components_in_M:
   1.590       "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   1.591  apply (simp add: Pair_def)
   1.592 -apply (blast dest: transM) 
   1.593 +apply (blast dest: transM)
   1.594  done
   1.595  
   1.596 -lemma (in M_trivial) cartprod_abs [simp]: 
   1.597 +lemma (in M_trivial) cartprod_abs [simp]:
   1.598       "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   1.599  apply (simp add: cartprod_def)
   1.600 -apply (rule iffI) 
   1.601 - apply (blast intro!: equalityI intro: transM dest!: rspec) 
   1.602 -apply (blast dest: transM) 
   1.603 +apply (rule iffI)
   1.604 + apply (blast intro!: equalityI intro: transM dest!: rspec)
   1.605 +apply (blast dest: transM)
   1.606  done
   1.607  
   1.608  subsubsection{*Absoluteness for Unions and Intersections*}
   1.609  
   1.610 -lemma (in M_trivial) union_abs [simp]: 
   1.611 +lemma (in M_trivial) union_abs [simp]:
   1.612       "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   1.613 -apply (simp add: union_def) 
   1.614 -apply (blast intro: transM) 
   1.615 +apply (simp add: union_def)
   1.616 +apply (blast intro: transM)
   1.617  done
   1.618  
   1.619 -lemma (in M_trivial) inter_abs [simp]: 
   1.620 +lemma (in M_trivial) inter_abs [simp]:
   1.621       "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   1.622 -apply (simp add: inter_def) 
   1.623 -apply (blast intro: transM) 
   1.624 +apply (simp add: inter_def)
   1.625 +apply (blast intro: transM)
   1.626  done
   1.627  
   1.628 -lemma (in M_trivial) setdiff_abs [simp]: 
   1.629 +lemma (in M_trivial) setdiff_abs [simp]:
   1.630       "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   1.631 -apply (simp add: setdiff_def) 
   1.632 -apply (blast intro: transM) 
   1.633 +apply (simp add: setdiff_def)
   1.634 +apply (blast intro: transM)
   1.635  done
   1.636  
   1.637 -lemma (in M_trivial) Union_abs [simp]: 
   1.638 +lemma (in M_trivial) Union_abs [simp]:
   1.639       "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   1.640 -apply (simp add: big_union_def) 
   1.641 -apply (blast intro!: equalityI dest: transM) 
   1.642 +apply (simp add: big_union_def)
   1.643 +apply (blast intro!: equalityI dest: transM)
   1.644  done
   1.645  
   1.646  lemma (in M_trivial) Union_closed [intro,simp]:
   1.647       "M(A) ==> M(Union(A))"
   1.648 -by (insert Union_ax, simp add: Union_ax_def) 
   1.649 +by (insert Union_ax, simp add: Union_ax_def)
   1.650  
   1.651  lemma (in M_trivial) Un_closed [intro,simp]:
   1.652       "[| M(A); M(B) |] ==> M(A Un B)"
   1.653 -by (simp only: Un_eq_Union, blast) 
   1.654 +by (simp only: Un_eq_Union, blast)
   1.655  
   1.656  lemma (in M_trivial) cons_closed [intro,simp]:
   1.657       "[| M(a); M(A) |] ==> M(cons(a,A))"
   1.658 -by (subst cons_eq [symmetric], blast) 
   1.659 +by (subst cons_eq [symmetric], blast)
   1.660  
   1.661 -lemma (in M_trivial) cons_abs [simp]: 
   1.662 +lemma (in M_trivial) cons_abs [simp]:
   1.663       "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
   1.664 -by (simp add: is_cons_def, blast intro: transM)  
   1.665 +by (simp add: is_cons_def, blast intro: transM)
   1.666  
   1.667 -lemma (in M_trivial) successor_abs [simp]: 
   1.668 +lemma (in M_trivial) successor_abs [simp]:
   1.669       "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
   1.670 -by (simp add: successor_def, blast)  
   1.671 +by (simp add: successor_def, blast)
   1.672  
   1.673  lemma (in M_trivial) succ_in_M_iff [iff]:
   1.674       "M(succ(a)) <-> M(a)"
   1.675 -apply (simp add: succ_def) 
   1.676 -apply (blast intro: transM) 
   1.677 +apply (simp add: succ_def)
   1.678 +apply (blast intro: transM)
   1.679  done
   1.680  
   1.681  subsubsection{*Absoluteness for Separation and Replacement*}
   1.682  
   1.683  lemma (in M_trivial) separation_closed [intro,simp]:
   1.684       "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   1.685 -apply (insert separation, simp add: separation_def) 
   1.686 -apply (drule rspec, assumption, clarify) 
   1.687 +apply (insert separation, simp add: separation_def)
   1.688 +apply (drule rspec, assumption, clarify)
   1.689  apply (subgoal_tac "y = Collect(A,P)", blast)
   1.690 -apply (blast dest: transM) 
   1.691 +apply (blast dest: transM)
   1.692  done
   1.693  
   1.694  lemma separation_iff:
   1.695       "separation(M,P) <-> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
   1.696 -by (simp add: separation_def is_Collect_def) 
   1.697 +by (simp add: separation_def is_Collect_def)
   1.698  
   1.699 -lemma (in M_trivial) Collect_abs [simp]: 
   1.700 +lemma (in M_trivial) Collect_abs [simp]:
   1.701       "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)"
   1.702  apply (simp add: is_Collect_def)
   1.703  apply (blast intro!: equalityI dest: transM)
   1.704 @@ -625,70 +630,68 @@
   1.705  lemma (in M_trivial) strong_replacementI [rule_format]:
   1.706      "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
   1.707       ==> strong_replacement(M,P)"
   1.708 -apply (simp add: strong_replacement_def, clarify) 
   1.709 -apply (frule replacementD [OF replacement], assumption, clarify) 
   1.710 -apply (drule_tac x=A in rspec, clarify)  
   1.711 -apply (drule_tac z=Y in separationD, assumption, clarify) 
   1.712 -apply (rule_tac x=y in rexI) 
   1.713 -apply (blast dest: transM)+
   1.714 +apply (simp add: strong_replacement_def, clarify)
   1.715 +apply (frule replacementD [OF replacement], assumption, clarify)
   1.716 +apply (drule_tac x=A in rspec, clarify)
   1.717 +apply (drule_tac z=Y in separationD, assumption, clarify)
   1.718 +apply (rule_tac x=y in rexI, force, assumption)
   1.719  done
   1.720  
   1.721 -
   1.722  subsubsection{*The Operator @{term is_Replace}*}
   1.723  
   1.724  
   1.725  lemma is_Replace_cong [cong]:
   1.726 -     "[| A=A'; 
   1.727 +     "[| A=A';
   1.728           !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y);
   1.729 -         z=z' |] 
   1.730 -      ==> is_Replace(M, A, %x y. P(x,y), z) <-> 
   1.731 -          is_Replace(M, A', %x y. P'(x,y), z')" 
   1.732 -by (simp add: is_Replace_def) 
   1.733 +         z=z' |]
   1.734 +      ==> is_Replace(M, A, %x y. P(x,y), z) <->
   1.735 +          is_Replace(M, A', %x y. P'(x,y), z')"
   1.736 +by (simp add: is_Replace_def)
   1.737  
   1.738 -lemma (in M_trivial) univalent_Replace_iff: 
   1.739 +lemma (in M_trivial) univalent_Replace_iff:
   1.740       "[| M(A); univalent(M,A,P);
   1.741 -         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] 
   1.742 +         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
   1.743        ==> u \<in> Replace(A,P) <-> (\<exists>x. x\<in>A & P(x,u))"
   1.744 -apply (simp add: Replace_iff univalent_def) 
   1.745 +apply (simp add: Replace_iff univalent_def)
   1.746  apply (blast dest: transM)
   1.747  done
   1.748  
   1.749  (*The last premise expresses that P takes M to M*)
   1.750  lemma (in M_trivial) strong_replacement_closed [intro,simp]:
   1.751 -     "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   1.752 +     "[| strong_replacement(M,P); M(A); univalent(M,A,P);
   1.753           !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
   1.754 -apply (simp add: strong_replacement_def) 
   1.755 -apply (drule_tac x=A in rspec, safe) 
   1.756 +apply (simp add: strong_replacement_def)
   1.757 +apply (drule_tac x=A in rspec, safe)
   1.758  apply (subgoal_tac "Replace(A,P) = Y")
   1.759 - apply simp 
   1.760 + apply simp
   1.761  apply (rule equality_iffI)
   1.762  apply (simp add: univalent_Replace_iff)
   1.763 -apply (blast dest: transM) 
   1.764 +apply (blast dest: transM)
   1.765  done
   1.766  
   1.767 -lemma (in M_trivial) Replace_abs: 
   1.768 +lemma (in M_trivial) Replace_abs:
   1.769       "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P);
   1.770 -         !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |] 
   1.771 +         !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |]
   1.772        ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
   1.773  apply (simp add: is_Replace_def)
   1.774 -apply (rule iffI) 
   1.775 -apply (rule M_equalityI) 
   1.776 -apply (simp_all add: univalent_Replace_iff, blast, blast) 
   1.777 +apply (rule iffI)
   1.778 +apply (rule M_equalityI)
   1.779 +apply (simp_all add: univalent_Replace_iff, blast, blast)
   1.780  done
   1.781  
   1.782  (*The first premise can't simply be assumed as a schema.
   1.783    It is essential to take care when asserting instances of Replacement.
   1.784    Let K be a nonconstructible subset of nat and define
   1.785 -  f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   1.786 +  f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a
   1.787    nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   1.788    even for f : M -> M.
   1.789  *)
   1.790  lemma (in M_trivial) RepFun_closed:
   1.791       "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   1.792        ==> M(RepFun(A,f))"
   1.793 -apply (simp add: RepFun_def) 
   1.794 -apply (rule strong_replacement_closed) 
   1.795 -apply (auto dest: transM  simp add: univalent_def) 
   1.796 +apply (simp add: RepFun_def)
   1.797 +apply (rule strong_replacement_closed)
   1.798 +apply (auto dest: transM  simp add: univalent_def)
   1.799  done
   1.800  
   1.801  lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
   1.802 @@ -701,69 +704,69 @@
   1.803        ==> M(RepFun(A, %x. f(x)))"
   1.804  apply (simp add: RepFun_def)
   1.805  apply (frule strong_replacement_closed, assumption)
   1.806 -apply (auto dest: transM  simp add: Replace_conj_eq univalent_def) 
   1.807 +apply (auto dest: transM  simp add: Replace_conj_eq univalent_def)
   1.808  done
   1.809  
   1.810  subsubsection {*Absoluteness for @{term Lambda}*}
   1.811  
   1.812  constdefs
   1.813   is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
   1.814 -    "is_lambda(M, A, is_b, z) == 
   1.815 +    "is_lambda(M, A, is_b, z) ==
   1.816         \<forall>p[M]. p \<in> z <->
   1.817          (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
   1.818  
   1.819  lemma (in M_trivial) lam_closed:
   1.820       "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   1.821        ==> M(\<lambda>x\<in>A. b(x))"
   1.822 -by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
   1.823 +by (simp add: lam_def, blast intro: RepFun_closed dest: transM)
   1.824  
   1.825  text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
   1.826  lemma (in M_trivial) lam_closed2:
   1.827    "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   1.828       M(A); \<forall>m[M]. m\<in>A --> M(b(m))|] ==> M(Lambda(A,b))"
   1.829  apply (simp add: lam_def)
   1.830 -apply (blast intro: RepFun_closed2 dest: transM)  
   1.831 +apply (blast intro: RepFun_closed2 dest: transM)
   1.832  done
   1.833  
   1.834 -lemma (in M_trivial) lambda_abs2 [simp]: 
   1.835 +lemma (in M_trivial) lambda_abs2 [simp]:
   1.836       "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
   1.837 -         Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |] 
   1.838 +         Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
   1.839        ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
   1.840  apply (simp add: Relativize1_def is_lambda_def)
   1.841  apply (rule iffI)
   1.842 - prefer 2 apply (simp add: lam_def) 
   1.843 + prefer 2 apply (simp add: lam_def)
   1.844  apply (rule M_equalityI)
   1.845 -  apply (simp add: lam_def) 
   1.846 +  apply (simp add: lam_def)
   1.847   apply (simp add: lam_closed2)+
   1.848  done
   1.849  
   1.850  lemma is_lambda_cong [cong]:
   1.851 -     "[| A=A';  z=z'; 
   1.852 -         !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] 
   1.853 -      ==> is_lambda(M, A, %x y. is_b(x,y), z) <-> 
   1.854 -          is_lambda(M, A', %x y. is_b'(x,y), z')" 
   1.855 -by (simp add: is_lambda_def) 
   1.856 +     "[| A=A';  z=z';
   1.857 +         !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
   1.858 +      ==> is_lambda(M, A, %x y. is_b(x,y), z) <->
   1.859 +          is_lambda(M, A', %x y. is_b'(x,y), z')"
   1.860 +by (simp add: is_lambda_def)
   1.861  
   1.862 -lemma (in M_trivial) image_abs [simp]: 
   1.863 +lemma (in M_trivial) image_abs [simp]:
   1.864       "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   1.865  apply (simp add: image_def)
   1.866 -apply (rule iffI) 
   1.867 - apply (blast intro!: equalityI dest: transM, blast) 
   1.868 +apply (rule iffI)
   1.869 + apply (blast intro!: equalityI dest: transM, blast)
   1.870  done
   1.871  
   1.872  text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   1.873        This result is one direction of absoluteness.*}
   1.874  
   1.875 -lemma (in M_trivial) powerset_Pow: 
   1.876 +lemma (in M_trivial) powerset_Pow:
   1.877       "powerset(M, x, Pow(x))"
   1.878  by (simp add: powerset_def)
   1.879  
   1.880  text{*But we can't prove that the powerset in @{text M} includes the
   1.881        real powerset.*}
   1.882 -lemma (in M_trivial) powerset_imp_subset_Pow: 
   1.883 +lemma (in M_trivial) powerset_imp_subset_Pow:
   1.884       "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   1.885 -apply (simp add: powerset_def) 
   1.886 -apply (blast dest: transM) 
   1.887 +apply (simp add: powerset_def)
   1.888 +apply (blast dest: transM)
   1.889  done
   1.890  
   1.891  subsubsection{*Absoluteness for the Natural Numbers*}
   1.892 @@ -774,126 +777,123 @@
   1.893  
   1.894  lemma (in M_trivial) nat_case_closed [intro,simp]:
   1.895    "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   1.896 -apply (case_tac "k=0", simp) 
   1.897 +apply (case_tac "k=0", simp)
   1.898  apply (case_tac "\<exists>m. k = succ(m)", force)
   1.899 -apply (simp add: nat_case_def) 
   1.900 +apply (simp add: nat_case_def)
   1.901  done
   1.902  
   1.903 -lemma (in M_trivial) quasinat_abs [simp]: 
   1.904 +lemma (in M_trivial) quasinat_abs [simp]:
   1.905       "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
   1.906  by (auto simp add: is_quasinat_def quasinat_def)
   1.907  
   1.908 -lemma (in M_trivial) nat_case_abs [simp]: 
   1.909 -     "[| relativize1(M,is_b,b); M(k); M(z) |] 
   1.910 +lemma (in M_trivial) nat_case_abs [simp]:
   1.911 +     "[| relativize1(M,is_b,b); M(k); M(z) |]
   1.912        ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
   1.913 -apply (case_tac "quasinat(k)") 
   1.914 - prefer 2 
   1.915 - apply (simp add: is_nat_case_def non_nat_case) 
   1.916 - apply (force simp add: quasinat_def) 
   1.917 +apply (case_tac "quasinat(k)")
   1.918 + prefer 2
   1.919 + apply (simp add: is_nat_case_def non_nat_case)
   1.920 + apply (force simp add: quasinat_def)
   1.921  apply (simp add: quasinat_def is_nat_case_def)
   1.922 -apply (elim disjE exE) 
   1.923 - apply (simp_all add: relativize1_def) 
   1.924 +apply (elim disjE exE)
   1.925 + apply (simp_all add: relativize1_def)
   1.926  done
   1.927  
   1.928 -(*NOT for the simplifier.  The assumption M(z') is apparently necessary, but 
   1.929 +(*NOT for the simplifier.  The assumption M(z') is apparently necessary, but
   1.930    causes the error "Failed congruence proof!"  It may be better to replace
   1.931    is_nat_case by nat_case before attempting congruence reasoning.*)
   1.932  lemma is_nat_case_cong:
   1.933       "[| a = a'; k = k';  z = z';  M(z');
   1.934         !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
   1.935        ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
   1.936 -by (simp add: is_nat_case_def) 
   1.937 +by (simp add: is_nat_case_def)
   1.938  
   1.939  
   1.940  subsection{*Absoluteness for Ordinals*}
   1.941  text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   1.942  
   1.943  lemma (in M_trivial) lt_closed:
   1.944 -     "[| j<i; M(i) |] ==> M(j)" 
   1.945 -by (blast dest: ltD intro: transM) 
   1.946 +     "[| j<i; M(i) |] ==> M(j)"
   1.947 +by (blast dest: ltD intro: transM)
   1.948  
   1.949 -lemma (in M_trivial) transitive_set_abs [simp]: 
   1.950 +lemma (in M_trivial) transitive_set_abs [simp]:
   1.951       "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   1.952  by (simp add: transitive_set_def Transset_def)
   1.953  
   1.954 -lemma (in M_trivial) ordinal_abs [simp]: 
   1.955 +lemma (in M_trivial) ordinal_abs [simp]:
   1.956       "M(a) ==> ordinal(M,a) <-> Ord(a)"
   1.957  by (simp add: ordinal_def Ord_def)
   1.958  
   1.959 -lemma (in M_trivial) limit_ordinal_abs [simp]: 
   1.960 -     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)" 
   1.961 -apply (unfold Limit_def limit_ordinal_def) 
   1.962 -apply (simp add: Ord_0_lt_iff) 
   1.963 -apply (simp add: lt_def, blast) 
   1.964 +lemma (in M_trivial) limit_ordinal_abs [simp]:
   1.965 +     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   1.966 +apply (unfold Limit_def limit_ordinal_def)
   1.967 +apply (simp add: Ord_0_lt_iff)
   1.968 +apply (simp add: lt_def, blast)
   1.969  done
   1.970  
   1.971 -lemma (in M_trivial) successor_ordinal_abs [simp]: 
   1.972 +lemma (in M_trivial) successor_ordinal_abs [simp]:
   1.973       "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   1.974  apply (simp add: successor_ordinal_def, safe)
   1.975 -apply (drule Ord_cases_disj, auto) 
   1.976 +apply (drule Ord_cases_disj, auto)
   1.977  done
   1.978  
   1.979  lemma finite_Ord_is_nat:
   1.980        "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   1.981  by (induct a rule: trans_induct3, simp_all)
   1.982  
   1.983 -lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   1.984 -by (induct a rule: nat_induct, auto)
   1.985 -
   1.986 -lemma (in M_trivial) finite_ordinal_abs [simp]: 
   1.987 +lemma (in M_trivial) finite_ordinal_abs [simp]:
   1.988       "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   1.989  apply (simp add: finite_ordinal_def)
   1.990 -apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   1.991 +apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord
   1.992               dest: Ord_trans naturals_not_limit)
   1.993  done
   1.994  
   1.995  lemma Limit_non_Limit_implies_nat:
   1.996       "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   1.997 -apply (rule le_anti_sym) 
   1.998 -apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   1.999 - apply (simp add: lt_def)  
  1.1000 - apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
  1.1001 +apply (rule le_anti_sym)
  1.1002 +apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)
  1.1003 + apply (simp add: lt_def)
  1.1004 + apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat)
  1.1005  apply (erule nat_le_Limit)
  1.1006  done
  1.1007  
  1.1008 -lemma (in M_trivial) omega_abs [simp]: 
  1.1009 +lemma (in M_trivial) omega_abs [simp]:
  1.1010       "M(a) ==> omega(M,a) <-> a = nat"
  1.1011 -apply (simp add: omega_def) 
  1.1012 +apply (simp add: omega_def)
  1.1013  apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
  1.1014  done
  1.1015  
  1.1016 -lemma (in M_trivial) number1_abs [simp]: 
  1.1017 +lemma (in M_trivial) number1_abs [simp]:
  1.1018       "M(a) ==> number1(M,a) <-> a = 1"
  1.1019 -by (simp add: number1_def) 
  1.1020 +by (simp add: number1_def)
  1.1021  
  1.1022 -lemma (in M_trivial) number2_abs [simp]: 
  1.1023 +lemma (in M_trivial) number2_abs [simp]:
  1.1024       "M(a) ==> number2(M,a) <-> a = succ(1)"
  1.1025 -by (simp add: number2_def) 
  1.1026 +by (simp add: number2_def)
  1.1027  
  1.1028 -lemma (in M_trivial) number3_abs [simp]: 
  1.1029 +lemma (in M_trivial) number3_abs [simp]:
  1.1030       "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
  1.1031 -by (simp add: number3_def) 
  1.1032 +by (simp add: number3_def)
  1.1033  
  1.1034  text{*Kunen continued to 20...*}
  1.1035  
  1.1036 -(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
  1.1037 +(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything
  1.1038    but the recursion variable must stay unchanged.  But then the recursion
  1.1039 -  equations only hold for x\<in>nat (or in some other set) and not for the 
  1.1040 +  equations only hold for x\<in>nat (or in some other set) and not for the
  1.1041    whole of the class M.
  1.1042    consts
  1.1043      natnumber_aux :: "[i=>o,i] => i"
  1.1044  
  1.1045    primrec
  1.1046        "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
  1.1047 -      "natnumber_aux(M,succ(n)) = 
  1.1048 -	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
  1.1049 +      "natnumber_aux(M,succ(n)) =
  1.1050 +	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x))
  1.1051  		     then 1 else 0)"
  1.1052  
  1.1053    constdefs
  1.1054      natnumber :: "[i=>o,i,i] => o"
  1.1055        "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
  1.1056  
  1.1057 -  lemma (in M_trivial) [simp]: 
  1.1058 +  lemma (in M_trivial) [simp]:
  1.1059         "natnumber(M,0,x) == x=0"
  1.1060  *)
  1.1061  
  1.1062 @@ -905,114 +905,110 @@
  1.1063    and Diff_separation:
  1.1064       "M(B) ==> separation(M, \<lambda>x. x \<notin> B)"
  1.1065    and cartprod_separation:
  1.1066 -     "[| M(A); M(B) |] 
  1.1067 +     "[| M(A); M(B) |]
  1.1068        ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
  1.1069    and image_separation:
  1.1070 -     "[| M(A); M(r) |] 
  1.1071 +     "[| M(A); M(r) |]
  1.1072        ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
  1.1073    and converse_separation:
  1.1074 -     "M(r) ==> separation(M, 
  1.1075 +     "M(r) ==> separation(M,
  1.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)))"
  1.1077    and restrict_separation:
  1.1078       "M(A) ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. pair(M,x,y,z)))"
  1.1079    and comp_separation:
  1.1080       "[| M(r); M(s) |]
  1.1081 -      ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 
  1.1082 -		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & 
  1.1083 +      ==> separation(M, \<lambda>xz. \<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
  1.1084 +		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) &
  1.1085                    xy\<in>s & yz\<in>r)"
  1.1086    and pred_separation:
  1.1087       "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & pair(M,y,x,p))"
  1.1088    and Memrel_separation:
  1.1089       "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
  1.1090    and funspace_succ_replacement:
  1.1091 -     "M(n) ==> 
  1.1092 -      strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M]. 
  1.1093 +     "M(n) ==>
  1.1094 +      strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M].
  1.1095                  pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
  1.1096                  upair(M,cnbf,cnbf,z))"
  1.1097    and well_ord_iso_separation:
  1.1098 -     "[| M(A); M(f); M(r) |] 
  1.1099 -      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M]. 
  1.1100 +     "[| M(A); M(f); M(r) |]
  1.1101 +      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M].
  1.1102  		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
  1.1103    and obase_separation:
  1.1104       --{*part of the order type formalization*}
  1.1105 -     "[| M(A); M(r) |] 
  1.1106 -      ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
  1.1107 +     "[| M(A); M(r) |]
  1.1108 +      ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
  1.1109  	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
  1.1110  	     order_isomorphism(M,par,r,x,mx,g))"
  1.1111    and obase_equals_separation:
  1.1112 -     "[| M(A); M(r) |] 
  1.1113 -      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M]. 
  1.1114 -			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M]. 
  1.1115 +     "[| M(A); M(r) |]
  1.1116 +      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].
  1.1117 +			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].
  1.1118  			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
  1.1119  			      order_isomorphism(M,pxr,r,y,my,g))))"
  1.1120    and omap_replacement:
  1.1121 -     "[| M(A); M(r) |] 
  1.1122 +     "[| M(A); M(r) |]
  1.1123        ==> strong_replacement(M,
  1.1124 -             \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
  1.1125 -	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
  1.1126 +             \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
  1.1127 +	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
  1.1128  	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
  1.1129    and is_recfun_separation:
  1.1130       --{*for well-founded recursion*}
  1.1131 -     "[| M(r); M(f); M(g); M(a); M(b) |] 
  1.1132 -     ==> separation(M, 
  1.1133 -            \<lambda>x. \<exists>xa[M]. \<exists>xb[M]. 
  1.1134 -                pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r & 
  1.1135 -                (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & 
  1.1136 +     "[| M(r); M(f); M(g); M(a); M(b) |]
  1.1137 +     ==> separation(M,
  1.1138 +            \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
  1.1139 +                pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r &
  1.1140 +                (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
  1.1141                                     fx \<noteq> gx))"
  1.1142  
  1.1143  lemma (in M_basic) cartprod_iff_lemma:
  1.1144 -     "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
  1.1145 +     "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
  1.1146           powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
  1.1147         ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
  1.1148 -apply (simp add: powerset_def) 
  1.1149 +apply (simp add: powerset_def)
  1.1150  apply (rule equalityI, clarify, simp)
  1.1151 - apply (frule transM, assumption) 
  1.1152 + apply (frule transM, assumption)
  1.1153   apply (frule transM, assumption, simp (no_asm_simp))
  1.1154 - apply blast 
  1.1155 + apply blast
  1.1156  apply clarify
  1.1157 -apply (frule transM, assumption, force) 
  1.1158 +apply (frule transM, assumption, force)
  1.1159  done
  1.1160  
  1.1161  lemma (in M_basic) cartprod_iff:
  1.1162 -     "[| M(A); M(B); M(C) |] 
  1.1163 -      ==> cartprod(M,A,B,C) <-> 
  1.1164 -          (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
  1.1165 +     "[| M(A); M(B); M(C) |]
  1.1166 +      ==> cartprod(M,A,B,C) <->
  1.1167 +          (\<exists>p1[M]. \<exists>p2[M]. powerset(M,A Un B,p1) & powerset(M,p1,p2) &
  1.1168                     C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
  1.1169  apply (simp add: Pair_def cartprod_def, safe)
  1.1170 -defer 1 
  1.1171 -  apply (simp add: powerset_def) 
  1.1172 - apply blast 
  1.1173 +defer 1
  1.1174 +  apply (simp add: powerset_def)
  1.1175 + apply blast
  1.1176  txt{*Final, difficult case: the left-to-right direction of the theorem.*}
  1.1177 -apply (insert power_ax, simp add: power_ax_def) 
  1.1178 -apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
  1.1179 -apply (blast, clarify) 
  1.1180 +apply (insert power_ax, simp add: power_ax_def)
  1.1181 +apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
  1.1182 +apply (blast, clarify)
  1.1183  apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
  1.1184  apply assumption
  1.1185 -apply (blast intro: cartprod_iff_lemma) 
  1.1186 +apply (blast intro: cartprod_iff_lemma)
  1.1187  done
  1.1188  
  1.1189  lemma (in M_basic) cartprod_closed_lemma:
  1.1190       "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
  1.1191  apply (simp del: cartprod_abs add: cartprod_iff)
  1.1192 -apply (insert power_ax, simp add: power_ax_def) 
  1.1193 -apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
  1.1194 -apply (blast, clarify) 
  1.1195 -apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
  1.1196 +apply (insert power_ax, simp add: power_ax_def)
  1.1197 +apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
  1.1198  apply (blast, clarify)
  1.1199 -apply (intro rexI exI conjI) 
  1.1200 -prefer 5 apply (rule refl) 
  1.1201 -prefer 3 apply assumption
  1.1202 -prefer 3 apply assumption
  1.1203 -apply (insert cartprod_separation [of A B], auto)
  1.1204 +apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec, auto)
  1.1205 +apply (intro rexI conjI, simp+)
  1.1206 +apply (insert cartprod_separation [of A B], simp)
  1.1207  done
  1.1208  
  1.1209  text{*All the lemmas above are necessary because Powerset is not absolute.
  1.1210        I should have used Replacement instead!*}
  1.1211 -lemma (in M_basic) cartprod_closed [intro,simp]: 
  1.1212 +lemma (in M_basic) cartprod_closed [intro,simp]:
  1.1213       "[| M(A); M(B) |] ==> M(A*B)"
  1.1214  by (frule cartprod_closed_lemma, assumption, force)
  1.1215  
  1.1216 -lemma (in M_basic) sum_closed [intro,simp]: 
  1.1217 +lemma (in M_basic) sum_closed [intro,simp]:
  1.1218       "[| M(A); M(B) |] ==> M(A+B)"
  1.1219  by (simp add: sum_def)
  1.1220  
  1.1221 @@ -1022,7 +1018,7 @@
  1.1222  
  1.1223  lemma (in M_trivial) Inl_in_M_iff [iff]:
  1.1224       "M(Inl(a)) <-> M(a)"
  1.1225 -by (simp add: Inl_def) 
  1.1226 +by (simp add: Inl_def)
  1.1227  
  1.1228  lemma (in M_trivial) Inl_abs [simp]:
  1.1229       "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
  1.1230 @@ -1030,7 +1026,7 @@
  1.1231  
  1.1232  lemma (in M_trivial) Inr_in_M_iff [iff]:
  1.1233       "M(Inr(a)) <-> M(a)"
  1.1234 -by (simp add: Inr_def) 
  1.1235 +by (simp add: Inr_def)
  1.1236  
  1.1237  lemma (in M_trivial) Inr_abs [simp]:
  1.1238       "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
  1.1239 @@ -1040,27 +1036,27 @@
  1.1240  subsubsection {*converse of a relation*}
  1.1241  
  1.1242  lemma (in M_basic) M_converse_iff:
  1.1243 -     "M(r) ==> 
  1.1244 -      converse(r) = 
  1.1245 -      {z \<in> Union(Union(r)) * Union(Union(r)). 
  1.1246 +     "M(r) ==>
  1.1247 +      converse(r) =
  1.1248 +      {z \<in> Union(Union(r)) * Union(Union(r)).
  1.1249         \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
  1.1250  apply (rule equalityI)
  1.1251 - prefer 2 apply (blast dest: transM, clarify, simp) 
  1.1252 -apply (simp add: Pair_def) 
  1.1253 -apply (blast dest: transM) 
  1.1254 + prefer 2 apply (blast dest: transM, clarify, simp)
  1.1255 +apply (simp add: Pair_def)
  1.1256 +apply (blast dest: transM)
  1.1257  done
  1.1258  
  1.1259 -lemma (in M_basic) converse_closed [intro,simp]: 
  1.1260 +lemma (in M_basic) converse_closed [intro,simp]:
  1.1261       "M(r) ==> M(converse(r))"
  1.1262  apply (simp add: M_converse_iff)
  1.1263  apply (insert converse_separation [of r], simp)
  1.1264  done
  1.1265  
  1.1266 -lemma (in M_basic) converse_abs [simp]: 
  1.1267 +lemma (in M_basic) converse_abs [simp]:
  1.1268       "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
  1.1269  apply (simp add: is_converse_def)
  1.1270  apply (rule iffI)
  1.1271 - prefer 2 apply blast 
  1.1272 + prefer 2 apply blast
  1.1273  apply (rule M_equalityI)
  1.1274    apply simp
  1.1275    apply (blast dest: transM)+
  1.1276 @@ -1069,98 +1065,98 @@
  1.1277  
  1.1278  subsubsection {*image, preimage, domain, range*}
  1.1279  
  1.1280 -lemma (in M_basic) image_closed [intro,simp]: 
  1.1281 +lemma (in M_basic) image_closed [intro,simp]:
  1.1282       "[| M(A); M(r) |] ==> M(r``A)"
  1.1283  apply (simp add: image_iff_Collect)
  1.1284 -apply (insert image_separation [of A r], simp) 
  1.1285 +apply (insert image_separation [of A r], simp)
  1.1286  done
  1.1287  
  1.1288 -lemma (in M_basic) vimage_abs [simp]: 
  1.1289 +lemma (in M_basic) vimage_abs [simp]:
  1.1290       "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
  1.1291  apply (simp add: pre_image_def)
  1.1292 -apply (rule iffI) 
  1.1293 - apply (blast intro!: equalityI dest: transM, blast) 
  1.1294 +apply (rule iffI)
  1.1295 + apply (blast intro!: equalityI dest: transM, blast)
  1.1296  done
  1.1297  
  1.1298 -lemma (in M_basic) vimage_closed [intro,simp]: 
  1.1299 +lemma (in M_basic) vimage_closed [intro,simp]:
  1.1300       "[| M(A); M(r) |] ==> M(r-``A)"
  1.1301  by (simp add: vimage_def)
  1.1302  
  1.1303  
  1.1304  subsubsection{*Domain, range and field*}
  1.1305  
  1.1306 -lemma (in M_basic) domain_abs [simp]: 
  1.1307 +lemma (in M_basic) domain_abs [simp]:
  1.1308       "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
  1.1309 -apply (simp add: is_domain_def) 
  1.1310 -apply (blast intro!: equalityI dest: transM) 
  1.1311 +apply (simp add: is_domain_def)
  1.1312 +apply (blast intro!: equalityI dest: transM)
  1.1313  done
  1.1314  
  1.1315 -lemma (in M_basic) domain_closed [intro,simp]: 
  1.1316 +lemma (in M_basic) domain_closed [intro,simp]:
  1.1317       "M(r) ==> M(domain(r))"
  1.1318  apply (simp add: domain_eq_vimage)
  1.1319  done
  1.1320  
  1.1321 -lemma (in M_basic) range_abs [simp]: 
  1.1322 +lemma (in M_basic) range_abs [simp]:
  1.1323       "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
  1.1324  apply (simp add: is_range_def)
  1.1325  apply (blast intro!: equalityI dest: transM)
  1.1326  done
  1.1327  
  1.1328 -lemma (in M_basic) range_closed [intro,simp]: 
  1.1329 +lemma (in M_basic) range_closed [intro,simp]:
  1.1330       "M(r) ==> M(range(r))"
  1.1331  apply (simp add: range_eq_image)
  1.1332  done
  1.1333  
  1.1334 -lemma (in M_basic) field_abs [simp]: 
  1.1335 +lemma (in M_basic) field_abs [simp]:
  1.1336       "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
  1.1337  by (simp add: domain_closed range_closed is_field_def field_def)
  1.1338  
  1.1339 -lemma (in M_basic) field_closed [intro,simp]: 
  1.1340 +lemma (in M_basic) field_closed [intro,simp]:
  1.1341       "M(r) ==> M(field(r))"
  1.1342 -by (simp add: domain_closed range_closed Un_closed field_def) 
  1.1343 +by (simp add: domain_closed range_closed Un_closed field_def)
  1.1344  
  1.1345  
  1.1346  subsubsection{*Relations, functions and application*}
  1.1347  
  1.1348 -lemma (in M_basic) relation_abs [simp]: 
  1.1349 +lemma (in M_basic) relation_abs [simp]:
  1.1350       "M(r) ==> is_relation(M,r) <-> relation(r)"
  1.1351 -apply (simp add: is_relation_def relation_def) 
  1.1352 +apply (simp add: is_relation_def relation_def)
  1.1353  apply (blast dest!: bspec dest: pair_components_in_M)+
  1.1354  done
  1.1355  
  1.1356 -lemma (in M_basic) function_abs [simp]: 
  1.1357 +lemma (in M_basic) function_abs [simp]:
  1.1358       "M(r) ==> is_function(M,r) <-> function(r)"
  1.1359 -apply (simp add: is_function_def function_def, safe) 
  1.1360 -   apply (frule transM, assumption) 
  1.1361 +apply (simp add: is_function_def function_def, safe)
  1.1362 +   apply (frule transM, assumption)
  1.1363    apply (blast dest: pair_components_in_M)+
  1.1364  done
  1.1365  
  1.1366 -lemma (in M_basic) apply_closed [intro,simp]: 
  1.1367 +lemma (in M_basic) apply_closed [intro,simp]:
  1.1368       "[|M(f); M(a)|] ==> M(f`a)"
  1.1369  by (simp add: apply_def)
  1.1370  
  1.1371 -lemma (in M_basic) apply_abs [simp]: 
  1.1372 +lemma (in M_basic) apply_abs [simp]:
  1.1373       "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
  1.1374 -apply (simp add: fun_apply_def apply_def, blast) 
  1.1375 +apply (simp add: fun_apply_def apply_def, blast)
  1.1376  done
  1.1377  
  1.1378 -lemma (in M_basic) typed_function_abs [simp]: 
  1.1379 +lemma (in M_basic) typed_function_abs [simp]:
  1.1380       "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
  1.1381 -apply (auto simp add: typed_function_def relation_def Pi_iff) 
  1.1382 +apply (auto simp add: typed_function_def relation_def Pi_iff)
  1.1383  apply (blast dest: pair_components_in_M)+
  1.1384  done
  1.1385  
  1.1386 -lemma (in M_basic) injection_abs [simp]: 
  1.1387 +lemma (in M_basic) injection_abs [simp]:
  1.1388       "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
  1.1389  apply (simp add: injection_def apply_iff inj_def apply_closed)
  1.1390 -apply (blast dest: transM [of _ A]) 
  1.1391 +apply (blast dest: transM [of _ A])
  1.1392  done
  1.1393  
  1.1394 -lemma (in M_basic) surjection_abs [simp]: 
  1.1395 +lemma (in M_basic) surjection_abs [simp]:
  1.1396       "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
  1.1397  by (simp add: surjection_def surj_def)
  1.1398  
  1.1399 -lemma (in M_basic) bijection_abs [simp]: 
  1.1400 +lemma (in M_basic) bijection_abs [simp]:
  1.1401       "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
  1.1402  by (simp add: bijection_def bij_def)
  1.1403  
  1.1404 @@ -1168,31 +1164,31 @@
  1.1405  subsubsection{*Composition of relations*}
  1.1406  
  1.1407  lemma (in M_basic) M_comp_iff:
  1.1408 -     "[| M(r); M(s) |] 
  1.1409 -      ==> r O s = 
  1.1410 -          {xz \<in> domain(s) * range(r).  
  1.1411 +     "[| M(r); M(s) |]
  1.1412 +      ==> r O s =
  1.1413 +          {xz \<in> domain(s) * range(r).
  1.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}"
  1.1415  apply (simp add: comp_def)
  1.1416 -apply (rule equalityI) 
  1.1417 - apply clarify 
  1.1418 - apply simp 
  1.1419 +apply (rule equalityI)
  1.1420 + apply clarify
  1.1421 + apply simp
  1.1422   apply  (blast dest:  transM)+
  1.1423  done
  1.1424  
  1.1425 -lemma (in M_basic) comp_closed [intro,simp]: 
  1.1426 +lemma (in M_basic) comp_closed [intro,simp]:
  1.1427       "[| M(r); M(s) |] ==> M(r O s)"
  1.1428  apply (simp add: M_comp_iff)
  1.1429 -apply (insert comp_separation [of r s], simp) 
  1.1430 +apply (insert comp_separation [of r s], simp)
  1.1431  done
  1.1432  
  1.1433 -lemma (in M_basic) composition_abs [simp]: 
  1.1434 -     "[| M(r); M(s); M(t) |] 
  1.1435 +lemma (in M_basic) composition_abs [simp]:
  1.1436 +     "[| M(r); M(s); M(t) |]
  1.1437        ==> composition(M,r,s,t) <-> t = r O s"
  1.1438  apply safe
  1.1439   txt{*Proving @{term "composition(M, r, s, r O s)"}*}
  1.1440 - prefer 2 
  1.1441 + prefer 2
  1.1442   apply (simp add: composition_def comp_def)
  1.1443 - apply (blast dest: transM) 
  1.1444 + apply (blast dest: transM)
  1.1445  txt{*Opposite implication*}
  1.1446  apply (rule M_equalityI)
  1.1447    apply (simp add: composition_def comp_def)
  1.1448 @@ -1200,18 +1196,18 @@
  1.1449  done
  1.1450  
  1.1451  text{*no longer needed*}
  1.1452 -lemma (in M_basic) restriction_is_function: 
  1.1453 -     "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
  1.1454 +lemma (in M_basic) restriction_is_function:
  1.1455 +     "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]
  1.1456        ==> function(z)"
  1.1457 -apply (simp add: restriction_def ball_iff_equiv) 
  1.1458 -apply (unfold function_def, blast) 
  1.1459 +apply (simp add: restriction_def ball_iff_equiv)
  1.1460 +apply (unfold function_def, blast)
  1.1461  done
  1.1462  
  1.1463 -lemma (in M_basic) restriction_abs [simp]: 
  1.1464 -     "[| M(f); M(A); M(z) |] 
  1.1465 +lemma (in M_basic) restriction_abs [simp]:
  1.1466 +     "[| M(f); M(A); M(z) |]
  1.1467        ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
  1.1468  apply (simp add: ball_iff_equiv restriction_def restrict_def)
  1.1469 -apply (blast intro!: equalityI dest: transM) 
  1.1470 +apply (blast intro!: equalityI dest: transM)
  1.1471  done
  1.1472  
  1.1473  
  1.1474 @@ -1219,16 +1215,16 @@
  1.1475       "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
  1.1476  by (simp add: restrict_def, blast dest: transM)
  1.1477  
  1.1478 -lemma (in M_basic) restrict_closed [intro,simp]: 
  1.1479 +lemma (in M_basic) restrict_closed [intro,simp]:
  1.1480       "[| M(A); M(r) |] ==> M(restrict(r,A))"
  1.1481  apply (simp add: M_restrict_iff)
  1.1482 -apply (insert restrict_separation [of A], simp) 
  1.1483 +apply (insert restrict_separation [of A], simp)
  1.1484  done
  1.1485  
  1.1486 -lemma (in M_basic) Inter_abs [simp]: 
  1.1487 +lemma (in M_basic) Inter_abs [simp]:
  1.1488       "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
  1.1489 -apply (simp add: big_inter_def Inter_def) 
  1.1490 -apply (blast intro!: equalityI dest: transM) 
  1.1491 +apply (simp add: big_inter_def Inter_def)
  1.1492 +apply (blast intro!: equalityI dest: transM)
  1.1493  done
  1.1494  
  1.1495  lemma (in M_basic) Inter_closed [intro,simp]:
  1.1496 @@ -1238,7 +1234,7 @@
  1.1497  lemma (in M_basic) Int_closed [intro,simp]:
  1.1498       "[| M(A); M(B) |] ==> M(A Int B)"
  1.1499  apply (subgoal_tac "M({A,B})")
  1.1500 -apply (frule Inter_closed, force+) 
  1.1501 +apply (frule Inter_closed, force+)
  1.1502  done
  1.1503  
  1.1504  lemma (in M_basic) Diff_closed [intro,simp]:
  1.1505 @@ -1250,7 +1246,7 @@
  1.1506  lemma (in M_basic) separation_conj:
  1.1507       "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
  1.1508  by (simp del: separation_closed
  1.1509 -         add: separation_iff Collect_Int_Collect_eq [symmetric]) 
  1.1510 +         add: separation_iff Collect_Int_Collect_eq [symmetric])
  1.1511  
  1.1512  (*???equalities*)
  1.1513  lemma Collect_Un_Collect_eq:
  1.1514 @@ -1262,90 +1258,74 @@
  1.1515  by blast
  1.1516  
  1.1517  lemma (in M_trivial) Collect_rall_eq:
  1.1518 -     "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) = 
  1.1519 +     "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) =
  1.1520                 (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
  1.1521 -apply simp 
  1.1522 -apply (blast intro!: equalityI dest: transM) 
  1.1523 +apply simp
  1.1524 +apply (blast intro!: equalityI dest: transM)
  1.1525  done
  1.1526  
  1.1527  lemma (in M_basic) separation_disj:
  1.1528       "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
  1.1529  by (simp del: separation_closed
  1.1530 -         add: separation_iff Collect_Un_Collect_eq [symmetric]) 
  1.1531 +         add: separation_iff Collect_Un_Collect_eq [symmetric])
  1.1532  
  1.1533  lemma (in M_basic) separation_neg:
  1.1534       "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
  1.1535  by (simp del: separation_closed
  1.1536 -         add: separation_iff Diff_Collect_eq [symmetric]) 
  1.1537 +         add: separation_iff Diff_Collect_eq [symmetric])
  1.1538  
  1.1539  lemma (in M_basic) separation_imp:
  1.1540 -     "[|separation(M,P); separation(M,Q)|] 
  1.1541 +     "[|separation(M,P); separation(M,Q)|]
  1.1542        ==> separation(M, \<lambda>z. P(z) --> Q(z))"
  1.1543 -by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric]) 
  1.1544 +by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric])
  1.1545  
  1.1546 -text{*This result is a hint of how little can be done without the Reflection 
  1.1547 +text{*This result is a hint of how little can be done without the Reflection
  1.1548    Theorem.  The quantifier has to be bounded by a set.  We also need another
  1.1549    instance of Separation!*}
  1.1550  lemma (in M_basic) separation_rall:
  1.1551 -     "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y)); 
  1.1552 +     "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y));
  1.1553          \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
  1.1554 -      ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))" 
  1.1555 +      ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))"
  1.1556  apply (simp del: separation_closed rall_abs
  1.1557 -         add: separation_iff Collect_rall_eq) 
  1.1558 -apply (blast intro!: Inter_closed RepFun_closed dest: transM) 
  1.1559 +         add: separation_iff Collect_rall_eq)
  1.1560 +apply (blast intro!: Inter_closed RepFun_closed dest: transM)
  1.1561  done
  1.1562  
  1.1563  
  1.1564  subsubsection{*Functions and function space*}
  1.1565  
  1.1566 -text{*M contains all finite functions*}
  1.1567 -lemma (in M_basic) finite_fun_closed_lemma [rule_format]: 
  1.1568 -     "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
  1.1569 -apply (induct_tac n, simp)
  1.1570 -apply (rule ballI)  
  1.1571 -apply (simp add: succ_def) 
  1.1572 -apply (frule fun_cons_restrict_eq)
  1.1573 -apply (erule ssubst) 
  1.1574 -apply (subgoal_tac "M(f`x) & restrict(f,x) \<in> x -> A") 
  1.1575 - apply (simp add: cons_closed nat_into_M apply_closed) 
  1.1576 -apply (blast intro: apply_funtype transM restrict_type2) 
  1.1577 -done
  1.1578 -
  1.1579 -lemma (in M_basic) finite_fun_closed [rule_format]: 
  1.1580 -     "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
  1.1581 -by (blast intro: finite_fun_closed_lemma) 
  1.1582 -
  1.1583 -text{*The assumption @{term "M(A->B)"} is unusual, but essential: in 
  1.1584 +text{*The assumption @{term "M(A->B)"} is unusual, but essential: in
  1.1585  all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
  1.1586  lemma (in M_basic) is_funspace_abs [simp]:
  1.1587       "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
  1.1588  apply (simp add: is_funspace_def)
  1.1589  apply (rule iffI)
  1.1590 - prefer 2 apply blast 
  1.1591 + prefer 2 apply blast
  1.1592  apply (rule M_equalityI)
  1.1593    apply simp_all
  1.1594  done
  1.1595  
  1.1596  lemma (in M_basic) succ_fun_eq2:
  1.1597       "[|M(B); M(n->B)|] ==>
  1.1598 -      succ(n) -> B = 
  1.1599 +      succ(n) -> B =
  1.1600        \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
  1.1601  apply (simp add: succ_fun_eq)
  1.1602 -apply (blast dest: transM)  
  1.1603 +apply (blast dest: transM)
  1.1604  done
  1.1605  
  1.1606  lemma (in M_basic) funspace_succ:
  1.1607       "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
  1.1608 -apply (insert funspace_succ_replacement [of n], simp) 
  1.1609 -apply (force simp add: succ_fun_eq2 univalent_def) 
  1.1610 +apply (insert funspace_succ_replacement [of n], simp)
  1.1611 +apply (force simp add: succ_fun_eq2 univalent_def)
  1.1612  done
  1.1613  
  1.1614  text{*@{term M} contains all finite function spaces.  Needed to prove the
  1.1615 -absoluteness of transitive closure.*}
  1.1616 +absoluteness of transitive closure.  See the definition of
  1.1617 +@{text rtrancl_alt} in in @{text WF_absolute.thy}.*}
  1.1618  lemma (in M_basic) finite_funspace_closed [intro,simp]:
  1.1619       "[|n\<in>nat; M(B)|] ==> M(n->B)"
  1.1620  apply (induct_tac n, simp)
  1.1621 -apply (simp add: funspace_succ nat_into_M) 
  1.1622 +apply (simp add: funspace_succ nat_into_M)
  1.1623  done
  1.1624  
  1.1625  
  1.1626 @@ -1356,50 +1336,50 @@
  1.1627     "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
  1.1628  
  1.1629    is_not :: "[i=>o, i, i] => o"
  1.1630 -   "is_not(M,a,z) == (number1(M,a)  & empty(M,z)) | 
  1.1631 +   "is_not(M,a,z) == (number1(M,a)  & empty(M,z)) |
  1.1632                       (~number1(M,a) & number1(M,z))"
  1.1633  
  1.1634    is_and :: "[i=>o, i, i, i] => o"
  1.1635 -   "is_and(M,a,b,z) == (number1(M,a)  & z=b) | 
  1.1636 +   "is_and(M,a,b,z) == (number1(M,a)  & z=b) |
  1.1637                         (~number1(M,a) & empty(M,z))"
  1.1638  
  1.1639    is_or :: "[i=>o, i, i, i] => o"
  1.1640 -   "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) | 
  1.1641 +   "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) |
  1.1642                        (~number1(M,a) & z=b)"
  1.1643  
  1.1644 -lemma (in M_trivial) bool_of_o_abs [simp]: 
  1.1645 -     "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)" 
  1.1646 -by (simp add: is_bool_of_o_def bool_of_o_def) 
  1.1647 +lemma (in M_trivial) bool_of_o_abs [simp]:
  1.1648 +     "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)"
  1.1649 +by (simp add: is_bool_of_o_def bool_of_o_def)
  1.1650  
  1.1651  
  1.1652 -lemma (in M_trivial) not_abs [simp]: 
  1.1653 +lemma (in M_trivial) not_abs [simp]:
  1.1654       "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)"
  1.1655 -by (simp add: Bool.not_def cond_def is_not_def) 
  1.1656 +by (simp add: Bool.not_def cond_def is_not_def)
  1.1657  
  1.1658 -lemma (in M_trivial) and_abs [simp]: 
  1.1659 +lemma (in M_trivial) and_abs [simp]:
  1.1660       "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b"
  1.1661 -by (simp add: Bool.and_def cond_def is_and_def) 
  1.1662 +by (simp add: Bool.and_def cond_def is_and_def)
  1.1663  
  1.1664 -lemma (in M_trivial) or_abs [simp]: 
  1.1665 +lemma (in M_trivial) or_abs [simp]:
  1.1666       "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b"
  1.1667  by (simp add: Bool.or_def cond_def is_or_def)
  1.1668  
  1.1669  
  1.1670  lemma (in M_trivial) bool_of_o_closed [intro,simp]:
  1.1671       "M(bool_of_o(P))"
  1.1672 -by (simp add: bool_of_o_def) 
  1.1673 +by (simp add: bool_of_o_def)
  1.1674  
  1.1675  lemma (in M_trivial) and_closed [intro,simp]:
  1.1676       "[| M(p); M(q) |] ==> M(p and q)"
  1.1677 -by (simp add: and_def cond_def) 
  1.1678 +by (simp add: and_def cond_def)
  1.1679  
  1.1680  lemma (in M_trivial) or_closed [intro,simp]:
  1.1681       "[| M(p); M(q) |] ==> M(p or q)"
  1.1682 -by (simp add: or_def cond_def) 
  1.1683 +by (simp add: or_def cond_def)
  1.1684  
  1.1685  lemma (in M_trivial) not_closed [intro,simp]:
  1.1686       "M(p) ==> M(not(p))"
  1.1687 -by (simp add: Bool.not_def cond_def) 
  1.1688 +by (simp add: Bool.not_def cond_def)
  1.1689  
  1.1690  
  1.1691  subsection{*Relativization and Absoluteness for List Operators*}
  1.1692 @@ -1422,7 +1402,7 @@
  1.1693  by (simp add: is_Nil_def Nil_def)
  1.1694  
  1.1695  lemma (in M_trivial) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
  1.1696 -by (simp add: Cons_def) 
  1.1697 +by (simp add: Cons_def)
  1.1698  
  1.1699  lemma (in M_trivial) Cons_abs [simp]:
  1.1700       "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
  1.1701 @@ -1439,35 +1419,35 @@
  1.1702  
  1.1703    list_case' :: "[i, [i,i]=>i, i] => i"
  1.1704      --{*A version of @{term list_case} that's always defined.*}
  1.1705 -    "list_case'(a,b,xs) == 
  1.1706 -       if quasilist(xs) then list_case(a,b,xs) else 0"  
  1.1707 +    "list_case'(a,b,xs) ==
  1.1708 +       if quasilist(xs) then list_case(a,b,xs) else 0"
  1.1709  
  1.1710    is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
  1.1711      --{*Returns 0 for non-lists*}
  1.1712 -    "is_list_case(M, a, is_b, xs, z) == 
  1.1713 +    "is_list_case(M, a, is_b, xs, z) ==
  1.1714         (is_Nil(M,xs) --> z=a) &
  1.1715         (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
  1.1716         (is_quasilist(M,xs) | empty(M,z))"
  1.1717  
  1.1718    hd' :: "i => i"
  1.1719      --{*A version of @{term hd} that's always defined.*}
  1.1720 -    "hd'(xs) == if quasilist(xs) then hd(xs) else 0"  
  1.1721 +    "hd'(xs) == if quasilist(xs) then hd(xs) else 0"
  1.1722  
  1.1723    tl' :: "i => i"
  1.1724      --{*A version of @{term tl} that's always defined.*}
  1.1725 -    "tl'(xs) == if quasilist(xs) then tl(xs) else 0"  
  1.1726 +    "tl'(xs) == if quasilist(xs) then tl(xs) else 0"
  1.1727  
  1.1728    is_hd :: "[i=>o,i,i] => o"
  1.1729       --{* @{term "hd([]) = 0"} no constraints if not a list.
  1.1730            Avoiding implication prevents the simplifier's looping.*}
  1.1731 -    "is_hd(M,xs,H) == 
  1.1732 +    "is_hd(M,xs,H) ==
  1.1733         (is_Nil(M,xs) --> empty(M,H)) &
  1.1734         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
  1.1735         (is_quasilist(M,xs) | empty(M,H))"
  1.1736  
  1.1737    is_tl :: "[i=>o,i,i] => o"
  1.1738       --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
  1.1739 -    "is_tl(M,xs,T) == 
  1.1740 +    "is_tl(M,xs,T) ==
  1.1741         (is_Nil(M,xs) --> T=xs) &
  1.1742         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
  1.1743         (is_quasilist(M,xs) | empty(M,T))"
  1.1744 @@ -1491,8 +1471,8 @@
  1.1745  lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)"
  1.1746  by (simp add: list_case'_def quasilist_def)
  1.1747  
  1.1748 -lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0" 
  1.1749 -by (simp add: quasilist_def list_case'_def) 
  1.1750 +lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0"
  1.1751 +by (simp add: quasilist_def list_case'_def)
  1.1752  
  1.1753  lemma list_case'_eq_list_case [simp]:
  1.1754       "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
  1.1755 @@ -1500,25 +1480,25 @@
  1.1756  
  1.1757  lemma (in M_basic) list_case'_closed [intro,simp]:
  1.1758    "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
  1.1759 -apply (case_tac "quasilist(k)") 
  1.1760 - apply (simp add: quasilist_def, force) 
  1.1761 -apply (simp add: non_list_case) 
  1.1762 +apply (case_tac "quasilist(k)")
  1.1763 + apply (simp add: quasilist_def, force)
  1.1764 +apply (simp add: non_list_case)
  1.1765  done
  1.1766  
  1.1767 -lemma (in M_trivial) quasilist_abs [simp]: 
  1.1768 +lemma (in M_trivial) quasilist_abs [simp]:
  1.1769       "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
  1.1770  by (auto simp add: is_quasilist_def quasilist_def)
  1.1771  
  1.1772 -lemma (in M_trivial) list_case_abs [simp]: 
  1.1773 -     "[| relativize2(M,is_b,b); M(k); M(z) |] 
  1.1774 +lemma (in M_trivial) list_case_abs [simp]:
  1.1775 +     "[| relativize2(M,is_b,b); M(k); M(z) |]
  1.1776        ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
  1.1777 -apply (case_tac "quasilist(k)") 
  1.1778 - prefer 2 
  1.1779 - apply (simp add: is_list_case_def non_list_case) 
  1.1780 - apply (force simp add: quasilist_def) 
  1.1781 +apply (case_tac "quasilist(k)")
  1.1782 + prefer 2
  1.1783 + apply (simp add: is_list_case_def non_list_case)
  1.1784 + apply (force simp add: quasilist_def)
  1.1785  apply (simp add: quasilist_def is_list_case_def)
  1.1786 -apply (elim disjE exE) 
  1.1787 - apply (simp_all add: relativize2_def) 
  1.1788 +apply (elim disjE exE)
  1.1789 + apply (simp_all add: relativize2_def)
  1.1790  done
  1.1791  
  1.1792  
  1.1793 @@ -1529,34 +1509,34 @@
  1.1794  
  1.1795  lemma (in M_trivial) is_hd_Cons:
  1.1796       "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
  1.1797 -by (force simp add: is_hd_def) 
  1.1798 +by (force simp add: is_hd_def)
  1.1799  
  1.1800  lemma (in M_trivial) hd_abs [simp]:
  1.1801       "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
  1.1802  apply (simp add: hd'_def)
  1.1803  apply (intro impI conjI)
  1.1804 - prefer 2 apply (force simp add: is_hd_def) 
  1.1805 + prefer 2 apply (force simp add: is_hd_def)
  1.1806  apply (simp add: quasilist_def is_hd_def)
  1.1807  apply (elim disjE exE, auto)
  1.1808 -done 
  1.1809 +done
  1.1810  
  1.1811  lemma (in M_trivial) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
  1.1812  by (simp add: is_tl_def)
  1.1813  
  1.1814  lemma (in M_trivial) is_tl_Cons:
  1.1815       "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
  1.1816 -by (force simp add: is_tl_def) 
  1.1817 +by (force simp add: is_tl_def)
  1.1818  
  1.1819  lemma (in M_trivial) tl_abs [simp]:
  1.1820       "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
  1.1821  apply (simp add: tl'_def)
  1.1822  apply (intro impI conjI)
  1.1823 - prefer 2 apply (force simp add: is_tl_def) 
  1.1824 + prefer 2 apply (force simp add: is_tl_def)
  1.1825  apply (simp add: quasilist_def is_tl_def)
  1.1826  apply (elim disjE exE, auto)
  1.1827 -done 
  1.1828 +done
  1.1829  
  1.1830 -lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')"  
  1.1831 +lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')"
  1.1832  by (simp add: relativize1_def)
  1.1833  
  1.1834  lemma hd'_Nil: "hd'([]) = 0"
  1.1835 @@ -1572,8 +1552,8 @@
  1.1836  by (simp add: tl'_def)
  1.1837  
  1.1838  lemma iterates_tl_Nil: "n \<in> nat ==> tl'^n ([]) = []"
  1.1839 -apply (induct_tac n) 
  1.1840 -apply (simp_all add: tl'_Nil) 
  1.1841 +apply (induct_tac n)
  1.1842 +apply (simp_all add: tl'_Nil)
  1.1843  done
  1.1844  
  1.1845  lemma (in M_basic) tl'_closed: "M(x) ==> M(tl'(x))"