Theory utp_rel
section ‹ Alphabetised Relations ›
theory utp_rel
imports
utp_pred_laws
utp_healthy
utp_lift
utp_tactics
begin
text ‹ An alphabetised relation is simply a predicate whose state-space is a product type. In this
theory we construct the core operators of the relational calculus, and prove a libary of
associated theorems, based on Chapters 2 and 5 of the UTP book~\<^cite>‹"Hoare&98"›. ›
subsection ‹ Relational Alphabets ›
text ‹ We set up convenient syntax to refer to the input and output parts of the alphabet, as is
common in UTP. Since we are in a product space, these are simply the lenses @{term "fst⇩L"} and
@{term "snd⇩L"}. ›
definition inα :: "('α ⟹ 'α × 'β)" where
[lens_defs]: "inα = fst⇩L"
definition outα :: "('β ⟹ 'α × 'β)" where
[lens_defs]: "outα = snd⇩L"
lemma inα_uvar [simp]: "vwb_lens inα"
by (unfold_locales, auto simp add: inα_def)
lemma outα_uvar [simp]: "vwb_lens outα"
by (unfold_locales, auto simp add: outα_def)
lemma var_in_alpha [simp]: "x ;⇩L inα = ivar x"
by (simp add: fst_lens_def inα_def in_var_def)
lemma var_out_alpha [simp]: "x ;⇩L outα = ovar x"
by (simp add: outα_def out_var_def snd_lens_def)
lemma drop_pre_inv [simp]: "⟦ outα ♯ p ⟧ ⟹ ⌈⌊p⌋⇩<⌉⇩< = p"
by (pred_simp)
lemma usubst_lookup_ivar_unrest [usubst]:
"inα ♯ σ ⟹ ⟨σ⟩⇩s (ivar x) = $x"
by (rel_simp, metis fstI)
lemma usubst_lookup_ovar_unrest [usubst]:
"outα ♯ σ ⟹ ⟨σ⟩⇩s (ovar x) = $x´"
by (rel_simp, metis sndI)
lemma out_alpha_in_indep [simp]:
"outα ⨝ in_var x" "in_var x ⨝ outα"
by (simp_all add: in_var_def outα_def lens_indep_def fst_lens_def snd_lens_def lens_comp_def)
lemma in_alpha_out_indep [simp]:
"inα ⨝ out_var x" "out_var x ⨝ inα"
by (simp_all add: in_var_def inα_def lens_indep_def fst_lens_def lens_comp_def)
text ‹ The following two functions lift a predicate substitution to a relational one. ›
abbreviation usubst_rel_lift :: "'α usubst ⇒ ('α × 'β) usubst" ("⌈_⌉⇩s") where
"⌈σ⌉⇩s ≡ σ ⊕⇩s inα"
abbreviation usubst_rel_drop :: "('α × 'α) usubst ⇒ 'α usubst" ("⌊_⌋⇩s") where
"⌊σ⌋⇩s ≡ σ ↾⇩s inα"
text ‹ The alphabet of a relation then consists wholly of the input and output portions. ›
lemma alpha_in_out:
"Σ ≈⇩L inα +⇩L outα"
by (simp add: fst_snd_id_lens inα_def lens_equiv_refl outα_def)
subsection ‹ Relational Types and Operators ›
text ‹ We create type synonyms for conditions (which are simply predicates) -- i.e. relations
without dashed variables --, alphabetised relations where the input and output alphabet can
be different, and finally homogeneous relations. ›
type_synonym 'α cond = "'α upred"
type_synonym ('α, 'β) urel = "('α × 'β) upred"
type_synonym 'α hrel = "('α × 'α) upred"
type_synonym ('a, 'α) hexpr = "('a, 'α × 'α) uexpr"
translations
(type) "('α, 'β) urel" <= (type) "('α × 'β) upred"
text ‹ We set up some overloaded constants for sequential composition and the identity in case
we want to overload their definitions later. ›
consts
useq :: "'a ⇒ 'b ⇒ 'c" (infixr ";;" 61)
uassigns :: "'a usubst ⇒ 'b" ("⟨_⟩⇩a")
uskip :: "'a" ("II")
text ‹ We define a specialised version of the conditional where the condition can refer only to
undashed variables, as is usually the case in programs, but not universally in UTP models.
We implement this by lifting the condition predicate into the relational state-space with
construction @{term "⌈b⌉⇩<"}. ›
definition lift_rcond ("⌈_⌉⇩←") where
[upred_defs]: "⌈b⌉⇩← = ⌈b⌉⇩<"
abbreviation
rcond :: "('α, 'β) urel ⇒ 'α cond ⇒ ('α, 'β) urel ⇒ ('α, 'β) urel"
("(3_ ◃ _ ▹⇩r/ _)" [52,0,53] 52)
where "(P ◃ b ▹⇩r Q) ≡ (P ◃ ⌈b⌉⇩← ▹ Q)"
text ‹ Sequential composition is heterogeneous, and simply requires that the output alphabet
of the first matches then input alphabet of the second. We define it by lifting HOL's
built-in relational composition operator (@{term "(O)"}). Since this returns a set, the
definition states that the state binding $b$ is an element of this set. ›
lift_definition seqr::"('α, 'β) urel ⇒ ('β, 'γ) urel ⇒ ('α × 'γ) upred"
is "λ P Q b. b ∈ ({p. P p} O {q. Q q})" .
adhoc_overloading
useq seqr
text ‹ We also set up a homogeneous sequential composition operator, and versions of @{term true}
and @{term false} that are explicitly typed by a homogeneous alphabet. ›
abbreviation seqh :: "'α hrel ⇒ 'α hrel ⇒ 'α hrel" (infixr ";;⇩h" 61) where
"seqh P Q ≡ (P ;; Q)"
abbreviation truer :: "'α hrel" ("true⇩h") where
"truer ≡ true"
abbreviation falser :: "'α hrel" ("false⇩h") where
"falser ≡ false"
text ‹ We define the relational converse operator as an alphabet extrusion on the bijective
lens @{term swap⇩L} that swaps the elements of the product state-space. ›
abbreviation conv_r :: "('a, 'α × 'β) uexpr ⇒ ('a, 'β × 'α) uexpr" ("_⇧-" [999] 999)
where "conv_r e ≡ e ⊕⇩p swap⇩L"
text ‹ Assignment is defined using substitutions, where latter defines what each variable should
map to. This approach, which is originally due to Back~\<^cite>‹"Back1998"›, permits more general
assignment expressions. The definition of the operator identifies the after state binding, $b'$,
with the substitution function applied to the before state binding $b$. ›
lift_definition assigns_r :: "'α usubst ⇒ 'α hrel"
is "λ σ (b, b'). b' = σ(b)" .
adhoc_overloading
uassigns assigns_r
text ‹ Relational identity, or skip, is then simply an assignment with the identity substitution:
it simply identifies all variables. ›
definition skip_r :: "'α hrel" where
[urel_defs]: "skip_r = assigns_r id"
adhoc_overloading
uskip skip_r
text ‹ Non-deterministic assignment, also known as ``choose'', assigns an arbitrarily chosen value
to the given variable ›
definition nd_assign :: "('a ⟹ 'α) ⇒ 'α hrel" where
[urel_defs]: "nd_assign x = (⨅ v ∙ assigns_r [x ↦⇩s «v»])"
text ‹ We set up iterated sequential composition which iterates an indexed predicate over the
elements of a list. ›
definition seqr_iter :: "'a list ⇒ ('a ⇒ 'b hrel) ⇒ 'b hrel" where
[urel_defs]: "seqr_iter xs P = foldr (λ i Q. P(i) ;; Q) xs II"
text ‹ A singleton assignment simply applies a singleton substitution function, and similarly
for a double assignment. ›
abbreviation assign_r :: "('t ⟹ 'α) ⇒ ('t, 'α) uexpr ⇒ 'α hrel"
where "assign_r x v ≡ ⟨[x ↦⇩s v]⟩⇩a"
abbreviation assign_2_r ::
"('t1 ⟹ 'α) ⇒ ('t2 ⟹ 'α) ⇒ ('t1, 'α) uexpr ⇒ ('t2, 'α) uexpr ⇒ 'α hrel"
where "assign_2_r x y u v ≡ assigns_r [x ↦⇩s u, y ↦⇩s v]"
text ‹ We also define the alphabetised skip operator that identifies all input and output variables
in the given alphabet lens. All other variables are unrestricted. We also set up syntax for it. ›
definition skip_ra :: "('β, 'α) lens ⇒'α hrel" where
[urel_defs]: "skip_ra v = ($v´ =⇩u $v)"
text ‹ Similarly, we define the alphabetised assignment operator. ›
definition assigns_ra :: "'α usubst ⇒ ('β, 'α) lens ⇒ 'α hrel" ("⟨_⟩⇘_⇙") where
"⟨σ⟩⇘a⇙ = (⌈σ⌉⇩s † skip_ra a)"
text ‹ Assumptions ($c^{\top}$) and assertions ($c_{\bot}$) are encoded as conditionals. An assumption
behaves like skip if the condition is true, and otherwise behaves like @{term false} (miracle).
An assertion is the same, but yields @{term true}, which is an abort. They are the same as
tests, as in Kleene Algebra with Tests~\<^cite>‹"kozen1997kleene" and "Armstrong2015"›
(KAT), which embeds a Boolean algebra into a Kleene algebra to represent conditions. ›
definition rassume :: "'α upred ⇒ 'α hrel" where
[urel_defs]: "rassume c = II ◃ c ▹⇩r false"
definition rassert :: "'α upred ⇒ 'α hrel" where
[urel_defs]: "rassert c = II ◃ c ▹⇩r true"
text ‹ We define two variants of while loops based on strongest and weakest fixed points. The former
is @{term false} for an infinite loop, and the latter is @{term true}. ›
definition while_top :: "'α cond ⇒ 'α hrel ⇒ 'α hrel" where
[urel_defs]: "while_top b P = (ν X ∙ (P ;; X) ◃ b ▹⇩r II)"
definition while_bot :: "'α cond ⇒ 'α hrel ⇒ 'α hrel" where
[urel_defs]: "while_bot b P = (μ X ∙ (P ;; X) ◃ b ▹⇩r II)"
text ‹ While loops with invariant decoration (cf. \<^cite>‹"Armstrong2015"›) -- partial correctness. ›
definition while_inv :: "'α cond ⇒ 'α cond ⇒ 'α hrel ⇒ 'α hrel" where
[urel_defs]: "while_inv b p S = while_top b S"
text ‹ While loops with invariant decoration -- total correctness. ›
definition while_inv_bot :: "'α cond ⇒ 'α cond ⇒ 'α hrel ⇒ 'α hrel" where
[urel_defs]: "while_inv_bot b p S = while_bot b S"
text ‹ While loops with invariant and variant decorations -- total correctness. ›
definition while_vrt ::
"'α cond ⇒ 'α cond ⇒ (nat, 'α) uexpr ⇒ 'α hrel ⇒ 'α hrel" where
[urel_defs]: "while_vrt b p v S = while_bot b S"
syntax
"_uassume" :: "uexp ⇒ logic" ("[_]⇧⊤")
"_uassume" :: "uexp ⇒ logic" ("?[_]")
"_uassert" :: "uexp ⇒ logic" ("{_}⇩⊥")
"_uwhile" :: "uexp ⇒ logic ⇒ logic" ("while⇧⊤ _ do _ od")
"_uwhile_top" :: "uexp ⇒ logic ⇒ logic" ("while _ do _ od")
"_uwhile_bot" :: "uexp ⇒ logic ⇒ logic" ("while⇩⊥ _ do _ od")
"_uwhile_inv" :: "uexp ⇒ uexp ⇒ logic ⇒ logic" ("while _ invr _ do _ od")
"_uwhile_inv_bot" :: "uexp ⇒ uexp ⇒ logic ⇒ logic" ("while⇩⊥ _ invr _ do _ od" 71)
"_uwhile_vrt" :: "uexp ⇒ uexp ⇒ uexp ⇒ logic ⇒ logic" ("while _ invr _ vrt _ do _ od")
translations
"_uassume b" == "CONST rassume b"
"_uassert b" == "CONST rassert b"
"_uwhile b P" == "CONST while_top b P"
"_uwhile_top b P" == "CONST while_top b P"
"_uwhile_bot b P" == "CONST while_bot b P"
"_uwhile_inv b p S" == "CONST while_inv b p S"
"_uwhile_inv_bot b p S" == "CONST while_inv_bot b p S"
"_uwhile_vrt b p v S" == "CONST while_vrt b p v S"
text ‹ We implement a poor man's version of alphabet restriction that hides a variable within
a relation. ›
definition rel_var_res :: "'α hrel ⇒ ('a ⟹ 'α) ⇒ 'α hrel" (infix "↾⇩α" 80) where
[urel_defs]: "P ↾⇩α x = (∃ $x ∙ ∃ $x´ ∙ P)"
text ‹ Alphabet extension and restriction add additional variables by the given lens in both
their primed and unprimed versions. ›
definition rel_aext :: "'β hrel ⇒ ('β ⟹ 'α) ⇒ 'α hrel"
where [upred_defs]: "rel_aext P a = P ⊕⇩p (a ×⇩L a)"
definition rel_ares :: "'α hrel ⇒ ('β ⟹ 'α) ⇒ 'β hrel"
where [upred_defs]: "rel_ares P a = (P ↾⇩p (a × a))"
text ‹ We next describe frames and antiframes with the help of lenses. A frame states that $P$
defines how variables in $a$ changed, and all those outside of $a$ remain the same. An
antiframe describes the converse: all variables outside $a$ are specified by $P$, and all those in
remain the same. For more information please see \<^cite>‹"Morgan90a"›.›
definition frame :: "('a ⟹ 'α) ⇒ 'α hrel ⇒ 'α hrel" where
[urel_defs]: "frame a P = (P ∧ $❙v´ =⇩u $❙v ⊕ $❙v´ on &a)"
definition antiframe :: "('a ⟹ 'α) ⇒ 'α hrel ⇒ 'α hrel" where
[urel_defs]: "antiframe a P = (P ∧ $❙v´ =⇩u $❙v´ ⊕ $❙v on &a)"
text ‹ Frame extension combines alphabet extension with the frame operator to both add additional
variables and then frame those. ›
definition rel_frext :: "('β ⟹ 'α) ⇒ 'β hrel ⇒ 'α hrel" where
[upred_defs]: "rel_frext a P = frame a (rel_aext P a)"
text ‹ The nameset operator can be used to hide a portion of the after-state that lies outside
the lens $a$. It can be useful to partition a relation's variables in order to conjoin it
with another relation. ›
definition nameset :: "('a ⟹ 'α) ⇒ 'α hrel ⇒ 'α hrel" where
[urel_defs]: "nameset a P = (P ↾⇩v {$❙v,$a´})"
subsection ‹ Syntax Translations ›
syntax
"_utp_if" :: "uexp ⇒ logic ⇒ logic ⇒ logic" ("(if⇩u (_)/ then (_)/ else (_))" [0, 0, 71] 71)
"_seqr_iter" :: "pttrn ⇒ 'a list ⇒ 'σ hrel ⇒ 'σ hrel" ("(3;; _ : _ ∙/ _)" [0, 0, 10] 10)
"_assignment" :: "svids ⇒ uexprs ⇒ 'α hrel" ("'(_') := '(_')")
"_assignment" :: "svids ⇒ uexprs ⇒ 'α hrel" (infixr ":=" 62)
"_nd_assign" :: "svids ⇒ logic" ("_ := *" [62] 62)
"_mk_usubst" :: "svids ⇒ uexprs ⇒ 'α usubst"
"_skip_ra" :: "salpha ⇒ logic" ("II⇘_⇙")
"_frame" :: "salpha ⇒ logic ⇒ logic" ("_:[_]" [99,0] 100)
"_antiframe" :: "salpha ⇒ logic ⇒ logic" ("_:⟦_⟧" [79,0] 80)
"_rel_aext" :: "logic ⇒ salpha ⇒ logic" (infixl "⊕⇩r" 90)
"_rel_ares" :: "logic ⇒ salpha ⇒ logic" (infixl "↾⇩r" 90)
"_rel_frext" :: "salpha ⇒ logic ⇒ logic" ("_:[_]⇧+" [99,0] 100)
"_nameset" :: "salpha ⇒ logic ⇒ logic" ("ns _ ∙ _" [0,999] 999)
translations
"_utp_if b P Q" => "P ◃ b ▹⇩r Q"
";; x : l ∙ P" ⇌ "(CONST seqr_iter) l (λx. P)"
"_mk_usubst σ (_svid_unit x) v" ⇌ "σ(&x ↦⇩s v)"
"_mk_usubst σ (_svid_list x xs) (_uexprs v vs)" ⇌ "(_mk_usubst (σ(&x ↦⇩s v)) xs vs)"
"_assignment xs vs" => "CONST uassigns (_mk_usubst (CONST id) xs vs)"
"_assignment x v" <= "CONST uassigns (CONST subst_upd (CONST id) x v)"
"_assignment x v" <= "_assignment (_spvar x) v"
"_nd_assign x" => "CONST nd_assign (_mk_svid_list x)"
"_nd_assign x" <= "CONST nd_assign x"
"x,y := u,v" <= "CONST uassigns (CONST subst_upd (CONST subst_upd (CONST id) (CONST svar x) u) (CONST svar y) v)"
"_skip_ra v" ⇌ "CONST skip_ra v"
"_frame x P" => "CONST frame x P"
"_frame (_salphaset (_salphamk x)) P" <= "CONST frame x P"
"_antiframe x P" => "CONST antiframe x P"
"_antiframe (_salphaset (_salphamk x)) P" <= "CONST antiframe x P"
"_nameset x P" == "CONST nameset x P"
"_rel_aext P a" == "CONST rel_aext P a"
"_rel_ares P a" == "CONST rel_ares P a"
"_rel_frext a P" == "CONST rel_frext a P"
text ‹ The following code sets up pretty-printing for homogeneous relational expressions. We cannot
do this via the ``translations'' command as we only want the rule to apply when the input and output
alphabet types are the same. The code has to deconstruct a @{typ "('a, 'α) uexpr"} type, determine
that it is relational (product alphabet), and then checks if the types \emph{alpha} and \emph{beta}
are the same. If they are, the type is printed as a \emph{hexpr}. Otherwise, we have no match.
We then set up a regular translation for the \emph{hrel} type that uses this. ›
print_translation ‹
let
fun tr' ctxt [ a
, Const (@{type_syntax "prod"},_) $ alpha $ beta ] =
if (alpha = beta)
then Syntax.const @{type_syntax "hexpr"} $ a $ alpha
else raise Match;
in [(@{type_syntax "uexpr"},tr')]
end
›
translations
(type) "'α hrel" <= (type) "(bool, 'α) hexpr"
subsection ‹ Relation Properties ›
text ‹ We describe some properties of relations, including functional and injective relations. We
also provide operators for extracting the domain and range of a UTP relation. ›
definition ufunctional :: "('a, 'b) urel ⇒ bool"
where [urel_defs]: "ufunctional R ⟷ II ⊑ R⇧- ;; R"
definition uinj :: "('a, 'b) urel ⇒ bool"
where [urel_defs]: "uinj R ⟷ II ⊑ R ;; R⇧-"
definition Dom :: "'α hrel ⇒ 'α upred"
where [upred_defs]: "Dom P = ⌊∃ $❙v´ ∙ P⌋⇩<"
definition Ran :: "'α hrel ⇒ 'α upred"
where [upred_defs]: "Ran P = ⌊∃ $❙v ∙ P⌋⇩>"
update_uexpr_rep_eq_thms
subsection ‹ Introduction laws ›
lemma urel_refine_ext:
"⟦ ⋀ s s'. P⟦«s»,«s'»/$❙v,$❙v´⟧ ⊑ Q⟦«s»,«s'»/$❙v,$❙v´⟧ ⟧ ⟹ P ⊑ Q"
by (rel_auto)
lemma urel_eq_ext:
"⟦ ⋀ s s'. P⟦«s»,«s'»/$❙v,$❙v´⟧ = Q⟦«s»,«s'»/$❙v,$❙v´⟧ ⟧ ⟹ P = Q"
by (rel_auto)
subsection ‹ Unrestriction Laws ›
lemma unrest_iuvar [unrest]: "outα ♯ $x"
by (metis fst_snd_lens_indep lift_pre_var outα_def unrest_aext_indep)
lemma unrest_ouvar [unrest]: "inα ♯ $x´"
by (metis inα_def lift_post_var snd_fst_lens_indep unrest_aext_indep)
lemma unrest_semir_undash [unrest]:
fixes x :: "('a ⟹ 'α)"
assumes "$x ♯ P"
shows "$x ♯ P ;; Q"
using assms by (rel_auto)
lemma unrest_semir_dash [unrest]:
fixes x :: "('a ⟹ 'α)"
assumes "$x´ ♯ Q"
shows "$x´ ♯ P ;; Q"
using assms by (rel_auto)
lemma unrest_cond [unrest]:
"⟦ x ♯ P; x ♯ b; x ♯ Q ⟧ ⟹ x ♯ P ◃ b ▹ Q"
by (rel_auto)
lemma unrest_lift_rcond [unrest]:
"x ♯ ⌈b⌉⇩< ⟹ x ♯ ⌈b⌉⇩←"
by (simp add: lift_rcond_def)
lemma unrest_inα_var [unrest]:
"⟦ mwb_lens x; inα ♯ (P :: ('a, ('α × 'β)) uexpr) ⟧ ⟹ $x ♯ P"
by (rel_auto)
lemma unrest_outα_var [unrest]:
"⟦ mwb_lens x; outα ♯ (P :: ('a, ('α × 'β)) uexpr) ⟧ ⟹ $x´ ♯ P"
by (rel_auto)
lemma unrest_pre_outα [unrest]: "outα ♯ ⌈b⌉⇩<"
by (transfer, auto simp add: outα_def)
lemma unrest_post_inα [unrest]: "inα ♯ ⌈b⌉⇩>"
by (transfer, auto simp add: inα_def)
lemma unrest_pre_in_var [unrest]:
"x ♯ p1 ⟹ $x ♯ ⌈p1⌉⇩<"
by (transfer, simp)
lemma unrest_post_out_var [unrest]:
"x ♯ p1 ⟹ $x´ ♯ ⌈p1⌉⇩>"
by (transfer, simp)
lemma unrest_convr_outα [unrest]:
"inα ♯ p ⟹ outα ♯ p⇧-"
by (transfer, auto simp add: lens_defs)
lemma unrest_convr_inα [unrest]:
"outα ♯ p ⟹ inα ♯ p⇧-"
by (transfer, auto simp add: lens_defs)
lemma unrest_in_rel_var_res [unrest]:
"vwb_lens x ⟹ $x ♯ (P ↾⇩α x)"
by (simp add: rel_var_res_def unrest)
lemma unrest_out_rel_var_res [unrest]:
"vwb_lens x ⟹ $x´ ♯ (P ↾⇩α x)"
by (simp add: rel_var_res_def unrest)
lemma unrest_out_alpha_usubst_rel_lift [unrest]:
"outα ♯ ⌈σ⌉⇩s"
by (rel_auto)
lemma unrest_in_rel_aext [unrest]: "x ⨝ y ⟹ $y ♯ P ⊕⇩r x"
by (simp add: rel_aext_def unrest_aext_indep)
lemma unrest_out_rel_aext [unrest]: "x ⨝ y ⟹ $y´ ♯ P ⊕⇩r x"
by (simp add: rel_aext_def unrest_aext_indep)
lemma rel_aext_false [alpha]:
"false ⊕⇩r a = false"
by (pred_auto)
lemma rel_aext_seq [alpha]:
"weak_lens a ⟹ (P ;; Q) ⊕⇩r a = (P ⊕⇩r a ;; Q ⊕⇩r a)"
apply (rel_auto)
apply (rename_tac aa b y)
apply (rule_tac x="create⇘a⇙ y" in exI)
apply (simp)
done
lemma rel_aext_cond [alpha]:
"(P ◃ b ▹⇩r Q) ⊕⇩r a = (P ⊕⇩r a ◃ b ⊕⇩p a ▹⇩r Q ⊕⇩r a)"
by (rel_auto)
subsection ‹ Substitution laws ›
lemma subst_seq_left [usubst]:
"outα ♯ σ ⟹ σ † (P ;; Q) = (σ † P) ;; Q"
by (rel_simp, (metis (no_types, lifting) Pair_inject surjective_pairing)+)
lemma subst_seq_right [usubst]:
"inα ♯ σ ⟹ σ † (P ;; Q) = P ;; (σ † Q)"
by (rel_simp, (metis (no_types, lifting) Pair_inject surjective_pairing)+)
text ‹ The following laws support substitution in heterogeneous relations for polymorphically
typed literal expressions. These cannot be supported more generically due to limitations
in HOL's type system. The laws are presented in a slightly strange way so as to be as
general as possible. ›
lemma bool_seqr_laws [usubst]:
fixes x :: "(bool ⟹ 'α)"
shows
"⋀ P Q σ. σ($x ↦⇩s true) † (P ;; Q) = σ † (P⟦true/$x⟧ ;; Q)"
"⋀ P Q σ. σ($x ↦⇩s false) † (P ;; Q) = σ † (P⟦false/$x⟧ ;; Q)"
"⋀ P Q σ. σ($x´ ↦⇩s true) † (P ;; Q) = σ † (P ;; Q⟦true/$x´⟧)"
"⋀ P Q σ. σ($x´ ↦⇩s false) † (P ;; Q) = σ † (P ;; Q⟦false/$x´⟧)"
by (rel_auto)+
lemma zero_one_seqr_laws [usubst]:
fixes x :: "(_ ⟹ 'α)"
shows
"⋀ P Q σ. σ($x ↦⇩s 0) † (P ;; Q) = σ † (P⟦0/$x⟧ ;; Q)"
"⋀ P Q σ. σ($x ↦⇩s 1) † (P ;; Q) = σ † (P⟦1/$x⟧ ;; Q)"
"⋀ P Q σ. σ($x´ ↦⇩s 0) † (P ;; Q) = σ † (P ;; Q⟦0/$x´⟧)"
"⋀ P Q σ. σ($x´ ↦⇩s 1) † (P ;; Q) = σ † (P ;; Q⟦1/$x´⟧)"
by (rel_auto)+
lemma numeral_seqr_laws [usubst]:
fixes x :: "(_ ⟹ 'α)"
shows
"⋀ P Q σ. σ($x ↦⇩s numeral n) † (P ;; Q) = σ † (P⟦numeral n/$x⟧ ;; Q)"
"⋀ P Q σ. σ($x´ ↦⇩s numeral n) † (P ;; Q) = σ † (P ;; Q⟦numeral n/$x´⟧)"
by (rel_auto)+
lemma usubst_condr [usubst]:
"σ † (P ◃ b ▹ Q) = (σ † P ◃ σ † b ▹ σ † Q)"
by (rel_auto)
lemma subst_skip_r [usubst]:
"outα ♯ σ ⟹ σ † II = ⟨⌊σ⌋⇩s⟩⇩a"
by (rel_simp, (metis (mono_tags, lifting) prod.sel(1) sndI surjective_pairing)+)
lemma subst_pre_skip [usubst]: "⌈σ⌉⇩s † II = ⟨σ⟩⇩a"
by (rel_auto)
lemma subst_rel_lift_seq [usubst]:
"⌈σ⌉⇩s † (P ;; Q) = (⌈σ⌉⇩s † P) ;; Q"
by (rel_auto)
lemma subst_rel_lift_comp [usubst]:
"⌈σ⌉⇩s ∘ ⌈ρ⌉⇩s = ⌈σ ∘ ρ⌉⇩s"
by (rel_auto)
lemma usubst_upd_in_comp [usubst]:
"σ(&inα:x ↦⇩s v) = σ($x ↦⇩s v)"
by (simp add: pr_var_def fst_lens_def inα_def in_var_def)
lemma usubst_upd_out_comp [usubst]:
"σ(&outα:x ↦⇩s v) = σ($x´ ↦⇩s v)"
by (simp add: pr_var_def outα_def out_var_def snd_lens_def)
lemma subst_lift_upd [alpha]:
fixes x :: "('a ⟹ 'α)"
shows "⌈σ(x ↦⇩s v)⌉⇩s = ⌈σ⌉⇩s($x ↦⇩s ⌈v⌉⇩<)"
by (simp add: alpha usubst, simp add: pr_var_def fst_lens_def inα_def in_var_def)
lemma subst_drop_upd [alpha]:
fixes x :: "('a ⟹ 'α)"
shows "⌊σ($x ↦⇩s v)⌋⇩s = ⌊σ⌋⇩s(x ↦⇩s ⌊v⌋⇩<)"
by pred_simp
lemma subst_lift_pre [usubst]: "⌈σ⌉⇩s † ⌈b⌉⇩< = ⌈σ † b⌉⇩<"
by (metis apply_subst_ext fst_vwb_lens inα_def)
lemma unrest_usubst_lift_in [unrest]:
"x ♯ P ⟹ $x ♯ ⌈P⌉⇩s"
by pred_simp
lemma unrest_usubst_lift_out [unrest]:
fixes x :: "('a ⟹ 'α)"
shows "$x´ ♯ ⌈P⌉⇩s"
by pred_simp
lemma subst_lift_cond [usubst]: "⌈σ⌉⇩s † ⌈s⌉⇩← = ⌈σ † s⌉⇩←"
by (rel_auto)
lemma msubst_seq [usubst]: "(P(x) ;; Q(x))⟦x→«v»⟧ = ((P(x))⟦x→«v»⟧ ;; (Q(x))⟦x→«v»⟧)"
by (rel_auto)
subsection ‹ Alphabet laws ›
lemma aext_cond [alpha]:
"(P ◃ b ▹ Q) ⊕⇩p a = ((P ⊕⇩p a) ◃ (b ⊕⇩p a) ▹ (Q ⊕⇩p a))"
by (rel_auto)
lemma aext_seq [alpha]:
"wb_lens a ⟹ ((P ;; Q) ⊕⇩p (a ×⇩L a)) = ((P ⊕⇩p (a ×⇩L a)) ;; (Q ⊕⇩p (a ×⇩L a)))"
by (rel_simp, metis wb_lens_weak weak_lens.put_get)
lemma rcond_lift_true [simp]:
"⌈true⌉⇩← = true"
by rel_auto
lemma rcond_lift_false [simp]:
"⌈false⌉⇩← = false"
by rel_auto
lemma rel_ares_aext [alpha]:
"vwb_lens a ⟹ (P ⊕⇩r a) ↾⇩r a = P"
by (rel_auto)
lemma rel_aext_ares [alpha]:
"{$a, $a´} ♮ P ⟹ P ↾⇩r a ⊕⇩r a = P"
by (rel_auto)
lemma rel_aext_uses [unrest]:
"vwb_lens a ⟹ {$a, $a´} ♮ (P ⊕⇩r a)"
by (rel_auto)
subsection ‹ Relational unrestriction ›
text ‹ Relational unrestriction states that a variable is both unchanged by a relation, and is
not "read" by the relation. ›
definition RID :: "('a ⟹ 'α) ⇒ 'α hrel ⇒ 'α hrel"
where "RID x P = ((∃ $x ∙ ∃ $x´ ∙ P) ∧ $x´ =⇩u $x)"
declare RID_def [urel_defs]
lemma RID1: "vwb_lens x ⟹ (∀ v. x := «v» ;; P = P ;; x := «v») ⟹ RID(x)(P) = P"
apply (rel_auto)
apply (metis vwb_lens.put_eq)
apply (metis vwb_lens_wb wb_lens.get_put wb_lens_weak weak_lens.put_get)
done
lemma RID2: "vwb_lens x ⟹ x := «v» ;; RID(x)(P) = RID(x)(P) ;; x := «v»"
apply (rel_auto)
apply (metis mwb_lens.put_put vwb_lens_mwb vwb_lens_wb wb_lens.get_put wb_lens_def weak_lens.put_get)
apply blast
done
lemma RID_assign_commute:
"vwb_lens x ⟹ P = RID(x)(P) ⟷ (∀ v. x := «v» ;; P = P ;; x := «v»)"
by (metis RID1 RID2)
lemma RID_idem:
"mwb_lens x ⟹ RID(x)(RID(x)(P)) = RID(x)(P)"
by (rel_auto)
lemma RID_mono:
"P ⊑ Q ⟹ RID(x)(P) ⊑ RID(x)(Q)"
by (rel_auto)
lemma RID_pr_var [simp]:
"RID (pr_var x) = RID x"
by (simp add: pr_var_def)
lemma RID_skip_r:
"vwb_lens x ⟹ RID(x)(II) = II"
apply (rel_auto) using vwb_lens.put_eq by fastforce
lemma skip_r_RID [closure]: "vwb_lens x ⟹ II is RID(x)"
by (simp add: Healthy_def RID_skip_r)
lemma RID_disj:
"RID(x)(P ∨ Q) = (RID(x)(P) ∨ RID(x)(Q))"
by (rel_auto)
lemma disj_RID [closure]: "⟦ P is RID(x); Q is RID(x) ⟧ ⟹ (P ∨ Q) is RID(x)"
by (simp add: Healthy_def RID_disj)
lemma RID_conj:
"vwb_lens x ⟹ RID(x)(RID(x)(P) ∧ RID(x)(Q)) = (RID(x)(P) ∧ RID(x)(Q))"
by (rel_auto)
lemma conj_RID [closure]: "⟦ vwb_lens x; P is RID(x); Q is RID(x) ⟧ ⟹ (P ∧ Q) is RID(x)"
by (metis Healthy_if Healthy_intro RID_conj)
lemma RID_assigns_r_diff:
"⟦ vwb_lens x; x ♯ σ ⟧ ⟹ RID(x)(⟨σ⟩⇩a) = ⟨σ⟩⇩a"
apply (rel_auto)
apply (metis vwb_lens.put_eq)
apply (metis vwb_lens_wb wb_lens.get_put wb_lens_weak weak_lens.put_get)
done
lemma assigns_r_RID [closure]: "⟦ vwb_lens x; x ♯ σ ⟧ ⟹ ⟨σ⟩⇩a is RID(x)"
by (simp add: Healthy_def RID_assigns_r_diff)
lemma RID_assign_r_same:
"vwb_lens x ⟹ RID(x)(x := v) = II"
apply (rel_auto)
using vwb_lens.put_eq apply fastforce
done
lemma RID_seq_left:
assumes "vwb_lens x"
shows "RID(x)(RID(x)(P) ;; Q) = (RID(x)(P) ;; RID(x)(Q))"
proof -
have "RID(x)(RID(x)(P) ;; Q) = ((∃ $x ∙ ∃ $x´ ∙ ((∃ $x ∙ ∃ $x´ ∙ P) ∧ $x´ =⇩u $x) ;; Q) ∧ $x´ =⇩u $x)"
by (simp add: RID_def usubst)
also from assms have "... = ((((∃ $x ∙ ∃ $x´ ∙ P) ∧ (∃ $x ∙ $x´ =⇩u $x)) ;; (∃ $x´ ∙ Q)) ∧ $x´ =⇩u $x)"
by (rel_auto)
also from assms have "... = (((∃ $x ∙ ∃ $x´ ∙ P) ;; (∃ $x ∙ ∃ $x´ ∙ Q)) ∧ $x´ =⇩u $x)"
apply (rel_auto)
apply (metis vwb_lens.put_eq)
apply (metis mwb_lens.put_put vwb_lens_mwb)
done
also from assms have "... = ((((∃ $x ∙ ∃ $x´ ∙ P) ∧ $x´ =⇩u $x) ;; (∃ $x ∙ ∃ $x´ ∙ Q)) ∧ $x´ =⇩u $x)"
by (rel_simp, metis (full_types) mwb_lens.put_put vwb_lens_def wb_lens_weak weak_lens.put_get)
also have "... = ((((∃ $x ∙ ∃ $x´ ∙ P) ∧ $x´ =⇩u $x) ;; ((∃ $x ∙ ∃ $x´ ∙ Q) ∧ $x´ =⇩u $x)) ∧ $x´ =⇩u $x)"
by (rel_simp, fastforce)
also have "... = ((((∃ $x ∙ ∃ $x´ ∙ P) ∧ $x´ =⇩u $x) ;; ((∃ $x ∙ ∃ $x´ ∙ Q) ∧ $x´ =⇩u $x)))"
by (rel_auto)
also have "... = (RID(x)(P) ;; RID(x)(Q))"
by (rel_auto)
finally show ?thesis .
qed
lemma RID_seq_right:
assumes "vwb_lens x"
shows "RID(x)(P ;; RID(x)(Q)) = (RID(x)(P) ;; RID(x)(Q))"
proof -
have "RID(x)(P ;; RID(x)(Q)) = ((∃ $x ∙ ∃ $x´ ∙ P ;; ((∃ $x ∙ ∃ $x´ ∙ Q) ∧ $x´ =⇩u $x)) ∧ $x´ =⇩u $x)"
by (simp add: RID_def usubst)
also from assms have "... = (((∃ $x ∙ P) ;; (∃ $x ∙ ∃ $x´ ∙ Q) ∧ (∃ $x´ ∙ $x´ =⇩u $x)) ∧ $x´ =⇩u $x)"
by (rel_auto)
also from assms have "... = (((∃ $x ∙ ∃ $x´ ∙ P) ;; (∃ $x ∙ ∃ $x´ ∙ Q)) ∧ $x´ =⇩u $x)"
apply (rel_auto)
apply (metis vwb_lens.put_eq)
apply (metis mwb_lens.put_put vwb_lens_mwb)
done
also from assms have "... = ((((∃ $x ∙ ∃ $x´ ∙ P) ∧ $x´ =⇩u $x) ;; (∃ $x ∙ ∃ $x´ ∙ Q)) ∧ $x´ =⇩u $x)"
by (rel_simp robust, metis (full_types) mwb_lens.put_put vwb_lens_def wb_lens_weak weak_lens.put_get)
also have "... = ((((∃ $x ∙ ∃ $x´ ∙ P) ∧ $x´ =⇩u $x) ;; ((∃ $x ∙ ∃ $x´ ∙ Q) ∧ $x´ =⇩u $x)) ∧ $x´ =⇩u $x)"
by (rel_simp, fastforce)
also have "... = ((((∃ $x ∙ ∃ $x´ ∙ P) ∧ $x´ =⇩u $x) ;; ((∃ $x ∙ ∃ $x´ ∙ Q) ∧ $x´ =⇩u $x)))"
by (rel_auto)
also have "... = (RID(x)(P) ;; RID(x)(Q))"
by (rel_auto)
finally show ?thesis .
qed
lemma seqr_RID_closed [closure]: "⟦ vwb_lens x; P is RID(x); Q is RID(x) ⟧ ⟹ P ;; Q is RID(x)"
by (metis Healthy_def RID_seq_right)
definition unrest_relation :: "('a ⟹ 'α) ⇒ 'α hrel ⇒ bool" (infix "♯♯" 20)
where "(x ♯♯ P) ⟷ (P is RID(x))"
declare unrest_relation_def [urel_defs]
lemma runrest_assign_commute:
"⟦ vwb_lens x; x ♯♯ P ⟧ ⟹ x := «v» ;; P = P ;; x := «v»"
by (metis RID2 Healthy_def unrest_relation_def)
lemma runrest_ident_var:
assumes "x ♯♯ P"
shows "($x ∧ P) = (P ∧ $x´)"
proof -
have "P = ($x´ =⇩u $x ∧ P)"
by (metis RID_def assms Healthy_def unrest_relation_def utp_pred_laws.inf.cobounded2 utp_pred_laws.inf_absorb2)
moreover have "($x´ =⇩u $x ∧ ($x ∧ P)) = ($x´ =⇩u $x ∧ (P ∧ $x´))"
by (rel_auto)
ultimately show ?thesis
by (metis utp_pred_laws.inf.assoc utp_pred_laws.inf_left_commute)
qed
lemma skip_r_runrest [unrest]:
"vwb_lens x ⟹ x ♯♯ II"
by (simp add: unrest_relation_def closure)
lemma assigns_r_runrest:
"⟦ vwb_lens x; x ♯ σ ⟧ ⟹ x ♯♯ ⟨σ⟩⇩a"
by (simp add: unrest_relation_def closure)
lemma seq_r_runrest [unrest]:
assumes "vwb_lens x" "x ♯♯ P" "x ♯♯ Q"
shows "x ♯♯ (P ;; Q)"
using assms by (simp add: unrest_relation_def closure )
lemma false_runrest [unrest]: "x ♯♯ false"
by (rel_auto)
lemma and_runrest [unrest]: "⟦ vwb_lens x; x ♯♯ P; x ♯♯ Q ⟧ ⟹ x ♯♯ (P ∧ Q)"
by (metis RID_conj Healthy_def unrest_relation_def)
lemma or_runrest [unrest]: "⟦ x ♯♯ P; x ♯♯ Q ⟧ ⟹ x ♯♯ (P ∨ Q)"
by (simp add: RID_disj Healthy_def unrest_relation_def)
end