Quelle  Option_Helpers.thy

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