# Theory Option_Helpers

theory Option_Helpers
```section‹Option Helpers›
text‹These definitions were contributed by Peter Lammich.›
theory Option_Helpers
begin

primrec oassert :: "bool ⇒ unit option" where
"oassert True = Some ()" | "oassert False = None"

lemma oassert_iff[simp]:
"oassert Φ = Some x ⟷ Φ"
"oassert Φ = None ⟷ ¬Φ"
by (cases Φ) auto

text‹The idea is that we want the result of some computation to be @{term "Some v"} and the contents of @{term v} to satisfy some property @{term Q}.›

primrec ospec :: "('a option) ⇒ ('a ⇒ bool) ⇒ bool" where
"ospec None _ = False"
| "ospec (Some v) Q = Q v"

named_theorems ospec_rules

lemma oreturn_rule[ospec_rules]: "⟦ P r ⟧ ⟹ ospec (Some r) P" by simp

lemma obind_rule[ospec_rules]: "⟦ ospec m Q; ⋀r. Q r ⟹ ospec (f r) P ⟧ ⟹ ospec (m ⤜ f) P"
apply (cases m)
apply (auto split: Option.bind_splits)
done

lemma ospec_alt: "ospec m P = (case m of None ⇒ False | Some x ⇒ P x)"
by (auto split: option.splits)

lemma ospec_bind_simp: "ospec (m ⤜ f) P ⟷ (ospec m (λr. ospec (f r) P))"
apply (cases m)
apply (auto split: Option.bind_splits)
done

lemma ospec_cons:
assumes "ospec m Q"
assumes "⋀r. Q r ⟹ P r"
shows "ospec m P"
using assms by (cases m) auto

lemma oreturn_synth: "ospec (Some x) (λr. r=x)" by simp

lemma ospecD: "ospec x P ⟹ x = Some y ⟹ P y" by simp
lemma ospecD2: "ospec x P ⟹ ∃y. x = Some y ∧ P y" by(cases x) simp_all

end
```