Theory SepLogic_Misc

theory SepLogic_Misc
imports SepLog_Misc DataRefinement
begin


    
subsection {* Relators *} 
  
definition nrest_rel where 
  nres_rel_def_internal: "nrest_rel R ≡ {(c,a). c ≤ ⇓R a}"

lemma nrest_rel_def: "⟨R⟩nrest_rel ≡ {(c,a). c ≤ ⇓R a}"
  by (simp add: nres_rel_def_internal relAPP_def)

lemma nrest_relD: "(c,a)∈⟨R⟩nrest_rel ⟹ c ≤⇓R a" by (simp add: nrest_rel_def)
lemma nrest_relI: "c ≤⇓R a ⟹ (c,a)∈⟨R⟩nrest_rel" by (simp add: nrest_rel_def)

lemma nrest_rel_comp: "⟨A⟩nrest_rel O ⟨B⟩nrest_rel = ⟨A O B⟩nrest_rel"
  by (auto simp: nrest_rel_def conc_fun_chain[symmetric] conc_trans)

lemma pw_nrest_rel_iff: "(a,b)∈⟨A⟩nrest_rel ⟷ nofailT (⇓ A b) ⟶ nofailT a ∧ (∀x t. inresT a x t ⟶ inresT (⇓ A b) x t)"
  by (simp add: pw_le_iff nrest_rel_def)
    
     

lemma param_FAIL[param]: "(FAILT,FAILT) ∈ ⟨R⟩nrest_rel"
  by (auto simp: nrest_rel_def)
 

lemma param_RETURN[param]: 
  "(RETURNT,RETURNT) ∈ R → ⟨R⟩nrest_rel"
  by (auto simp: nrest_rel_def RETURNT_refine)

lemma param_bind[param]:
  "(bindT,bindT) ∈ ⟨Ra⟩nrest_rel → (Ra→⟨Rb⟩nrest_rel) → ⟨Rb⟩nrest_rel"
  by (auto simp: nrest_rel_def intro: bindT_refine dest: fun_relD)


end