Theory 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 ≤⇓(⟨R⟩option_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 ≤⇓(⟨R⟩option_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