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