src/ZF/Constructible/Relative.thy
 changeset 13436 8fd1d803a3d3 parent 13434 78b93a667c01 child 13505 52a16cb7fefb
```     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.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