move useful lemmas to Main
authorkuncar
Tue Aug 13 15:59:22 2013 +0200 (2013-08-13)
changeset 53010ec5e6f69bd65
parent 53009 bb18eed53ed6
child 53011 aeee0a4be6cf
move useful lemmas to Main
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Option.thy
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Library/Quotient_Option.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Option.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -50,12 +50,6 @@
     1.4    "option_rel (op =) = (op =)"
     1.5    by (simp add: option_rel_unfold fun_eq_iff split: option.split)
     1.6  
     1.7 -lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
     1.8 -  by (metis option.exhaust) (* TODO: move to Option.thy *)
     1.9 -
    1.10 -lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
    1.11 -  by (metis option.exhaust) (* TODO: move to Option.thy *)
    1.12 -
    1.13  lemma option_rel_mono[relator_mono]:
    1.14    assumes "A \<le> B"
    1.15    shows "(option_rel A) \<le> (option_rel B)"
     2.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Aug 13 14:20:22 2013 +0200
     2.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Aug 13 15:59:22 2013 +0200
     2.3 @@ -50,12 +50,6 @@
     2.4    "sum_rel (op =) (op =) = (op =)"
     2.5    by (simp add: sum_rel_unfold fun_eq_iff split: sum.split)
     2.6  
     2.7 -lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
     2.8 -  by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
     2.9 -
    2.10 -lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
    2.11 -  by (metis sum.exhaust) (* TODO: move to Sum_Type.thy *)
    2.12 -
    2.13  lemma sum_rel_mono[relator_mono]:
    2.14    assumes "A \<le> C"
    2.15    assumes "B \<le> D"
     3.1 --- a/src/HOL/Option.thy	Tue Aug 13 14:20:22 2013 +0200
     3.2 +++ b/src/HOL/Option.thy	Tue Aug 13 15:59:22 2013 +0200
     3.3 @@ -30,10 +30,15 @@
     3.4    | (Some) y where "x = Some y" and "Q y"
     3.5    using c by (cases x) simp_all
     3.6  
     3.7 +lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
     3.8 +by (auto intro: option.induct)
     3.9 +
    3.10 +lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
    3.11 +using split_option_all[of "\<lambda>x. \<not>P x"] by blast
    3.12 +
    3.13  lemma UNIV_option_conv: "UNIV = insert None (range Some)"
    3.14  by(auto intro: classical)
    3.15  
    3.16 -
    3.17  subsubsection {* Operations *}
    3.18  
    3.19  primrec the :: "'a option => 'a" where
     4.1 --- a/src/HOL/Sum_Type.thy	Tue Aug 13 14:20:22 2013 +0200
     4.2 +++ b/src/HOL/Sum_Type.thy	Tue Aug 13 15:59:22 2013 +0200
     4.3 @@ -115,6 +115,11 @@
     4.4    qed
     4.5  qed
     4.6  
     4.7 +lemma split_sum_all: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
     4.8 +  by (auto intro: sum.induct)
     4.9 +
    4.10 +lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
    4.11 +using split_sum_all[of "\<lambda>x. \<not>P x"] by blast
    4.12  
    4.13  subsection {* Projections *}
    4.14