Theory ROBDD.Option_Helpers

section‹Option Helpers›
text‹These definitions were contributed by Peter Lammich.›
theory Option_Helpers
imports Main "HOL-Library.Monad_Syntax"
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