Theory HOL.Option

(*  Title:      HOL/Option.thy
    Author:     Folklore
*)

section ‹Datatype option›

theory Option
  imports Lifting
begin

datatype 'a option =
    None
  | Some (the: 'a)

datatype_compat option

lemma [case_names None Some, cases type: option]:
  ― ‹for backward compatibility -- names of variables differ›
  "(y = None ⟹ P) ⟹ (⋀a. y = Some a ⟹ P) ⟹ P"
  by (rule option.exhaust)

lemma [case_names None Some, induct type: option]:
  ― ‹for backward compatibility -- names of variables differ›
  "P None ⟹ (⋀option. P (Some option)) ⟹ P option"
  by (rule option.induct)

text ‹Compatibility:›
setup ‹Sign.mandatory_path "option"›
lemmas inducts = option.induct
lemmas cases = option.case
setup ‹Sign.parent_path›

lemma not_None_eq [iff]: "x ≠ None ⟷ (∃y. x = Some y)"
  by (induct x) auto

lemma not_Some_eq [iff]: "(∀y. x ≠ Some y) ⟷ x = None"
  by (induct x) auto

lemma comp_the_Some[simp]: "the o Some = id"
by auto

text ‹Although it may appear that both of these equalities are helpful
only when applied to assumptions, in practice it seems better to give
them the uniform iff attribute.›

lemma inj_Some [simp]: "inj_on Some A"
  by (rule inj_onI) simp

lemma case_optionE:
  assumes c: "(case x of None ⇒ P | Some y ⇒ Q y)"
  obtains
    (None) "x = None" and P
  | (Some) y where "x = Some y" and "Q y"
  using c by (cases x) simp_all

lemma split_option_all: "(∀x. P x) ⟷ P None ∧ (∀x. P (Some x))"
  by (auto intro: option.induct)

lemma split_option_ex: "(∃x. P x) ⟷ P None ∨ (∃x. P (Some x))"
  using split_option_all[of "λx. ¬ P x"] by blast

lemma UNIV_option_conv: "UNIV = insert None (range Some)"
  by (auto intro: classical)

lemma rel_option_None1 [simp]: "rel_option P None x ⟷ x = None"
  by (cases x) simp_all

lemma rel_option_None2 [simp]: "rel_option P x None ⟷ x = None"
  by (cases x) simp_all

lemma option_rel_Some1: "rel_option A (Some x) y ⟷ (∃y'. y = Some y' ∧ A x y')" (* Option *)
by(cases y) simp_all

lemma option_rel_Some2: "rel_option A x (Some y) ⟷ (∃x'. x = Some x' ∧ A x' y)" (* Option *)
by(cases x) simp_all

lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)"
  (is "?lhs = ?rhs")
proof (rule antisym)
  show "?lhs ≤ ?rhs" by (auto elim: option.rel_cases)
  show "?rhs ≤ ?lhs" by (auto elim: option.rel_mono_strong)
qed

lemma rel_option_reflI:
  "(⋀x. x ∈ set_option y ⟹ P x x) ⟹ rel_option P y y"
  by (cases y) auto


subsubsection ‹Operations›

lemma ospec [dest]: "(∀x∈set_option A. P x) ⟹ A = Some x ⟹ P x"
  by simp

setup ‹map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec}))›

lemma elem_set [iff]: "(x ∈ set_option xo) = (xo = Some x)"
  by (cases xo) auto

lemma set_empty_eq [simp]: "(set_option xo = {}) = (xo = None)"
  by (cases xo) auto

lemma map_option_case: "map_option f y = (case y of None ⇒ None | Some x ⇒ Some (f x))"
  by (auto split: option.split)

lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
  by (simp add: map_option_case split: option.split)

lemma None_eq_map_option_iff [iff]: "None = map_option f x ⟷ x = None"
by(cases x) simp_all

lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (∃z. xo = Some z ∧ f z = y)"
  by (simp add: map_option_case split: option.split)

lemma map_option_o_case_sum [simp]:
    "map_option f ∘ case_sum g h = case_sum (map_option f ∘ g) (map_option f ∘ h)"
  by (rule o_case_sum)

lemma map_option_cong: "x = y ⟹ (⋀a. y = Some a ⟹ f a = g a) ⟹ map_option f x = map_option g y"
  by (cases x) auto

lemma map_option_idI: "(⋀y. y ∈ set_option x ⟹ f y = y) ⟹ map_option f x = x"
by(cases x)(simp_all)

