src/ZF/Constructible/Relative.thy
changeset 13254 5146ccaedf42
parent 13251 74cb2af8811e
child 13268 240509babf00
     1.1 --- a/src/ZF/Constructible/Relative.thy	Fri Jun 28 11:24:36 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Jun 28 11:25:46 2002 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  constdefs
     1.6    empty :: "[i=>o,i] => o"
     1.7 -    "empty(M,z) == \<forall>x. M(x) --> x \<notin> z"
     1.8 +    "empty(M,z) == \<forall>x[M]. x \<notin> z"
     1.9  
    1.10    subset :: "[i=>o,i,i] => o"
    1.11      "subset(M,A,B) == \<forall>x\<in>A. M(x) --> x \<in> B"
    1.12 @@ -15,42 +15,42 @@
    1.13      "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x\<in>z. M(x) --> x = a | x = b)"
    1.14  
    1.15    pair :: "[i=>o,i,i,i] => o"
    1.16 -    "pair(M,a,b,z) == \<exists>x. M(x) & upair(M,a,a,x) & 
    1.17 -                          (\<exists>y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))"
    1.18 +    "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & 
    1.19 +                          (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
    1.20  
    1.21    union :: "[i=>o,i,i,i] => o"
    1.22 -    "union(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a | x \<in> b)"
    1.23 +    "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"
    1.24  
    1.25    successor :: "[i=>o,i,i] => o"
    1.26 -    "successor(M,a,z) == \<exists>x. M(x) & upair(M,a,a,x) & union(M,x,a,z)"
    1.27 +    "successor(M,a,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,a,z)"
    1.28  
    1.29    powerset :: "[i=>o,i,i] => o"
    1.30 -    "powerset(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> subset(M,x,A))"
    1.31 +    "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
    1.32  
    1.33    inter :: "[i=>o,i,i,i] => o"
    1.34 -    "inter(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<in> b)"
    1.35 +    "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
    1.36  
    1.37    setdiff :: "[i=>o,i,i,i] => o"
    1.38 -    "setdiff(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<notin> b)"
    1.39 +    "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
    1.40  
    1.41    big_union :: "[i=>o,i,i] => o"
    1.42 -    "big_union(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y))"
    1.43 +    "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y)"
    1.44  
    1.45    big_inter :: "[i=>o,i,i] => o"
    1.46      "big_inter(M,A,z) == 
    1.47               (A=0 --> z=0) &
    1.48 -	     (A\<noteq>0 --> (\<forall>x. M(x) --> (x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y))))"
    1.49 +	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y)))"
    1.50  
    1.51    cartprod :: "[i=>o,i,i,i] => o"
    1.52      "cartprod(M,A,B,z) == 
    1.53 -	\<forall>u. M(u) --> (u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u))))"
    1.54 +	\<forall>u[M]. u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u)))"
    1.55  
    1.56    is_converse :: "[i=>o,i,i] => o"
    1.57      "is_converse(M,r,z) == 
    1.58  	\<forall>x. M(x) --> 
    1.59              (x \<in> z <-> 
    1.60               (\<exists>w\<in>r. M(w) & 
    1.61 -              (\<exists>u v. M(u) & M(v) & pair(M,u,v,w) & pair(M,v,u,x))))"
    1.62 +              (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x))))"
    1.63  
    1.64    pre_image :: "[i=>o,i,i,i] => o"
    1.65      "pre_image(M,r,A,z) == 
    1.66 @@ -224,17 +224,17 @@
    1.67  by (blast intro: univ0_downwards_mem) 
    1.68  
    1.69  text{*Congruence rule for separation: can assume the variable is in @{text M}*}
    1.70 -lemma [cong]:
    1.71 +lemma separation_cong [cong]:
    1.72       "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"
    1.73  by (simp add: separation_def) 
    1.74  
    1.75  text{*Congruence rules for replacement*}
    1.76 -lemma [cong]:
    1.77 +lemma univalent_cong [cong]:
    1.78       "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
    1.79        ==> univalent(M,A,P) <-> univalent(M,A',P')"
    1.80  by (simp add: univalent_def) 
    1.81  
    1.82 -lemma [cong]:
    1.83 +lemma strong_replacement_cong [cong]:
    1.84       "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
    1.85        ==> strong_replacement(M,P) <-> strong_replacement(M,P')" 
    1.86  by (simp add: strong_replacement_def) 
    1.87 @@ -398,8 +398,8 @@
    1.88       "[| M(A); M(r) |] 
    1.89        ==> separation(M, \<lambda>x. \<exists>p\<in>r. M(p) & (\<exists>y\<in>A. M(x) & pair(M,x,y,p)))"
    1.90    and converse_separation:
    1.91 -     "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. M(p) & (\<exists>x y. M(x) & M(y) & 
    1.92 -				     pair(M,x,y,p) & pair(M,y,x,z)))"
    1.93 +     "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. 
    1.94 +                    M(p) & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
    1.95    and restrict_separation:
    1.96       "M(A) 
    1.97        ==> separation(M, \<lambda>z. \<exists>x\<in>A. M(x) & (\<exists>y. M(y) & pair(M,x,y,z)))"
    1.98 @@ -507,7 +507,7 @@
    1.99       "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   1.100  apply (simp add: cartprod_def)
   1.101  apply (rule iffI) 
   1.102 -apply (blast intro!: equalityI intro: transM dest!: spec) 
   1.103 + apply (blast intro!: equalityI intro: transM dest!: rspec) 
   1.104  apply (blast dest: transM) 
   1.105  done
   1.106  
   1.107 @@ -616,15 +616,6 @@
   1.108        ==> M(\<lambda>x\<in>A. b(x))"
   1.109  by (simp add: lam_def, blast dest: transM) 
   1.110  
   1.111 -lemma (in M_axioms) converse_abs [simp]: 
   1.112 -     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   1.113 -apply (simp add: is_converse_def)
   1.114 -apply (rule iffI)
   1.115 - apply (rule equalityI) 
   1.116 -  apply (blast dest: transM) 
   1.117 - apply (clarify, frule transM, assumption, simp, blast) 
   1.118 -done
   1.119 -
   1.120  lemma (in M_axioms) image_abs [simp]: 
   1.121       "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   1.122  apply (simp add: image_def)
   1.123 @@ -648,11 +639,14 @@
   1.124  done
   1.125  
   1.126  lemma (in M_axioms) cartprod_iff_lemma:
   1.127 -     "[| M(C); \<forall>u. M(u) --> u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   1.128 -       powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
   1.129 +     "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   1.130 +         powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   1.131         ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   1.132  apply (simp add: powerset_def) 
   1.133 -apply (rule equalityI, clarify, simp) 
   1.134 +apply (rule equalityI, clarify, simp)
   1.135 +
   1.136 + apply (frule transM, assumption) 
   1.137 +
   1.138   apply (frule transM, assumption, simp) 
   1.139   apply blast 
   1.140  apply clarify
   1.141 @@ -751,8 +745,7 @@
   1.142  lemma (in M_axioms) M_converse_iff:
   1.143       "M(r) ==> 
   1.144        converse(r) = 
   1.145 -      {z \<in> range(r) * domain(r). 
   1.146 -        \<exists>p\<in>r. \<exists>x. M(x) & (\<exists>y. M(y) & p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>)}"
   1.147 +      {z \<in> range(r) * domain(r). \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
   1.148  by (blast dest: transM)
   1.149  
   1.150  lemma (in M_axioms) converse_closed [intro,simp]: 
   1.151 @@ -761,6 +754,16 @@
   1.152  apply (insert converse_separation [of r], simp)
   1.153  done
   1.154  
   1.155 +lemma (in M_axioms) converse_abs [simp]: 
   1.156 +     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   1.157 +apply (simp add: is_converse_def)
   1.158 +apply (rule iffI)
   1.159 + prefer 2 apply (blast intro: elim:); 
   1.160 +apply (rule M_equalityI)
   1.161 +  apply (simp add: )
   1.162 +  apply (blast dest: transM)+
   1.163 +done
   1.164 +
   1.165  lemma (in M_axioms) relation_abs [simp]: 
   1.166       "M(r) ==> is_relation(M,r) <-> relation(r)"
   1.167  apply (simp add: is_relation_def relation_def)