Theory Refine_Monadic_Add

(* TODO: Move to Refine-Monadic *)
theory Refine_Monadic_Add
imports Refine_Monadic_Thin
begin

  lemma bind_res_singleton[simp]: "bind (RES {x}) f = f x"
    by (auto simp: pw_eq_iff refine_pw_simps)



  lemma option_rel_inv_conv:
    "(x,Some v')∈⟨V⟩option_rel ⟷ (∃v. x=Some v ∧ (v,v')∈V)"
    "(Some v,x')∈⟨V⟩option_rel ⟷ (∃v'. x'=Some v' ∧ (v,v')∈V)"
    subgoal by (cases x; auto)
    subgoal by (cases x'; auto)
    done



  definition "monadic_WHILEIT I b f s ≡ do {
    RECT (λD s. do {
      ASSERT (I s);
      bv ← b s;
      if bv then do {
        s ← f s;
        D s
      } else do {RETURN s}
    }) s
  }"
  
  
  
  lemma WHILEIT_to_monadic: "WHILEIT I b f s = monadic_WHILEIT I (λs. RETURN (b s)) f s"
    unfolding WHILEIT_def monadic_WHILEIT_def
    unfolding WHILEI_body_def bind_ASSERT_eq_if
    by (simp cong: if_cong)
  

