diff -r 3e79279c10ca -r 0b7bdb75f451 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Tue May 31 12:24:43 2016 +0200
+++ b/src/HOL/Option.thy	Tue May 31 13:02:44 2016 +0200
@@ -136,6 +136,43 @@
     | _ \<Rightarrow> False)"
   by (auto split: prod.split option.split)
 
+
+definition combine_options :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> 'a option"
+  where "combine_options f x y = 
+           (case x of None \<Rightarrow> y | Some x \<Rightarrow> (case y of None \<Rightarrow> Some x | Some y \<Rightarrow> Some (f x y)))"
+
+lemma combine_options_simps [simp]:
+  "combine_options f None y = y"
+  "combine_options f x None = x"
+  "combine_options f (Some a) (Some b) = Some (f a b)"
+  by (simp_all add: combine_options_def split: option.splits)
+  
+lemma combine_options_cases [case_names None1 None2 Some]:
+  "(x = None \<Longrightarrow> P x y) \<Longrightarrow> (y = None \<Longrightarrow> P x y) \<Longrightarrow> 
+     (\<And>a b. x = Some a \<Longrightarrow> y = Some b \<Longrightarrow> P x y) \<Longrightarrow> P x y"
+  by (cases x; cases y) simp_all
+
+lemma combine_options_commute: 
+  "(\<And>x y. f x y = f y x) \<Longrightarrow> combine_options f x y = combine_options f y x"
+  using combine_options_cases[of x ]
+  by (induction x y rule: combine_options_cases) simp_all
+
+lemma combine_options_assoc:
+  "(\<And>x y z. f (f x y) z = f x (f y z)) \<Longrightarrow> 
+     combine_options f (combine_options f x y) z =
+     combine_options f x (combine_options f y z)"
+  by (auto simp: combine_options_def split: option.splits)
+
+lemma combine_options_left_commute:
+  "(\<And>x y. f x y = f y x) \<Longrightarrow> (\<And>x y z. f (f x y) z = f x (f y z)) \<Longrightarrow> 
+     combine_options f y (combine_options f x z) =
+     combine_options f x (combine_options f y z)"
+  by (auto simp: combine_options_def split: option.splits)
+
+lemmas combine_options_ac = 
+  combine_options_commute combine_options_assoc combine_options_left_commute
+
+
 context
 begin