src/HOL/Option.thy
changeset 63194 0b7bdb75f451
parent 61799 4cf66f21b764
child 63343 fb5d8a50c641
     1.1 --- a/src/HOL/Option.thy	Tue May 31 12:24:43 2016 +0200
     1.2 +++ b/src/HOL/Option.thy	Tue May 31 13:02:44 2016 +0200
     1.3 @@ -136,6 +136,43 @@
     1.4      | _ \<Rightarrow> False)"
     1.5    by (auto split: prod.split option.split)
     1.6  
     1.7 +
     1.8 +definition combine_options :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> 'a option"
     1.9 +  where "combine_options f x y = 
    1.10 +           (case x of None \<Rightarrow> y | Some x \<Rightarrow> (case y of None \<Rightarrow> Some x | Some y \<Rightarrow> Some (f x y)))"
    1.11 +
    1.12 +lemma combine_options_simps [simp]:
    1.13 +  "combine_options f None y = y"
    1.14 +  "combine_options f x None = x"
    1.15 +  "combine_options f (Some a) (Some b) = Some (f a b)"
    1.16 +  by (simp_all add: combine_options_def split: option.splits)
    1.17 +  
    1.18 +lemma combine_options_cases [case_names None1 None2 Some]:
    1.19 +  "(x = None \<Longrightarrow> P x y) \<Longrightarrow> (y = None \<Longrightarrow> P x y) \<Longrightarrow> 
    1.20 +     (\<And>a b. x = Some a \<Longrightarrow> y = Some b \<Longrightarrow> P x y) \<Longrightarrow> P x y"
    1.21 +  by (cases x; cases y) simp_all
    1.22 +
    1.23 +lemma combine_options_commute: 
    1.24 +  "(\<And>x y. f x y = f y x) \<Longrightarrow> combine_options f x y = combine_options f y x"
    1.25 +  using combine_options_cases[of x ]
    1.26 +  by (induction x y rule: combine_options_cases) simp_all
    1.27 +
    1.28 +lemma combine_options_assoc:
    1.29 +  "(\<And>x y z. f (f x y) z = f x (f y z)) \<Longrightarrow> 
    1.30 +     combine_options f (combine_options f x y) z =
    1.31 +     combine_options f x (combine_options f y z)"
    1.32 +  by (auto simp: combine_options_def split: option.splits)
    1.33 +
    1.34 +lemma combine_options_left_commute:
    1.35 +  "(\<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> 
    1.36 +     combine_options f y (combine_options f x z) =
    1.37 +     combine_options f x (combine_options f y z)"
    1.38 +  by (auto simp: combine_options_def split: option.splits)
    1.39 +
    1.40 +lemmas combine_options_ac = 
    1.41 +  combine_options_commute combine_options_assoc combine_options_left_commute
    1.42 +
    1.43 +
    1.44  context
    1.45  begin
    1.46