src/ZF/Constructible/Relative.thy
changeset 13299 3a932abf97e8
parent 13298 b4f370679c65
child 13306 6eebcddee32b
     1.1 --- a/src/ZF/Constructible/Relative.thy	Thu Jul 04 16:59:54 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Thu Jul 04 18:29:50 2002 +0200
     1.3 @@ -47,29 +47,28 @@
     1.4  
     1.5    is_converse :: "[i=>o,i,i] => o"
     1.6      "is_converse(M,r,z) == 
     1.7 -	\<forall>x. M(x) --> 
     1.8 -            (x \<in> z <-> 
     1.9 -             (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x))))"
    1.10 +	\<forall>x[M]. x \<in> z <-> 
    1.11 +             (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
    1.12  
    1.13    pre_image :: "[i=>o,i,i,i] => o"
    1.14      "pre_image(M,r,A,z) == 
    1.15 -	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w))))"
    1.16 +	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
    1.17  
    1.18    is_domain :: "[i=>o,i,i] => o"
    1.19      "is_domain(M,r,z) == 
    1.20 -	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))"
    1.21 +	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))"
    1.22  
    1.23    image :: "[i=>o,i,i,i] => o"
    1.24      "image(M,r,A,z) == 
    1.25 -        \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))"
    1.26 +        \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))"
    1.27  
    1.28    is_range :: "[i=>o,i,i] => o"
    1.29      --{*the cleaner 
    1.30 -      @{term "\<exists>r'. M(r') & is_converse(M,r,r') & is_domain(M,r',z)"}
    1.31 +      @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
    1.32        unfortunately needs an instance of separation in order to prove 
    1.33          @{term "M(converse(r))"}.*}
    1.34      "is_range(M,r,z) == 
    1.35 -	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))"
    1.36 +	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))"
    1.37  
    1.38    is_field :: "[i=>o,i,i] => o"
    1.39      "is_field(M,r,z) == 
    1.40 @@ -82,18 +81,17 @@
    1.41  
    1.42    is_function :: "[i=>o,i] => o"
    1.43      "is_function(M,r) == 
    1.44 -	(\<forall>x y y' p p'. M(x) --> M(y) --> M(y') --> M(p) --> M(p') --> 
    1.45 -                      pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> 
    1.46 -                      y=y')"
    1.47 +	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 
    1.48 +           pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
    1.49  
    1.50    fun_apply :: "[i=>o,i,i,i] => o"
    1.51      "fun_apply(M,f,x,y) == 
    1.52 -	(\<forall>y'. M(y') --> ((\<exists>u\<in>f. M(u) & pair(M,x,y',u)) <-> y=y'))"
    1.53 +	(\<forall>y'[M]. (\<exists>u[M]. u\<in>f & pair(M,x,y',u)) <-> y=y')"
    1.54  
    1.55    typed_function :: "[i=>o,i,i,i] => o"
    1.56      "typed_function(M,A,B,r) == 
    1.57          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
    1.58 -        (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
    1.59 +        (\<forall>u[M]. u\<in>r --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
    1.60  
    1.61    is_funspace :: "[i=>o,i,i,i] => o"
    1.62      "is_funspace(M,A,B,F) == 
    1.63 @@ -101,8 +99,8 @@
    1.64  
    1.65    composition :: "[i=>o,i,i,i] => o"
    1.66      "composition(M,r,s,t) == 
    1.67 -        \<forall>p. M(p) --> (p \<in> t <-> 
    1.68 -                      (\<exists>x. M(x) & (\<exists>y. M(y) & (\<exists>z. M(z) & 
    1.69 +        \<forall>p[M]. (p \<in> t <-> 
    1.70 +                      (\<exists>x[M]. (\<exists>y[M]. (\<exists>z[M]. 
    1.71                             p = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))))"
    1.72  
    1.73  
    1.74 @@ -116,29 +114,29 @@
    1.75    surjection :: "[i=>o,i,i,i] => o"
    1.76      "surjection(M,A,B,f) == 
    1.77          typed_function(M,A,B,f) &
    1.78 -        (\<forall>y\<in>B. M(y) --> (\<exists>x\<in>A. M(x) & fun_apply(M,f,x,y)))"
    1.79 +        (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
    1.80  
    1.81    bijection :: "[i=>o,i,i,i] => o"
    1.82      "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
    1.83  
    1.84    restriction :: "[i=>o,i,i,i] => o"
    1.85      "restriction(M,r,A,z) == 
    1.86 -	\<forall>x. M(x) --> 
    1.87 +	\<forall>x[M]. 
    1.88              (x \<in> z <-> 
    1.89 -             (x \<in> r & (\<exists>u\<in>A. M(u) & (\<exists>v. M(v) & pair(M,u,v,x)))))"
    1.90 +             (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x)))))"
    1.91  
    1.92    transitive_set :: "[i=>o,i] => o"
    1.93 -    "transitive_set(M,a) == \<forall>x\<in>a. M(x) --> subset(M,x,a)"
    1.94 +    "transitive_set(M,a) == \<forall>x[M]. x\<in>a --> subset(M,x,a)"
    1.95  
    1.96    ordinal :: "[i=>o,i] => o"
    1.97       --{*an ordinal is a transitive set of transitive sets*}
    1.98 -    "ordinal(M,a) == transitive_set(M,a) & (\<forall>x\<in>a. M(x) --> transitive_set(M,x))"
    1.99 +    "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a --> transitive_set(M,x))"
   1.100  
   1.101    limit_ordinal :: "[i=>o,i] => o"
   1.102      --{*a limit ordinal is a non-empty, successor-closed ordinal*}
   1.103      "limit_ordinal(M,a) == 
   1.104  	ordinal(M,a) & ~ empty(M,a) & 
   1.105 -        (\<forall>x\<in>a. M(x) --> (\<exists>y\<in>a. M(y) & successor(M,x,y)))"
   1.106 +        (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
   1.107  
   1.108    successor_ordinal :: "[i=>o,i] => o"
   1.109      --{*a successor ordinal is any ordinal that is neither empty nor limit*}
   1.110 @@ -149,20 +147,20 @@
   1.111      --{*an ordinal is finite if neither it nor any of its elements are limit*}
   1.112      "finite_ordinal(M,a) == 
   1.113  	ordinal(M,a) & ~ limit_ordinal(M,a) & 
   1.114 -        (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
   1.115 +        (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   1.116  
   1.117    omega :: "[i=>o,i] => o"
   1.118      --{*omega is a limit ordinal none of whose elements are limit*}
   1.119 -    "omega(M,a) == limit_ordinal(M,a) & (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
   1.120 +    "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
   1.121  
   1.122    number1 :: "[i=>o,i] => o"
   1.123 -    "number1(M,a) == (\<exists>x. M(x) & empty(M,x) & successor(M,x,a))"
   1.124 +    "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
   1.125  
   1.126    number2 :: "[i=>o,i] => o"
   1.127 -    "number2(M,a) == (\<exists>x. M(x) & number1(M,x) & successor(M,x,a))"
   1.128 +    "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
   1.129  
   1.130    number3 :: "[i=>o,i] => o"
   1.131 -    "number3(M,a) == (\<exists>x. M(x) & number2(M,x) & successor(M,x,a))"
   1.132 +    "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
   1.133  
   1.134  
   1.135  subsection {*The relativized ZF axioms*}
   1.136 @@ -179,32 +177,32 @@
   1.137  	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
   1.138  
   1.139    upair_ax :: "(i=>o) => o"
   1.140 -    "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z. M(z) & upair(M,x,y,z))"
   1.141 +    "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z[M]. upair(M,x,y,z))"
   1.142  
   1.143    Union_ax :: "(i=>o) => o"
   1.144 -    "Union_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & big_union(M,x,z))"
   1.145 +    "Union_ax(M) == \<forall>x[M]. (\<exists>z[M]. big_union(M,x,z))"
   1.146  
   1.147    power_ax :: "(i=>o) => o"
   1.148 -    "power_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & powerset(M,x,z))"
   1.149 +    "power_ax(M) == \<forall>x[M]. (\<exists>z[M]. powerset(M,x,z))"
   1.150  
   1.151    univalent :: "[i=>o, i, [i,i]=>o] => o"
   1.152      "univalent(M,A,P) == 
   1.153 -	(\<forall>x\<in>A. M(x) --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"
   1.154 +	(\<forall>x[M]. x\<in>A --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"
   1.155  
   1.156    replacement :: "[i=>o, [i,i]=>o] => o"
   1.157      "replacement(M,P) == 
   1.158 -      \<forall>A. M(A) --> univalent(M,A,P) -->
   1.159 -      (\<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y)))"
   1.160 +      \<forall>A[M]. univalent(M,A,P) -->
   1.161 +      (\<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)))"
   1.162  
   1.163    strong_replacement :: "[i=>o, [i,i]=>o] => o"
   1.164      "strong_replacement(M,P) == 
   1.165 -      \<forall>A. M(A) --> univalent(M,A,P) -->
   1.166 -      (\<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b)))))"
   1.167 +      \<forall>A[M]. univalent(M,A,P) -->
   1.168 +      (\<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))))"
   1.169  
   1.170    foundation_ax :: "(i=>o) => o"
   1.171      "foundation_ax(M) == 
   1.172 -	\<forall>x. M(x) --> (\<exists>y\<in>x. M(y))
   1.173 -                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & z \<in> y))"
   1.174 +	\<forall>x[M]. (\<exists>y\<in>x. M(y))
   1.175 +                 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
   1.176  
   1.177  
   1.178  subsection{*A trivial consistency proof for $V_\omega$ *}
   1.179 @@ -281,8 +279,10 @@
   1.180  
   1.181  text{*Union axiom*}
   1.182  lemma "Union_ax(\<lambda>x. x \<in> univ(0))"  
   1.183 -apply (simp add: Union_ax_def big_union_def)  
   1.184 -apply (blast intro: Union_in_univ Transset_0 univ0_downwards_mem) 
   1.185 +apply (simp add: Union_ax_def big_union_def, clarify) 
   1.186 +apply (rule_tac x="\<Union>x" in bexI)  
   1.187 + apply (blast intro: univ0_downwards_mem)
   1.188 +apply (blast intro: Union_in_univ Transset_0) 
   1.189  done
   1.190  
   1.191  text{*Powerset axiom*}
   1.192 @@ -293,14 +293,17 @@
   1.193  done
   1.194  
   1.195  lemma "power_ax(\<lambda>x. x \<in> univ(0))"  
   1.196 -apply (simp add: power_ax_def powerset_def subset_def)  
   1.197 -apply (blast intro: Pow_in_univ Transset_0 univ0_downwards_mem) 
   1.198 +apply (simp add: power_ax_def powerset_def subset_def, clarify) 
   1.199 +apply (rule_tac x="Pow(x)" in bexI)
   1.200 + apply (blast intro: univ0_downwards_mem)
   1.201 +apply (blast intro: Pow_in_univ Transset_0) 
   1.202  done
   1.203  
   1.204  text{*Foundation axiom*}
   1.205  lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"  
   1.206  apply (simp add: foundation_ax_def, clarify)
   1.207 -apply (cut_tac A=x in foundation, blast) 
   1.208 +apply (cut_tac A=x in foundation) 
   1.209 +apply (blast intro: univ0_downwards_mem)
   1.210  done
   1.211  
   1.212  lemma "replacement(\<lambda>x. x \<in> univ(0), P)"  
   1.213 @@ -341,12 +344,12 @@
   1.214  
   1.215  lemma replacementD:
   1.216      "[| replacement(M,P); M(A);  univalent(M,A,P) |]
   1.217 -     ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y))"
   1.218 +     ==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y))"
   1.219  by (simp add: replacement_def) 
   1.220  
   1.221  lemma strong_replacementD:
   1.222      "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
   1.223 -     ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b))))"
   1.224 +     ==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b))))"
   1.225  by (simp add: strong_replacement_def) 
   1.226  
   1.227  lemma separationD:
   1.228 @@ -368,12 +371,11 @@
   1.229  
   1.230    pred_set :: "[i=>o,i,i,i,i] => o"
   1.231      "pred_set(M,A,x,r,B) == 
   1.232 -	\<forall>y. M(y) --> (y \<in> B <-> (\<exists>p\<in>r. M(p) & y \<in> A & pair(M,y,x,p)))"
   1.233 +	\<forall>y[M]. y \<in> B <-> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
   1.234  
   1.235    membership :: "[i=>o,i,i] => o" --{*membership relation*}
   1.236      "membership(M,A,r) == 
   1.237 -	\<forall>p. M(p) --> 
   1.238 -             (p \<in> r <-> (\<exists>x\<in>A. \<exists>y\<in>A. M(x) & M(y) & x\<in>y & pair(M,x,y,p)))"
   1.239 +	\<forall>p[M]. p \<in> r <-> (\<exists>x\<in>A. \<exists>y\<in>A. M(x) & M(y) & x\<in>y & pair(M,x,y,p))"
   1.240  
   1.241  
   1.242  subsection{*Absoluteness for a transitive class model*}
   1.243 @@ -407,7 +409,7 @@
   1.244  by (blast intro: transM) 
   1.245  
   1.246  lemma (in M_triv_axioms) ball_iff_equiv: 
   1.247 -     "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <-> 
   1.248 +     "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <-> 
   1.249                 (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   1.250  by (blast intro: transM)
   1.251  
   1.252 @@ -525,13 +527,14 @@
   1.253  
   1.254  text{*Probably the premise and conclusion are equivalent*}
   1.255  lemma (in M_triv_axioms) strong_replacementI [rule_format]:
   1.256 -    "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
   1.257 +    "[| \<forall>A[M]. separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
   1.258       ==> strong_replacement(M,P)"
   1.259  apply (simp add: strong_replacement_def, clarify) 
   1.260  apply (frule replacementD [OF replacement], assumption, clarify) 
   1.261 -apply (drule_tac x=A in spec, clarify)  
   1.262 +apply (drule_tac x=A in rspec, clarify)  
   1.263  apply (drule_tac z=Y in separationD, assumption, clarify) 
   1.264 -apply (blast dest: transM) 
   1.265 +apply (rule_tac x=y in rexI) 
   1.266 +apply (blast dest: transM)+
   1.267  done
   1.268  
   1.269  
   1.270 @@ -540,7 +543,7 @@
   1.271       "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   1.272         !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   1.273  apply (simp add: strong_replacement_def) 
   1.274 -apply (drule spec [THEN mp], auto) 
   1.275 +apply (drule rspec, auto) 
   1.276  apply (subgoal_tac "Replace(A,P) = Y")
   1.277   apply simp 
   1.278  apply (rule equality_iffI) 
   1.279 @@ -548,7 +551,7 @@
   1.280   apply (blast dest: transM) 
   1.281  apply (frule transM, assumption) 
   1.282   apply (simp add: univalent_def)
   1.283 - apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)
   1.284 + apply (drule rspec [THEN iffD1], assumption, assumption)
   1.285   apply (blast dest: transM) 
   1.286  done
   1.287  
   1.288 @@ -636,7 +639,7 @@
   1.289  done
   1.290  
   1.291  lemma (in M_triv_axioms) successor_ordinal_abs [simp]: 
   1.292 -     "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b. M(b) & a = succ(b))"
   1.293 +     "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
   1.294  apply (simp add: successor_ordinal_def, safe)
   1.295  apply (drule Ord_cases_disj, auto) 
   1.296  done
   1.297 @@ -694,7 +697,7 @@
   1.298    primrec
   1.299        "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   1.300        "natnumber_aux(M,succ(n)) = 
   1.301 -	   (\<lambda>x\<in>nat. if (\<exists>y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   1.302 +	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   1.303  		     then 1 else 0)"
   1.304  
   1.305    constdefs
   1.306 @@ -742,12 +745,12 @@
   1.307                  pair(M,f,b,p) & pair(M,n,b,nb) & z = {cons(nb,f)})"
   1.308    and well_ord_iso_separation:
   1.309       "[| M(A); M(f); M(r) |] 
   1.310 -      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) & (\<exists>p. M(p) & 
   1.311 +      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M]. 
   1.312  		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
   1.313    and obase_equals_separation:
   1.314       "[| M(A); M(r) |] 
   1.315        ==> separation
   1.316 -      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. M(y) & (\<exists>g. M(g) &
   1.317 +      (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. (\<exists>g. M(g) &
   1.318  	      ordinal(M,y) & (\<exists>my pxr. M(my) & M(pxr) &
   1.319  	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   1.320  	      order_isomorphism(M,pxr,r,y,my,g)))))"
   1.321 @@ -786,24 +789,25 @@
   1.322   apply blast 
   1.323  txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   1.324  apply (insert power_ax, simp add: power_ax_def) 
   1.325 -apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   1.326 -apply (erule impE, blast, clarify) 
   1.327 -apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   1.328 +apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   1.329 +apply (blast, clarify) 
   1.330 +apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
   1.331 +apply assumption
   1.332  apply (blast intro: cartprod_iff_lemma) 
   1.333  done
   1.334  
   1.335  lemma (in M_axioms) cartprod_closed_lemma:
   1.336 -     "[| M(A); M(B) |] ==> \<exists>C. M(C) & cartprod(M,A,B,C)"
   1.337 +     "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
   1.338  apply (simp del: cartprod_abs add: cartprod_iff)
   1.339  apply (insert power_ax, simp add: power_ax_def) 
   1.340 -apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   1.341 -apply (erule impE, blast, clarify) 
   1.342 -apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   1.343 -apply (erule impE, blast, clarify)
   1.344 -apply (intro exI conjI) 
   1.345 -prefer 6 apply (rule refl) 
   1.346 -prefer 4 apply assumption
   1.347 -prefer 4 apply assumption
   1.348 +apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   1.349 +apply (blast, clarify) 
   1.350 +apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec) 
   1.351 +apply (blast, clarify)
   1.352 +apply (intro rexI exI conjI) 
   1.353 +prefer 5 apply (rule refl) 
   1.354 +prefer 3 apply assumption
   1.355 +prefer 3 apply assumption
   1.356  apply (insert cartprod_separation [of A B], auto)
   1.357  done
   1.358