functor map_option: map_option
  by (simp_all add: option.map_comp fun_eq_iff option.map_id)

lemma case_map_option [simp]: "case_option g h (map_option f x) = case_option g (h ∘ f) x"
  by (cases x) simp_all

lemma None_notin_image_Some [simp]: "None ∉ Some ` A"
by auto

lemma notin_range_Some: "x ∉ range Some ⟷ x = None"
by(cases x) auto

lemma rel_option_iff:
  "rel_option R x y = (case (x, y) of (None, None) ⇒ True
    | (Some x, Some y) ⇒ R x y
    | _ ⇒ False)"
  by (auto split: prod.split option.split)


definition combine_options :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a option ⇒ 'a option ⇒ 'a option"
  where "combine_options f x y = 
           (case x of None ⇒ y | Some x ⇒ (case y of None ⇒ Some x | Some y ⇒ 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 ⟹ P x y) ⟹ (y = None ⟹ P x y) ⟹ 
     (⋀a b. x = Some a ⟹ y = Some b ⟹ P x y) ⟹ P x y"
  by (cases x; cases y) simp_all

lemma combine_options_commute: 
  "(⋀x y. f x y = f y x) ⟹ 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:
  "(⋀x y z. f (f x y) z = f x (f y z)) ⟹ 
     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:
  "(⋀x y. f x y = f y x) ⟹ (⋀x y z. f (f x y) z = f x (f y z)) ⟹ 
     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

qualified definition is_none :: "'a option ⇒ bool"
  where [code_post]: "is_none x ⟷ x = None"

lemma is_none_simps [simp]:
  "is_none None"
  "¬ is_none (Some x)"
  by (simp_all add: is_none_def)

lemma is_none_code [code]:
  "is_none None = True"
  "is_none (Some x) = False"
  by simp_all

lemma rel_option_unfold:
  "rel_option R x y ⟷
   (is_none x ⟷ is_none y) ∧ (¬ is_none x ⟶ ¬ is_none y ⟶ R (the x) (the y))"
  by (simp add: rel_option_iff split: option.split)

lemma rel_optionI:
  "⟦ is_none x ⟷ is_none y; ⟦ ¬ is_none x; ¬ is_none y ⟧ ⟹ P (the x) (the y) ⟧
  ⟹ rel_option P x y"
  by (simp add: rel_option_unfold)

lemma is_none_map_option [simp]: "is_none (map_option f x) ⟷ is_none x"
  by (simp add: is_none_def)

lemma the_map_option: "¬ is_none x ⟹ the (map_option f x) = f (the x)"
  by (auto simp add: is_none_def)


qualified primrec bind :: "'a option ⇒ ('a ⇒ 'b option) ⇒ 'b option"
where
  bind_lzero: "bind None f = None"
| bind_lunit: "bind (Some x) f = f x"

lemma is_none_bind: "is_none (bind f g) ⟷ is_none f ∨ is_none (g (the f))"
  by (cases f) simp_all

lemma bind_runit[simp]: "bind x Some = x"
  by (cases x) auto

lemma bind_assoc[simp]: "bind (bind x f) g = bind x (λy. bind (f y) g)"
  by (cases x) auto

lemma bind_rzero[simp]: "bind x (λx. None) = None"
  by (cases x) auto

qualified lemma bind_cong: "x = y ⟹ (⋀a. y = Some a ⟹ f a = g a) ⟹ bind x f = bind y g"
  by (cases x) auto

lemma bind_split: "P (bind m f) ⟷ (m = None ⟶ P None) ∧ (∀v. m = Some v ⟶ P (f v))"
  by (cases m) auto

lemma bind_split_asm: "P (bind m f) ⟷ ¬ (m = None ∧ ¬ P None ∨ (∃x. m = Some x ∧ ¬ P (f x)))"
  by (cases m) auto

lemmas bind_splits = bind_split bind_split_asm

lemma bind_eq_Some_conv: "bind f g = Some x ⟷ (∃y. f = Some y ∧ g y = Some x)"
  by (cases f) simp_all

lemma bind_eq_None_conv: "Option.bind a f = None ⟷ a = None ∨ f (the a) = None"
by(cases a) simp_all

lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f ∘ g)"
  by (cases x) simp_all

