src/HOL/Option.thy
changeset 53010 ec5e6f69bd65
parent 52435 6646bb548c6b
child 53940 36cf426cb1c6
     1.1 --- a/src/HOL/Option.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Option.thy	Tue Aug 13 15:59:22 2013 +0200
     1.3 @@ -30,10 +30,15 @@
     1.4    | (Some) y where "x = Some y" and "Q y"
     1.5    using c by (cases x) simp_all
     1.6  
     1.7 +lemma split_option_all: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P (Some x))"
     1.8 +by (auto intro: option.induct)
     1.9 +
    1.10 +lemma split_option_ex: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P (Some x))"
    1.11 +using split_option_all[of "\<lambda>x. \<not>P x"] by blast
    1.12 +
    1.13  lemma UNIV_option_conv: "UNIV = insert None (range Some)"
    1.14  by(auto intro: classical)
    1.15  
    1.16 -
    1.17  subsubsection {* Operations *}
    1.18  
    1.19  primrec the :: "'a option => 'a" where