# HG changeset patch
# User haftmann
# Date 1444720874 -7200
# Node ID 0dfcd0fb4172a7dd19a0e1dcdf53431f332c5cce
# Parent  e0825405d398d3e115bc0959eec75373b313500c
moved lemmas

diff -r e0825405d398 -r 0dfcd0fb4172 src/HOL/BNF_Def.thy
--- 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
 
diff -r e0825405d398 -r 0dfcd0fb4172 src/HOL/Product_Type.thy
--- 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>