# 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: "(\x. P x) \ P None \ (\x. P (Some x))" - by (metis option.exhaust) (* TODO: move to Option.thy *) - -lemma split_option_ex: "(\x. P x) \ P None \ (\x. P (Some x))" - by (metis option.exhaust) (* TODO: move to Option.thy *) - lemma option_rel_mono[relator_mono]: assumes "A \ B" shows "(option_rel A) \ (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: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" - by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) - -lemma split_sum_ex: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" - by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *) - lemma sum_rel_mono[relator_mono]: assumes "A \ C" assumes "B \ 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: "(\x. P x) \ P None \ (\x. P (Some x))" +by (auto intro: option.induct) + +lemma split_option_ex: "(\x. P x) \ P None \ (\x. P (Some x))" +using split_option_all[of "\x. \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: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" + by (auto intro: sum.induct) + +lemma split_sum_ex: "(\x. P x) \ (\x. P (Inl x)) \ (\x. P (Inr x))" +using split_sum_all[of "\x. \P x"] by blast subsection {* Projections *}