--- 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)"
--- 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"
--- 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
--- 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 *}