lemma monadic_WHILEIT_refine[refine]:  
  assumes [refine]: "(s',s) ∈ R"
  assumes [refine]: "⋀s' s. ⟦ (s',s)∈R; I s ⟧ ⟹ I' s'"  
  assumes [refine]: "⋀s' s. ⟦ (s',s)∈R; I s; I' s' ⟧ ⟹ b' s' ≤⇓bool_rel (b s)"
  assumes [refine]: "⋀s' s. ⟦ (s',s)∈R; I s; I' s'; nofail (b s); inres (b s) True ⟧ ⟹ f' s' ≤⇓R (f s)"
  shows "monadic_WHILEIT I' b' f' s' ≤⇓R (monadic_WHILEIT I b f s)"
  unfolding monadic_WHILEIT_def
  by (refine_rcg bind_refine'; assumption?; auto)
  
lemma monadic_WHILEIT_refine_WHILEIT[refine]:  
  assumes [refine]: "(s',s) ∈ R"
  assumes [refine]: "⋀s' s. ⟦ (s',s)∈R; I s ⟧ ⟹ I' s'"  
  assumes [THEN order_trans,refine_vcg]: "⋀s' s. ⟦ (s',s)∈R; I s; I' s' ⟧ ⟹ b' s' ≤ SPEC (λr. r = b s)"
  assumes [refine]: "⋀s' s. ⟦ (s',s)∈R; I s; I' s'; b s ⟧ ⟹ f' s' ≤⇓R (f s)"
  shows "monadic_WHILEIT I' b' f' s' ≤⇓R (WHILEIT I b f s)"
  unfolding WHILEIT_to_monadic
  by (refine_vcg; assumption?; auto)
  
lemma monadic_WHILEIT_refine_WHILET[refine]:  
  assumes [refine]: "(s',s) ∈ R"
  assumes [THEN order_trans,refine_vcg]: "⋀s' s. ⟦ (s',s)∈R ⟧ ⟹ b' s' ≤ SPEC (λr. r = b s)"
  assumes [refine]: "⋀s' s. ⟦ (s',s)∈R; b s ⟧ ⟹ f' s' ≤⇓R (f s)"
  shows "monadic_WHILEIT (λ_. True) b' f' s' ≤⇓R (WHILET b f s)"
  unfolding WHILET_def
  by (refine_vcg; assumption?)  


(* TODO: Move *)    
lemma monadic_WHILEIT_unfold:
  "monadic_WHILEIT I b f s = do { ASSERT (I s); bb←b s; if bb then do { s ← f s; monadic_WHILEIT I b f s } else RETURN s }"      
  unfolding monadic_WHILEIT_def
  apply (subst RECT_unfold)
  apply refine_mono
  by simp



(* TODO: Move *)
lemma WHILEIT_refine_new_invar':
  assumes R0: "I' x' ⟹ (x,x')∈R"
  assumes INV0: "⟦ I' x'; (x,x')∈R ⟧ ⟹ I x"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R; I x; I' x' ⟧ ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I x; I' x' ⟧ ⟹ f x ≤ ⇓R (f' x')"
  assumes STEP_INV: 
    "⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I x; I' x' ⟧ ⟹ f x ≤⇩n SPEC I"
  shows "WHILEIT I b f x ≤⇓R (WHILEIT I' b' f' x')"
  apply (rule WHILEIT_refine_genR[where 
    I=I and I'=I' and x'=x' and x=x and R=R and b=b and b'=b' and f'=f' and f=f
    and R'="{ (c,a). (c,a)∈R ∧ I c }"
    ])
  using assms STEP_INV[THEN leofD[rotated]]
  by (auto intro: add_invar_refineI)
  


abbreviation (do_notation) bind_doN where "bind_doN ≡ Refine_Basic.bind"

notation (output) bind_doN (infixr "⤜" 54)
notation (ASCII output) bind_doN (infixr ">>=" 54)

nonterminal doN_binds and doN_bind
syntax
  "_doN_block" :: "doN_binds ⇒ 'a" ("doN {//(2  _)//}" [12] 62)
  "_doN_bind"  :: "[pttrn, 'a] ⇒ doN_bind" ("(2_ ←/ _)" 13)
  "_doN_let" :: "[pttrn, 'a] ⇒ doN_bind" ("(2let _ =/ _)" [1000, 13] 13)
  "_doN_then" :: "'a ⇒ doN_bind" ("_" [14] 13)
  "_doN_final" :: "'a ⇒ doN_binds" ("_")
  "_doN_cons" :: "[doN_bind, doN_binds] ⇒ doN_binds" ("_;//_" [13, 12] 12)
  "_thenM" :: "['a, 'b] ⇒ 'c" (infixr "⪢" 54)

syntax (ASCII)
  "_doN_bind" :: "[pttrn, 'a] ⇒ doN_bind" ("(2_ <-/ _)" 13)
  "_thenM" :: "['a, 'b] ⇒ 'c" (infixr ">>" 54)

translations
  "_doN_block (_doN_cons (_doN_then t) (_doN_final e))"
    ⇌ "CONST bind_doN t (λ_. e)"
  "_doN_block (_doN_cons (_doN_bind p t) (_doN_final e))"
    ⇌ "CONST bind_doN t (λp. e)"
  "_doN_block (_doN_cons (_doN_let p t) bs)"
    ⇌ "let p = t in _doN_block bs"
  "_doN_block (_doN_cons b (_doN_cons c cs))"
    ⇌ "_doN_block (_doN_cons b (_doN_final (_doN_block (_doN_cons c cs))))"
  "_doN_cons (_doN_let p t) (_doN_final s)"
    ⇌ "_doN_final (let p = t in s)"
  "_doN_block (_doN_final e)" ⇀ "e"
(*  "(m ⪢ n)" ⇀ "(m ⤜ (λ_. n))"*)



lemma Nil_eq_upt_conv: "[] = [l..<h] ⟷ l≥h"
  by (metis upt_eq_Nil_conv zero_le)

lemma eq_upt_Cons_conv: "ll#xs = [l..<h] ⟷ (l<h ∧ ll=l ∧ xs = [l+1..<h])"
  by (metis upt_eq_Cons_conv)
  
(* TODO: Move! Ultimately, we want sepref-rules and a foreach-statement *)  
lemma nfoldli_upt_by_while:
  "nfoldli [l..<h] c f σ =
  doN { (_,σ)←WHILET (λ(i,σ). i<h ∧ c σ) (λ(i,σ). doN { σ ← f i σ; ASSERT (i<h); RETURN (i+1,σ) }) (l,σ); RETURN σ }
  "
proof (induction "[l..<h]" arbitrary: l σ)
  case Nil thus ?case
    apply (simp add: Nil_eq_upt_conv)
    apply (subst WHILET_unfold)
    by simp
next
  case (Cons ll xs)
  
  from Cons.hyps(2)[symmetric] have [simp]: "l<h" and [simp]: "ll=l" "[l..<h] = l#[l+1..<h]" "xs=[l+1..<h]"
    by (auto simp: upt_eq_Cons_conv)
  
  note IH = Cons.hyps(1)[of "Suc l",simplified,abs_def]  
    
  from Cons.hyps(2) show ?case
    apply (subst WHILET_unfold)
    apply (auto simp add: IH)
    done
    
qed    

  
end