tweaks involving Separation
authorpaulson
Wed Jul 31 14:39:47 2002 +0200 (2002-07-31)
changeset 134368fd1d803a3d3
parent 13435 05631e8f0258
child 13437 01b3fc0cc1b8
tweaks involving Separation
src/ZF/Constructible/Relative.thy
     1.1 --- a/src/ZF/Constructible/Relative.thy	Wed Jul 31 14:34:08 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Jul 31 14:39:47 2002 +0200
     1.3 @@ -2,10 +2,6 @@
     1.4  
     1.5  theory Relative = Main:
     1.6  
     1.7 -(*????????????????for IFOL.thy????????????????*)
     1.8 -lemma eq_commute: "a=b <-> b=a"
     1.9 -by blast 
    1.10 -
    1.11  subsection{* Relativized versions of standard set-theoretic concepts *}
    1.12  
    1.13  constdefs
    1.14 @@ -33,17 +29,20 @@
    1.15      "successor(M,a,z) == is_cons(M,a,a,z)"
    1.16  
    1.17    number1 :: "[i=>o,i] => o"
    1.18 -    "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
    1.19 +    "number1(M,a) == \<exists>x[M]. empty(M,x) & successor(M,x,a)"
    1.20  
    1.21    number2 :: "[i=>o,i] => o"
    1.22 -    "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
    1.23 +    "number2(M,a) == \<exists>x[M]. number1(M,x) & successor(M,x,a)"
    1.24  
    1.25    number3 :: "[i=>o,i] => o"
    1.26 -    "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
    1.27 +    "number3(M,a) == \<exists>x[M]. number2(M,x) & successor(M,x,a)"
    1.28  
    1.29    powerset :: "[i=>o,i,i] => o"
    1.30      "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
    1.31  
    1.32 +  is_Collect :: "[i=>o,i,i=>o,i] => o"
    1.33 +    "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)"
    1.34 +
    1.35    inter :: "[i=>o,i,i,i] => o"
    1.36      "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
    1.37  
    1.38 @@ -85,11 +84,11 @@
    1.39  
    1.40    is_domain :: "[i=>o,i,i] => o"
    1.41      "is_domain(M,r,z) == 
    1.42 -	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))"
    1.43 +	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
    1.44  
    1.45    image :: "[i=>o,i,i,i] => o"
    1.46      "image(M,r,A,z) == 
    1.47 -        \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))"
    1.48 +        \<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
    1.49  
    1.50    is_range :: "[i=>o,i,i] => o"
    1.51      --{*the cleaner 
    1.52 @@ -97,12 +96,12 @@
    1.53        unfortunately needs an instance of separation in order to prove 
    1.54          @{term "M(converse(r))"}.*}
    1.55      "is_range(M,r,z) == 
    1.56 -	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))"
    1.57 +	\<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
    1.58  
    1.59    is_field :: "[i=>o,i,i] => o"
    1.60      "is_field(M,r,z) == 
    1.61 -	\<exists>dr[M]. is_domain(M,r,dr) & 
    1.62 -            (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))"
    1.63 +	\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) & 
    1.64 +                        union(M,dr,rr,z)"
    1.65  
    1.66    is_relation :: "[i=>o,i] => o"
    1.67      "is_relation(M,r) == 
    1.68 @@ -594,6 +593,16 @@
    1.69  apply (blast dest: transM) 
    1.70  done
    1.71  
    1.72 +lemma separation_iff:
    1.73 +     "separation(M,P) <-> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
    1.74 +by (simp add: separation_def is_Collect_def) 
    1.75 +
    1.76 +lemma (in M_triv_axioms) Collect_abs [simp]: 
    1.77 +     "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)"
    1.78 +apply (simp add: is_Collect_def)
    1.79 +apply (blast intro!: equalityI dest: transM)
    1.80 +done
    1.81 +
    1.82  text{*Probably the premise and conclusion are equivalent*}
    1.83  lemma (in M_triv_axioms) strong_replacementI [rule_format]:
    1.84      "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
    1.85 @@ -857,6 +866,8 @@
    1.86  locale M_axioms = M_triv_axioms +
    1.87  assumes Inter_separation:
    1.88       "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
    1.89 +  and Diff_separation:
    1.90 +     "M(B) ==> separation(M, \<lambda>x. x \<notin> B)"
    1.91    and cartprod_separation:
    1.92       "[| M(A); M(B) |] 
    1.93        ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
    1.94 @@ -1195,6 +1206,61 @@
    1.95  apply (frule Inter_closed, force+) 
    1.96  done
    1.97  
    1.98 +lemma (in M_axioms) Diff_closed [intro,simp]:
    1.99 +     "[|M(A); M(B)|] ==> M(A-B)"
   1.100 +by (insert Diff_separation, simp add: Diff_def)
   1.101 +
   1.102 +subsubsection{*Some Facts About Separation Axioms*}
   1.103 +
   1.104 +lemma (in M_axioms) separation_conj:
   1.105 +     "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
   1.106 +by (simp del: separation_closed
   1.107 +         add: separation_iff Collect_Int_Collect_eq [symmetric]) 
   1.108 +
   1.109 +(*???equalities*)
   1.110 +lemma Collect_Un_Collect_eq:
   1.111 +     "Collect(A,P) Un Collect(A,Q) = Collect(A, %x. P(x) | Q(x))"
   1.112 +by blast
   1.113 +
   1.114 +lemma Diff_Collect_eq:
   1.115 +     "A - Collect(A,P) = Collect(A, %x. ~ P(x))"
   1.116 +by blast
   1.117 +
   1.118 +lemma (in M_triv_axioms) Collect_rall_eq:
   1.119 +     "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) = 
   1.120 +               (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
   1.121 +apply simp 
   1.122 +apply (blast intro!: equalityI dest: transM) 
   1.123 +done
   1.124 +
   1.125 +lemma (in M_axioms) separation_disj:
   1.126 +     "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
   1.127 +by (simp del: separation_closed
   1.128 +         add: separation_iff Collect_Un_Collect_eq [symmetric]) 
   1.129 +
   1.130 +lemma (in M_axioms) separation_neg:
   1.131 +     "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
   1.132 +by (simp del: separation_closed
   1.133 +         add: separation_iff Diff_Collect_eq [symmetric]) 
   1.134 +
   1.135 +lemma (in M_axioms) separation_imp:
   1.136 +     "[|separation(M,P); separation(M,Q)|] 
   1.137 +      ==> separation(M, \<lambda>z. P(z) --> Q(z))"
   1.138 +by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric]) 
   1.139 +
   1.140 +text{*This result is a hint of how little can be done without the Reflection 
   1.141 +  Theorem.  The quantifier has to be bounded by a set.  We also need another
   1.142 +  instance of Separation!*}
   1.143 +lemma (in M_axioms) separation_rall:
   1.144 +     "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y)); 
   1.145 +        \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
   1.146 +      ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))" 
   1.147 +apply (simp del: separation_closed rall_abs
   1.148 +         add: separation_iff Collect_rall_eq) 
   1.149 +apply (blast intro!: Inter_closed RepFun_closed dest: transM) 
   1.150 +done
   1.151 +
   1.152 +
   1.153  subsubsection{*Functions and function space*}
   1.154  
   1.155  text{*M contains all finite functions*}