1.1 --- a/NEWS	Fri Sep 07 07:20:55 2012 +0200
     1.2 +++ b/NEWS	Fri Sep 07 08:20:18 2012 +0200
     1.3 @@ -41,6 +41,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New combinator "Option.these" with type "'a option set => 'a option".
     1.8 +
     1.9  * Renamed theory Library/List_Prefix to Library/Sublist.
    1.10  INCOMPATIBILITY.  Related changes are:
    1.11  

     2.1 --- a/src/HOL/Option.thy	Fri Sep 07 07:20:55 2012 +0200
     2.2 +++ b/src/HOL/Option.thy	Fri Sep 07 08:20:18 2012 +0200
     2.3 @@ -117,9 +117,57 @@
     2.4  lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
     2.5  by (cases x) auto
     2.6  
     2.7 -hide_const (open) set map bind
     2.8 +definition these :: "'a option set \<Rightarrow> 'a set"
     2.9 +where
    2.10 +  "these A = the ` {x \<in> A. x \<noteq> None}"
    2.11 +
    2.12 +lemma these_empty [simp]:
    2.13 +  "these {} = {}"
    2.14 +  by (simp add: these_def)
    2.15 +
    2.16 +lemma these_insert_None [simp]:
    2.17 +  "these (insert None A) = these A"
    2.18 +  by (auto simp add: these_def)
    2.19 +
    2.20 +lemma these_insert_Some [simp]:
    2.21 +  "these (insert (Some x) A) = insert x (these A)"
    2.22 +proof -
    2.23 +  have "{y \<in> insert (Some x) A. y \<noteq> None} = insert (Some x) {y \<in> A. y \<noteq> None}"
    2.24 +    by auto
    2.25 +  then show ?thesis by (simp add: these_def)
    2.26 +qed
    2.27 +
    2.28 +lemma in_these_eq:
    2.29 +  "x \<in> these A \<longleftrightarrow> Some x \<in> A"
    2.30 +proof
    2.31 +  assume "Some x \<in> A"
    2.32 +  then obtain B where "A = insert (Some x) B" by auto
    2.33 +  then show "x \<in> these A" by (auto simp add: these_def intro!: image_eqI)
    2.34 +next
    2.35 +  assume "x \<in> these A"
    2.36 +  then show "Some x \<in> A" by (auto simp add: these_def)
    2.37 +qed
    2.38 +
    2.39 +lemma these_image_Some_eq [simp]:
    2.40 +  "these (Some ` A) = A"
    2.41 +  by (auto simp add: these_def intro!: image_eqI)
    2.42 +
    2.43 +lemma Some_image_these_eq:
    2.44 +  "Some ` these A = {x\<in>A. x \<noteq> None}"
    2.45 +  by (auto simp add: these_def image_image intro!: image_eqI)
    2.46 +
    2.47 +lemma these_empty_eq:
    2.48 +  "these B = {} \<longleftrightarrow> B = {} \<or> B = {None}"
    2.49 +  by (auto simp add: these_def)
    2.50 +
    2.51 +lemma these_not_empty_eq:
    2.52 +  "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
    2.53 +  by (auto simp add: these_empty_eq)
    2.54 +
    2.55 +hide_const (open) set map bind these
    2.56  hide_fact (open) map_cong bind_cong
    2.57  
    2.58 +
    2.59  subsubsection {* Code generator setup *}
    2.60  
    2.61  definition is_none :: "'a option \<Rightarrow> bool" where
    2.62 @@ -164,3 +212,4 @@
    2.63    Option None Some
    2.64  
    2.65  end
    2.66 +