Theory Refine_Basic
section ‹Basic Concepts›
theory Refine_Basic
imports Main
"HOL-Library.Monad_Syntax"
Refine_Misc
"Generic/RefineG_Recursion"
"Generic/RefineG_Assert"
begin
subsection ‹Nondeterministic Result Lattice and Monad›
text ‹
In this section we introduce a complete lattice of result sets with an
additional top element that represents failure. On this lattice, we define
a monad: The return operator models a result that consists of a single value,
and the bind operator models applying a function to all results.
Binding a failure yields always a failure.
In addition to the return operator, we also introduce the operator
‹RES›, that embeds a set of results into our lattice. Its synonym for
a predicate is ‹SPEC›.
Program correctness is expressed by refinement, i.e., the expression
‹M ≤ SPEC Φ› means that ‹M› is correct w.r.t.\
specification ‹Φ›. This suggests the following view on the program
lattice: The top-element is the result that is never correct. We call this
result ‹FAIL›. The bottom element is the program that is always correct.
It is called ‹SUCCEED›. An assertion can be encoded by failing if the
asserted predicate is not true. Symmetrically, an assumption is encoded by
succeeding if the predicate is not true.
›
datatype 'a nres = FAILi | RES "'a set"
text ‹
‹FAILi› is only an internal notation, that should not be exposed to
the user.
Instead, ‹FAIL› should be used, that is defined later as abbreviation
for the top element of the lattice.
›
instantiation nres :: (type) complete_lattice
begin
fun less_eq_nres where
"_ ≤ FAILi ⟷ True" |
"(RES a) ≤ (RES b) ⟷ a⊆b" |
"FAILi ≤ (RES _) ⟷ False"
fun less_nres where
"FAILi < _ ⟷ False" |
"(RES _) < FAILi ⟷ True" |
"(RES a) < (RES b) ⟷ a⊂b"
fun sup_nres where
"sup _ FAILi = FAILi" |
"sup FAILi _ = FAILi" |
"sup (RES a) (RES b) = RES (a∪b)"
fun inf_nres where
"inf x FAILi = x" |
"inf FAILi x = x" |
"inf (RES a) (RES b) = RES (a∩b)"
definition "Sup X ≡ if FAILi∈X then FAILi else RES (⋃{x . RES x ∈ X})"
definition "Inf X ≡ if ∃x. RES x∈X then RES (⋂{x . RES x ∈ X}) else FAILi"
definition "bot ≡ RES {}"
definition "top ≡ FAILi"
instance
apply (intro_classes)
unfolding Sup_nres_def Inf_nres_def bot_nres_def top_nres_def
apply (case_tac x, case_tac [!] y, auto) []
apply (case_tac x, auto) []
apply (case_tac x, case_tac [!] y, case_tac [!] z, auto) []
apply (case_tac x, (case_tac [!] y)?, auto) []
apply (case_tac x, (case_tac [!] y)?, simp_all) []
apply (case_tac x, (case_tac [!] y)?, auto) []
apply (case_tac x, case_tac [!] y, case_tac [!] z, auto) []
apply (case_tac x, (case_tac [!] y)?, auto) []
apply (case_tac x, (case_tac [!] y)?, auto) []
apply (case_tac x, case_tac [!] y, case_tac [!] z, auto) []
apply (case_tac x, auto) []
apply (case_tac z, fastforce+) []
apply (case_tac x, auto) []
apply (case_tac z, fastforce+) []
apply auto []
apply auto []
done
end
abbreviation "FAIL ≡ top::'a nres"
abbreviation "SUCCEED ≡ bot::'a nres"
abbreviation "SPEC Φ ≡ RES (Collect Φ)"
definition "RETURN x ≡ RES {x}"
text ‹We try to hide the original ‹FAILi›-element as well as possible.
›
lemma nres_cases[case_names FAIL RES, cases type]:
obtains "M=FAIL" | X where "M=RES X"
apply (cases M, fold top_nres_def) by auto
lemma nres_simp_internals:
"RES {} = SUCCEED"
"FAILi = FAIL"
unfolding top_nres_def bot_nres_def by simp_all
lemma nres_inequalities[simp]:
"FAIL ≠ RES X"
"FAIL ≠ SUCCEED"
"FAIL ≠ RETURN x"
"SUCCEED ≠ FAIL"
"SUCCEED ≠ RETURN x"
"RES X ≠ FAIL"
"RETURN x ≠ FAIL"
"RETURN x ≠ SUCCEED"
unfolding top_nres_def bot_nres_def RETURN_def
by auto
lemma nres_more_simps[simp]:
"SUCCEED = RES X ⟷ X={}"
"RES X = SUCCEED ⟷ X={}"
"RES X = RETURN x ⟷ X={x}"
"RES X = RES Y ⟷ X=Y"
"RETURN x = RES X ⟷ {x}=X"
"RETURN x = RETURN y ⟷ x=y"
unfolding top_nres_def bot_nres_def RETURN_def by auto
lemma nres_order_simps[simp]:
"⋀M. SUCCEED ≤ M"
"⋀M. M ≤ SUCCEED ⟷ M=SUCCEED"
"⋀M. M ≤ FAIL"
"⋀M. FAIL ≤ M ⟷ M=FAIL"
"⋀X Y. RES X ≤ RES Y ⟷ X≤Y"
"⋀X. Sup X = FAIL ⟷ FAIL∈X"
"⋀X f. Sup (f ` X) = FAIL ⟷ FAIL ∈ f ` X"
"⋀X. FAIL = Sup X ⟷ FAIL∈X"
"⋀X f. FAIL = Sup (f ` X) ⟷ FAIL ∈ f ` X"
"⋀X. FAIL∈X ⟹ Sup X = FAIL"
"⋀X. FAIL∈f ` X ⟹ Sup (f ` X) = FAIL"
"⋀A. Sup (RES ` A) = RES (Sup A)"
"⋀A. Sup (RES ` A) = RES (Sup A)"
"⋀A. A≠{} ⟹ Inf (RES`A) = RES (Inf A)"
"⋀A. A≠{} ⟹ Inf (RES ` A) = RES (Inf A)"
"Inf {} = FAIL"
"Inf UNIV = SUCCEED"
"Sup {} = SUCCEED"
"Sup UNIV = FAIL"
"⋀x y. RETURN x ≤ RETURN y ⟷ x=y"
"⋀x Y. RETURN x ≤ RES Y ⟷ x∈Y"
"⋀X y. RES X ≤ RETURN y ⟷ X ⊆ {y}"
unfolding Sup_nres_def Inf_nres_def RETURN_def
by (auto simp add: bot_unique top_unique nres_simp_internals)
lemma Sup_eq_RESE:
assumes "Sup A = RES B"
obtains C where "A=RES`C" and "B=Sup C"
proof -
show ?thesis
using assms unfolding Sup_nres_def
apply (simp split: if_split_asm)
apply (rule_tac C="{X. RES X ∈ A}" in that)
apply auto []
apply (case_tac x, auto simp: nres_simp_internals) []
apply (auto simp: nres_simp_internals) []
done
qed
declare nres_simp_internals[simp]
subsubsection ‹Pointwise Reasoning›
ML ‹
structure refine_pw_simps = Named_Thms
( val name = @{binding refine_pw_simps}
val description = "Refinement Framework: " ^
"Simplifier rules for pointwise reasoning" )
›
setup ‹refine_pw_simps.setup›
definition "nofail S ≡ S≠FAIL"
definition "inres S x ≡ RETURN x ≤ S"
lemma nofail_simps[simp, refine_pw_simps]:
"nofail FAIL ⟷ False"
"nofail (RES X) ⟷ True"
"nofail (RETURN x) ⟷ True"
"nofail SUCCEED ⟷ True"
unfolding nofail_def
by (simp_all add: RETURN_def)
lemma inres_simps[simp, refine_pw_simps]:
"inres FAIL = (λ_. True)"
"inres (RES X) = (λx. x∈X)"
"inres (RETURN x) = (λy. x=y)"
"inres SUCCEED = (λ_. False)"
unfolding inres_def [abs_def]
by (auto simp add: RETURN_def)
lemma not_nofail_iff:
"¬nofail S ⟷ S=FAIL" by (cases S) auto
lemma not_nofail_inres[simp, refine_pw_simps]:
"¬nofail S ⟹ inres S x"
apply (cases S) by auto
lemma intro_nofail[refine_pw_simps]:
"S≠FAIL ⟷ nofail S"
"FAIL≠S ⟷ nofail S"
by (cases S, simp_all)+
text ‹The following two lemmas will introduce pointwise reasoning for
orderings and equalities.›
lemma pw_le_iff:
"S ≤ S' ⟷ (nofail S'⟶ (nofail S ∧ (∀x. inres S x ⟶ inres S' x)))"
apply (cases S, simp_all)
apply (case_tac [!] S', auto)
done
lemma pw_eq_iff:
"S=S' ⟷ (nofail S = nofail S' ∧ (∀x. inres S x ⟷ inres S' x))"
apply (rule iffI)
apply simp
apply (rule antisym)
apply (simp_all add: pw_le_iff)
done
lemma pw_flat_le_iff: "flat_le S S' ⟷
(∃x. inres S x) ⟶ (nofail S ⟷ nofail S') ∧ (∀x. inres S x ⟷ inres S' x)"
by (auto simp : flat_ord_def pw_eq_iff)
lemma pw_flat_ge_iff: "flat_ge S S' ⟷
(nofail S) ⟶ nofail S' ∧ (∀x. inres S x ⟷ inres S' x)"
apply (simp add: flat_ord_def pw_eq_iff) apply safe
apply simp
apply simp
apply simp
apply (rule ccontr)
apply simp
done
lemmas pw_ords_iff = pw_le_iff pw_flat_le_iff pw_flat_ge_iff
lemma pw_leI:
"(nofail S'⟶ (nofail S ∧ (∀x. inres S x ⟶ inres S' x))) ⟹ S ≤ S'"
by (simp add: pw_le_iff)
lemma pw_leI':
assumes "nofail S' ⟹ nofail S"
assumes "⋀x. ⟦nofail S'; inres S x⟧ ⟹ inres S' x"
shows "S ≤ S'"
using assms
by (simp add: pw_le_iff)
lemma pw_eqI:
assumes "nofail S = nofail S'"
assumes "⋀x. inres S x ⟷ inres S' x"
shows "S=S'"
using assms by (simp add: pw_eq_iff)
lemma pwD1:
assumes "S≤S'" "nofail S'"
shows "nofail S"
using assms by (simp add: pw_le_iff)
lemma pwD2:
assumes "S≤S'" "inres S x"
shows "inres S' x"
using assms
by (auto simp add: pw_le_iff)
lemmas pwD = pwD1 pwD2
text ‹
When proving refinement, we may assume that the refined program does not
fail.›
lemma le_nofailI: "⟦ nofail M' ⟹ M ≤ M' ⟧ ⟹ M ≤ M'"
by (cases M') auto
text ‹The following lemmas push pointwise reasoning over operators,
thus converting an expression over lattice operators into a logical
formula.›
lemma pw_sup_nofail[refine_pw_simps]:
"nofail (sup a b) ⟷ nofail a ∧ nofail b"
apply (cases a, simp)
apply (cases b, simp_all)
done
lemma pw_sup_inres[refine_pw_simps]:
"inres (sup a b) x ⟷ inres a x ∨ inres b x"
apply (cases a, simp)
apply (cases b, simp)
apply (simp)
done
lemma pw_Sup_inres[refine_pw_simps]: "inres (Sup X) r ⟷ (∃M∈X. inres M r)"
apply (cases "Sup X")
apply (simp)
apply (erule bexI[rotated])
apply simp
apply (erule Sup_eq_RESE)
apply (simp)
done
lemma pw_SUP_inres [refine_pw_simps]: "inres (Sup (f ` X)) r ⟷ (∃M∈X. inres (f M) r)"
using pw_Sup_inres [of "f ` X"] by simp
lemma pw_Sup_nofail[refine_pw_simps]: "nofail (Sup X) ⟷ (∀x∈X. nofail x)"
apply (cases "Sup X")
apply force
apply simp
apply (erule Sup_eq_RESE)
apply auto
done
lemma pw_SUP_nofail [refine_pw_simps]: "nofail (Sup (f ` X)) ⟷ (∀x∈X. nofail (f x))"
using pw_Sup_nofail [of "f ` X"] by simp
lemma pw_inf_nofail[refine_pw_simps]:
"nofail (inf a b) ⟷ nofail a ∨ nofail b"
apply (cases a, simp)
apply (cases b, simp_all)
done
lemma pw_inf_inres[refine_pw_simps]:
"inres (inf a b) x ⟷ inres a x ∧ inres b x"
apply (cases a, simp)
apply (cases b, simp)
apply (simp)
done
lemma pw_Inf_nofail[refine_pw_simps]: "nofail (Inf C) ⟷ (∃x∈C. nofail x)"
apply (cases "C={}")
apply simp
apply (cases "Inf C")
apply (subgoal_tac "C={FAIL}")
apply simp
apply auto []
apply (subgoal_tac "C≠{FAIL}")
apply (auto simp: not_nofail_iff) []
apply auto []
done
lemma pw_INF_nofail [refine_pw_simps]: "nofail (Inf (f ` C)) ⟷ (∃x∈C. nofail (f x))"
using pw_Inf_nofail [of "f ` C"] by simp
lemma pw_Inf_inres[refine_pw_simps]: "inres (Inf C) r ⟷ (∀M∈C. inres M r)"
apply (unfold Inf_nres_def)
apply auto
apply (case_tac M)
apply force
apply force
apply (case_tac M)
apply force
apply force
done
lemma pw_INF_inres [refine_pw_simps]: "inres (Inf (f ` C)) r ⟷ (∀M∈C. inres (f M) r)"
using pw_Inf_inres [of "f ` C"] by simp
lemma nofail_RES_conv: "nofail m ⟷ (∃M. m=RES M)" by (cases m) auto
primrec the_RES where "the_RES (RES X) = X"
lemma the_RES_inv[simp]: "nofail m ⟹ RES (the_RES m) = m"
by (cases m) auto
definition [refine_pw_simps]: "nf_inres m x ≡ nofail m ∧ inres m x"
lemma nf_inres_RES[simp]: "nf_inres (RES X) x ⟷ x∈X"
by (simp add: refine_pw_simps)
lemma nf_inres_SPEC[simp]: "nf_inres (SPEC Φ) x ⟷ Φ x"
by (simp add: refine_pw_simps)
lemma nofail_antimono_fun: "f ≤ g ⟹ (nofail (g x) ⟶ nofail (f x))"
by (auto simp: pw_le_iff dest: le_funD)
subsubsection ‹Monad Operators›
definition bind where "bind M f ≡ case M of
FAILi ⇒ FAIL |
RES X ⇒ Sup (f`X)"
lemma bind_FAIL[simp]: "bind FAIL f = FAIL"
unfolding bind_def by (auto split: nres.split)
lemma bind_SUCCEED[simp]: "bind SUCCEED f = SUCCEED"
unfolding bind_def by (auto split: nres.split)
lemma bind_RES: "bind (RES X) f = Sup (f`X)" unfolding bind_def
by (auto)
adhoc_overloading
Monad_Syntax.bind Refine_Basic.bind
lemma pw_bind_nofail[refine_pw_simps]:
"nofail (bind M f) ⟷ (nofail M ∧ (∀x. inres M x ⟶ nofail (f x)))"
apply (cases M)
by (auto simp: bind_RES refine_pw_simps)
lemma pw_bind_inres[refine_pw_simps]:
"inres (bind M f) = (λx. nofail M ⟶ (∃y. (inres M y ∧ inres (f y) x)))"
apply (rule ext)
apply (cases M)
apply (auto simp add: bind_RES refine_pw_simps)
done
lemma pw_bind_le_iff:
"bind M f ≤ S ⟷ (nofail S ⟶ nofail M) ∧
(∀x. nofail M ∧ inres M x ⟶ f x ≤ S)"
by (auto simp: pw_le_iff refine_pw_simps)
lemma pw_bind_leI: "⟦
nofail S ⟹ nofail M; ⋀x. ⟦nofail M; inres M x⟧ ⟹ f x ≤ S⟧
⟹ bind M f ≤ S"
by (simp add: pw_bind_le_iff)
text ‹\paragraph{Monad Laws}›
lemma nres_monad1[simp]: "bind (RETURN x) f = f x"
by (rule pw_eqI) (auto simp: refine_pw_simps)
lemma nres_monad2[simp]: "bind M RETURN = M"
by (rule pw_eqI) (auto simp: refine_pw_simps)
lemma nres_monad3[simp]: "bind (bind M f) g = bind M (λx. bind (f x) g)"
by (rule pw_eqI) (auto simp: refine_pw_simps)
lemmas nres_monad_laws = nres_monad1 nres_monad2 nres_monad3
text ‹\paragraph{Congruence rule for bind}›
lemma bind_cong:
assumes "m=m'"
assumes "⋀x. RETURN x ≤ m' ⟹ f x = f' x"
shows "bind m f = bind m' f'"
using assms
by (auto simp: refine_pw_simps pw_eq_iff pw_le_iff)
text ‹\paragraph{Monotonicity and Related Properties}›
lemma bind_mono[refine_mono]:
"⟦ M ≤ M'; ⋀x. RETURN x ≤ M ⟹ f x ≤ f' x ⟧ ⟹ bind M f ≤ bind M' f'"
"⟦ flat_ge M M'; ⋀x. flat_ge (f x) (f' x) ⟧ ⟹ flat_ge (bind M f) (bind M' f')"
apply (auto simp: refine_pw_simps pw_ords_iff) []
apply (auto simp: refine_pw_simps pw_ords_iff) []
done
lemma bind_mono1[simp, intro!]: "mono (λM. bind M f)"
apply (rule monoI)
apply (rule bind_mono)
by auto
lemma bind_mono1'[simp, intro!]: "mono bind"
apply (rule monoI)
apply (rule le_funI)
apply (rule bind_mono)
by auto
lemma bind_mono2'[simp, intro!]: "mono (bind M)"
apply (rule monoI)
apply (rule bind_mono)
by (auto dest: le_funD)
lemma bind_distrib_sup1: "bind (sup M N) f = sup (bind M f) (bind N f)"
by (auto simp add: pw_eq_iff refine_pw_simps)
lemma bind_distrib_sup2: "bind m (λx. sup (f x) (g x)) = sup (bind m f) (bind m g)"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma bind_distrib_Sup1: "bind (Sup M) f = (SUP m∈M. bind m f)"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma bind_distrib_Sup2: "F≠{} ⟹ bind m (Sup F) = (SUP f∈F. bind m f)"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma RES_Sup_RETURN: "Sup (RETURN`X) = RES X"
by (rule pw_eqI) (auto simp add: refine_pw_simps)
subsection ‹VCG Setup›
lemma SPEC_cons_rule:
assumes "m ≤ SPEC Φ"
assumes "⋀x. Φ x ⟹ Ψ x"
shows "m ≤ SPEC Ψ"
using assms by (auto simp: pw_le_iff)
lemmas SPEC_trans = order_trans[where z="SPEC Postcond" for Postcond, zero_var_indexes]
ML ‹
structure Refine = struct
structure vcg = Named_Thms
( val name = @{binding refine_vcg}
val description = "Refinement Framework: " ^
"Verification condition generation rules (intro)" )
structure vcg_cons = Named_Thms
( val name = @{binding refine_vcg_cons}
val description = "Refinement Framework: " ^
"Consequence rules tried by VCG" )
structure refine0 = Named_Thms
( val name = @{binding refine0}
val description = "Refinement Framework: " ^
"Refinement rules applied first (intro)" )
structure refine = Named_Thms
( val name = @{binding refine}
val description = "Refinement Framework: Refinement rules (intro)" )
structure refine2 = Named_Thms
( val name = @{binding refine2}
val description = "Refinement Framework: " ^
"Refinement rules 2nd stage (intro)" )
val no_prod_split =
Attrib.setup_config_bool @{binding refine_no_prod_split} (K false);
fun rcg_tac add_thms ctxt =
let
val cons_thms = vcg_cons.get ctxt
val ref_thms = (refine0.get ctxt
@ add_thms @ refine.get ctxt @ refine2.get ctxt);
val prod_ss = (Splitter.add_split @{thm prod.split}
(put_simpset HOL_basic_ss ctxt));
val prod_simp_tac =
if Config.get ctxt no_prod_split then
K no_tac
else
(simp_tac prod_ss THEN'
REPEAT_ALL_NEW (resolve_tac ctxt @{thms impI allI}));
in
REPEAT_ALL_NEW_FWD (DETERM o FIRST' [
resolve_tac ctxt ref_thms,
resolve_tac ctxt cons_thms THEN' resolve_tac ctxt ref_thms,
prod_simp_tac
])
end;
fun post_tac ctxt = REPEAT_ALL_NEW_FWD (FIRST' [
eq_assume_tac,
SOLVED' (Tagged_Solver.solve_tac ctxt)])
end;
›
setup ‹Refine.vcg.setup›
setup ‹Refine.vcg_cons.setup›
setup ‹Refine.refine0.setup›
setup ‹Refine.refine.setup›
setup ‹Refine.refine2.setup›
method_setup refine_rcg =
‹Attrib.thms >> (fn add_thms => fn ctxt => SIMPLE_METHOD' (
Refine.rcg_tac add_thms ctxt THEN_ALL_NEW_FWD (TRY o Refine.post_tac ctxt)
))›
"Refinement framework: Generate refinement conditions"
method_setup refine_vcg =
‹Attrib.thms >> (fn add_thms => fn ctxt => SIMPLE_METHOD' (
Refine.rcg_tac (add_thms @ Refine.vcg.get ctxt) ctxt THEN_ALL_NEW_FWD (TRY o Refine.post_tac ctxt)
))›
"Refinement framework: Generate refinement and verification conditions"
declare SPEC_cons_rule[refine_vcg_cons]
subsection ‹Data Refinement›
text ‹
In this section we establish a notion of pointwise data refinement, by
lifting a relation ‹R› between concrete and abstract values to
our result lattice.
Given a relation ‹R›, we define a {\em concretization function}
‹⇓R› that takes an abstract result, and returns a concrete result.
The concrete result contains all values that are mapped by ‹R› to
a value in the abstract result.
Note that our concretization function forms no Galois connection, i.e.,
in general there is no ‹α› such that
‹m ≤⇓ R m'› is equivalent to ‹α m ≤ m'›.
However, we get a Galois connection for the special case of
single-valued relations.
Regarding data refinement as Galois connections is inspired by \<^cite>‹"mmo97"›,
that also uses the adjuncts of
a Galois connection to express data refinement by program refinement.
›
definition conc_fun ("⇓") where
"conc_fun R m ≡ case m of FAILi ⇒ FAIL | RES X ⇒ RES (R¯``X)"
definition abs_fun ("⇑") where
"abs_fun R m ≡ case m of FAILi ⇒ FAIL
| RES X ⇒ if X⊆Domain R then RES (R``X) else FAIL"
lemma
conc_fun_FAIL[simp]: "⇓R FAIL = FAIL" and
conc_fun_RES: "⇓R (RES X) = RES (R¯``X)"
unfolding conc_fun_def by (auto split: nres.split)
lemma abs_fun_simps[simp]:
"⇑R FAIL = FAIL"
"X⊆Domain R ⟹ ⇑R (RES X) = RES (R``X)"
"¬(X⊆Domain R) ⟹ ⇑R (RES X) = FAIL"
unfolding abs_fun_def by (auto split: nres.split)
context fixes R assumes SV: "single_valued R" begin
lemma conc_abs_swap: "m' ≤ ⇓R m ⟷ ⇑R m' ≤ m"
unfolding conc_fun_def abs_fun_def using SV
by (auto split: nres.split)
(metis ImageE converseD single_valuedD subsetD)
lemma ac_galois: "galois_connection (⇑R) (⇓R)"
apply (unfold_locales)
by (rule conc_abs_swap)
end
lemma pw_abs_nofail[refine_pw_simps]:
"nofail (⇑R M) ⟷ (nofail M ∧ (∀x. inres M x ⟶ x∈Domain R))"
apply (cases M)
apply simp
apply (auto simp: abs_fun_simps abs_fun_def)
done
lemma pw_abs_inres[refine_pw_simps]:
"inres (⇑R M) a ⟷ (nofail (⇑R M) ⟶ (∃c. inres M c ∧ (c,a)∈R))"
apply (cases M)
apply simp
apply (auto simp: abs_fun_def)
done
lemma pw_conc_nofail[refine_pw_simps]:
"nofail (⇓R S) = nofail S"
by (cases S) (auto simp: conc_fun_RES)
lemma pw_conc_inres[refine_pw_simps]:
"inres (⇓R S') = (λs. nofail S'
⟶ (∃s'. (s,s')∈R ∧ inres S' s'))"
apply (rule ext)
apply (cases S')
apply (auto simp: conc_fun_RES)
done
lemma abs_fun_strict[simp]:
"⇑ R SUCCEED = SUCCEED"
unfolding abs_fun_def by (auto split: nres.split)
lemma conc_fun_strict[simp]:
"⇓ R SUCCEED = SUCCEED"
unfolding conc_fun_def by (auto split: nres.split)
lemma conc_fun_mono[simp, intro!]: "mono (⇓R)"
by rule (auto simp: pw_le_iff refine_pw_simps)
lemma abs_fun_mono[simp, intro!]: "mono (⇑R)"
by rule (auto simp: pw_le_iff refine_pw_simps)
lemma conc_fun_R_mono:
assumes "R ⊆ R'"
shows "⇓R M ≤ ⇓R' M"
using assms
by (auto simp: pw_le_iff refine_pw_simps)
lemma conc_fun_chain: "⇓R (⇓S M) = ⇓(R O S) M"
unfolding conc_fun_def
by (auto split: nres.split)
lemma conc_Id[simp]: "⇓Id = id"
unfolding conc_fun_def [abs_def] by (auto split: nres.split)
lemma abs_Id[simp]: "⇑Id = id"
unfolding abs_fun_def [abs_def] by (auto split: nres.split)
lemma conc_fun_fail_iff[simp]:
"⇓R S = FAIL ⟷ S=FAIL"
"FAIL = ⇓R S ⟷ S=FAIL"
by (auto simp add: pw_eq_iff refine_pw_simps)
lemma conc_trans[trans]:
assumes A: "C ≤ ⇓R B" and B: "B ≤ ⇓R' A"
shows "C ≤ ⇓R (⇓R' A)"
using assms by (fastforce simp: pw_le_iff refine_pw_simps)
lemma abs_trans[trans]:
assumes A: "⇑R C ≤ B" and B: "⇑R' B ≤ A"
shows "⇑R' (⇑R C) ≤ A"
using assms by (fastforce simp: pw_le_iff refine_pw_simps)
subsubsection ‹Transitivity Reasoner Setup›
text ‹WARNING: The order of the single statements is important here!›
lemma conc_trans_additional[trans]:
"⋀A B C. A≤⇓R B ⟹ B≤ C ⟹ A≤⇓R C"
"⋀A B C. A≤⇓Id B ⟹ B≤⇓R C ⟹ A≤⇓R C"
"⋀A B C. A≤⇓R B ⟹ B≤⇓Id C ⟹ A≤⇓R C"
"⋀A B C. A≤⇓Id B ⟹ B≤⇓Id C ⟹ A≤ C"
"⋀A B C. A≤⇓Id B ⟹ B≤ C ⟹ A≤ C"
"⋀A B C. A≤ B ⟹ B≤⇓Id C ⟹ A≤ C"
using conc_trans[where R=R and R'=Id]
by (auto intro: order_trans)
text ‹WARNING: The order of the single statements is important here!›
lemma abs_trans_additional[trans]:
"⋀A B C. ⟦ A ≤ B; ⇑ R B ≤ C⟧ ⟹ ⇑ R A ≤ C"
"⋀A B C. ⟦⇑ Id A ≤ B; ⇑ R B ≤ C⟧ ⟹ ⇑ R A ≤ C"
"⋀A B C. ⟦⇑ R A ≤ B; ⇑ Id B ≤ C⟧ ⟹ ⇑ R A ≤ C"
"⋀A B C. ⟦⇑ Id A ≤ B; ⇑ Id B ≤ C⟧ ⟹ A ≤ C"
"⋀A B C. ⟦⇑ Id A ≤ B; B ≤ C⟧ ⟹ A ≤ C"
"⋀A B C. ⟦A ≤ B; ⇑ Id B ≤ C⟧ ⟹ A ≤ C"
apply (auto simp: refine_pw_simps pw_le_iff)
apply fastforce+
done
subsection ‹Derived Program Constructs›
text ‹
In this section, we introduce some programming constructs that are derived
from the basic monad and ordering operations of our nondeterminism monad.
›
subsubsection ‹ASSUME and ASSERT›
definition ASSERT where "ASSERT ≡ iASSERT RETURN"
definition ASSUME where "ASSUME ≡ iASSUME RETURN"
interpretation assert?: generic_Assert bind RETURN ASSERT ASSUME
apply unfold_locales
by (simp_all add: ASSERT_def ASSUME_def)
text ‹Order matters! ›
lemmas [refine_vcg] = ASSERT_leI
lemmas [refine_vcg] = le_ASSUMEI
lemmas [refine_vcg] = le_ASSERTI
lemmas [refine_vcg] = ASSUME_leI
lemma pw_ASSERT[refine_pw_simps]:
"nofail (ASSERT Φ) ⟷ Φ"
"inres (ASSERT Φ) x"
by (cases Φ, simp_all)+
lemma pw_ASSUME[refine_pw_simps]:
"nofail (ASSUME Φ)"
"inres (ASSUME Φ) x ⟷ Φ"
by (cases Φ, simp_all)+
subsubsection ‹Recursion›
lemma pw_REC_nofail:
shows "nofail (REC B x) ⟷ trimono B ∧
(∃F. (∀x.
nofail (F x) ⟶ nofail (B F x)
∧ (∀x'. inres (B F x) x' ⟶ inres (F x) x')
) ∧ nofail (F x))"
proof -
have "nofail (REC B x) ⟷ trimono B ∧
(∃F. (∀x. B F x ≤ F x) ∧ nofail (F x))"
unfolding REC_def lfp_def
apply (auto simp: refine_pw_simps intro: le_funI dest: le_funD)
done
thus ?thesis
unfolding pw_le_iff .
qed
lemma pw_REC_inres:
"inres (REC B x) x' = (trimono B ⟶
(∀F. (∀x''.
nofail (F x'') ⟶ nofail (B F x'')
∧ (∀x. inres (B F x'') x ⟶ inres (F x'') x))
⟶ inres (F x) x'))"
proof -
have "inres (REC B x) x'
⟷ (trimono B ⟶ (∀F. (∀x''. B F x'' ≤ F x'') ⟶ inres (F x) x'))"
unfolding REC_def lfp_def
by (auto simp: refine_pw_simps intro: le_funI dest: le_funD)
thus ?thesis unfolding pw_le_iff .
qed
lemmas pw_REC = pw_REC_inres pw_REC_nofail
lemma pw_RECT_nofail:
shows "nofail (RECT B x) ⟷ trimono B ∧
(∀F. (∀y. nofail (B F y) ⟶
nofail (F y) ∧ (∀x. inres (F y) x ⟶ inres (B F y) x)) ⟶
nofail (F x))"
proof -
have "nofail (RECT B x) ⟷ (trimono B ∧ (∀F. (∀y. F y ≤ B F y) ⟶ nofail (F x)))"
unfolding RECT_gfp_def gfp_def
by (auto simp: refine_pw_simps intro: le_funI dest: le_funD)
thus ?thesis
unfolding pw_le_iff .
qed
lemma pw_RECT_inres:
shows "inres (RECT B x) x' = (trimono B ⟶
(∃M. (∀y. nofail (B M y) ⟶
nofail (M y) ∧ (∀x. inres (M y) x ⟶ inres (B M y) x)) ∧
inres (M x) x'))"
proof -
have "inres (RECT B x) x' ⟷ trimono B ⟶ (∃M. (∀y. M y ≤ B M y) ∧ inres (M x) x')"
unfolding RECT_gfp_def gfp_def
by (auto simp: refine_pw_simps intro: le_funI dest: le_funD)
thus ?thesis unfolding pw_le_iff .
qed
lemmas pw_RECT = pw_RECT_inres pw_RECT_nofail
subsection ‹Proof Rules›
subsubsection ‹Proving Correctness›
text ‹
In this section, we establish Hoare-like rules to prove that a program
meets its specification.
›
lemma le_SPEC_UNIV_rule [refine_vcg]:
"m ≤ SPEC (λ_. True) ⟹ m ≤ RES UNIV" by auto
lemma RETURN_rule[refine_vcg]: "Φ x ⟹ RETURN x ≤ SPEC Φ"
by (auto simp: RETURN_def)
lemma RES_rule[refine_vcg]: "⟦⋀x. x∈S ⟹ Φ x⟧ ⟹ RES S ≤ SPEC Φ"
by auto
lemma SUCCEED_rule[refine_vcg]: "SUCCEED ≤ SPEC Φ" by auto
lemma FAIL_rule: "False ⟹ FAIL ≤ SPEC Φ" by auto
lemma SPEC_rule[refine_vcg]: "⟦⋀x. Φ x ⟹ Φ' x⟧ ⟹ SPEC Φ ≤ SPEC Φ'" by auto
lemma RETURN_to_SPEC_rule[refine_vcg]: "m≤SPEC ((=) v) ⟹ m≤RETURN v"
by (simp add: pw_le_iff refine_pw_simps)
lemma Sup_img_rule_complete:
"(∀x. x∈S ⟶ f x ≤ SPEC Φ) ⟷ Sup (f`S) ≤ SPEC Φ"
apply rule
apply (rule pw_leI)
apply (auto simp: pw_le_iff refine_pw_simps) []
apply (intro allI impI)
apply (rule pw_leI)
apply (auto simp: pw_le_iff refine_pw_simps) []
done
lemma SUP_img_rule_complete:
"(∀x. x∈S ⟶ f x ≤ SPEC Φ) ⟷ Sup (f ` S) ≤ SPEC Φ"
using Sup_img_rule_complete [of S f] by simp
lemma Sup_img_rule[refine_vcg]:
"⟦ ⋀x. x∈S ⟹ f x ≤ SPEC Φ ⟧ ⟹ Sup(f`S) ≤ SPEC Φ"
by (auto simp: SUP_img_rule_complete[symmetric])
text ‹This lemma is just to demonstrate that our rule is complete.›
lemma bind_rule_complete: "bind M f ≤ SPEC Φ ⟷ M ≤ SPEC (λx. f x ≤ SPEC Φ)"
by (auto simp: pw_le_iff refine_pw_simps)
lemma bind_rule[refine_vcg]:
"⟦ M ≤ SPEC (λx. f x ≤ SPEC Φ) ⟧ ⟹ bind M (λx. f x) ≤ SPEC Φ"
by (auto simp: bind_rule_complete)
lemma ASSUME_rule[refine_vcg]: "⟦Φ ⟹ Ψ ()⟧ ⟹ ASSUME Φ ≤ SPEC Ψ"
by (cases Φ) auto
lemma ASSERT_rule[refine_vcg]: "⟦Φ; Φ ⟹ Ψ ()⟧ ⟹ ASSERT Φ ≤ SPEC Ψ" by auto
lemma prod_rule[refine_vcg]:
"⟦⋀a b. p=(a,b) ⟹ S a b ≤ SPEC Φ⟧ ⟹ case_prod S p ≤ SPEC Φ"
by (auto split: prod.split)
lemma prod2_rule[refine_vcg]:
assumes "⋀a b c d. ⟦ab=(a,b); cd=(c,d)⟧ ⟹ f a b c d ≤ SPEC Φ"
shows "(λ(a,b) (c,d). f a b c d) ab cd ≤ SPEC Φ"
using assms
by (auto split: prod.split)
lemma if_rule[refine_vcg]:
"⟦ b ⟹ S1 ≤ SPEC Φ; ¬b ⟹ S2 ≤ SPEC Φ⟧
⟹ (if b then S1 else S2) ≤ SPEC Φ"
by (auto)
lemma option_rule[refine_vcg]:
"⟦ v=None ⟹ S1 ≤ SPEC Φ; ⋀x. v=Some x ⟹ f2 x ≤ SPEC Φ⟧
⟹ case_option S1 f2 v ≤ SPEC Φ"
by (auto split: option.split)
lemma Let_rule[refine_vcg]:
"f x ≤ SPEC Φ ⟹ Let x f ≤ SPEC Φ" by auto
lemma Let_rule':
assumes "⋀x. x=v ⟹ f x ≤ SPEC Φ"
shows "Let v (λx. f x) ≤ SPEC Φ"
using assms by simp
lemma REC_le_rule:
assumes M: "trimono body"
assumes I0: "(x,x')∈R"
assumes IS: "⋀f x x'. ⟦ ⋀x x'. (x,x')∈R ⟹ f x ≤ M x'; (x,x')∈R ⟧
⟹ body f x ≤ M x'"
shows "REC body x ≤ M x'"
by (rule REC_rule_arb[OF M, where pre="λx' x. (x,x')∈R", OF I0 IS])
subsubsection ‹Proving Monotonicity›
lemma nr_mono_bind:
assumes MA: "mono A" and MB: "⋀s. mono (B s)"
shows "mono (λF s. bind (A F s) (λs'. B s F s'))"
apply (rule monoI)
apply (rule le_funI)
apply (rule bind_mono)
apply (auto dest: monoD[OF MA, THEN le_funD]) []
apply (auto dest: monoD[OF MB, THEN le_funD]) []
done
lemma nr_mono_bind': "mono (λF s. bind (f s) F)"
apply rule
apply (rule le_funI)
apply (rule bind_mono)
apply (auto dest: le_funD)
done
lemmas nr_mono = nr_mono_bind nr_mono_bind' mono_const mono_if mono_id
subsubsection ‹Proving Refinement›
text ‹In this subsection, we establish rules to prove refinement between
structurally similar programs. All rules are formulated including a possible
data refinement via a refinement relation. If this is not required, the
refinement relation can be chosen to be the identity relation.
›
text ‹If we have two identical programs, this rule solves the refinement goal
immediately, using the identity refinement relation.›
lemma Id_refine[refine0]: "S ≤ ⇓Id S" by auto
lemma RES_refine:
"⟦ ⋀s. s∈S ⟹ ∃s'∈S'. (s,s')∈R⟧ ⟹ RES S ≤ ⇓R (RES S')"
by (auto simp: conc_fun_RES)
lemma SPEC_refine:
assumes "S ≤ SPEC (λx. ∃x'. (x,x')∈R ∧ Φ x')"
shows "S ≤ ⇓R (SPEC Φ)"
using assms
by (force simp: pw_le_iff refine_pw_simps)
lemma Id_SPEC_refine[refine]:
"S ≤ SPEC Φ ⟹ S ≤ ⇓Id (SPEC Φ)" by simp
lemma RETURN_refine[refine]:
assumes "(x,x')∈R"
shows "RETURN x ≤ ⇓R (RETURN x')"
using assms
by (auto simp: RETURN_def conc_fun_RES)
lemma RETURN_SPEC_refine:
assumes "∃x'. (x,x')∈R ∧ Φ x'"
shows "RETURN x ≤ ⇓R (SPEC Φ)"
using assms
by (auto simp: pw_le_iff refine_pw_simps)
lemma FAIL_refine[refine]: "X ≤ ⇓R FAIL" by auto
lemma SUCCEED_refine[refine]: "SUCCEED ≤ ⇓R X'" by auto
lemma sup_refine[refine]:
assumes "ai ≤⇓R a"
assumes "bi ≤⇓R b"
shows "sup ai bi ≤⇓R (sup a b)"
using assms by (auto simp: pw_le_iff refine_pw_simps)
text ‹The next two rules are incomplete, but a good approximation for refining
structurally similar programs.›
lemma bind_refine':
fixes R' :: "('a×'b) set" and R::"('c×'d) set"
assumes R1: "M ≤ ⇓ R' M'"
assumes R2: "⋀x x'. ⟦ (x,x')∈R'; inres M x; inres M' x';
nofail M; nofail M'
⟧ ⟹ f x ≤ ⇓ R (f' x')"
shows "bind M (λx. f x) ≤ ⇓ R (bind M' (λx'. f' x'))"
using assms
apply (simp add: pw_le_iff refine_pw_simps)
apply fast
done
lemma bind_refine[refine]:
fixes R' :: "('a×'b) set" and R::"('c×'d) set"
assumes R1: "M ≤ ⇓ R' M'"
assumes R2: "⋀x x'. ⟦ (x,x')∈R' ⟧
⟹ f x ≤ ⇓ R (f' x')"
shows "bind M (λx. f x) ≤ ⇓ R (bind M' (λx'. f' x'))"
apply (rule bind_refine') using assms by auto
lemma bind_refine_abs':
fixes R' :: "('a×'b) set" and R::"('c×'d) set"
assumes R1: "M ≤ ⇓ R' M'"
assumes R2: "⋀x x'. ⟦ (x,x')∈R'; nf_inres M' x'
⟧ ⟹ f x ≤ ⇓ R (f' x')"
shows "bind M (λx. f x) ≤ ⇓ R (bind M' (λx'. f' x'))"
using assms
apply (simp add: pw_le_iff refine_pw_simps)
apply blast
done
text ‹Special cases for refinement of binding to ‹RES›
statements›
lemma bind_refine_RES:
"⟦RES X ≤ ⇓ R' M';
⋀x x'. ⟦(x, x') ∈ R'; x ∈ X ⟧ ⟹ f x ≤ ⇓ R (f' x')⟧
⟹ RES X ⤜ (λx. f x) ≤ ⇓ R (M' ⤜ (λx'. f' x'))"
"⟦M ≤ ⇓ R' (RES X');
⋀x x'. ⟦(x, x') ∈ R'; x' ∈ X' ⟧ ⟹ f x ≤ ⇓ R (f' x')⟧
⟹ M ⤜ (λx. f x) ≤ ⇓ R (RES X' ⤜ (λx'. f' x'))"
"⟦RES X ≤ ⇓ R' (RES X');
⋀x x'. ⟦(x, x') ∈ R'; x ∈ X; x' ∈ X'⟧ ⟹ f x ≤ ⇓ R (f' x')⟧
⟹ RES X ⤜ (λx. f x) ≤ ⇓ R (RES X' ⤜ (λx'. f' x'))"
by (auto intro!: bind_refine')
declare bind_refine_RES(1,2)[refine]
declare bind_refine_RES(3)[refine]
lemma ASSERT_refine[refine]:
"⟦ Φ'⟹Φ ⟧ ⟹ ASSERT Φ ≤ ⇓Id (ASSERT Φ')"
by (cases Φ') auto
lemma ASSUME_refine[refine]:
"⟦ Φ ⟹ Φ' ⟧ ⟹ ASSUME Φ ≤ ⇓Id (ASSUME Φ')"
by (cases Φ) auto
text ‹
Assertions and assumptions are treated specially in bindings
›
lemma ASSERT_refine_right:
assumes "Φ ⟹ S ≤⇓R S'"
shows "S ≤⇓R (do {ASSERT Φ; S'})"
using assms by (cases Φ) auto
lemma ASSERT_refine_right_pres:
assumes "Φ ⟹ S ≤⇓R (do {ASSERT Φ; S'})"
shows "S ≤⇓R (do {ASSERT Φ; S'})"
using assms by (cases Φ) auto
lemma ASSERT_refine_left:
assumes "Φ"
assumes "Φ ⟹ S ≤ ⇓R S'"
shows "do{ASSERT Φ; S} ≤ ⇓R S'"
using assms by (cases Φ) auto
lemma ASSUME_refine_right:
assumes "Φ"
assumes "Φ ⟹ S ≤⇓R S'"
shows "S ≤⇓R (do {ASSUME Φ; S'})"
using assms by (cases Φ) auto
lemma ASSUME_refine_left:
assumes "Φ ⟹ S ≤ ⇓R S'"
shows "do {ASSUME Φ; S} ≤ ⇓R S'"
using assms by (cases Φ) auto
lemma ASSUME_refine_left_pres:
assumes "Φ ⟹ do {ASSUME Φ; S} ≤ ⇓R S'"
shows "do {ASSUME Φ; S} ≤ ⇓R S'"
using assms by (cases Φ) auto
text ‹Warning: The order of ‹[refine]›-declarations is
important here, as preconditions should be generated before
additional proof obligations.›
lemmas [refine0] = ASSUME_refine_right
lemmas [refine0] = ASSERT_refine_left
lemmas [refine0] = ASSUME_refine_left
lemmas [refine0] = ASSERT_refine_right
text ‹For backward compatibility, as ‹intro refine› still
seems to be used instead of ‹refine_rcg›.›
lemmas [refine] = ASSUME_refine_right
lemmas [refine] = ASSERT_refine_left
lemmas [refine] = ASSUME_refine_left
lemmas [refine] = ASSERT_refine_right
definition lift_assn :: "('a × 'b) set ⇒ ('b ⇒ bool) ⇒ ('a ⇒ bool)"
where "lift_assn R Φ s ≡ ∃s'. (s,s')∈R ∧ Φ s'"
lemma lift_assnI: "⟦(s,s')∈R; Φ s'⟧ ⟹ lift_assn R Φ s"
unfolding lift_assn_def by auto
lemma REC_refine[refine]:
assumes M: "trimono body"
assumes R0: "(x,x')∈R"
assumes RS: "⋀f f' x x'. ⟦ ⋀x x'. (x,x')∈R ⟹ f x ≤⇓S (f' x'); (x,x')∈R;
REC body' = f' ⟧
⟹ body f x ≤⇓S (body' f' x')"
shows "REC (λf x. body f x) x ≤⇓S (REC (λf' x'. body' f' x') x')"
unfolding REC_def
apply (clarsimp simp add: M)
apply (rule lfp_induct_pointwise[where pre="λx' x. (x,x')∈R" and B=body])
apply rule
apply clarsimp
apply (blast intro: SUP_least)
apply simp
apply (simp add: trimonoD[OF M])
apply (rule R0)
apply (subst lfp_unfold, simp add: trimonoD)
apply (rule RS)
apply blast
apply blast
apply (simp add: REC_def[abs_def])
done
lemma RECT_refine[refine]:
assumes M: "trimono body"
assumes R0: "(x,x')∈R"
assumes RS: "⋀f f' x x'. ⟦ ⋀x x'. (x,x')∈R ⟹ f x ≤⇓S (f' x'); (x,x')∈R ⟧
⟹ body f x ≤⇓S (body' f' x')"
shows "RECT (λf x. body f x) x ≤⇓S (RECT (λf' x'. body' f' x') x')"
unfolding RECT_def
apply (clarsimp simp add: M)
apply (rule flatf_fixp_transfer[where
fp'="flatf_gfp body"
and B'=body
and P="λx x'. (x',x)∈R",
OF _ _ flatf_ord.fixp_unfold[OF M[THEN trimonoD_flatf_ge]] R0])
apply simp
apply (simp add: trimonoD)
by (rule RS)
lemma if_refine[refine]:
assumes "b ⟷ b'"
assumes "⟦b;b'⟧ ⟹ S1 ≤ ⇓R S1'"
assumes "⟦¬b;¬b'⟧ ⟹ S2 ≤ ⇓R S2'"
shows "(if b then S1 else S2) ≤ ⇓R (if b' then S1' else S2')"
using assms by auto
lemma Let_unfold_refine[refine]:
assumes "f x ≤ ⇓R (f' x')"
shows "Let x f ≤ ⇓R (Let x' f')"
using assms by auto
text ‹The next lemma is sometimes more convenient, as it prevents
large let-expressions from exploding by being completely unfolded.›
lemma Let_refine:
assumes "(m,m')∈R'"
assumes "⋀x x'. (x,x')∈R' ⟹ f x ≤ ⇓R (f' x')"
shows "Let m (λx. f x) ≤⇓R (Let m' (λx'. f' x'))"
using assms by auto
lemma Let_refine':
assumes "(m,m')∈R"
assumes "(m,m')∈R ⟹ f m ≤⇓S (f' m')"
shows "Let m f ≤ ⇓S (Let m' f')"
using assms by simp
lemma case_option_refine[refine]:
assumes "(v,v')∈⟨Ra⟩option_rel"
assumes "⟦v=None; v'=None⟧ ⟹ n ≤ ⇓ Rb n'"
assumes "⋀x x'. ⟦ v=Some x; v'=Some x'; (x, x') ∈ Ra ⟧
⟹ f x ≤ ⇓ Rb (f' x')"
shows "case_option n f v ≤⇓Rb (case_option n' f' v')"
using assms
by (auto split: option.split simp: option_rel_def)
lemma list_case_refine[refine]:
assumes "(li,l)∈⟨S⟩list_rel"
assumes "fni ≤⇓R fn"
assumes "⋀xi x xsi xs. ⟦ (xi,x)∈S; (xsi,xs)∈⟨S⟩list_rel; li=xi#xsi; l=x#xs ⟧ ⟹ fci xi xsi ≤⇓R (fc x xs)"
shows "(case li of [] ⇒ fni | xi#xsi ⇒ fci xi xsi) ≤ ⇓R (case l of [] ⇒ fn | x#xs ⇒ fc x xs)"
using assms by (auto split: list.split)
text ‹It is safe to split conjunctions in refinement goals.›
declare conjI[refine]
text ‹The following rules try to compensate for some structural changes,
like inlining lets or converting binds to lets.›
lemma remove_Let_refine[refine2]:
assumes "M ≤ ⇓R (f x)"
shows "M ≤ ⇓R (Let x f)" using assms by auto
lemma intro_Let_refine[refine2]:
assumes "f x ≤ ⇓R M'"
shows "Let x f ≤ ⇓R M'" using assms by auto
lemma bind2let_refine[refine2]:
assumes "RETURN x ≤ ⇓R' M'"
assumes "⋀x'. (x,x')∈R' ⟹ f x ≤ ⇓R (f' x')"
shows "Let x f ≤ ⇓R (bind M' (λx'. f' x'))"
using assms
apply (simp add: pw_le_iff refine_pw_simps)
apply fast
done
lemma bind_Let_refine2[refine2]: "⟦
m' ≤⇓R' (RETURN x);
⋀x'. ⟦inres m' x'; (x',x)∈R'⟧ ⟹ f' x' ≤ ⇓R (f x)
⟧ ⟹ m'⤜(λx'. f' x') ≤ ⇓R (Let x (λx. f x))"
apply (simp add: pw_le_iff refine_pw_simps)
apply blast
done
lemma bind2letRETURN_refine[refine2]:
assumes "RETURN x ≤ ⇓R' M'"
assumes "⋀x'. (x,x')∈R' ⟹ RETURN (f x) ≤ ⇓R (f' x')"
shows "RETURN (Let x f) ≤ ⇓R (bind M' (λx'. f' x'))"
using assms
apply (simp add: pw_le_iff refine_pw_simps)
apply fast
done
lemma RETURN_as_SPEC_refine[refine2]:
assumes "M ≤ SPEC (λc. (c,a)∈R)"
shows "M ≤ ⇓R (RETURN a)"
using assms
by (simp add: pw_le_iff refine_pw_simps)
lemma RETURN_as_SPEC_refine_old:
"⋀M R. M ≤ ⇓R (SPEC (λx. x=v)) ⟹ M ≤⇓R (RETURN v)"
by (simp add: RETURN_def)
lemma if_RETURN_refine [refine2]:
assumes "b ⟷ b'"
assumes "⟦b;b'⟧ ⟹ RETURN S1 ≤ ⇓R S1'"
assumes "⟦¬b;¬b'⟧ ⟹ RETURN S2 ≤ ⇓R S2'"
shows "RETURN (if b then S1 else S2) ≤ ⇓R (if b' then S1' else S2')"
using assms
by (simp add: pw_le_iff refine_pw_simps)
lemma RES_sng_as_SPEC_refine[refine2]:
assumes "M ≤ SPEC (λc. (c,a)∈R)"
shows "M ≤ ⇓R (RES {a})"
using assms
by (simp add: pw_le_iff refine_pw_simps)
lemma intro_spec_refine_iff:
"(bind (RES X) f ≤ ⇓R M) ⟷ (∀x∈X. f x ≤ ⇓R M)"
apply (simp add: pw_le_iff refine_pw_simps)
apply blast
done
lemma intro_spec_refine[refine2]:
assumes "⋀x. x∈X ⟹ f x ≤ ⇓R M"
shows "bind (RES X) (λx. f x) ≤ ⇓R M"
using assms
by (simp add: intro_spec_refine_iff)
text ‹The following rules are intended for manual application, to reflect
some common structural changes, that, however, are not suited to be applied
automatically.›
text ‹Replacing a let by a deterministic computation›
lemma let2bind_refine:
assumes "m ≤ ⇓R' (RETURN m')"
assumes "⋀x x'. (x,x')∈R' ⟹ f x ≤ ⇓R (f' x')"
shows "bind m (λx. f x) ≤ ⇓R (Let m' (λx'. f' x'))"
using assms
apply (simp add: pw_le_iff refine_pw_simps)
apply blast
done
text ‹Introduce a new binding, without a structural match in the abstract
program›
lemma intro_bind_refine:
assumes "m ≤ ⇓R' (RETURN m')"
assumes "⋀x. (x,m')∈R' ⟹ f x ≤ ⇓R m''"
shows "bind m (λx. f x) ≤ ⇓R m''"
using assms
apply (simp add: pw_le_iff refine_pw_simps)
apply blast
done
lemma intro_bind_refine_id:
assumes "m ≤ (SPEC ((=) m'))"
assumes "f m' ≤ ⇓R m''"
shows "bind m f ≤ ⇓R m''"
using assms
apply (simp add: pw_le_iff refine_pw_simps)
apply blast
done
text ‹The following set of rules executes a step on the LHS or RHS of
a refinement proof obligation, without changing the other side.
These kind of rules is useful for performing refinements with
invisible steps.›
lemma lhs_step_If:
"⟦ b ⟹ t ≤ m; ¬b ⟹ e ≤ m ⟧ ⟹ If b t e ≤ m" by simp
lemma lhs_step_RES:
"⟦ ⋀x. x∈X ⟹ RETURN x ≤ m ⟧ ⟹ RES X ≤ m"
by (simp add: pw_le_iff)
lemma lhs_step_SPEC:
"⟦ ⋀x. Φ x ⟹ RETURN x ≤ m ⟧ ⟹ SPEC (λx. Φ x) ≤ m"
by (simp add: pw_le_iff)
lemma lhs_step_bind:
fixes m :: "'a nres" and f :: "'a ⇒ 'b nres"
assumes "nofail m' ⟹ nofail m"
assumes "⋀x. nf_inres m x ⟹ f x ≤ m'"
shows "do {x←m; f x} ≤ m'"
using assms
by (simp add: pw_le_iff refine_pw_simps) blast
lemma rhs_step_bind:
assumes "m ≤ ⇓R m'" "inres m x" "⋀x'. (x,x')∈R ⟹ lhs ≤⇓S (f' x')"
shows "lhs ≤ ⇓S (m' ⤜ f')"
using assms
by (simp add: pw_le_iff refine_pw_simps) blast
lemma rhs_step_bind_RES:
assumes "x'∈X'"
assumes "m ≤ ⇓R (f' x')"
shows "m ≤ ⇓R (RES X' ⤜ f')"
using assms by (simp add: pw_le_iff refine_pw_simps) blast
lemma rhs_step_bind_SPEC:
assumes "Φ x'"
assumes "m ≤ ⇓R (f' x')"
shows "m ≤ ⇓R (SPEC Φ ⤜ f')"
using assms by (simp add: pw_le_iff refine_pw_simps) blast
lemma RES_bind_choose:
assumes "x∈X"
assumes "m ≤ f x"
shows "m ≤ RES X ⤜ f"
using assms by (auto simp: pw_le_iff refine_pw_simps)
lemma pw_RES_bind_choose:
"nofail (RES X ⤜ f) ⟷ (∀x∈X. nofail (f x))"
"inres (RES X ⤜ f) y ⟷ (∃x∈X. inres (f x) y)"
by (auto simp: refine_pw_simps)
lemma prod_case_refine:
assumes "(p',p)∈R1×⇩rR2"
assumes "⋀x1' x2' x1 x2. ⟦ p'=(x1',x2'); p=(x1,x2); (x1',x1)∈R1; (x2',x2)∈R2⟧ ⟹ f' x1' x2' ≤ ⇓R (f x1 x2)"
shows "(case p' of (x1',x2') ⇒ f' x1' x2') ≤⇓R (case p of (x1,x2) ⇒ f x1 x2)"
using assms by (auto split: prod.split)
subsection ‹Relators›
declare fun_relI[refine]
definition nres_rel where
nres_rel_def_internal: "nres_rel R ≡ {(c,a). c ≤ ⇓R a}"
lemma nres_rel_def: "⟨R⟩nres_rel ≡ {(c,a). c ≤ ⇓R a}"
by (simp add: nres_rel_def_internal relAPP_def)
lemma nres_relD: "(c,a)∈⟨R⟩nres_rel ⟹ c ≤⇓R a" by (simp add: nres_rel_def)
lemma nres_relI[refine]: "c ≤⇓R a ⟹ (c,a)∈⟨R⟩nres_rel" by (simp add: nres_rel_def)
lemma nres_rel_comp: "⟨A⟩nres_rel O ⟨B⟩nres_rel = ⟨A O B⟩nres_rel"
by (auto simp: nres_rel_def conc_fun_chain[symmetric] conc_trans)
lemma pw_nres_rel_iff: "(a,b)∈⟨A⟩nres_rel ⟷ nofail (⇓ A b) ⟶ nofail a ∧ (∀x. inres a x ⟶ inres (⇓ A b) x)"
by (simp add: pw_le_iff nres_rel_def)
lemma param_SUCCEED[param]: "(SUCCEED,SUCCEED) ∈ ⟨R⟩nres_rel"
by (auto simp: nres_rel_def)
lemma param_FAIL[param]: "(FAIL,FAIL) ∈ ⟨R⟩nres_rel"
by (auto simp: nres_rel_def)
lemma param_RES[param]:
"(RES,RES) ∈ ⟨R⟩set_rel → ⟨R⟩nres_rel"
unfolding set_rel_def nres_rel_def
by (fastforce intro: RES_refine)
lemma param_RETURN[param]:
"(RETURN,RETURN) ∈ R → ⟨R⟩nres_rel"
by (auto simp: nres_rel_def RETURN_refine)
lemma param_bind[param]:
"(bind,bind) ∈ ⟨Ra⟩nres_rel → (Ra→⟨Rb⟩nres_rel) → ⟨Rb⟩nres_rel"
by (auto simp: nres_rel_def intro: bind_refine dest: fun_relD)
lemma param_ASSERT_bind[param]: "⟦
(Φ,Ψ) ∈ bool_rel;
⟦ Φ; Ψ ⟧ ⟹ (f,g)∈⟨R⟩nres_rel
⟧ ⟹ (ASSERT Φ ⪢ f, ASSERT Ψ ⪢ g) ∈ ⟨R⟩nres_rel"
by (auto intro: nres_relI)
subsection ‹Autoref Setup›
consts i_nres :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of nres_rel i_nres]
definition [simp]: "op_nres_ASSERT_bnd Φ m ≡ do {ASSERT Φ; m}"
lemma param_op_nres_ASSERT_bnd[param]:
assumes "Φ' ⟹ Φ"
assumes "⟦Φ'; Φ⟧ ⟹ (m,m')∈⟨R⟩nres_rel"
shows "(op_nres_ASSERT_bnd Φ m, op_nres_ASSERT_bnd Φ' m') ∈ ⟨R⟩nres_rel"
using assms
by (auto simp: pw_le_iff refine_pw_simps nres_rel_def)
context begin interpretation autoref_syn .
lemma id_ASSERT[autoref_op_pat_def]:
"do {ASSERT Φ; m} ≡ OP (op_nres_ASSERT_bnd Φ)$m"
by simp
definition [simp]: "op_nres_ASSUME_bnd Φ m ≡ do {ASSUME Φ; m}"
lemma id_ASSUME[autoref_op_pat_def]:
"do {ASSUME Φ; m} ≡ OP (op_nres_ASSUME_bnd Φ)$m"
by simp
end
lemma autoref_SUCCEED[autoref_rules]: "(SUCCEED,SUCCEED) ∈ ⟨R⟩nres_rel"
by (auto simp: nres_rel_def)
lemma autoref_FAIL[autoref_rules]: "(FAIL,FAIL) ∈ ⟨R⟩nres_rel"
by (auto simp: nres_rel_def)
lemma autoref_RETURN[autoref_rules]:
"(RETURN,RETURN) ∈ R → ⟨R⟩nres_rel"
by (auto simp: nres_rel_def RETURN_refine)
lemma autoref_bind[autoref_rules]:
"(bind,bind) ∈ ⟨R1⟩nres_rel → (R1→⟨R2⟩nres_rel) → ⟨R2⟩nres_rel"
apply (intro fun_relI)
apply (rule nres_relI)
apply (rule bind_refine)
apply (erule nres_relD)
apply (erule (1) fun_relD[THEN nres_relD])
done
context begin interpretation autoref_syn .
lemma autoref_ASSERT[autoref_rules]:
assumes "Φ ⟹ (m',m)∈⟨R⟩nres_rel"
shows "(
m',
(OP (op_nres_ASSERT_bnd Φ) ::: ⟨R⟩nres_rel → ⟨R⟩nres_rel) $ m)∈⟨R⟩nres_rel"
using assms unfolding nres_rel_def
by (simp add: ASSERT_refine_right)
lemma autoref_ASSUME[autoref_rules]:
assumes "SIDE_PRECOND Φ"
assumes "Φ ⟹ (m',m)∈⟨R⟩nres_rel"
shows "(
m',
(OP (op_nres_ASSUME_bnd Φ) ::: ⟨R⟩nres_rel → ⟨R⟩nres_rel) $ m)∈⟨R⟩nres_rel"
using assms unfolding nres_rel_def
by (simp add: ASSUME_refine_right)
lemma autoref_REC[autoref_rules]:
assumes "(B,B')∈(Ra→⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel"
assumes "DEFER trimono B"
shows "(REC B,
(OP REC
::: ((Ra→⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel)$B'
) ∈ Ra → ⟨Rr⟩nres_rel"
apply (intro fun_relI)
using assms
apply (auto simp: nres_rel_def intro!: REC_refine)
apply (simp add: fun_rel_def)
apply blast
done
theorem param_RECT[param]:
assumes "(B, B') ∈ (Ra → ⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel"
and "trimono B"
shows "(REC⇩T B, REC⇩T B')∈ Ra → ⟨Rr⟩nres_rel"
apply (intro fun_relI)
using assms
apply (auto simp: nres_rel_def intro!: RECT_refine)
apply (simp add: fun_rel_def)
apply blast
done
lemma autoref_RECT[autoref_rules]:
assumes "(B,B') ∈ (Ra→⟨Rr⟩nres_rel) → Ra→⟨Rr⟩nres_rel"
assumes "DEFER trimono B"
shows "(RECT B,
(OP RECT
::: ((Ra→⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel) → Ra → ⟨Rr⟩nres_rel)$B'
) ∈ Ra → ⟨Rr⟩nres_rel"
using assms
unfolding autoref_tag_defs
by (rule param_RECT)
end
subsection ‹Convenience Rules›
text ‹
In this section, we define some lemmas that simplify common prover tasks.
›
lemma ref_two_step: "A≤⇓R B ⟹ B≤C ⟹ A≤⇓R C"
by (rule conc_trans_additional)
lemma pw_ref_iff:
shows "S ≤ ⇓R S'
⟷ (nofail S'
⟶ nofail S ∧ (∀x. inres S x ⟶ (∃s'. (x, s') ∈ R ∧ inres S' s')))"
by (simp add: pw_le_iff refine_pw_simps)
lemma pw_ref_I:
assumes "nofail S'
⟶ nofail S ∧ (∀x. inres S x ⟶ (∃s'. (x, s') ∈ R ∧ inres S' s'))"
shows "S ≤ ⇓R S'"
using assms
by (simp add: pw_ref_iff)
text ‹Introduce an abstraction relation. Usage:
‹rule introR[where R=absRel]›
›
lemma introR: "(a,a')∈R ⟹ (a,a')∈R" .
lemma intro_prgR: "c ≤ ⇓R a ⟹ c ≤ ⇓R a" by auto
lemma refine_IdI: "m ≤ m' ⟹ m ≤ ⇓Id m'" by simp
lemma le_ASSERTI_pres:
assumes "Φ ⟹ S ≤ do {ASSERT Φ; S'}"
shows "S ≤ do {ASSERT Φ; S'}"
using assms by (auto intro: le_ASSERTI)
lemma RETURN_ref_SPECD:
assumes "RETURN c ≤ ⇓R (SPEC Φ)"
obtains a where "(c,a)∈R" "Φ a"
using assms
by (auto simp: pw_le_iff refine_pw_simps)
lemma RETURN_ref_RETURND:
assumes "RETURN c ≤ ⇓R (RETURN a)"
shows "(c,a)∈R"
using assms
apply (auto simp: pw_le_iff refine_pw_simps)
done
lemma return_refine_prop_return:
assumes "nofail m"
assumes "RETURN x ≤ ⇓R m"
obtains x' where "(x,x')∈R" "RETURN x' ≤ m"
using assms
by (auto simp: refine_pw_simps pw_le_iff)
lemma ignore_snd_refine_conv:
"(m ≤ ⇓(R×⇩rUNIV) m') ⟷ m⤜(RETURN o fst) ≤⇓R (m'⤜(RETURN o fst))"
by (auto simp: pw_le_iff refine_pw_simps)
lemma ret_le_down_conv:
"nofail m ⟹ RETURN c ≤ ⇓R m ⟷ (∃a. (c,a)∈R ∧ RETURN a ≤ m)"
by (auto simp: pw_le_iff refine_pw_simps)
lemma SPEC_eq_is_RETURN:
"SPEC ((=) x) = RETURN x"
"SPEC (λx. x=y) = RETURN y"
by (auto simp: RETURN_def)
lemma RETURN_SPEC_conv: "RETURN r = SPEC (λx. x=r)"
by (simp add: RETURN_def)
lemma refine2spec_aux:
"a ≤ ⇓R b ⟷ ( (nofail b ⟶ a ≤ SPEC ( λr. (∃x. inres b x ∧ (r,x)∈R) )) )"
by (auto simp: pw_le_iff refine_pw_simps)
lemma refine2specI:
assumes "nofail b ⟹ a ≤ SPEC (λr. (∃x. inres b x ∧ (r,x)∈R) )"
shows "a ≤ ⇓R b"
using assms by (simp add: refine2spec_aux)
lemma specify_left:
assumes "m ≤ SPEC Φ"
assumes "⋀x. Φ x ⟹ f x ≤ M"
shows "do { x ← m; f x } ≤ M"
using assms by (auto simp: pw_le_iff refine_pw_simps)
lemma build_rel_SPEC:
"M ≤ SPEC ( λx. Φ (α x) ∧ I x) ⟹ M ≤ ⇓(build_rel α I) (SPEC Φ)"
by (auto simp: pw_le_iff refine_pw_simps build_rel_def)
lemma build_rel_SPEC_conv: "⇓(br α I) (SPEC Φ) = SPEC (λx. I x ∧ Φ (α x))"
by (auto simp: br_def pw_eq_iff refine_pw_simps)
lemma refine_IdD: "c ≤ ⇓Id a ⟹ c ≤ a" by simp
lemma bind_sim_select_rule:
assumes "m⤜f' ≤ SPEC Ψ"
assumes "⋀x. ⟦nofail m; inres m x; f' x≤SPEC Ψ⟧ ⟹ f x≤SPEC Φ"
shows "m⤜f ≤ SPEC Φ"
using assms
by (auto simp: pw_le_iff refine_pw_simps)
lemma assert_bind_spec_conv: "ASSERT Φ ⪢ m ≤ SPEC Ψ ⟷ (Φ ∧ m ≤ SPEC Ψ)"
by (auto simp: pw_le_iff refine_pw_simps)
lemma summarize_ASSERT_conv: "do {ASSERT Φ; ASSERT Ψ; m} = do {ASSERT (Φ ∧ Ψ); m}"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma bind_ASSERT_eq_if: "do { ASSERT Φ; m } = (if Φ then m else FAIL)"
by auto
lemma le_RES_nofailI:
assumes "a≤RES x"
shows "nofail a"
using assms
by (metis nofail_simps(2) pwD1)
lemma add_invar_refineI:
assumes "f x ≤⇓R (f' x')"
and "nofail (f x) ⟹ f x ≤ SPEC I"
shows "f x ≤ ⇓ {(c, a). (c, a) ∈ R ∧ I c} (f' x')"
using assms
by (simp add: pw_le_iff refine_pw_simps sv_add_invar)
lemma bind_RES_RETURN_eq: "bind (RES X) (λx. RETURN (f x)) =
RES { f x | x. x∈X }"
by (simp add: pw_eq_iff refine_pw_simps)
blast
lemma bind_RES_RETURN2_eq: "bind (RES X) (λ(x,y). RETURN (f x y)) =
RES { f x y | x y. (x,y)∈X }"
apply (simp add: pw_eq_iff refine_pw_simps)
apply blast
done
lemma le_SPEC_bindI:
assumes "Φ x"
assumes "m ≤ f x"
shows "m ≤ SPEC Φ ⤜ f"
using assms by (auto simp add: pw_le_iff refine_pw_simps)
lemma bind_assert_refine:
assumes "m1 ≤ SPEC Φ"
assumes "⋀x. Φ x ⟹ m2 x ≤ m'"
shows "do {x←m1; ASSERT (Φ x); m2 x} ≤ m'"
using assms
by (simp add: pw_le_iff refine_pw_simps) blast
lemma RETURN_refine_iff[simp]: "RETURN x ≤⇓R (RETURN y) ⟷ (x,y)∈R"
by (auto simp: pw_le_iff refine_pw_simps)
lemma RETURN_RES_refine_iff:
"RETURN x ≤⇓R (RES Y) ⟷ (∃y∈Y. (x,y)∈R)"
by (auto simp: pw_le_iff refine_pw_simps)
lemma RETURN_RES_refine:
assumes "∃x'. (x,x')∈R ∧ x'∈X"
shows "RETURN x ≤ ⇓R (RES X)"
using assms
by (auto simp: pw_le_iff refine_pw_simps)
lemma in_nres_rel_iff: "(a,b)∈⟨R⟩nres_rel ⟷ a ≤⇓R b"
by (auto simp: nres_rel_def)
lemma inf_RETURN_RES:
"inf (RETURN x) (RES X) = (if x∈X then RETURN x else SUCCEED)"
"inf (RES X) (RETURN x) = (if x∈X then RETURN x else SUCCEED)"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma inf_RETURN_SPEC[simp]:
"inf (RETURN x) (SPEC (λy. Φ y)) = SPEC (λy. y=x ∧ Φ x)"
"inf (SPEC (λy. Φ y)) (RETURN x) = SPEC (λy. y=x ∧ Φ x)"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma RES_sng_eq_RETURN: "RES {x} = RETURN x"
by simp
lemma nofail_inf_serialize:
"⟦nofail a; nofail b⟧ ⟹ inf a b = do {x←a; ASSUME (inres b x); RETURN x}"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma conc_fun_SPEC:
"⇓R (SPEC (λx. Φ x)) = SPEC (λy. ∃x. (y,x)∈R ∧ Φ x)"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma conc_fun_RETURN:
"⇓R (RETURN x) = SPEC (λy. (y,x)∈R)"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma use_spec_rule:
assumes "m ≤ SPEC Ψ"
assumes "m ≤ SPEC (λs. Ψ s ⟶ Φ s)"
shows "m ≤ SPEC Φ"
using assms
by (auto simp: pw_le_iff refine_pw_simps)
lemma strengthen_SPEC: "m ≤ SPEC Φ ⟹ m ≤ SPEC(λs. inres m s ∧ nofail m ∧ Φ s)"
by (auto simp: pw_le_iff refine_pw_simps)
lemma weaken_SPEC:
"m ≤ SPEC Φ ⟹ (⋀x. Φ x ⟹ Ψ x) ⟹ m ≤ SPEC Ψ"
by (force elim!: order_trans)
lemma bind_le_nofailI:
assumes "nofail m"
assumes "⋀x. RETURN x ≤ m ⟹ f x ≤ m'"
shows "m⤜f ≤ m'"
using assms
by (simp add: refine_pw_simps pw_le_iff) blast
lemma bind_le_shift:
"bind m f ≤ m'
⟷ m ≤ (if nofail m' then SPEC (λx. f x ≤ m') else FAIL)"
by (auto simp: pw_le_iff refine_pw_simps)
lemma If_bind_distrib[simp]:
fixes t e :: "'a nres"
shows "(If b t e ⤜ (λx. f x)) = (If b (t⤜(λx. f x)) (e⤜(λx. f x)))"
by simp
lemma unused_bind_conv:
assumes "NO_MATCH (ASSERT Φ) m"
assumes "NO_MATCH (ASSUME Φ) m"
shows "(m⤜(λx. c)) = (ASSERT (nofail m) ⤜ (λ_. ASSUME (∃x. inres m x) ⤜ (λx. c)))"
by (auto simp: pw_eq_iff refine_pw_simps)
text ‹The following rules are useful for massaging programs before the
refinement takes place›
lemma let_to_bind_conv:
"Let x f = RETURN x⤜f"
by simp
lemmas bind_to_let_conv = let_to_bind_conv[symmetric]
lemma pull_out_let_conv: "RETURN (Let x f) = Let x (λx. RETURN (f x))"
by simp
lemma push_in_let_conv:
"Let x (λx. RETURN (f x)) = RETURN (Let x f)"
"Let x (RETURN o f) = RETURN (Let x f)"
by simp_all
lemma pull_out_RETURN_case_option:
"case_option (RETURN a) (λv. RETURN (f v)) x = RETURN (case_option a f x)"
by (auto split: option.splits)
lemma if_bind_cond_refine:
assumes "ci ≤ RETURN b"
assumes "b ⟹ ti≤⇓R t"
assumes "¬b ⟹ ei≤⇓R e"
shows "do {b←ci; if b then ti else ei} ≤ ⇓R (if b then t else e)"
using assms
by (auto simp add: refine_pw_simps pw_le_iff)
lemma intro_RETURN_Let_refine:
assumes "RETURN (f x) ≤ ⇓R M'"
shows "RETURN (Let x f) ≤ ⇓R M'"
using assms by auto
lemma ife_FAIL_to_ASSERT_cnv:
"(if Φ then m else FAIL) = op_nres_ASSERT_bnd Φ m"
by (cases Φ, auto)
lemma nres_bind_let_law: "(do { x ← do { let y=v; f y }; g x } :: _ nres)
= do { let y=v; x← f y; g x }" by auto
lemma unused_bind_RES_ne[simp]: "X≠{} ⟹ do { _ ← RES X; m} = m"
by (auto simp: pw_eq_iff refine_pw_simps)
lemma le_ASSERT_defI1:
assumes "c ≡ do {ASSERT Φ; m}"
assumes "Φ ⟹ m' ≤ c"
shows "m' ≤ c"
using assms
by (simp add: le_ASSERTI)
lemma refine_ASSERT_defI1:
assumes "c ≡ do {ASSERT Φ; m}"
assumes "Φ ⟹ m' ≤ ⇓R c"
shows "m' ≤ ⇓R c"
using assms
by (simp, refine_vcg)
lemma le_ASSERT_defI2:
assumes "c ≡ do {ASSERT Φ; ASSERT Ψ; m}"
assumes "⟦Φ; Ψ⟧ ⟹ m' ≤ c"
shows "m' ≤ c"
using assms
by (simp add: le_ASSERTI)
lemma refine_ASSERT_defI2:
assumes "c ≡ do {ASSERT Φ; ASSERT Ψ; m}"
assumes "⟦Φ; Ψ⟧ ⟹ m' ≤ ⇓R c"
shows "m' ≤ ⇓R c"
using assms
by (simp, refine_vcg)
lemma ASSERT_le_defI:
assumes "c ≡ do { ASSERT Φ; m'}"
assumes "Φ"
assumes "Φ ⟹ m' ≤ m"
shows "c ≤ m"
using assms by (auto)
lemma ASSERT_same_eq_conv: "(ASSERT Φ ⪢ m) = (ASSERT Φ ⪢ n) ⟷ (Φ ⟶ m=n)"
by auto
lemma case_prod_bind_simp[simp]: "
(λx. (case x of (a, b) ⇒ f a b) ≤ SPEC Φ) = (λ(a,b). f a b ≤ SPEC Φ)"
by auto
lemma RECT_eq_REC': "nofail (RECT B x) ⟹ RECT B x = REC B x"
by (subst RECT_eq_REC; simp_all add: nofail_def)
lemma rel2p_nres_RETURN[rel2p]: "rel2p (⟨A⟩nres_rel) (RETURN x) (RETURN y) = rel2p A x y"
by (auto simp: rel2p_def dest: nres_relD intro: nres_relI)
subsubsection ‹Boolean Operations on Specifications›
lemma SPEC_iff:
assumes "P ≤ SPEC (λs. Q s ⟶ R s)"
and "P ≤ SPEC (λs. ¬ Q s ⟶ ¬ R s)"
shows "P ≤ SPEC (λs. Q s ⟷ R s)"
using assms[THEN pw_le_iff[THEN iffD1]]
by (auto intro!: pw_leI)
lemma SPEC_rule_conjI:
assumes "A ≤ SPEC P" and "A ≤ SPEC Q"
shows "A ≤ SPEC (λv. P v ∧ Q v)"
proof -
have "A ≤ inf (SPEC P) (SPEC Q)" using assms by (rule_tac inf_greatest) assumption
thus ?thesis by (auto simp add:Collect_conj_eq)
qed
lemma SPEC_rule_conjunct1:
assumes "A ≤ SPEC (λv. P v ∧ Q v)"
shows "A ≤ SPEC P"
proof -
note assms
also have "… ≤ SPEC P" by (rule SPEC_rule) auto
finally show ?thesis .
qed
lemma SPEC_rule_conjunct2:
assumes "A ≤ SPEC (λv. P v ∧ Q v)"
shows "A ≤ SPEC Q"
proof -
note assms
also have "… ≤ SPEC Q" by (rule SPEC_rule) auto
finally show ?thesis .
qed
subsubsection ‹Pointwise Reasoning›
lemma inres_if:
"⟦ inres (if P then Q else R) x; ⟦P; inres Q x⟧ ⟹ S; ⟦¬ P; inres R x⟧ ⟹ S ⟧ ⟹ S"
by (metis (full_types))
lemma inres_SPEC:
"inres M x ⟹ M ≤ SPEC Φ ⟹ Φ x"
by (auto dest: pwD2)
lemma SPEC_nofail:
"X ≤ SPEC Φ ⟹ nofail X"
by (auto dest: pwD1)
lemma nofail_SPEC: "nofail m ⟹ m ≤ SPEC (λ_. True)"
by (simp add: pw_le_iff)
lemma nofail_SPEC_iff: "nofail m ⟷ m ≤ SPEC (λ_. True)"
by (simp add: pw_le_iff)
lemma nofail_SPEC_triv_refine: "⟦ nofail m; ⋀x. Φ x ⟧ ⟹ m ≤ SPEC Φ"
by (simp add: pw_le_iff)
end