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')Voption_rel  (v. x=Some v  (v,v')V)"
    "(Some v,x')Voption_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); bbb 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]  lh"
  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