Theory Refine_Monadic_Add
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?)
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
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"
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)
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