Theory Exc_Nres_Monad
section ‹Exception Monad for Refine-Monadic›
theory Exc_Nres_Monad
imports "Refine_Monadic.Refine_Monadic" DRAT_Misc
begin
declare TrueI[refine_vcg]
type_synonym ('e,'a) enres = "('e + 'a) nres"
named_theorems enres_unfolds ‹Unfolding theorems from enres to nres›
definition [enres_unfolds]: "ERETURN x ≡ RETURN (Inr x)"
definition ebind :: "('e,'a) enres ⇒ ('a ⇒ ('e,'b) enres) ⇒ ('e,'b) enres"
where [enres_unfolds]:
"ebind m f ≡ do {
x ← m;
case x of Inl e ⇒ RETURN (Inl e) | Inr x ⇒ f x
}"
definition [enres_unfolds]: "THROW e == RETURN (Inl e)"
definition [enres_unfolds]: "ESPEC Φ Ψ ≡ SPEC (λInl e ⇒ Φ e | Inr r ⇒ Ψ r)"
definition [enres_unfolds]: "CATCH m h ≡ do { r←m; case r of Inl e ⇒ h e | Inr r ⇒ RETURN (Inr r) }"
abbreviation (do_notation) bind_doE where "bind_doE ≡ ebind"
notation (output) bind_doE (infixl "⤜" 54)
notation (ASCII output) bind_doE (infixl ">>=" 54)
nonterminal doE_binds and doE_bind
syntax
"_doE_block" :: "doE_binds ⇒ 'a" ("doE {//(2 _)//}" [12] 62)
"_doE_bind" :: "[pttrn, 'a] ⇒ doE_bind" ("(2_ ←/ _)" 13)
"_doE_let" :: "[pttrn, 'a] ⇒ doE_bind" ("(2let _ =/ _)" [1000, 13] 13)
"_doE_then" :: "'a ⇒ doE_bind" ("_" [14] 13)
"_doE_final" :: "'a ⇒ doE_binds" ("_")
"_doE_cons" :: "[doE_bind, doE_binds] ⇒ doE_binds" ("_;//_" [13, 12] 12)
"_thenM" :: "['a, 'b] ⇒ 'c" (infixl "⪢" 54)
syntax (ASCII)
"_doE_bind" :: "[pttrn, 'a] ⇒ doE_bind" ("(2_ <-/ _)" 13)
"_thenM" :: "['a, 'b] ⇒ 'c" (infixl ">>" 54)
translations
"_doE_block (_doE_cons (_doE_then t) (_doE_final e))"
⇌ "CONST bind_doE t (λ_. e)"
"_doE_block (_doE_cons (_doE_bind p t) (_doE_final e))"
⇌ "CONST bind_doE t (λp. e)"
"_doE_block (_doE_cons (_doE_let p t) bs)"
⇌ "let p = t in _doE_block bs"
"_doE_block (_doE_cons b (_doE_cons c cs))"
⇌ "_doE_block (_doE_cons b (_doE_final (_doE_block (_doE_cons c cs))))"
"_doE_cons (_doE_let p t) (_doE_final s)"
⇌ "_doE_final (let p = t in s)"
"_doE_block (_doE_final e)" ⇀ "e"
"(m ⪢ n)" ⇀ "(m ⤜ (λ_. n))"
definition [enres_unfolds]: "CHECK Φ e ≡ if Φ then ERETURN () else THROW e"
definition [enres_unfolds]: "EASSUME Φ ≡ if Φ then ERETURN () else SUCCEED"
definition [enres_unfolds]: "EASSERT Φ ≡ if Φ then ERETURN () else FAIL"
lemma EASSUME_simps[simp]:
"EASSUME True = ERETURN ()"
"EASSUME False = SUCCEED"
unfolding EASSUME_def by auto
lemma EASSERT_simps[simp]:
"EASSERT True = ERETURN ()"
"EASSERT False = FAIL"
unfolding EASSERT_def by auto
lemma CHECK_simps[simp]:
"CHECK True e = ERETURN ()"
"CHECK False e = THROW e"
unfolding CHECK_def by auto
lemma pw_ESPEC[simp, refine_pw_simps]:
"nofail (ESPEC Φ Ψ)"
"inres (ESPEC Φ Ψ) (Inl e) ⟷ Φ e"
"inres (ESPEC Φ Ψ) (Inr x) ⟷ Ψ x"
unfolding enres_unfolds
by auto
lemma pw_ERETURN[simp, refine_pw_simps]:
"nofail (ERETURN x)"
"¬inres (ERETURN x) (Inl e)"
"inres (ERETURN x) (Inr y) ⟷ x=y"
unfolding enres_unfolds
by auto
lemma pw_ebind[refine_pw_simps]:
"nofail (ebind m f) ⟷ nofail m ∧ (∀x. inres m (Inr x) ⟶ nofail (f x))"
"inres (ebind m f) (Inl e) ⟷ inres m (Inl e) ∨ (∃x. inres m (Inr x) ∧ inres (f x) (Inl e))"
"inres (ebind m f) (Inr x) ⟷ nofail m ⟶ (∃y. inres m (Inr y) ∧ inres (f y) (Inr x))"
unfolding enres_unfolds
apply (auto simp: refine_pw_simps split: sum.split)
using sum.exhaust_sel apply blast
using sum.exhaust_sel apply blast
done
lemma pw_THROW[simp,refine_pw_simps]:
"nofail (THROW e)"
"inres (THROW e) (Inl f) ⟷ f=e"
"¬inres (THROW e) (Inr x)"
unfolding enres_unfolds
by (auto simp: refine_pw_simps)
lemma pw_CHECK[simp, refine_pw_simps]:
"nofail (CHECK Φ e)"
"inres (CHECK Φ e) (Inl f) ⟷ ¬Φ ∧ f=e"
"inres (CHECK Φ e) (Inr u) ⟷ Φ"
unfolding enres_unfolds
by (auto simp: refine_pw_simps)
lemma pw_EASSUME[simp, refine_pw_simps]:
"nofail (EASSUME Φ)"
"¬inres (EASSUME Φ) (Inl e)"
"inres (EASSUME Φ) (Inr u) ⟷ Φ"
unfolding EASSUME_def
by (auto simp: refine_pw_simps)
lemma pw_EASSERT[simp, refine_pw_simps]:
"nofail (EASSERT Φ) ⟷ Φ"
"inres (EASSERT Φ) (Inr u)"
"inres (EASSERT Φ) (Inl e) ⟷ ¬Φ"
unfolding EASSERT_def
by (auto simp: refine_pw_simps)
lemma pw_CATCH[refine_pw_simps]:
"nofail (CATCH m h) ⟷ (nofail m ∧ (∀x. inres m (Inl x) ⟶ nofail (h x)))"
"inres (CATCH m h) (Inl e) ⟷ (nofail m ⟶ (∃e'. inres m (Inl e') ∧ inres (h e') (Inl e)))"
"inres (CATCH m h) (Inr x) ⟷ inres m (Inr x) ∨ (∃e. inres m (Inl e) ∧ inres (h e) (Inr x))"
unfolding CATCH_def
apply (auto simp add: refine_pw_simps split: sum.splits)
using sum.exhaust_sel apply blast
using sum.exhaust_sel apply blast
done
lemma pw_ele_iff: "m ≤ n ⟷ (nofail n ⟶
nofail m
∧ (∀e. inres m (Inl e) ⟶ inres n (Inl e))
∧ (∀x. inres m (Inr x) ⟶ inres n (Inr x))
)"
apply (auto simp: pw_le_iff)
by (metis sum.exhaust_sel)
lemma pw_eeq_iff: "m = n ⟷
(nofail m ⟷ nofail n)
∧ (∀e. inres m (Inl e) ⟷ inres n (Inl e))
∧ (∀x. inres m (Inr x) ⟷ inres n (Inr x))"
apply (auto simp: pw_eq_iff)
by (metis sum.exhaust_sel)+
lemma enres_monad_laws[simp]:
"ebind (ERETURN x) f = f x"
"ebind m (ERETURN) = m"
"ebind (ebind m f) g = ebind m (λx. ebind (f x) g)"
by (auto simp: pw_eeq_iff refine_pw_simps)
lemma enres_additional_laws[simp]:
"ebind (THROW e) f = THROW e"
"CATCH (THROW e) h = h e"
"CATCH (ERETURN x) h = ERETURN x"
"CATCH m THROW = m"
apply (auto simp: pw_eeq_iff refine_pw_simps)
done
lemmas ESPEC_trans = order_trans[where z="ESPEC Error_Postcond Normal_Postcond" for Error_Postcond Normal_Postcond, zero_var_indexes]
lemma ESPEC_cons:
assumes "m ≤ ESPEC E Q"
assumes "⋀e. E e ⟹ E' e"
assumes "⋀x. Q x ⟹ Q' x"
shows "m ≤ ESPEC E' Q'"
using assms by (auto simp: pw_ele_iff)
lemma ebind_rule_iff: "doE { x←m; f x } ≤ ESPEC Φ Ψ ⟷ m ≤ ESPEC Φ (λx. f x ≤ ESPEC Φ Ψ)"
by (auto simp: pw_ele_iff refine_pw_simps)
lemmas ebind_rule[refine_vcg] = ebind_rule_iff[THEN iffD2]
lemma ERETURN_rule_iff[simp]: "ERETURN x ≤ ESPEC Φ Ψ ⟷ Ψ x"
by (auto simp: pw_ele_iff refine_pw_simps)
lemmas ERETURN_rule[refine_vcg] = ERETURN_rule_iff[THEN iffD2]
lemma ESPEC_rule_iff: "ESPEC Φ Ψ ≤ ESPEC Φ' Ψ' ⟷ (∀e. Φ e ⟶ Φ' e) ∧ (∀x. Ψ x ⟶ Ψ' x)"
by (auto simp: pw_ele_iff refine_pw_simps)
lemmas ESPEC_rule[refine_vcg] = ESPEC_rule_iff[THEN iffD2]
lemma THROW_rule_iff: "THROW e ≤ ESPEC Φ Ψ ⟷ Φ e"
by (auto simp: pw_ele_iff refine_pw_simps)
lemmas THROW_rule[refine_vcg] = THROW_rule_iff[THEN iffD2]
lemma CATCH_rule_iff: "CATCH m h ≤ ESPEC Φ Ψ ⟷ m ≤ ESPEC (λe. h e ≤ ESPEC Φ Ψ) Ψ"
by (auto simp: pw_ele_iff refine_pw_simps)
lemmas CATCH_rule[refine_vcg] = CATCH_rule_iff[THEN iffD2]
lemma CHECK_rule_iff: "CHECK c e ≤ ESPEC Φ Ψ ⟷ (c ⟶ Ψ ()) ∧ (¬c ⟶ Φ e)"
by (auto simp: pw_ele_iff refine_pw_simps)
lemma CHECK_rule[refine_vcg]:
assumes "c ⟹ Ψ ()"
assumes "¬c ⟹ Φ e"
shows "CHECK c e ≤ ESPEC Φ Ψ"
using assms by (simp add: CHECK_rule_iff)
lemma EASSUME_rule[refine_vcg]: "⟦Φ ⟹ Ψ ()⟧ ⟹ EASSUME Φ ≤ ESPEC E Ψ"
by (cases Φ) auto
lemma EASSERT_rule[refine_vcg]: "⟦Φ; Φ ⟹ Ψ ()⟧ ⟹ EASSERT Φ ≤ ESPEC E Ψ" by auto
lemma eprod_rule[refine_vcg]:
"⟦⋀a b. p=(a,b) ⟹ S a b ≤ ESPEC Φ Ψ⟧ ⟹ (case p of (a,b) ⇒ S a b) ≤ ESPEC Φ Ψ"
by (auto split: prod.split)
lemma eprod2_rule[refine_vcg]:
assumes "⋀a b c d. ⟦ab=(a,b); cd=(c,d)⟧ ⟹ f a b c d ≤ ESPEC Φ Ψ"
shows "(λ(a,b) (c,d). f a b c d) ab cd ≤ ESPEC Φ Ψ"
using assms
by (auto split: prod.split)
lemma eif_rule[refine_vcg]:
"⟦ b ⟹ S1 ≤ ESPEC Φ Ψ; ¬b ⟹ S2 ≤ ESPEC Φ Ψ⟧
⟹ (if b then S1 else S2) ≤ ESPEC Φ Ψ"
by (auto)
lemma eoption_rule[refine_vcg]:
"⟦ v=None ⟹ S1 ≤ ESPEC Φ Ψ; ⋀x. v=Some x ⟹ f2 x ≤ ESPEC Φ Ψ⟧
⟹ case_option S1 f2 v ≤ ESPEC Φ Ψ"
by (auto split: option.split)
lemma eLet_rule[refine_vcg]: "f v ≤ ESPEC Φ Ψ ⟹ (let x=v in f x) ≤ ESPEC Φ Ψ" by simp
lemma eLet_rule':
assumes "⋀x. x=v ⟹ f x ≤ ESPEC Φ Ψ"
shows "Let v (λx. f x) ≤ ESPEC Φ Ψ"
using assms by simp
definition [enres_unfolds]: "EWHILEIT I c f s ≡ WHILEIT
(λInl _ ⇒ True | Inr s ⇒ I s)
(λInl _ ⇒ False | Inr s ⇒ c s)
(λs. ASSERT (¬isl s) ⪢ (let s = projr s in f s))
(Inr s)"
definition [enres_unfolds]: "EWHILET ≡ EWHILEIT (λ_. True)"
lemma EWHILEIT_rule[refine_vcg]:
assumes WF: "wf R"
and I0: "I s⇩0"
and IS: "⋀s. ⟦I s; b s; (s,s⇩0)∈R⇧*⟧ ⟹ f s ≤ ESPEC E (λs'. I s' ∧ (s', s) ∈ R)"
and IMP: "⋀s. ⟦I s; ¬ b s; (s,s⇩0)∈R⇧*⟧ ⟹ Φ s"
shows "EWHILEIT I b f s⇩0 ≤ ESPEC E Φ"
unfolding EWHILEIT_def ESPEC_def
apply (rule order_trans[OF WHILEIT_weaken[where I="λInl e ⇒ E e | Inr s ⇒ I s ∧ (s,s⇩0)∈R⇧*"]])
apply (auto split: sum.splits) []
apply (rule WHILEIT_rule[where R="inv_image (less_than <*lex*> R) (λInl e ⇒ (0,undefined) | Inr s ⇒ (1,s))"])
subgoal using WF by auto
subgoal using I0 by auto
subgoal
apply (clarsimp split: sum.splits simp: ESPEC_def)
apply (rule order_trans[OF IS])
apply (auto simp: ESPEC_def)
done
subgoal using IMP by (auto split: sum.splits)
done
lemma EWHILET_rule:
assumes WF: "wf R"
and I0: "I s⇩0"
and IS: "⋀s. ⟦I s; b s; (s,s⇩0)∈R⇧*⟧ ⟹ f s ≤ ESPEC E (λs'. I s' ∧ (s', s) ∈ R)"
and IMP: "⋀s. ⟦I s; ¬ b s; (s,s⇩0)∈R⇧*⟧ ⟹ Φ s"
shows "EWHILET b f s⇩0 ≤ ESPEC E Φ"
unfolding EWHILET_def EWHILEIT_def ESPEC_def
apply (rule order_trans[OF WHILEIT_weaken[where I="λInl e ⇒ E e | Inr s ⇒ I s ∧ (s,s⇩0)∈R⇧*"]])
apply (auto split: sum.splits) []
apply (rule WHILEIT_rule[where R="inv_image (less_than <*lex*> R) (λInl e ⇒ (0,undefined) | Inr s ⇒ (1,s))"])
subgoal using WF by auto
subgoal using I0 by auto
subgoal
apply (clarsimp split: sum.splits simp: ESPEC_def)
apply (rule order_trans[OF IS])
apply (auto simp: ESPEC_def)
done
subgoal using IMP by (auto split: sum.splits)
done
lemma EWHILEIT_weaken:
assumes "⋀x. I x ⟹ I' x"
shows "EWHILEIT I' b f x ≤ EWHILEIT I b f x"
unfolding enres_unfolds
apply (rule WHILEIT_weaken)
using assms by (auto split: sum.split)
text ‹Explicitly specify a different invariant. ›
lemma EWHILEIT_expinv_rule:
assumes WF: "wf R"
and I0: "I s⇩0"
and IS: "⋀s. ⟦I s; b s; (s,s⇩0)∈R⇧*⟧ ⟹ f s ≤ ESPEC E (λs'. I s' ∧ (s', s) ∈ R)"
and IMP: "⋀s. ⟦I s; ¬ b s; (s,s⇩0)∈R⇧*⟧ ⟹ Φ s"
and INVIMP: "⋀s. I s ⟹ I' s"
shows "EWHILEIT I' b f s⇩0 ≤ ESPEC E Φ"
apply (rule order_trans[OF EWHILEIT_weaken])
using INVIMP apply assumption
apply (rule EWHILEIT_rule; fact+)
done
definition [enres_unfolds]: "enfoldli l c f s ≡
nfoldli l (λInl e⇒False | Inr x ⇒ c x) (λx s. do {ASSERT (¬isl s); let s=projr s; f x s}) (Inr s)"
lemma enfoldli_simps[simp]:
"enfoldli [] c f s = ERETURN s"
"enfoldli (x#ls) c f s =
(if c s then doE { s←f x s; enfoldli ls c f s} else ERETURN s)"
unfolding enres_unfolds
by (auto split: sum.split intro!: arg_cong[where f = "Refine_Basic.bind _"] ext)
lemma enfoldli_rule:
assumes I0: "I [] l0 σ0"
assumes IS: "⋀x l1 l2 σ. ⟦ l0=l1@x#l2; I l1 (x#l2) σ; c σ ⟧ ⟹ f x σ ≤ ESPEC E (I (l1@[x]) l2)"
assumes FNC: "⋀l1 l2 σ. ⟦ l0=l1@l2; I l1 l2 σ; ¬c σ ⟧ ⟹ P σ"
assumes FC: "⋀σ. ⟦ I l0 [] σ; c σ ⟧ ⟹ P σ"
shows "enfoldli l0 c f σ0 ≤ ESPEC E P"
unfolding enfoldli_def ESPEC_def
apply (rule nfoldli_rule[where I="λl1 l2. λInl e ⇒ E e | Inr σ ⇒ I l1 l2 σ"])
subgoal by (auto simp: I0)
subgoal
apply (simp split: sum.splits)
apply (erule (2) order_trans[OF IS])
apply (auto simp: ESPEC_def)
done
subgoal using FNC by (auto split: sum.split)
subgoal using FC by (auto split: sum.split)
done
subsection ‹Data Refinement›
lemma sum_rel_conv:
"(Inl l, s') ∈ ⟨L,R⟩sum_rel ⟷ (∃l'. s'=Inl l' ∧ (l,l')∈L)"
"(Inr r, s') ∈ ⟨L,R⟩sum_rel ⟷ (∃r'. s'=Inr r' ∧ (r,r')∈R)"
"(s, Inl l') ∈ ⟨L,R⟩sum_rel ⟷ (∃l. s=Inl l ∧ (l,l')∈L)"
"(s, Inr r') ∈ ⟨L,R⟩sum_rel ⟷ (∃r. s=Inr r ∧ (r,r')∈R)"
"(∀l. s ≠ Inl l) ⟷ (∃r. s=Inr r)"
"(∀r. s ≠ Inr r) ⟷ (∃l. s=Inl l)"
apply -
subgoal by (cases s'; auto)
subgoal by (cases s'; auto)
subgoal by (cases s; auto)
subgoal by (cases s; auto)
subgoal by (cases s; auto)
subgoal by (cases s; auto)
done
definition econc_fun ("⇓⇩E") where [enres_unfolds]: "econc_fun E R ≡ ⇓(⟨E,R⟩sum_rel)"
lemma RELATES_pat_erefine[refine_dref_pattern]: "⟦RELATES R; mi ≤⇓⇩E E R m ⟧ ⟹ mi ≤⇓⇩E E R m" .
lemma pw_econc_iff[refine_pw_simps]:
"inres (⇓⇩E E R m) (Inl ei) ⟷ (nofail m ⟶ (∃e. inres m (Inl e) ∧ (ei,e)∈E))"
"inres (⇓⇩E E R m) (Inr xi) ⟷ (nofail m ⟶ (∃x. inres m (Inr x) ∧ (xi,x)∈R))"
"nofail (⇓⇩E E R m) ⟷ nofail m"
by (auto simp: refine_pw_simps econc_fun_def sum_rel_conv)
lemma econc_fun_id[simp]: "⇓⇩E Id Id = (λx. x)"
by (auto simp: pw_eeq_iff refine_pw_simps intro!: ext)
lemma econc_fun_ESPEC: "⇓⇩E E R (ESPEC Φ Ψ) = ESPEC (λei. ∃e. (ei,e)∈E ∧ Φ e) (λri. ∃r. (ri,r)∈R ∧ Ψ r)"
by (auto simp: pw_eeq_iff refine_pw_simps)
lemma econc_fun_ERETURN: "⇓⇩E E R (ERETURN x) = ESPEC (λ_. False) (λxi. (xi,x)∈R)"
by (auto simp: pw_eeq_iff refine_pw_simps)
lemma econc_fun_univ_id[simp]: "⇓⇩E UNIV Id (ESPEC Φ Ψ) = ESPEC (λ_. Ex Φ) Ψ"
by (auto simp: pw_eeq_iff refine_pw_simps)
lemma erefine_same_sup_Id[simp]: "⟦ Id⊆E; Id⊆R ⟧ ⟹ m ≤⇓⇩E E R m" by (auto simp: pw_ele_iff refine_pw_simps)
lemma econc_mono3: "m≤m' ⟹ ⇓⇩E E R m ≤ ⇓⇩E E R m'"
by (auto simp: pw_ele_iff refine_pw_simps)
lemma econc_x_trans[trans]:
"x ≤ ⇓⇩E E R y ⟹ y ≤ z ⟹ x ≤ ⇓⇩E E R z"
by (force simp: pw_ele_iff refine_pw_simps)
lemma econc_econc_trans[trans]:
"x ≤⇓⇩E E1 R1 y ⟹ y ≤ ⇓⇩E E2 R2 z ⟹ x ≤ ⇓⇩E (E1 O E2) (R1 O R2) z"
by (force simp: pw_ele_iff refine_pw_simps)
lemma ERETURN_refine[refine]:
assumes "(xi,x)∈R"
shows "ERETURN xi ≤ ⇓⇩EE R (ERETURN x)"
using assms
by (auto simp: pw_ele_iff refine_pw_simps)
lemma EASSERT_bind_refine_right:
assumes "Φ ⟹ mi ≤⇓⇩E E R m"
shows "mi ≤⇓⇩E E R (doE {EASSERT Φ; m})"
using assms
by (simp add: pw_ele_iff refine_pw_simps)
lemma EASSERT_bind_refine_left:
assumes "Φ"
assumes "mi ≤⇓⇩E E R m"
shows "(doE {EASSERT Φ; mi}) ≤⇓⇩E E R m"
using assms
by simp
lemma EASSUME_bind_refine_right:
assumes "Φ"
assumes "mi ≤⇓⇩E E R m"
shows "mi ≤⇓⇩E E R (doE {EASSUME Φ; m})"
using assms
by (simp)
lemma EASSUME_bind_refine_left:
assumes "Φ ⟹ mi ≤⇓⇩E E R m"
shows "(doE {EASSUME Φ; mi}) ≤⇓⇩E E R m"
using assms
by (simp add: pw_ele_iff refine_pw_simps)
lemma ebind_refine:
assumes "mi ≤⇓⇩E E R' m"
assumes "⋀xi x. (xi,x)∈R' ⟹ fi xi ≤⇓⇩E E R (f x)"
shows "doE { xi ← mi; fi xi } ≤ ⇓⇩E E R (doE { x ← m; f x })"
using assms
by (simp add: pw_ele_iff refine_pw_simps) blast
text ‹Order of this lemmas matters!›
lemmas [refine] =
ebind_refine
EASSERT_bind_refine_left EASSUME_bind_refine_right
EASSUME_bind_refine_left EASSERT_bind_refine_right
thm refine(1-10)
lemma ebind_refine':
assumes "mi ≤⇓⇩E E R' m"
assumes "⋀xi x. ⟦(xi,x)∈R'; inres mi (Inr xi); inres m (Inr x); nofail mi; nofail m⟧ ⟹ fi xi ≤⇓⇩E E R (f x)"
shows "doE { xi ← mi; fi xi } ≤ ⇓⇩E E R (doE { x ← m; f x })"
using assms
by (simp add: pw_ele_iff refine_pw_simps) blast
lemma THROW_refine[refine]: "(ei,e)∈E ⟹ THROW ei ≤⇓⇩E E R (THROW e)"
by (auto simp: pw_ele_iff refine_pw_simps)
lemma CATCH_refine':
assumes "mi ≤ ⇓⇩E E' R m"
assumes "⋀ei e. ⟦ (ei,e)∈E'; inres mi (Inl ei); inres m (Inl e); nofail mi; nofail m ⟧ ⟹ hi ei ≤⇓⇩E E R (h e)"
shows "CATCH mi hi ≤ ⇓⇩E E R (CATCH m h)"
using assms
by (simp add: pw_ele_iff refine_pw_simps) blast
lemma CATCH_refine[refine]:
assumes "mi ≤ ⇓⇩E E' R m"
assumes "⋀ei e. ⟦ (ei,e)∈E' ⟧ ⟹ hi ei ≤⇓⇩E E R (h e)"
shows "CATCH mi hi ≤ ⇓⇩E E R (CATCH m h)"
using assms CATCH_refine' by metis
lemma CHECK_refine[refine]:
assumes "Φi ⟷ Φ"
assumes "¬Φ ⟹ (msgi,msg)∈E"
shows "CHECK Φi msgi ≤⇓⇩E E Id (CHECK Φ msg)"
using assms by (auto simp: pw_ele_iff refine_pw_simps)
text ‹This must be declared after @{thm CHECK_refine}!›
lemma CHECK_bind_refine[refine]:
assumes "Φi ⟷ Φ"
assumes "¬Φ ⟹ (msgi,msg)∈E"
assumes "Φ ⟹ mi ≤⇓⇩E E R m"
shows "doE {CHECK Φi msgi;mi} ≤⇓⇩E E R (doE {CHECK Φ msg; m})"
using assms by (auto simp: pw_ele_iff refine_pw_simps)
lemma Let_unfold_refine[refine]:
assumes "f x ≤ ⇓⇩E E R (f' x')"
shows "Let x f ≤ ⇓⇩E E R (Let x' f')"
using assms by auto
lemma Let_refine:
assumes "(m,m')∈R'"
assumes "⋀x x'. (x,x')∈R' ⟹ f x ≤ ⇓⇩E E R (f' x')"
shows "Let m (λx. f x) ≤⇓⇩E E R (Let m' (λx'. f' x'))"
using assms by auto
lemma eif_refine[refine]:
assumes "(b,b')∈bool_rel"
assumes "⟦b;b'⟧ ⟹ S1 ≤ ⇓⇩E E R S1'"
assumes "⟦¬b;¬b'⟧ ⟹ S2 ≤ ⇓⇩E E R S2'"
shows "(if b then S1 else S2) ≤ ⇓⇩E E R (if b' then S1' else S2')"
using assms by auto
lemma enfoldli_refine[refine]:
assumes "(li, l) ∈ ⟨S⟩list_rel"
and "(si, s) ∈ R"
and CR: "(ci, c) ∈ R → bool_rel"
and FR: "⋀xi x si s. ⟦ (xi,x)∈S; (si,s)∈R; c s ⟧ ⟹ fi xi si ≤ ⇓⇩E E R (f x s)"
shows "enfoldli li ci fi si ≤ ⇓⇩E E R (enfoldli l c f s)"
unfolding enres_unfolds
apply (rule nfoldli_refine)
apply (rule assms(1))
apply (simp add: assms(2))
subgoal using CR[param_fo] by (auto split: sum.split simp: sum_rel_conv)
subgoal
apply refine_rcg
applyS (auto split: sum.splits simp: sum_rel_conv)
apply (rule FR[unfolded enres_unfolds])
by (auto split: sum.splits simp: sum_rel_conv)
done
lemma EWHILET_refine[refine]:
assumes R0: "(x,x')∈R"
assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R ⟧ ⟹ b x = b' x'"
assumes STEP_REF:
"⋀x x'. ⟦ (x,x')∈R; b x; b' x' ⟧ ⟹ f x ≤ ⇓⇩E E R (f' x')"
shows "EWHILET b f x ≤⇓⇩E E R (EWHILET b' f' x')"
unfolding enres_unfolds
apply refine_rcg
using assms
by (auto split: sum.splits simp: econc_fun_def)
thm WHILEIT_refine
lemma EWHILEIT_refine[refine]:
assumes R0: "I' x' ⟹ (x,x')∈R"
assumes I_REF: "⋀x x'. ⟦ (x,x')∈R; I' x' ⟧ ⟹ 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 ≤ ⇓⇩E E R (f' x')"
shows "EWHILEIT I b f x ≤⇓⇩E E R (EWHILEIT I' b' f' x')"
unfolding enres_unfolds
apply refine_rcg
using assms
by (auto split: sum.splits simp: econc_fun_def)
subsubsection ‹Refine2- heuristics›
lemma remove_eLet_refine:
assumes "M ≤ ⇓⇩E E R (f x)"
shows "M ≤ ⇓⇩E E R (Let x f)" using assms by auto
lemma intro_eLet_refine:
assumes "f x ≤ ⇓⇩E E R M'"
shows "Let x f ≤ ⇓⇩E E R M'" using assms by auto
lemma ebind2let_refine[refine2]:
assumes "ERETURN x ≤ ⇓⇩E E R' M'"
assumes "⋀x'. (x,x')∈R' ⟹ f x ≤ ⇓⇩E E R (f' x')"
shows "Let x f ≤ ⇓⇩E E R (ebind M' (λx'. f' x'))"
using assms
apply (simp add: pw_ele_iff refine_pw_simps)
apply fast
done
lemma ebind_Let_refine2[refine2]: "⟦
m' ≤⇓⇩E E R' (ERETURN x);
⋀x'. ⟦inres m' (Inr x'); (x',x)∈R'⟧ ⟹ f' x' ≤ ⇓⇩E E R (f x)
⟧ ⟹ ebind m' (λx'. f' x') ≤ ⇓⇩E E R (Let x (λx. f x))"
apply (simp add: pw_ele_iff refine_pw_simps)
apply blast
done
lemma ebind2letRETURN_refine[refine2]:
assumes "ERETURN x ≤ ⇓⇩E E R' M'"
assumes "⋀x'. (x,x')∈R' ⟹ ERETURN (f x) ≤ ⇓⇩E E R (f' x')"
shows "ERETURN (Let x f) ≤ ⇓⇩E E R (ebind M' (λx'. f' x'))"
using assms
apply (simp add: pw_ele_iff refine_pw_simps)
apply fast
done
lemma ERETURN_as_SPEC_refine[refine2]:
assumes "RELATES R"
assumes "M ≤ ESPEC (λ_. False) (λc. (c,a)∈R)"
shows "M ≤ ⇓⇩E E R (ERETURN a)"
using assms
by (simp add: pw_ele_iff refine_pw_simps)
lemma if_ERETURN_refine[refine2]:
assumes "b ⟷ b'"
assumes "⟦b;b'⟧ ⟹ ERETURN S1 ≤ ⇓⇩E E R S1'"
assumes "⟦¬b;¬b'⟧ ⟹ ERETURN S2 ≤ ⇓⇩E E R S2'"
shows "ERETURN (if b then S1 else S2) ≤ ⇓⇩E E R (if b' then S1' else S2')"
using assms
by (simp add: pw_le_iff refine_pw_simps)
text ‹Breaking down enres-monad ›
definition enres_lift :: "'a nres ⇒ (_,'a) enres" where
"enres_lift m ≡ do { x ← m; RETURN (Inr x) }"
lemma enres_lift_rule[refine_vcg]: "m≤SPEC Φ ⟹ enres_lift m ≤ ESPEC E Φ"
by (auto simp: pw_ele_iff pw_le_iff refine_pw_simps enres_lift_def)
named_theorems_rev enres_breakdown
lemma [enres_breakdown]:
"ERETURN x = enres_lift (RETURN x)"
"EASSERT Φ = enres_lift (ASSERT Φ)"
"doE { x ← enres_lift m; ef x } = do { x ← m; ef x }"
unfolding enres_unfolds enres_lift_def
apply (auto split: sum.splits simp: pw_eq_iff refine_pw_simps)
done
lemma [enres_breakdown]:
"do { x ← m; enres_lift (f x) } = enres_lift (do { x ← m; f x })"
"do { let x = v; enres_lift (f x) } = enres_lift (do { let x=v; f x })"
unfolding enres_unfolds enres_lift_def
apply (auto split: sum.splits simp: pw_eq_iff refine_pw_simps)
done
lemma [enres_breakdown]:
"CATCH (enres_lift m) h = enres_lift m"
unfolding enres_unfolds enres_lift_def
apply (auto split: sum.splits simp: pw_eq_iff refine_pw_simps)
done
lemma enres_lift_fail[simp]: "enres_lift FAIL = FAIL"
unfolding enres_lift_def by auto
lemma [enres_breakdown]: "EWHILEIT I c (λs. enres_lift (f s)) s = enres_lift (WHILEIT I c f s)"
(is "?lhs = ?rhs")
proof (rule antisym)
show "?lhs ≤ ?rhs"
unfolding enres_unfolds WHILEIT_def WHILET_def
apply (rule RECT_transfer_rel'[where P="λc a. c = Inr a"])
apply (simp add: while.WHILEI_body_trimono)
apply (simp add: while.WHILEI_body_trimono)
apply simp
apply simp
by (auto simp: WHILEI_body_def enres_lift_def pw_le_iff refine_pw_simps)
show "?rhs ≤ ?lhs"
unfolding enres_unfolds WHILEIT_def WHILET_def
apply (rule RECT_transfer_rel'[where P="λa c. c = Inr a"])
apply (simp add: while.WHILEI_body_trimono)
apply (simp add: while.WHILEI_body_trimono)
apply simp
apply simp
by (auto simp: WHILEI_body_def enres_lift_def pw_le_iff refine_pw_simps)
qed
lemma [enres_breakdown]: "EWHILET c (λs. enres_lift (f s)) s = enres_lift (WHILET c f s)"
unfolding EWHILET_def WHILET_def enres_breakdown ..
lemma [enres_breakdown]: "enfoldli l c (λx s. enres_lift (f x s)) s = enres_lift (nfoldli l c f s)"
apply (induction l arbitrary: s)
by (auto simp: enres_breakdown)
lemma [enres_breakdown]:
"(λ(a,b). enres_lift (f a b)) = (λx. enres_lift (case x of (a,b) ⇒ f a b))" by auto
lemmas [enres_breakdown] = nres_monad_laws nres_bind_let_law
lemma [enres_breakdown]:
"doE { CHECK Φ e; m } = (if Φ then m else THROW e)"
by (auto simp: enres_unfolds)
lemma [enres_breakdown]: "(if b then enres_lift m else enres_lift n) = enres_lift (if b then m else n)"
by simp
lemma option_case_enbd[enres_breakdown]:
"case_option (enres_lift fn) (λv. enres_lift (fs v)) = (λx. enres_lift (case_option fn fs x))"
by (auto split: option.split)
named_theorems enres_inline
method opt_enres_unfold = ((unfold enres_inline)?; (unfold enres_monad_laws)?; (unfold enres_breakdown)?; (rule refl)?; (unfold enres_unfolds enres_lift_def nres_monad_laws)?; (rule refl)?)
subsection ‹More Combinators›
subsubsection ‹CHECK-Monadic›
definition [enres_unfolds]: "CHECK_monadic c e ≡ doE { b ← c; CHECK b e }"
lemma CHECK_monadic_rule_iff:
"(CHECK_monadic c e ≤ ESPEC E P) ⟷ (c ≤ ESPEC E (λr. (r ⟶ P ()) ∧ (¬r ⟶ E e)))"
by (auto simp: pw_ele_iff CHECK_monadic_def refine_pw_simps)
lemma CHECK_monadic_pw[refine_pw_simps]:
"nofail (CHECK_monadic c e) ⟷ nofail c"
"inres (CHECK_monadic c e) (Inl ee) ⟷ (inres c (Inl ee) ∨ inres c (Inr False) ∧ ee=e)"
"inres (CHECK_monadic c e) (Inr x) ⟷ (inres c (Inr True))"
unfolding CHECK_monadic_def
by (auto simp: refine_pw_simps)
lemma CHECK_monadic_rule[refine_vcg]:
assumes "c ≤ ESPEC E (λr. (r ⟶ P ()) ∧ (¬r ⟶ E e))"
shows "CHECK_monadic c e ≤ ESPEC E P"
using assms by (simp add: CHECK_monadic_rule_iff)
lemma CHECK_monadic_refine[refine]:
assumes "ci ≤ ⇓⇩E ER bool_rel c"
assumes "(ei,e)∈ER"
shows "CHECK_monadic ci ei ≤⇓⇩E ER unit_rel (CHECK_monadic c e)"
using assms
by (auto simp: pw_ele_iff refine_pw_simps)
lemma CHECK_monadic_CHECK_refine[refine]:
assumes "ci ≤ ESPEC (λe'. (e',e)∈ER ∧ ¬c) (λr. r ⟷ c)"
assumes "(ei,e)∈ER"
shows "CHECK_monadic ci ei ≤⇓⇩E ER unit_rel (CHECK c e)"
using assms
by (auto simp: pw_ele_iff refine_pw_simps)
lemma CHECK_monadic_endb[enres_breakdown]: "CHECK_monadic (enres_lift c) e =
do {b ← c; CHECK b e}"
by (auto simp: enres_unfolds enres_lift_def)
end