Theory The_Optional

theory The_Optional
  imports Main
begin

definition The_optional :: "('a ⇒ bool) ⇒ 'a option" where
  "The_optional P = (if ∃!x. P x then Some (THE x. P x) else None)"

lemma The_optional_eq_SomeD: "The_optional P = Some x ⟹ P x"
  unfolding The_optional_def
  by (metis option.discI option.inject theI_unique)

lemma Some_eq_The_optionalD: "Some x = The_optional P ⟹ P x"
  using The_optional_eq_SomeD by metis

lemma The_optional_eq_NoneD: "The_optional P = None ⟹ ∄!x. P x"
  unfolding The_optional_def
  by (metis option.discI)

lemma None_eq_The_optionalD: "None = The_optional P ⟹ ∄!x. P x"
  unfolding The_optional_def
  by (metis option.discI)

lemma The_optional_eq_SomeI:
  assumes "∃⇩≤⇩1x. P x" and "P x"
  shows "The_optional P = Some x"
  using assms by (metis The_optional_def the1_equality')

end