Theory Refinement
theory Refinement imports Main
begin
section‹Monotonic Predicate Transformers›
text‹
In this section we introduce the basics of refinement calculus \<^cite>‹"back-wright-98"›.
Part of this theory is a reformulation of some definitions from \<^cite>‹"preoteasa:back:2010a"›,
but here they are given for predicates, while \<^cite>‹"preoteasa:back:2010a"› uses
sets.
›
notation
bot (‹⊥›) and
top (‹⊤›) and
inf (infixl ‹⊓› 70)
and sup (infixl ‹⊔› 65)
subsection‹Basic predicate transformers›
definition
demonic :: "('a => 'b::lattice) => 'b => 'a ⇒ bool" (‹[: _ :]› [0] 1000) where
"[:Q:] p s = (Q s ≤ p)"
definition
assert::"'a::semilattice_inf => 'a => 'a" (‹{. _ .}› [0] 1000) where
"{.p.} q ≡ p ⊓ q"
definition
"assume"::"('a::boolean_algebra) => 'a => 'a" (‹[. _ .]› [0] 1000) where
"[.p.] q ≡ (-p ⊔ q)"
definition
angelic :: "('a ⇒ 'b::{semilattice_inf,order_bot}) ⇒ 'b ⇒ 'a ⇒ bool" (‹{: _ :}› [0] 1000) where
"{:Q:} p s = (Q s ⊓ p ≠ ⊥)"
syntax
"_assert" :: "patterns => logic => logic" (‹(1{._./ _.})›)
translations
"_assert (_patterns x xs) P" == "CONST assert (CONST id (_abs (_pattern x xs) P))"
"_assert x P" == "CONST assert (CONST id (_abs x P))"
term "{.x,z . P x y.}"
syntax "_update" :: "patterns => patterns => logic => logic" (‹_ ↝ _ . _› 0)
translations
"_update (_patterns x xs) (_patterns y ys) t" == "CONST id (_abs
(_pattern x xs) (CONST id (_abs (_pattern y ys) t)))"
"_update x y t" == "CONST id (_abs x (CONST id (_abs y t)))"
term "[: x ↝ z . (P::'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool) x y y' z :]"
term "[: x, y ↝ y', z . (P::'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool) x y y' z :]"
term "{: x, y ↝ y', z . (P::'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ bool) x y y' z :}"
lemma demonic_demonic: "[:r:] o [:r':] = [:r OO r':]"
by (simp add: fun_eq_iff le_fun_def demonic_def, auto)
lemma assert_demonic_comp: "{.p.} o [:r:] o {.p'.} o [:r':] =
{.x . p x ∧ (∀ y . r x y ⟶ p' y).} o [:r OO r':]"
by (auto simp add: fun_eq_iff le_fun_def assert_def demonic_def)
lemma demonic_assert_comp: "[:r:] o {.p.} = {.x.(∀ y . r x y ⟶ p y).} o [:r:]"
by (auto simp add: fun_eq_iff le_fun_def assert_def demonic_def)
lemma assert_assert_comp: "{.p::'a::lattice.} o {.p'.} = {.p ⊓ p'.}"
by (simp add: fun_eq_iff le_fun_def assert_def demonic_def inf_assoc)
definition "inpt r x = (∃ y . r x y)"
definition "trs r = {. inpt r.} o [:r:]"
lemma "trs (λ x y . x = y) q x = q x"
by (simp add: trs_def fun_eq_iff assert_def demonic_def inpt_def bot_fun_def le_fun_def)
lemma assert_demonic_prop: "{.p.} o [:r:] = {.p.} o [:(λ x y . p x) ⊓ r:]"
by (auto simp add: fun_eq_iff assert_def demonic_def)
lemma relcompp_exists: "relcompp r r' x y = (∃ u . r x u ∧ r' u y)"
by auto
lemma trs_trs: "(trs r) o (trs r') = trs ((λ s t. (∀ s' . r s s' ⟶ (inpt r' s'))) ⊓ (r OO r'))" (is "?S = ?T")
proof -
have [simp]: "(λx. inpt r x ∧ (∀y. r x y ⟶ inpt r' y)) = inpt ((λs t. ∀s'. r s s' ⟶ inpt r' s') ⊓ r OO r')"
by (auto simp add: fun_eq_iff inpt_def relcompp_exists, blast)
have [simp]: "(λx y. inpt r x ∧ (∀y. r x y ⟶ inpt r' y)) ⊓ r OO r' = (λs t. ∀s'. r s s' ⟶ inpt r' s') ⊓ r OO r'"
by (auto simp add: fun_eq_iff inpt_def)
have "?S = {. inpt r .} ∘ [: r :] ∘ {. inpt r' .} ∘ [: r' :]"
by (simp add: trs_def comp_assoc[symmetric])
also have "... = {. λx. inpt r x ∧ (∀y. r x y ⟶ inpt r' y) .} ∘ [: r OO r' :]"
by (simp add: assert_demonic_comp)
also have "... = {. λx. inpt r x ∧ (∀y. r x y ⟶ inpt r' y) .} o [:(λ x y . inpt r x ∧ (∀y. r x y ⟶ inpt r' y)) ⊓ (r OO r'):]"
by (subst assert_demonic_prop, simp)
also have "... = ?T"
by (simp add: trs_def)
finally show ?thesis by simp
qed
lemma assert_demonic_refinement: "({.p.} o [:r:] ≤ {.p'.} o [:r':]) = (p ≤ p' ∧ (∀ x . p x ⟶ r' x ≤ r x))"
by (auto simp add: le_fun_def assert_def demonic_def)
lemma trs_refinement: "(trs r ≤ trs r') = ((∀ x . inpt r x ⟶ inpt r' x) ∧ (∀ x . inpt r x ⟶ r' x ≤ r x))"
by (simp add: trs_def assert_demonic_refinement, simp add: le_fun_def)
lemma "trs (λ x y . x ≥ 0) ≤ trs (λ x y . x = y)"
by (simp add: trs_def le_fun_def assert_def demonic_def inpt_def)
lemma "trs (λ x y . x ≥ 0) q x = (if q = ⊤ then x ≥ 0 else False)"
by (auto simp add: trs_def fun_eq_iff assert_def demonic_def inpt_def bot_fun_def)
lemma "[:r:] ⊓ [:r':] = [:r ⊔ r':]"
by (simp add: fun_eq_iff demonic_def)
lemma spec_demonic_choice: "({.p.} o [:r:]) ⊓ ({.p'.} o [:r':]) = ({.p ⊓ p'.} o [:r ⊔ r':])"
by (auto simp add: fun_eq_iff demonic_def assert_def)
lemma trs_demonic_choice: "trs r ⊓ trs r' = trs ((λ x y . inpt r x ∧ inpt r' x) ⊓ (r ⊔ r'))"
proof -
have [simp]: "inpt ((λx y. inpt r x ∧ inpt r' x) ⊓ (r ⊔ r')) = inpt r ⊓ inpt r'"
by (auto simp add: fun_eq_iff inpt_def)
have "trs r ⊓ trs r' = {. inpt r ⊓ inpt r' .} ∘ [: r ⊔ r' :]"
by (simp add: trs_def spec_demonic_choice)
also have "... = {. inpt r ⊓ inpt r' .} ∘ [: (λ x y . inpt r x ∧ inpt r' x) ⊓ (r ⊔ r') :]"
by (subst assert_demonic_prop, simp)
also have "... = trs ((λ x y . inpt r x ∧ inpt r' x) ⊓ (r ⊔ r'))"
by (simp add: trs_def)
finally show ?thesis by simp
qed
lemma "p ⊓ p' = ⊥ ⟹ ({.p.} o [:r:]) ⊔ ({.p'.} o [:r':]) = {.p ⊔ p'.} o [:(λ x y . p x ⟶ r x y) ⊓ ((λ x y . p' x ⟶ r' x y)):]"
by (simp add: fun_eq_iff assert_def demonic_def, auto)
subsection‹Conjunctive predicate transformers›
definition "conjunctive (S::'a::complete_lattice ⇒ 'b::complete_lattice) = (∀ Q . S (Inf Q) = Inf (S ` Q))"
definition "sconjunctive (S::'a::complete_lattice ⇒ 'b::complete_lattice) = (∀ Q . (∃ x . x ∈ Q) ⟶ S (Inf Q) = Inf (S ` Q))"
lemma [simp]: "conjunctive S ⟹ sconjunctive S"
by (simp add: conjunctive_def sconjunctive_def)
lemma [simp]: "conjunctive ⊤"
by (simp add: conjunctive_def)
lemma conjuncive_demonic [simp]: "conjunctive [:r:]"
proof (auto simp add: conjunctive_def fun_eq_iff demonic_def)
fix Q:: "'a set" fix y::'a fix x :: 'b
assume A: "y ∈ Q"
assume "r x ≤ Inf Q"
also from A have "Inf Q ≤ y"
by (rule Inf_lower)
finally show "r x ≤ y" by simp
next
fix Q:: "'a set" fix x :: 'b
assume A : "∀y∈Q. r x ≤ y"
show "r x ≤ Inf Q"
by (rule Inf_greatest, simp add: A)
qed
lemma sconjunctive_assert [simp]: "sconjunctive {.p.}"
proof (auto simp add: sconjunctive_def assert_def image_def cong: INF_cong_simp, rule antisym, auto)
fix Q :: "'a set"
have [simp]: "⋀ x . x ∈ Q ⟹ Inf Q ≤ x"
by (rule Inf_lower, simp)
have A: "⋀ x . x ∈ Q ⟹ p ⊓ Inf Q ≤ p ⊓ x"
by (simp, rule_tac y = "Inf Q" in order_trans, simp_all)
show "p ⊓ Inf Q ≤ (INF x∈Q. p ⊓ x)"
by (rule Inf_greatest, safe, rule A, simp)
next
fix Q :: "'a set"
fix x :: 'a
assume A: "x ∈ Q"
have "Inf {y. ∃x∈Q. y = p ⊓ x} ≤ p ⊓ x"
by (rule Inf_lower, cut_tac A, auto)
also have "... ≤ p"
by simp
finally show "(INF x∈Q. p ⊓ x) ≤ p"
by (simp only: image_def)
next
fix Q :: "'a set"
show "(INF x∈Q. p ⊓ x) ≤ Inf Q"
proof (rule Inf_greatest)
fix x::'a
assume A: "x ∈ Q"
have "Inf {y. ∃x∈Q. y = p ⊓ x} ≤ p ⊓ x"
by (cut_tac A, rule Inf_lower, blast)
also have "... ≤ x"
by simp
finally show "(INF x∈Q. p ⊓ x) ≤ x"
by (simp only: image_def)
qed
qed
lemma sconjunctive_simp: "x ∈ Q ⟹ sconjunctive S ⟹ S (Inf Q) = Inf (S ` Q)"
by (auto simp add: sconjunctive_def)
lemma sconjunctive_INF_simp: "x ∈ X ⟹ sconjunctive S ⟹ S (Inf (Q ` X)) = Inf (S ` (Q ` X))"
by (cut_tac x = "Q x" and Q = "Q ` X" in sconjunctive_simp, auto)
lemma demonic_comp [simp]: "sconjunctive S ⟹ sconjunctive S' ⟹ sconjunctive (S o S')"
proof (subst sconjunctive_def, safe)
fix X :: "'c set"
fix a :: 'c
assume [simp]: "sconjunctive S"
assume [simp]: "sconjunctive S'"
assume [simp]: "a ∈ X"
have A: "S' (Inf X) = Inf (S' ` X)"
by (rule_tac x = a in sconjunctive_simp, auto)
also have B: "S (Inf (S' ` X)) = Inf (S ` (S' ` X))"
by (rule_tac x = "S' a" in sconjunctive_simp, auto)
finally show "(S o S') (Inf X) = Inf ((S ∘ S') ` X)" by (simp add: image_comp)
qed
lemma [simp]:"conjunctive S ⟹ S (Inf (Q ` X)) = (Inf ((S o Q) ` X))"
by (metis INF_image conjunctive_def)
lemma conjunctive_simp: "conjunctive S ⟹ S (Inf Q) = Inf (S ` Q)"
by (metis conjunctive_def)
lemma conjunctive_monotonic: "sconjunctive S ⟹ mono S"
proof (rule monoI)
fix a b :: 'a
assume [simp]: "a ≤ b"
assume [simp]: "sconjunctive S"
have [simp]: "a ⊓ b = a"
by (rule antisym, auto)
have A: "S a = S a ⊓ S b"
by (cut_tac S = S and x = a and Q = "{a, b}" in sconjunctive_simp, auto)
show "S a ≤ S b"
by (subst A, simp)
qed
definition "grd S = - S ⊥"
lemma "grd [:r:] = inpt r"
by (simp add: fun_eq_iff grd_def demonic_def le_fun_def inpt_def)
definition "fail S = -(S ⊤)"
definition "term S = (S ⊤)"
lemma "fail ({.p.} o [:r :: 'a ⇒ 'b ⇒ bool:]) = -p"
by (simp add: fail_def fun_eq_iff assert_def demonic_def le_fun_def top_fun_def)
definition "Fail = ⊥"
lemma "mono (S::'a::boolean_algebra ⇒ 'b::boolean_algebra) ⟹ (S = Fail) = (fail S = ⊤)"
proof auto
show "fail (Fail::'a ⇒ 'b) = ⊤"
by (metis Fail_def bot_apply compl_bot_eq fail_def)
next
assume A: "mono S"
assume B: "fail S = ⊤"
show "S = Fail"
proof (rule antisym)
show "S ≤ Fail"
by (metis (opaque_lifting, no_types) A B bot.extremum_unique compl_le_compl_iff fail_def le_fun_def monoD top_greatest)
next
show "Fail ≤ S"
by (metis Fail_def bot.extremum)
qed
qed
definition "Skip = id"
lemma [simp]: "{.⊤::'a::bounded_lattice.} = Skip"
by (simp add: fun_eq_iff assert_def Skip_def)
lemma [simp]:"Skip o S = S"
by (simp add: fun_eq_iff assert_def Skip_def)
lemma [simp]:"S o Skip = S"
by (simp add: fun_eq_iff assert_def Skip_def)
lemma [simp]: "mono S ⟹ mono S' ⟹ mono (S o S')"
by (simp add: mono_def)
lemma [simp]: "mono {.p::('a ⇒ bool).}"
by (simp add: conjunctive_monotonic)
lemma [simp]: "mono [:r::('a ⇒ 'b ⇒ bool):]"
by (simp add: conjunctive_monotonic)
lemma [simp]:"{. λ x . True .} = Skip"
by (simp add: fun_eq_iff assert_def Skip_def)
lemma [simp]: "⊥ o S = ⊥"
by (simp add: fun_eq_iff)
lemma [simp]: "{.⊥::'a::boolean_algebra.} = ⊥"
by (simp add: fun_eq_iff assert_def)
lemma [simp]: "⊤ o S = ⊤"
by (simp add: fun_eq_iff)
lemma left_comp: "T o U = T' o U' ⟹ S o T o U = S o T' o U'"
by (simp add: comp_assoc)
lemma assert_demonic: "{.p.} o [:r:] = {.p.} o [:λ x y . p x ∧ r x y:]"
by (auto simp add: fun_eq_iff assert_def demonic_def le_fun_def)
lemma "trs r ⊓ trs r' = trs (λ x y . inpt r x ∧ inpt r' x ∧ (r x y ∨ r' x y))"
by (auto simp add: fun_eq_iff trs_def assert_def demonic_def inpt_def)
subsection‹Fusion of predicate transformers›
text‹
In this section we define the fusion operator from \<^cite>‹"back:butler:1995"›. The fusion
of two programs $S$ and $T$ is intuitively equivalent with the parallel execution of the two
programs. If $S$ and $T$ assign nondeterministically some value to some program variable
$x$, then the fusion of $S$ and $T$ will assign a value to $x$ which can be assigned by
both $S$ and $T$.
›
definition fusion :: "(('a ⇒ bool) ⇒ ('b ⇒ bool)) ⇒ (('a ⇒ bool) ⇒ ('b ⇒ bool)) ⇒ (('a ⇒ bool) ⇒ ('b ⇒ bool))" (infixl ‹∥› 70) where
"(S ∥ S') q x = (∃ (p::'a⇒bool) p' . p ⊓ p' ≤ q ∧ S p x ∧ S' p' x)"
lemma fusion_spec: "({.p.} ∘ [:r:]) ∥ ({.p'.} ∘ [:r':]) = ({.p ⊓ p'.} ∘ [:r ⊓ r':])"
by (auto simp add: fun_eq_iff fusion_def assert_def demonic_def le_fun_def)
lemma fusion_assoc: "S ∥ (T ∥ U) = (S ∥ T) ∥ U"
proof (rule antisym, auto simp add: fusion_def)
fix p p' q s s' :: "'a ⇒ bool"
fix a
assume A: "p ⊓ p' ≤ q" and B: "s ⊓ s' ≤ p'"
assume C: "S p a" and D: "T s a" and E: "U s' a"
from A and B have F: "(p ⊓ s) ⊓ s' ≤ q"
by (simp add: le_fun_def)
have "(∃v v'. v ⊓ v' ≤ (p ⊓ s) ∧ S v a ∧ T v' a)"
by (metis C D order_refl)
show "∃u u' . u ⊓ u' ≤ q ∧ (∃v v'. v ⊓ v' ≤ u ∧ S v a ∧ T v' a) ∧ U u' a"
by (metis F C D E order_refl)
next
fix p p' q s s' :: "'a ⇒ bool"
fix a
assume A: "p ⊓ p' ≤ q" and B: "s ⊓ s' ≤ p"
assume C: "S s a" and D: "T s' a" and E: "U p' a"
from A and B have F: "s ⊓ (s' ⊓ p') ≤ q"
by (simp add: le_fun_def)
have "(∃v v'. v ⊓ v' ≤ s' ⊓ p' ∧ T v a ∧ U v' a)"
by (metis D E eq_iff)
show "∃u u'. u ⊓ u' ≤ q ∧ S u a ∧ (∃v v'. v ⊓ v' ≤ u' ∧ T v a ∧ U v' a)"
by (metis F C D E order_refl)
qed
lemma "P ≤ Q ⟹ P' ≤ Q' ⟹ P ∥ P' ≤ Q ∥ Q'"
by (simp add: le_fun_def fusion_def, metis)
lemma "conjunctive S ⟹ S ∥ ⊤ = ⊤"
by (auto simp add: fun_eq_iff fusion_def le_fun_def conjunctive_def)
lemma fusion_spec_local: "a ∈ init ⟹ ([:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.p.} ∘ [:r:]) ∥ ({.p'.} ∘ [:r':])
= [:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.u,x . p (u, x) ∧ p' x.} ∘ [:u, x ↝ y . r (u, x) y ∧ r' x y:]" (is "?p ⟹ ?S = ?T")
proof -
assume "?p"
from this have [simp]: "(λx. ∀a. a ∈ init ⟶ p (a, x) ∧ p' x) = (λx. ∀a. a ∈ init ⟶ p (a, x)) ⊓ p'"
by auto
have [simp]: "(λx (u, y). u ∈ init ∧ x = y) OO (λ(u, x) y. r (u, x) y ∧ r' x y) = (λx (u, y). u ∈ init ∧ x = y) OO r ⊓ r'"
by auto
have "?S =
({. λx. ∀a. a ∈ init ⟶ p (a, x) .} ∘ [: λx (u, y). u ∈ init ∧ x = y :] ∘ [: r :]) ∥ ({. p' .} ∘ [: r' :])"
by (simp add: demonic_assert_comp)
also have "... = {. (λx. ∀a. a ∈ init ⟶ p (a, x)) ⊓ p' .} ∘ [: (λx (u, y). u ∈ init ∧ x = y) OO r ⊓ r' :]"
by (simp add: comp_assoc demonic_demonic fusion_spec)
also have "... = ?T"
by (simp add: demonic_assert_comp comp_assoc demonic_demonic fusion_spec)
finally show ?thesis by simp
qed
lemma fusion_spec_local_a: "a ∈ init ⟹ ([:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.p.} ∘ [:r:]) ∥ [:r':]
= ([:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.p.} ∘ [:u, x ↝ y . r (u, x) y ∧ r' x y:])"
by (cut_tac p' = "⊤" and init = init and p = p and r = r and r' = r' in fusion_spec_local, auto)
lemma fusion_local_refinement:
"a ∈ init ⟹ (⋀ x u y . u ∈ init ⟹ p' x ⟹ r (u, x) y ⟹ r' x y) ⟹
{.p'.} o (([:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.p.} ∘ [:r:]) ∥ [:r':]) ≤ [:x ↝ u, y . u ∈ init ∧ x = y:] ∘ {.p.} ∘ [:r:]"
proof -
assume A: "a ∈ init"
assume [simp]: "(⋀ x u y . u ∈ init ⟹ p' x ⟹ r (u, x) y ⟹ r' x y)"
have " {. x. p' x ∧ (∀a. a ∈ init ⟶ p (a, x)) .} ∘ [: (λx (u, y). u ∈ init ∧ x = y) OO (λ(u, x) y. r (u, x) y ∧ r' x y) :]
≤ {. λx. ∀a. a ∈ init ⟶ p (a, x) .} ∘ [: (λx (u, y). u ∈ init ∧ x = y) OO r :]"
by (auto simp add: assert_demonic_refinement)
from this have " {. x. p' x ∧ (∀a. a ∈ init ⟶ p (a, x)) .} ∘ [: (λx (u, y). u ∈ init ∧ x = y) OO (λ(u, x) y. r (u, x) y ∧ r' x y) :]
≤ {. λx. ∀a. a ∈ init ⟶ p (a, x) .} ∘ [: λx (u, y). u ∈ init ∧ x = y :] ∘ [: r :]"
by (simp add: comp_assoc demonic_demonic)
from this have "{. p' .} ∘ [: λx (u, y). u ∈ init ∧ x = y :] ∘ {. p .} ∘ [: λ(u, x) y. r (u, x) y ∧ r' x y :]
≤ [: x ↝ u, y. u ∈ init ∧ x = y :] ∘ {. p .} ∘ [: r :]"
by (simp add: demonic_assert_comp assert_demonic_comp)
from this have "{. p' .} ∘ ([: x ↝ (u, y) . u ∈ init ∧ x = y :] ∘ {. p .} ∘ [: (u, x) ↝ y . r (u, x) y ∧ r' x y :])
≤ [: x ↝ (u, y) . u ∈ init ∧ x = y :] ∘ {. p .} ∘ [: r :]"
by (simp add: comp_assoc [THEN sym])
from A and this show ?thesis
by (unfold fusion_spec_local_a, simp)
qed
end