--- a/src/HOL/BNF_Def.thy Mon Oct 12 22:03:24 2015 +0200
+++ b/src/HOL/BNF_Def.thy Tue Oct 13 09:21:14 2015 +0200
@@ -176,15 +176,6 @@
lemma flip_pred: "A \<subseteq> Collect (case_prod (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (case_prod R)"
by auto
-lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
- by auto
-
-lemma Collect_split_mono_strong:
- "\<lbrakk>X = fst ` A; Y = snd ` A; \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (case_prod P)\<rbrakk> \<Longrightarrow>
- A \<subseteq> Collect (case_prod Q)"
- by fastforce
-
-
lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
by simp
--- a/src/HOL/Product_Type.thy Mon Oct 12 22:03:24 2015 +0200
+++ b/src/HOL/Product_Type.thy Tue Oct 13 09:21:14 2015 +0200
@@ -1084,6 +1084,19 @@
"{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q "
by (fact SetCompr_Sigma_eq)
+lemma Collect_splitD:
+ "x \<in> Collect (uncurry A) \<Longrightarrow> A (fst x) (snd x)"
+ by auto
+
+lemma Collect_split_mono:
+ "A \<le> B \<Longrightarrow> Collect (uncurry A) \<subseteq> Collect (uncurry B)"
+ by auto (auto elim!: le_funE)
+
+lemma Collect_split_mono_strong:
+ "X = fst ` A \<Longrightarrow> Y = snd ` A \<Longrightarrow> \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b
+ \<Longrightarrow> A \<subseteq> Collect (uncurry P) \<Longrightarrow> A \<subseteq> Collect (uncurry Q)"
+ by fastforce
+
lemma UN_Times_distrib:
"(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
-- \<open>Suggested by Pierre Chartier\<close>