header {* \isaheader{Basic Concepts} *}
theory Refine_Basic
imports Main
"~~/src/HOL/Library/Monad_Syntax"
"Refine_Misc"
"Generic/RefineG_Recursion"
"Generic/RefineG_Assert"
begin
subsection {* Setup *}
ML {*
structure Refine = struct
structure vcg = Named_Thms
( val name = @{binding refine_vcg}
val description = "Refinement Framework: " ^
"Verification condition generation rules (intro)" )
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)" )
structure refine_pw_simps = Named_Thms
( val name = @{binding refine_pw_simps}
val description = "Refinement Framework: " ^
"Simplifier rules for pointwise reasoning" )
(* Replaced by respective solvers in tagged solver
structure refine_post = Named_Thms
( val name = @{binding refine_post}
val description = "Refinement Framework: " ^
"Postprocessing rules" )
*)
(* If set to true, the product splitter of refine_rcg is disabled. *)
val no_prod_split =
Attrib.setup_config_bool @{binding refine_no_prod_split} (K false);
fun rcg_tac add_thms ctxt =
let
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 @{thms impI allI}));
in
REPEAT_ALL_NEW (DETERM o (resolve_tac ref_thms ORELSE' prod_simp_tac))
end;
fun post_tac ctxt = let
(*val thms = refine_post.get ctxt;*)
in
REPEAT_ALL_NEW (FIRST' [
eq_assume_tac,
(*match_tac thms,*)
SOLVED' (Tagged_Solver.solve_tac ctxt)])
(* TODO: Get rid of refine_post! Use tagged_solver instead *)
end;
end;
*}
setup {* Refine.vcg.setup *}
setup {* Refine.refine0.setup *}
setup {* Refine.refine.setup *}
setup {* Refine.refine2.setup *}
setup {* Refine.refine_pw_simps.setup *}
method_setup refine_rcg =
{* Attrib.thms >> (fn add_thms => fn ctxt => SIMPLE_METHOD' (
Refine.rcg_tac add_thms ctxt THEN_ALL_NEW (TRY o Refine.post_tac ctxt)
)) *}
"Refinement framework: Generate refinement conditions"
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
@{text RES}, that embeds a set of results into our lattice. Its synonym for
a predicate is @{text SPEC}.
Program correctness is expressed by refinement, i.e., the expression
@{text "M ≤ SPEC Φ"} means that @{text M} is correct w.r.t.\
specification @{text Φ}. This suggests the following view on the program
lattice: The top-element is the result that is never correct. We call this
result @{text FAIL}. The bottom element is the program that is always correct.
It is called @{text 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 {*
@{text FAILi} is only an internal notation, that should not be exposed to
the user.
Instead, @{text 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 (\<Union>{x . RES x ∈ X})"
definition "Inf X ≡ if ∃x. RES x∈X then RES (\<Inter>{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 @{text "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. SUPREMUM X f = FAIL <-> FAIL ∈ f ` X"
"!!X. FAIL = Sup X <-> FAIL∈X"
"!!X f. FAIL = SUPREMUM X f <-> FAIL ∈ f ` X"
"!!X. FAIL∈X ==> Sup X = FAIL"
"!!X. FAIL∈f ` X ==> SUPREMUM X f = FAIL"
"!!A. Sup (RES ` A) = RES (Sup A)"
"!!A. SUPREMUM A RES = RES (Sup A)"
"!!A. A≠{} ==> Inf (RES`A) = RES (Inf A)"
"!!A. A≠{} ==> INFIMUM A RES = 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 SUP_def INF_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: split_if_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 *}
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 (SUPREMUM X f) 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 (SUPREMUM X f) <-> (∀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 (INFIMUM C f) <-> (∃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 (INFIMUM C f) r <-> (∀M∈C. inres (f M) r)"
using pw_Inf_inres [of "f ` C"] by simp
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{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
thm partial_function_mono
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_sup: "bind (sup M N) f = sup (bind M f) (bind N f)"
by (auto simp add: 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 {* Data Refinement *}
text {*
In this section we establish a notion of pointwise data refinement, by
lifting a relation @{text "R"} between concrete and abstract values to
our result lattice.
Given a relation @{text R}, we define a {\em concretization function}
@{text "\<Down>R"} that takes an abstract result, and returns a concrete result.
The concrete result contains all values that are mapped by @{text R} to
a value in the abstract result.
Note that our concretization function forms no Galois connection, i.e.,
in general there is no @{text α} such that
@{text "m ≤\<Down> R m'"} is equivalent to @{text "α 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 ("\<Down>") where
"conc_fun R m ≡ case m of FAILi => FAIL | RES X => RES (R¯``X)"
definition abs_fun ("\<Up>") 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]: "\<Down>R FAIL = FAIL" and
conc_fun_RES: "\<Down>R (RES X) = RES (R¯``X)"
unfolding conc_fun_def by (auto split: nres.split)
lemma abs_fun_simps[simp]:
"\<Up>R FAIL = FAIL"
"X⊆Domain R ==> \<Up>R (RES X) = RES (R``X)"
"¬(X⊆Domain R) ==> \<Up>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' ≤ \<Down>R m <-> \<Up>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 (\<Up>R) (\<Down>R)"
apply (unfold_locales)
by (rule conc_abs_swap)
end
lemma pw_abs_nofail[refine_pw_simps]:
"nofail (\<Up>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 (\<Up>R M) a <-> (nofail (\<Up>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 (\<Down>R S) = nofail S"
by (cases S) (auto simp: conc_fun_RES)
lemma pw_conc_inres[refine_pw_simps]:
"inres (\<Down>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]:
"\<Up> R SUCCEED = SUCCEED"
unfolding abs_fun_def by (auto split: nres.split)
lemma conc_fun_strict[simp]:
"\<Down> R SUCCEED = SUCCEED"
unfolding conc_fun_def by (auto split: nres.split)
lemma conc_fun_mono[simp, intro!]: "mono (\<Down>R)"
by rule (auto simp: pw_le_iff refine_pw_simps)
lemma abs_fun_mono[simp, intro!]: "mono (\<Up>R)"
by rule (auto simp: pw_le_iff refine_pw_simps)
lemma conc_fun_chain: "\<Down>R (\<Down>S M) = \<Down>(R O S) M"
unfolding conc_fun_def
by (auto split: nres.split)
lemma conc_Id[simp]: "\<Down>Id = id"
unfolding conc_fun_def [abs_def] by (auto split: nres.split)
lemma abs_Id[simp]: "\<Up>Id = id"
unfolding abs_fun_def [abs_def] by (auto split: nres.split)
lemma conc_fun_fail_iff[simp]:
"\<Down>R S = FAIL <-> S=FAIL"
"FAIL = \<Down>R S <-> S=FAIL"
by (auto simp add: pw_eq_iff refine_pw_simps)
lemma conc_trans[trans]:
assumes A: "C ≤ \<Down>R B" and B: "B ≤ \<Down>R' A"
shows "C ≤ \<Down>R (\<Down>R' A)"
using assms by (fastforce simp: pw_le_iff refine_pw_simps)
lemma abs_trans[trans]:
assumes A: "\<Up>R C ≤ B" and B: "\<Up>R' B ≤ A"
shows "\<Up>R' (\<Up>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≤\<Down>R B ==> B≤ C ==> A≤\<Down>R C"
"!!A B C. A≤\<Down>Id B ==> B≤\<Down>R C ==> A≤\<Down>R C"
"!!A B C. A≤\<Down>R B ==> B≤\<Down>Id C ==> A≤\<Down>R C"
"!!A B C. A≤\<Down>Id B ==> B≤\<Down>Id C ==> A≤ C"
"!!A B C. A≤\<Down>Id B ==> B≤ C ==> A≤ C"
"!!A B C. A≤ B ==> B≤\<Down>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; \<Up> R B ≤ C|] ==> \<Up> R A ≤ C"
"!!A B C. [|\<Up> Id A ≤ B; \<Up> R B ≤ C|] ==> \<Up> R A ≤ C"
"!!A B C. [|\<Up> R A ≤ B; \<Up> Id B ≤ C|] ==> \<Up> R A ≤ C"
"!!A B C. [|\<Up> Id A ≤ B; \<Up> Id B ≤ C|] ==> A ≤ C"
"!!A B C. [|\<Up> Id A ≤ B; B ≤ C|] ==> A ≤ C"
"!!A B C. [|A ≤ B; \<Up> 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)
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 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 (op = 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 Φ) <-> SUPREMUM S f ≤ 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 Φ"
-- {* Note: @{text "η"}-expanded version helps Isabelle's unification to keep meaningful
variable names from the program *}
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 ≤ \<Down>Id S" by auto
lemma RES_refine:
"[| !!s. s∈S ==> ∃s'∈S'. (s,s')∈R|] ==> RES S ≤ \<Down>R (RES S')"
by (auto simp: conc_fun_RES)
lemma SPEC_refine:
assumes "S ≤ SPEC (λx. ∃x'. (x,x')∈R ∧ Φ x')"
shows "S ≤ \<Down>R (SPEC Φ)"
using assms
by (force simp: pw_le_iff refine_pw_simps)
lemma Id_SPEC_refine[refine]:
"S ≤ SPEC Φ ==> S ≤ \<Down>Id (SPEC Φ)" by simp
lemma RETURN_refine[refine]:
assumes "(x,x')∈R"
shows "RETURN x ≤ \<Down>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 ≤ \<Down>R (SPEC Φ)"
using assms
by (auto simp: pw_le_iff refine_pw_simps)
lemma FAIL_refine[refine]: "X ≤ \<Down>R FAIL" by auto
lemma SUCCEED_refine[refine]: "SUCCEED ≤ \<Down>R X'" by auto
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 ≤ \<Down> R' M'"
assumes R2: "!!x x'. [| (x,x')∈R'; inres M x; inres M' x';
nofail M; nofail M'
|] ==> f x ≤ \<Down> R (f' x')"
shows "bind M (λx. f x) ≤ \<Down> 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 ≤ \<Down> R' M'"
assumes R2: "!!x x'. [| (x,x')∈R' |]
==> f x ≤ \<Down> R (f' x')"
shows "bind M (λx. f x) ≤ \<Down> R (bind M' (λx'. f' x'))"
apply (rule bind_refine') using assms by auto
text {* Special cases for refinement of binding to @{text "RES"}
statements *}
lemma bind_refine_RES:
"[|RES X ≤ \<Down> R' M';
!!x x'. [|(x, x') ∈ R'; x ∈ X |] ==> f x ≤ \<Down> R (f' x')|]
==> RES X »= (λx. f x) ≤ \<Down> R (M' »= (λx'. f' x'))"
"[|M ≤ \<Down> R' (RES X');
!!x x'. [|(x, x') ∈ R'; x' ∈ X' |] ==> f x ≤ \<Down> R (f' x')|]
==> M »= (λx. f x) ≤ \<Down> R (RES X' »= (λx'. f' x'))"
"[|RES X ≤ \<Down> R' (RES X');
!!x x'. [|(x, x') ∈ R'; x ∈ X; x' ∈ X'|] ==> f x ≤ \<Down> R (f' x')|]
==> RES X »= (λx. f x) ≤ \<Down> 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 Φ ≤ \<Down>Id (ASSERT Φ')"
by (cases Φ') auto
lemma ASSUME_refine[refine]:
"[| Φ ==> Φ' |] ==> ASSUME Φ ≤ \<Down>Id (ASSUME Φ')"
by (cases Φ) auto
text {*
Assertions and assumptions are treated specially in bindings
*}
lemma ASSERT_refine_right:
assumes "Φ ==> S ≤\<Down>R S'"
shows "S ≤\<Down>R (do {ASSERT Φ; S'})"
using assms by (cases Φ) auto
lemma ASSERT_refine_right_pres:
assumes "Φ ==> S ≤\<Down>R (do {ASSERT Φ; S'})"
shows "S ≤\<Down>R (do {ASSERT Φ; S'})"
using assms by (cases Φ) auto
lemma ASSERT_refine_left:
assumes "Φ"
assumes "Φ ==> S ≤ \<Down>R S'"
shows "do{ASSERT Φ; S} ≤ \<Down>R S'"
using assms by (cases Φ) auto
lemma ASSUME_refine_right:
assumes "Φ"
assumes "Φ ==> S ≤\<Down>R S'"
shows "S ≤\<Down>R (do {ASSUME Φ; S'})"
using assms by (cases Φ) auto
lemma ASSUME_refine_left:
assumes "Φ ==> S ≤ \<Down>R S'"
shows "do {ASSUME Φ; S} ≤ \<Down>R S'"
using assms by (cases Φ) auto
lemma ASSUME_refine_left_pres:
assumes "Φ ==> do {ASSUME Φ; S} ≤ \<Down>R S'"
shows "do {ASSUME Φ; S} ≤ \<Down>R S'"
using assms by (cases Φ) auto
text {* Warning: The order of @{text "[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 @{text "intro refine"} still
seems to be used instead of @{text "refine_rcg"}. *}
lemmas [refine] = ASSUME_refine_right
lemmas [refine] = ASSERT_refine_left
lemmas [refine] = ASSUME_refine_left
lemmas [refine] = ASSERT_refine_right
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 ≤\<Down>S (f' x'); (x,x')∈R;
REC body' = f' |]
==> body f x ≤\<Down>S (body' f' x')"
shows "REC (λf x. body f x) x ≤\<Down>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 ≤\<Down>S (f' x'); (x,x')∈R |]
==> body f x ≤\<Down>S (body' f' x')"
shows "RECT (λf x. body f x) x ≤\<Down>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 ≤ \<Down>R S1'"
assumes "[|¬b;¬b'|] ==> S2 ≤ \<Down>R S2'"
shows "(if b then S1 else S2) ≤ \<Down>R (if b' then S1' else S2')"
using assms by auto
lemma Let_unfold_refine[refine]:
assumes "f x ≤ \<Down>R (f' x')"
shows "Let x f ≤ \<Down>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 ≤ \<Down>R (f' x')"
shows "Let m (λx. f x) ≤\<Down>R (Let m' (λx'. f' x'))"
using assms by auto
lemma case_option_refine[refine]:
assumes "(x,x')∈Id"
assumes "fn ≤ \<Down>R fn'"
assumes "!!v v'. [|x=Some v; (v,v')∈Id|] ==> fs v ≤ \<Down>R (fs' v')"
shows "case_option fn (λv. fs v) x ≤ \<Down>R (case_option fn' (λv'. fs' v') x')"
using assms by (auto split: option.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 ≤ \<Down>R (f x)"
shows "M ≤ \<Down>R (Let x f)" using assms by auto
lemma intro_Let_refine[refine2]:
assumes "f x ≤ \<Down>R M'"
shows "Let x f ≤ \<Down>R M'" using assms by auto
lemma bind2let_refine[refine2]:
assumes "RETURN x ≤ \<Down>R' M'"
assumes "!!x'. (x,x')∈R' ==> f x ≤ \<Down>R (f' x')"
shows "Let x f ≤ \<Down>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' ≤\<Down>R' (RETURN x);
!!x'. [|inres m' x'; (x',x)∈R'|] ==> f' x' ≤ \<Down>R (f x)
|] ==> m'»=(λx'. f' x') ≤ \<Down>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 ≤ \<Down>R' M'"
assumes "!!x'. (x,x')∈R' ==> RETURN (f x) ≤ \<Down>R (f' x')"
shows "RETURN (Let x f) ≤ \<Down>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 ≤ \<Down>R (RETURN a)"
using assms
by (simp add: pw_le_iff refine_pw_simps)
lemma RETURN_as_SPEC_refine_old:
"!!M R. M ≤ \<Down>R (SPEC (λx. x=v)) ==> M ≤\<Down>R (RETURN v)"
by (simp add: RETURN_def)
lemma if_RETURN_refine [refine2]:
assumes "b <-> b'"
assumes "[|b;b'|] ==> RETURN S1 ≤ \<Down>R S1'"
assumes "[|¬b;¬b'|] ==> RETURN S2 ≤ \<Down>R S2'"
shows "RETURN (if b then S1 else S2) ≤ \<Down>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 ≤ \<Down>R (RES {a})"
using assms
by (simp add: pw_le_iff refine_pw_simps)
lemma intro_spec_refine_iff:
"(bind (RES X) f ≤ \<Down>R M) <-> (∀x∈X. f x ≤ \<Down>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 ≤ \<Down>R M"
shows "bind (RES X) (λx. f x) ≤ \<Down>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 ≤ \<Down>R' (RETURN m')"
assumes "!!x x'. (x,x')∈R' ==> f x ≤ \<Down>R (f' x')"
shows "bind m (λx. f x) ≤ \<Down>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 ≤ \<Down>R' (RETURN m')"
assumes "!!x. (x,m')∈R' ==> f x ≤ \<Down>R m''"
shows "bind m (λx. f x) ≤ \<Down>R m''"
using assms
apply (simp add: pw_le_iff refine_pw_simps)
apply blast
done
lemma intro_bind_refine_id:
assumes "m ≤ (SPEC (op = m'))"
assumes "f m' ≤ \<Down>R m''"
shows "bind m f ≤ \<Down>R m''"
using assms
apply (simp add: pw_le_iff refine_pw_simps)
apply blast
done
subsection {* Relators *}
definition nres_rel where
nres_rel_def_internal: "nres_rel R ≡ {(c,a). c ≤ \<Down>R a}"
lemma nres_rel_def: "⟨R⟩nres_rel ≡ {(c,a). c ≤ \<Down>R a}"
by (simp add: nres_rel_def_internal relAPP_def)
lemma nres_relD: "(c,a)∈⟨R⟩nres_rel ==> c ≤\<Down>R a" by (simp add: nres_rel_def)
lemma nres_relI: "c ≤\<Down>R a ==> (c,a)∈⟨R⟩nres_rel" by (simp add: 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)
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}"
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
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"
apply (intro fun_relI)
using assms
apply (auto simp: nres_rel_def intro!: RECT_refine)
apply (simp add: fun_rel_def)
apply blast
done
end
subsection {* Convenience Rules*}
text {*
In this section, we define some lemmas that simplify common prover tasks.
*}
lemma ref_two_step: "A≤\<Down>R B ==> B≤C ==> A≤\<Down>R C"
by (rule conc_trans_additional)
lemma pw_ref_iff:
shows "S ≤ \<Down>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 ≤ \<Down>R S'"
using assms
by (simp add: pw_ref_iff)
text {* Introduce an abstraction relation. Usage:
@{text "rule introR[where R=absRel]"}
*}
lemma introR: "(a,a')∈R ==> (a,a')∈R" .
lemma intro_prgR: "c ≤ \<Down>R a ==> c ≤ \<Down>R a" by auto
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 ≤ \<Down>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 ≤ \<Down>R (RETURN a)"
shows "(c,a)∈R"
using assms
apply (auto simp: pw_le_iff refine_pw_simps)
done
lemma SPEC_eq_is_RETURN:
"SPEC (op = 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 build_rel_SPEC:
"M ≤ SPEC ( λx. Φ (α x) ∧ I x) ==> M ≤ \<Down>(build_rel α I) (SPEC Φ)"
by (auto simp: pw_le_iff refine_pw_simps build_rel_def)
lemma refine_IdD: "c ≤ \<Down>Id a ==> c ≤ a" by simp
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 ≤\<Down>R (f' x')"
and "nofail (f x) ==> f x ≤ SPEC I"
shows "f x ≤ \<Down> {(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\<leftarrow>m1; ASSERT (Φ x); m2 x} ≤ m'"
using assms
by (simp add: pw_le_iff refine_pw_simps) blast
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≤\<Down>R t"
assumes "¬b ==> ei≤\<Down>R e"
shows "do {b\<leftarrow>ci; if b then ti else ei} ≤ \<Down>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) ≤ \<Down>R M'"
shows "RETURN (Let x f) ≤ \<Down>R M'"
using assms by auto
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)
end