Theory Refine_Monadic.Refine_More_Comb

section ‹More Combinators›
theory Refine_More_Comb
imports Refine_Basic Refine_Heuristics Refine_Leof
begin

subsubsection ‹OBTAIN Combinator›

text ‹Obtain value with given property, asserting that there exists one.›  
definition OBTAIN :: "('a  bool)  'a nres" 
  where
  "OBTAIN P  ASSERT (x. P x)  SPEC P"

lemma OBTAIN_nofail[refine_pw_simps]: "nofail (OBTAIN P)  (x. P x)"
  unfolding OBTAIN_def
  by (auto simp: refine_pw_simps)
lemma OBTAIN_inres[refine_pw_simps]: "inres (OBTAIN P) x  (x. ¬P x)  P x"
  unfolding OBTAIN_def
  by (auto simp: refine_pw_simps)
lemma OBTAIN_rule[refine_vcg]: " x. P x; x. P x  Q x    OBTAIN P  SPEC Q"
  unfolding OBTAIN_def
  by auto
lemma OBTAIN_refine_iff: "OBTAIN P R (OBTAIN Q)  (Ex Q  Ex P  Collect P  R¯``Collect Q)"
  unfolding OBTAIN_def by (auto simp: pw_le_iff refine_pw_simps)

lemma OBTAIN_refine[refine]:
  assumes "RELATES R"
  assumes "x. Q x  Ex P"
  assumes "x y. Q x; P y  x'. (y,x')R  Q x'"
  shows "OBTAIN P R (OBTAIN Q)"
  using assms unfolding OBTAIN_refine_iff 
  by blast
  
subsubsection ‹SELECT Combinator›

text ‹Select some value with given property, or None› if there is none.›  
definition SELECT :: "('a  bool)  'a option nres"
  where "SELECT P  if x. P x then RES {Some x| x. P x} else RETURN None"
  
lemma SELECT_rule[refine_vcg]:
  assumes "x. P x  Q (Some x)"
  assumes "x. ¬P x  Q None"
  shows "SELECT P  SPEC Q"
  unfolding SELECT_def
  using assms
  by auto

lemma SELECT_refine_iff: "(SELECT P (Roption_rel) (SELECT P')) 
   (  
    (Ex P'  Ex P) 
    (x. P x  (x'. (x,x')R  P' x'))
  )"  
  by (force simp: SELECT_def pw_le_iff refine_pw_simps) 

lemma SELECT_refine[refine]:
  assumes "RELATES R"
  assumes "x'. P' x'  x. P x"
  assumes "x. P x  x'. (x,x')R  P' x'"
  shows "SELECT P (Roption_rel) (SELECT P')"
  unfolding SELECT_refine_iff using assms by blast

lemma SELECT_as_SPEC: "SELECT P = SPEC (λNone  x. ¬P x | Some x  P x)"
  unfolding SELECT_def by (auto simp: pw_eq_iff split: option.split)

lemma SELECT_pw[refine_pw_simps]:
  "nofail (SELECT P)"  
  "inres (SELECT P) r  (r=None  (x. ¬P x))  (x. r=Some x  P x)"
  unfolding SELECT_def
  by auto

lemma SELECT_pw_simps[simp]:
  "nofail (SELECT P)"
  "inres (SELECT P) None  (x. ¬P x)"
  "inres (SELECT P) (Some x)  P x"
  by (auto simp: refine_pw_simps)

end