src/ZF/equalities.thy

 theory equalities = pair:
 
 text{*These cover union, intersection, converse, domain, range, etc.  Philippe
 de Groote proved many of the inclusions.*}
 
-(*FIXME: move to ZF.thy or even to FOL.thy??*)
-lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
-by blast
-
-(*FIXME: move to ZF.thy or even to FOL.thy??*)
-lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
-by blast
-
-(** Monotonicity of implications -- some could go to FOL **)
-
 lemma in_mono: "A<=B ==> x:A --> x:B"
 by blast
-
-lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
-
-lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
-
-lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
-
-lemma imp_refl: "P-->P"
-by (rule impI, assumption)
-
-(*The quantifier monotonicity rules are also intuitionistically valid*)
-lemma ex_mono:
-    "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"
-by blast
-
-lemma all_mono:
-    "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"
-by blast
-
 
 lemma the_eq_0 [simp]: "(THE x. False) = 0"
 by (blast intro: the_0)
 
 subsection{*Bounded Quantifiers*}

 by (blast elim!: equalityE)
 
 lemma Union_empty_iff: "Union(A) = 0 <-> (\<forall>B\<in>A. B=0)"
 by blast
 
+lemma Int_Union2: "Union(B) Int A = (UN C:B. C Int A)"
+by blast
+
 (** Big Intersection is the greatest lower bound of a nonempty set **)
 
 lemma Inter_subset_iff: "a: A  ==>  C <= Inter(A) <-> (\<forall>x\<in>A. C <= x)"
 by blast
 

      "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
 by blast
 
 lemma Collect_Union_eq [simp]:
      "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
+by blast
+
+lemma Collect_Int_left: "{x:A. P(x)} Int B = {x : A Int B. P(x)}"
+by blast
+
+lemma Collect_Int_right: "A Int {x:B. P(x)} = {x : A Int B. P(x)}"
+by blast
+
+lemma Collect_disj_eq: "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"
+by blast
+
+lemma Collect_conj_eq: "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"
 by blast
 
 lemmas subset_SIs = subset_refl cons_subsetI subset_consI 
                     Union_least UN_least Un_least 
                     Inter_greatest Int_greatest RepFun_subset

 val Union_cons = thm "Union_cons";
 val Union_Un_distrib = thm "Union_Un_distrib";
 val Union_Int_subset = thm "Union_Int_subset";
 val Union_disjoint = thm "Union_disjoint";
 val Union_empty_iff = thm "Union_empty_iff";
+val Int_Union2 = thm "Int_Union2";
 val Inter_0 = thm "Inter_0";
 val Inter_Un_subset = thm "Inter_Un_subset";
 val Inter_Un_distrib = thm "Inter_Un_distrib";
 val Union_singleton = thm "Union_singleton";
 val Inter_singleton = thm "Inter_singleton";

 val Collect_Diff = thm "Collect_Diff";
 val Collect_cons = thm "Collect_cons";
 val Int_Collect_self_eq = thm "Int_Collect_self_eq";
 val Collect_Collect_eq = thm "Collect_Collect_eq";
 val Collect_Int_Collect_eq = thm "Collect_Int_Collect_eq";
+val Collect_disj_eq = thm "Collect_disj_eq";
+val Collect_conj_eq = thm "Collect_conj_eq";
 
 val Int_ac = thms "Int_ac";
 val Un_ac = thms "Un_ac";
 val Int_absorb1 = thm "Int_absorb1";
 val Int_absorb2 = thm "Int_absorb2";