Theory Option_Helpers

section‹Option to List and Option to Set›
theory Option_Helpers
imports Main
begin

text‹Those are just syntactic helpers.›

definition option2set :: "'a option ⇒ 'a set" where
  "option2set n ≡ (case n of None ⇒ {} | Some s ⇒ {s})"

definition option2list :: "'a option ⇒ 'a list" where
  "option2list n ≡ (case n of None ⇒ [] | Some s ⇒ [s])"

lemma set_option2list[simp]: "set (option2list k) = option2set k"
  unfolding option2list_def option2set_def by (simp split: option.splits)

lemma option2list_simps[simp]: "option2list (Some x) = [x]" "option2list (None) = []"
  unfolding option2list_def option.simps by(fact refl)+

lemma option2set_None: "option2set None = {}"
  by(simp add: option2set_def)

lemma option2list_map: "option2list (map_option f n) = map f (option2list n)"
  by(simp add: option2list_def split: option.split)

lemma option2set_map: "option2set (map_option f n) = f ` option2set n"
  by(simp add: option2set_def split: option.split)

end