# HG changeset patch
# User kuncar
# Date 1376402362 -7200
# Node ID ec5e6f69bd653a31f222771c5b574832bbb75a56
# Parent  bb18eed53ed689d6af57993225ba50a8c5cd73e3
move useful lemmas to Main

diff -r bb18eed53ed6 -r ec5e6f69bd65 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -50,12 +50,6 @@
   "option_rel (op =) = (op =)"
   by (simp add: option_rel_unfold fun_eq_iff split: option.split)
 
-lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
-  by (metis option.exhaust) (* TODO: move to Option.thy *)
-
-lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
-  by (metis option.exhaust) (* TODO: move to Option.thy *)
-
 lemma option_rel_mono[relator_mono]:
   assumes "A \<le> B"
   shows "(option_rel A) \<le> (option_rel B)"
diff -r bb18eed53ed6 -r ec5e6f69bd65 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -50,12 +50,6 @@
   "sum_rel (op =) (op =) = (op =)"
   by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
 
-lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
-  by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
-
-lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
-  by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
-
 lemma sum_rel_mono[relator_mono]:
   assumes "A \<le> C"
   assumes "B \<le> D"
diff -r bb18eed53ed6 -r ec5e6f69bd65 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Option.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -30,10 +30,15 @@
   | (Some) y where "x = Some y" and "Q y"
   using c by (cases x) simp_all
 
+lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
+by (auto intro: option.induct)
+
+lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
+using split_option_all[of "\<lambda>x. \<not>P x"] by blast
+
 lemma UNIV_option_conv: "UNIV = insert None (range Some)"
 by(auto intro: classical)
 
-
 subsubsection {* Operations *}
 
 primrec the :: "'a option => 'a" where
diff -r bb18eed53ed6 -r ec5e6f69bd65 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Sum_Type.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -115,6 +115,11 @@
   qed
 qed
 
+lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
+  by (auto intro: sum.induct)
+
+lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
+using split_sum_all[of "\<lambda>x. \<not>P x"] by blast
 
 subsection {* Projections *}