src/ZF/Constructible/Relative.thy

--- a/src/ZF/Constructible/Relative.thy	Wed Jul 31 14:34:08 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Wed Jul 31 14:39:47 2002 +0200
@@ -2,10 +2,6 @@
 
 theory Relative = Main:
 
-(*????????????????for IFOL.thy????????????????*)
-lemma eq_commute: "a=b <-> b=a"
-by blast 
-
 subsection{* Relativized versions of standard set-theoretic concepts *}
 
 constdefs
@@ -33,17 +29,20 @@
     "successor(M,a,z) == is_cons(M,a,a,z)"
 
   number1 :: "[i=>o,i] => o"
-    "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
+    "number1(M,a) == \<exists>x[M]. empty(M,x) & successor(M,x,a)"
 
   number2 :: "[i=>o,i] => o"
-    "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
+    "number2(M,a) == \<exists>x[M]. number1(M,x) & successor(M,x,a)"
 
   number3 :: "[i=>o,i] => o"
-    "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
+    "number3(M,a) == \<exists>x[M]. number2(M,x) & successor(M,x,a)"
 
   powerset :: "[i=>o,i,i] => o"
     "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
 
+  is_Collect :: "[i=>o,i,i=>o,i] => o"
+    "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)"
+
   inter :: "[i=>o,i,i,i] => o"
     "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
 
@@ -85,11 +84,11 @@
 
   is_domain :: "[i=>o,i,i] => o"
     "is_domain(M,r,z) == 
-	\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))"
+	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
 
   image :: "[i=>o,i,i,i] => o"
     "image(M,r,A,z) == 
-        \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))"
+        \<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
 
   is_range :: "[i=>o,i,i] => o"
     --{*the cleaner 
@@ -97,12 +96,12 @@
       unfortunately needs an instance of separation in order to prove 
         @{term "M(converse(r))"}.*}
     "is_range(M,r,z) == 
-	\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))"
+	\<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
 
   is_field :: "[i=>o,i,i] => o"
     "is_field(M,r,z) == 
-	\<exists>dr[M]. is_domain(M,r,dr) & 
-            (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))"
+	\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) & 
+                        union(M,dr,rr,z)"
 
   is_relation :: "[i=>o,i] => o"
     "is_relation(M,r) == 
@@ -594,6 +593,16 @@
 apply (blast dest: transM) 
 done
 
+lemma separation_iff:
+     "separation(M,P) <-> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
+by (simp add: separation_def is_Collect_def) 
+
+lemma (in M_triv_axioms) Collect_abs [simp]: 
+     "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)"
+apply (simp add: is_Collect_def)
+apply (blast intro!: equalityI dest: transM)
+done
+
 text{*Probably the premise and conclusion are equivalent*}
 lemma (in M_triv_axioms) strong_replacementI [rule_format]:
     "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
@@ -857,6 +866,8 @@
 locale M_axioms = M_triv_axioms +
 assumes Inter_separation:
      "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
+  and Diff_separation:
+     "M(B) ==> separation(M, \<lambda>x. x \<notin> B)"
   and cartprod_separation:
      "[| M(A); M(B) |] 
       ==> separation(M, \<lambda>z. \<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,z)))"
@@ -1195,6 +1206,61 @@
 apply (frule Inter_closed, force+) 
 done
 
+lemma (in M_axioms) Diff_closed [intro,simp]:
+     "[|M(A); M(B)|] ==> M(A-B)"
+by (insert Diff_separation, simp add: Diff_def)
+
+subsubsection{*Some Facts About Separation Axioms*}
+
+lemma (in M_axioms) separation_conj:
+     "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
+by (simp del: separation_closed
+         add: separation_iff Collect_Int_Collect_eq [symmetric]) 
+
+(*???equalities*)
+lemma Collect_Un_Collect_eq:
+     "Collect(A,P) Un Collect(A,Q) = Collect(A, %x. P(x) | Q(x))"
+by blast
+
+lemma Diff_Collect_eq:
+     "A - Collect(A,P) = Collect(A, %x. ~ P(x))"
+by blast
+
+lemma (in M_triv_axioms) Collect_rall_eq:
+     "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) = 
+               (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
+apply simp 
+apply (blast intro!: equalityI dest: transM) 
+done
+
+lemma (in M_axioms) separation_disj:
+     "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
+by (simp del: separation_closed
+         add: separation_iff Collect_Un_Collect_eq [symmetric]) 
+
+lemma (in M_axioms) separation_neg:
+     "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
+by (simp del: separation_closed
+         add: separation_iff Diff_Collect_eq [symmetric]) 
+
+lemma (in M_axioms) separation_imp:
+     "[|separation(M,P); separation(M,Q)|] 
+      ==> separation(M, \<lambda>z. P(z) --> Q(z))"
+by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric]) 
+
+text{*This result is a hint of how little can be done without the Reflection 
+  Theorem.  The quantifier has to be bounded by a set.  We also need another
+  instance of Separation!*}
+lemma (in M_axioms) separation_rall:
+     "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y)); 
+        \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
+      ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))" 
+apply (simp del: separation_closed rall_abs
+         add: separation_iff Collect_rall_eq) 
+apply (blast intro!: Inter_closed RepFun_closed dest: transM) 
+done
+
+
 subsubsection{*Functions and function space*}
 
 text{*M contains all finite functions*}