Quelle  utp_rel.thy

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⌉_\<leftarrow> = ⌈b⌉_<"
    
abbreviation 
  rcond :: "('α, 'β) urel ==> 'α cond ==> ('α, 'β) urel ==> ('α, 'β) urel"
  (‹(3_ ◃ _ ▹_r/ _)› [52,0,53] 52)
  where "(P ◃ b ▹_r Q) ≡ (P ◃ ⌈b⌉_\<leftarrow> ▹ 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
"⟨σ⟩ = (⌈σ⌉_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›)

syntax_consts
  "_uassume" == rassume and
  "_uassert" == rassert and
  "_uwhile" "_uwhile_top" == while_top and
  "_uwhile_bot" == while_bot and
  "_uwhile_inv" == while_inv and
  "_uwhile_inv_bot" == while_inv_bot and
  "_uwhile_vrt" == while_vrt

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 🛇_\<alpha> 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
  ― ‹ Alternative traditional conditional syntax ›
  "_utp_if" :: "uexp ==> logic ==> logic ==> logic" (‹(if_u (_)/ then (_)/ else (_))› [0, 0, 71] 71)
  ― ‹ Iterated sequential composition ›
  "_seqr_iter" :: "pttrn ==> 'a list ==> 'σ hrel ==> 'σ hrel" (‹(3;; _ : _ ∙/ _)› [0, 0, 10] 10)
  ― ‹ Single and multiple assignement ›
  "_assignment"     :: "svids ==> uexprs ==> 'α hrel"  (‹'(_') := '(_')›)  
  "_assignment"     :: "svids ==> uexprs ==> 'α hrel"  (infixr ‹:=› 62)
  ― ‹ Non-deterministic assignment ›
  "_nd_assign" :: "svids ==> logic" (‹_ := *› [62] 62)
  ― ‹ Substitution constructor ›
  "_mk_usubst"      :: "svids ==> uexprs ==> 'α usubst"
  ― ‹ Alphabetised skip ›
  "_skip_ra"        :: "salpha ==> logic" (‹II›)
  ― ‹ Frame ›
  "_frame"          :: "salpha ==> logic ==> logic" (‹_:[_]› [99,0] 100)
  ― ‹ Antiframe ›
  "_antiframe"      :: "salpha ==> logic ==> logic" (‹_:[_]› [79,0] 80)
  ― ‹ Relational Alphabet Extension ›
  "_rel_aext"  :: "logic ==> salpha ==> logic" (infixl ‹⊕_r› 90)
  ― ‹ Relational Alphabet Restriction ›
  "_rel_ares"  :: "logic ==> salpha ==> logic" (infixl ‹🛇_r› 90)
  ― ‹ Frame Extension ›
  "_rel_frext" :: "salpha ==> logic ==> logic" (‹_:[_]⁺› [99,0] 100)
  ― ‹ Nameset ›
  "_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 ‹
 
  tr' ctxt [ a
 , Const (@{type_syntax "prod"},_) $ alpha $ beta ] =
 if (alpha = beta)
 then Syntax.const @{type_syntax "hexpr"} $ a $ alpha
 else raise Match;
  [(@{type_syntax "uexpr"},tr')]
 
 ›
  
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⌋_>"
  
― ‹ Configuration for UTP tactics. ›

update_uexpr_rep_eq_thms ― ‹ Reread @{text rep_eq} theorems. ›

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⌉_\<leftarrow>"
  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 🛇_\<alpha> x)"
  by (simp add: rel_var_res_def unrest)

lemma unrest_out_rel_var_res [unrest]:
  "vwb_lens x ==> $x🍋 ♯ (P 🛇_\<alpha> 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 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⌉_\<leftarrow> = ⌈σ † s⌉_\<leftarrow>"
  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⌉_\<leftarrow> = true"
  by rel_auto

lemma rcond_lift_false [simp]:
  "⌈false⌉_\<leftarrow> = 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