lemma bind_option_cong:
  "⟦ x = y; ⋀z. z ∈ set_option y ⟹ f z = g z ⟧ ⟹ bind x f = bind y g"
  by (cases y) simp_all

lemma bind_option_cong_simp:
  "⟦ x = y; ⋀z. z ∈ set_option y =simp=> f z = g z ⟧ ⟹ bind x f = bind y g"
  unfolding simp_implies_def by (rule bind_option_cong)

lemma bind_option_cong_code: "x = y ⟹ bind x f = bind y f"
  by simp

lemma bind_map_option: "bind (map_option f x) g = bind x (g ∘ f)"
by(cases x) simp_all

lemma set_bind_option [simp]: "set_option (bind x f) = (⋃((set_option ∘ f) ` set_option x))"
by(cases x) auto

lemma map_conv_bind_option: "map_option f x = Option.bind x (Some ∘ f)"
by(cases x) simp_all

end

setup ‹Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})›


context
begin

qualified definition these :: "'a option set ⇒ 'a set"
  where "these A = the ` {x ∈ A. x ≠ None}"

lemma these_empty [simp]: "these {} = {}"
  by (simp add: these_def)

lemma these_insert_None [simp]: "these (insert None A) = these A"
  by (auto simp add: these_def)

lemma these_insert_Some [simp]: "these (insert (Some x) A) = insert x (these A)"
proof -
  have "{y ∈ insert (Some x) A. y ≠ None} = insert (Some x) {y ∈ A. y ≠ None}"
    by auto
  then show ?thesis by (simp add: these_def)
qed

lemma in_these_eq: "x ∈ these A ⟷ Some x ∈ A"
proof
  assume "Some x ∈ A"
  then obtain B where "A = insert (Some x) B" by auto
  then show "x ∈ these A" by (auto simp add: these_def intro!: image_eqI)
next
  assume "x ∈ these A"
  then show "Some x ∈ A" by (auto simp add: these_def)
qed

lemma these_image_Some_eq [simp]: "these (Some ` A) = A"
  by (auto simp add: these_def intro!: image_eqI)

lemma Some_image_these_eq: "Some ` these A = {x∈A. x ≠ None}"
  by (auto simp add: these_def image_image intro!: image_eqI)

lemma these_empty_eq: "these B = {} ⟷ B = {} ∨ B = {None}"
  by (auto simp add: these_def)

lemma these_not_empty_eq: "these B ≠ {} ⟷ B ≠ {} ∧ B ≠ {None}"
  by (auto simp add: these_empty_eq)

end

lemma finite_range_Some: "finite (range (Some :: 'a ⇒ 'a option)) = finite (UNIV :: 'a set)"
  by (auto dest: finite_imageD intro: inj_Some)


subsection ‹Transfer rules for the Transfer package›

context includes lifting_syntax
begin

lemma option_bind_transfer [transfer_rule]:
  "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
    Option.bind Option.bind"
  unfolding rel_fun_def split_option_all by simp

lemma pred_option_parametric [transfer_rule]:
  "((A ===> (=)) ===> rel_option A ===> (=)) pred_option pred_option"
  by (rule rel_funI)+ (auto simp add: rel_option_unfold Option.is_none_def dest: rel_funD)

end


subsubsection ‹Interaction with finite sets›

lemma finite_option_UNIV [simp]:
  "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
  by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)

instance option :: (finite) finite
  by standard (simp add: UNIV_option_conv)


subsubsection ‹Code generator setup›

lemma equal_None_code_unfold [code_unfold]:
  "HOL.equal x None ⟷ Option.is_none x"
  "HOL.equal None = Option.is_none"
  by (auto simp add: equal Option.is_none_def)

code_printing
  type_constructor option ⇀
    (SML) "_ option"
    and (OCaml) "_ option"
    and (Haskell) "Maybe _"
    and (Scala) "!Option[(_)]"
| constant None ⇀
    (SML) "NONE"
    and (OCaml) "None"
    and (Haskell) "Nothing"
    and (Scala) "!None"
| constant Some ⇀
    (SML) "SOME"
    and (OCaml) "Some _"
    and (Haskell) "Just"
    and (Scala) "Some"
| class_instance option :: equal ⇀
    (Haskell) -
| constant "HOL.equal :: 'a option ⇒ 'a option ⇒ bool" ⇀
    (Haskell) infix 4 "=="

code_reserved SML
  option NONE SOME

code_reserved OCaml
  option None Some

code_reserved Scala
  Option None Some

end