Theory utp_subst

section ‹ Substitution ›

theory utp_subst
imports
  utp_expr
  utp_unrest
begin

subsection ‹ Substitution definitions ›

text ‹ Variable substitution, like unrestriction, will be characterised semantically using lenses
  and state-spaces. Effectively a substitution $\sigma$ is simply a function on the state-space which
  can be applied to an expression $e$ using the syntax $\sigma \mathop{\dagger} e$.  We introduce 
  a polymorphic constant that will be used to represent application of a substitution, and also a 
  set of theorems to represent laws. ›

consts
  usubst :: "'s ⇒ 'a ⇒ 'b" (infixr "†" 80)

named_theorems usubst

text ‹ A substitution is simply a transformation on the alphabet; it shows how variables
  should be mapped to different values. Most of the time these will be homogeneous functions 
  but for flexibility we also allow some operations to be heterogeneous. ›

type_synonym ('α,'β) psubst = "'α ⇒ 'β"
type_synonym 'α usubst = "'α ⇒ 'α"

text ‹ Application of a substitution simply applies the function $\sigma$ to the state binding
  $b$ before it is handed to $e$ as an input. This effectively ensures all variables are updated
  in $e$. ›
  
lift_definition subst :: "('α, 'β) psubst ⇒ ('a, 'β) uexpr ⇒ ('a, 'α) uexpr" is
"λ σ e b. e (σ b)" .

adhoc_overloading
  usubst subst

text ‹ Substitutions can be updated by associating variables with expressions. We thus create an 
  additional polymorphic constant to represent updating the value of a variable to an expression 
  in a substitution, where the variable is modelled by type @{typ "'v"}. This again allows us
  to support different notions of variables, such as deep variables, later. ›

consts subst_upd :: "('α,'β) psubst ⇒ 'v ⇒ ('a, 'α) uexpr ⇒ ('α,'β) psubst"

text ‹ The following function takes a substitution form state-space @{typ "'α"} to @{typ "'β"}, a
  lens with source @{typ "'β"} and view "'a", and an expression over @{typ "'α"} and returning
  a value of type "@{typ "'a"}, and produces an updated substitution. It does this by constructing
  a substitution function that takes state binding $b$, and updates the state first by applying
  the original substitution $\sigma$, and then updating the part of the state associated with lens
  $x$ with expression evaluated in the context of $b$. This effectively means that $x$ is now
  associated with expression $v$. We add this definition to our overloaded constant. ›
  
definition subst_upd_uvar :: "('α,'β) psubst ⇒ ('a ⟹ 'β) ⇒ ('a, 'α) uexpr ⇒ ('α,'β) psubst" where
"subst_upd_uvar σ x v = (λ b. put⇘x⇙ (σ b) (⟦v⟧⇩eb))"

adhoc_overloading
  subst_upd subst_upd_uvar

text ‹ The next function looks up the expression associated with a variable in a substitution
  by use of the \emph{get} lens function. ›

lift_definition usubst_lookup :: "('α,'β) psubst ⇒ ('a ⟹ 'β) ⇒ ('a, 'α) uexpr" ("⟨_⟩⇩s")
is "λ σ x b. get⇘x⇙ (σ b)" .

text ‹ Substitutions also exhibit a natural notion of unrestriction which states that $\sigma$
  does not restrict $x$ if application of $\sigma$ to an arbitrary state $\rho$ will not effect
  the valuation of $x$. Put another way, it requires that \emph{put} and the substitution commute. ›
  
definition unrest_usubst :: "('a ⟹ 'α) ⇒ 'α usubst ⇒ bool"
where "unrest_usubst x σ = (∀ ρ v. σ (put⇘x⇙ ρ v) = put⇘x⇙ (σ ρ) v)"

adhoc_overloading
  unrest unrest_usubst

text ‹ A conditional substitution deterministically picks one of the two substitutions based on a
  Booolean expression which is evaluated on the present state-space. It is analogous to a functional
  if-then-else. ›
  
definition cond_subst :: "'α usubst ⇒ (bool, 'α) uexpr ⇒ 'α usubst ⇒ 'α usubst" ("(3_ ◃ _ ▹⇩s/ _)" [52,0,53] 52) where
"cond_subst σ b ρ = (λ s. if ⟦b⟧⇩e s then σ(s) else ρ(s))"
  
text ‹ Parallel substitutions allow us to divide the state space into three segments using two
  lens, A and B. They correspond to the part of the state that should be updated by the 
  respective substitution. The two lenses should be independent. If any part of the state
  is not covered by either lenses then this area is left unchanged (framed). ›
  
definition par_subst :: "'α usubst ⇒ ('a ⟹ 'α) ⇒ ('b ⟹ 'α) ⇒ 'α usubst ⇒ 'α usubst" where
"par_subst σ⇩1 A B σ⇩2 = (λ s. (s ⊕⇩L (σ⇩1 s) on A) ⊕⇩L (σ⇩2 s) on B)"
  
subsection ‹ Syntax translations ›

text ‹ We support two kinds of syntax for substitutions, one where we construct a substitution
  using a maplet-style syntax, with variables mapping to expressions. Such a constructed substitution
  can be applied to an expression. Alternatively, we support the more traditional notation, 
  $P \llbracket v / x \rrbracket$, which also support multiple simultaneous substitutions. We 
  have to use double square brackets as the single ones are already well used. 

  We set up non-terminals to represent a single substitution maplet, a sequence of maplets, a
  list of expressions, and a list of alphabets. The parser effectively uses @{term subst_upd}
  to construct substitutions from multiple variables. 
›
  
nonterminal smaplet and smaplets and uexp and uexprs and salphas

syntax
  "_smaplet"  :: "[salpha, 'a] => smaplet"             ("_ /↦⇩s/ _")
  ""          :: "smaplet => smaplets"            ("_")
  "_SMaplets" :: "[smaplet, smaplets] => smaplets" ("_,/ _")
  "_SubstUpd" :: "['m usubst, smaplets] => 'm usubst" ("_/'(_')" [900,0] 900)
  "_Subst"    :: "smaplets => 'a ⇀ 'b"            ("(1[_])")
  "_psubst"  :: "[logic, svars, uexprs] ⇒ logic"
  "_subst"   :: "logic ⇒ uexprs ⇒ salphas ⇒ logic" ("(_⟦_'/_⟧)" [990,0,0] 991)
  "_uexp_l"  :: "logic ⇒ uexp" ("_" [64] 64)
  "_uexprs"  :: "[uexp, uexprs] => uexprs" ("_,/ _")
  ""         :: "uexp => uexprs" ("_")
  "_salphas" :: "[salpha, salphas] => salphas" ("_,/ _")
  ""         :: "salpha => salphas" ("_")
  "_par_subst" :: "logic ⇒ salpha ⇒ salpha ⇒ logic ⇒ logic" ("_ [_|_]⇩s _" [100,0,0,101] 101)
    
translations
  "_SubstUpd m (_SMaplets xy ms)"     == "_SubstUpd (_SubstUpd m xy) ms"
  "_SubstUpd m (_smaplet x y)"        == "CONST subst_upd m x y"
  "_Subst ms"                         == "_SubstUpd (CONST id) ms"
  "_Subst (_SMaplets ms1 ms2)"        <= "_SubstUpd (_Subst ms1) ms2"
  "_SMaplets ms1 (_SMaplets ms2 ms3)" <= "_SMaplets (_SMaplets ms1 ms2) ms3"
  "_subst P es vs" => "CONST subst (_psubst (CONST id) vs es) P"
  "_psubst m (_salphas x xs) (_uexprs v vs)" => "_psubst (_psubst m x v) xs vs"
  "_psubst m x v"  => "CONST subst_upd m x v"
  "_subst P v x" <= "CONST usubst (CONST subst_upd (CONST id) x v) P"
  "_subst P v x" <= "_subst P (_spvar x) v"
  "_par_subst σ⇩1 A B σ⇩2" == "CONST par_subst σ⇩1 A B σ⇩2"
  "_uexp_l e" => "e"

text ‹ Thus we can write things like @{term "σ(x ↦⇩s v)"} to update a variable $x$ in $\sigma$ with
  expression $v$, @{term "[x ↦⇩s e, y ↦⇩s f]"} to construct a substitution with two variables,
  and finally @{term "P⟦v/x⟧"}, the traditional syntax.

  We can now express deletion of a substitution maplet. ›

definition subst_del :: "'α usubst ⇒ ('a ⟹ 'α) ⇒ 'α usubst" (infix "-⇩s" 85) where
"subst_del σ x = σ(x ↦⇩s &x)"

subsection ‹ Substitution Application Laws ›

text ‹ We set up a simple substitution tactic that applies substitution and unrestriction laws ›

method subst_tac = (simp add: usubst unrest)?

text ‹ Evaluation of a substitution expression involves application of the substitution to different
  variables. Thus we first prove laws for these cases. The simplest substitution, $id$, when applied
  to any variable $x$ simply returns the variable expression, since $id$ has no effect. ›
  
lemma usubst_lookup_id [usubst]: "⟨id⟩⇩s x = var x"
  by (transfer, simp)

lemma subst_upd_id_lam [usubst]: "subst_upd (λ x. x) x v = subst_upd id x v"
  by (simp add: id_def)
    
text ‹ A substitution update naturally yields the given expression. ›
    
lemma usubst_lookup_upd [usubst]:
  assumes "weak_lens x"
  shows "⟨σ(x ↦⇩s v)⟩⇩s x = v"
  using assms
  by (simp add: subst_upd_uvar_def, transfer) (simp)

lemma usubst_lookup_upd_pr_var [usubst]:
  assumes "weak_lens x"
  shows "⟨σ(x ↦⇩s v)⟩⇩s (pr_var x) = v"
  using assms
  by (simp add: subst_upd_uvar_def pr_var_def, transfer) (simp)
    
text ‹ Substitution update is idempotent. ›
    
lemma usubst_upd_idem [usubst]:
  assumes "mwb_lens x"
  shows "σ(x ↦⇩s u, x ↦⇩s v) = σ(x ↦⇩s v)"
  by (simp add: subst_upd_uvar_def assms comp_def)

lemma usubst_upd_idem_sub [usubst]:
  assumes "x ⊆⇩L y" "mwb_lens y"
  shows "σ(x ↦⇩s u, y ↦⇩s v) = σ(y ↦⇩s v)"
  by (simp add: subst_upd_uvar_def assms comp_def fun_eq_iff sublens_put_put)

text ‹ Substitution updates commute when the lenses are independent. ›
    
lemma usubst_upd_comm:
  assumes "x ⨝ y"
  shows "σ(x ↦⇩s u, y ↦⇩s v) = σ(y ↦⇩s v, x ↦⇩s u)"
  using assms
  by (rule_tac ext, auto simp add: subst_upd_uvar_def assms comp_def lens_indep_comm)

lemma usubst_upd_comm2:
  assumes "z ⨝ y"
  shows "σ(x ↦⇩s u, y ↦⇩s v, z ↦⇩s s) = σ(x ↦⇩s u, z ↦⇩s s, y ↦⇩s v)"
  using assms
  by (rule_tac ext, auto simp add: subst_upd_uvar_def assms comp_def lens_indep_comm)

lemma subst_upd_pr_var: "s(&x ↦⇩s v) = s(x ↦⇩s v)"
  by (simp add: pr_var_def) 

text ‹ A substitution which swaps two independent variables is an injective function. ›
    
lemma swap_usubst_inj:
  fixes x y :: "('a ⟹ 'α)"
  assumes "vwb_lens x" "vwb_lens y" "x ⨝ y"
  shows "inj [x ↦⇩s &y, y ↦⇩s &x]"
proof (rule injI)
  fix b⇩1 :: 'α and b⇩2 :: 'α
  assume "[x ↦⇩s &y, y ↦⇩s &x] b⇩1 = [x ↦⇩s &y, y ↦⇩s &x] b⇩2"
  hence a: "put⇘y⇙ (put⇘x⇙ b⇩1 (⟦&y⟧⇩e b⇩1)) (⟦&x⟧⇩e b⇩1) = put⇘y⇙ (put⇘x⇙ b⇩2 (⟦&y⟧⇩e b⇩2)) (⟦&x⟧⇩e b⇩2)"
    by (auto simp add: subst_upd_uvar_def)
  then have "(∀a b c. put⇘x⇙ (put⇘y⇙ a b) c = put⇘y⇙ (put⇘x⇙ a c) b) ∧ 
             (∀a b. get⇘x⇙ (put⇘y⇙ a b) = get⇘x⇙ a) ∧ (∀a b. get⇘y⇙ (put⇘x⇙ a b) = get⇘y⇙ a)"
    by (simp add: assms(3) lens_indep.lens_put_irr2 lens_indep_comm)
  then show "b⇩1 = b⇩2"
    by (metis a assms(1) assms(2) pr_var_def var.rep_eq vwb_lens.source_determination vwb_lens_def wb_lens_def weak_lens.put_get)   
qed

lemma usubst_upd_var_id [usubst]:
  "vwb_lens x ⟹ [x ↦⇩s var x] = id"
  apply (simp add: subst_upd_uvar_def)
  apply (transfer)
  apply (rule ext)
  apply (auto)
  done

lemma usubst_upd_pr_var_id [usubst]:
  "vwb_lens x ⟹ [x ↦⇩s var (pr_var x)] = id"
  apply (simp add: subst_upd_uvar_def pr_var_def)
  apply (transfer)
  apply (rule ext)
  apply (auto)
  done
  
lemma usubst_upd_comm_dash [usubst]:
  fixes x :: "('a ⟹ 'α)"
  shows "σ($x´ ↦⇩s v, $x ↦⇩s u) = σ($x ↦⇩s u, $x´ ↦⇩s v)"
  using out_in_indep usubst_upd_comm by blast

lemma subst_upd_lens_plus [usubst]: 
  "subst_upd σ (x +⇩L y) «(u,v)» = σ(y ↦⇩s «v», x ↦⇩s «u»)"
  by (simp add: lens_defs uexpr_defs subst_upd_uvar_def, transfer, auto)

lemma subst_upd_in_lens_plus [usubst]: 
  "subst_upd σ (ivar (x +⇩L y)) «(u,v)» = σ($y ↦⇩s «v», $x ↦⇩s «u»)"
  by (simp add: lens_defs uexpr_defs subst_upd_uvar_def, transfer, auto simp add: prod.case_eq_if)

lemma subst_upd_out_lens_plus [usubst]: 
  "subst_upd σ (ovar (x +⇩L y)) «(u,v)» = σ($y´ ↦⇩s «v», $x´ ↦⇩s «u»)"
  by (simp add: lens_defs uexpr_defs subst_upd_uvar_def, transfer, auto simp add: prod.case_eq_if)
    
lemma usubst_lookup_upd_indep [usubst]:
  assumes "mwb_lens x" "x ⨝ y"
  shows "⟨σ(y ↦⇩s v)⟩⇩s x = ⟨σ⟩⇩s x"
  using assms
  by (simp add: subst_upd_uvar_def, transfer, simp)

lemma subst_upd_plus [usubst]: 
  "x ⨝ y ⟹ subst_upd s (x +⇩L y) e = s(x ↦⇩s π⇩1(e), y ↦⇩s π⇩2(e))"
  by (simp add: subst_upd_uvar_def lens_defs, transfer, auto simp add: fun_eq_iff prod.case_eq_if lens_indep_comm)

text ‹ If a variable is unrestricted in a substitution then it's application has no effect. ›

lemma usubst_apply_unrest [usubst]:
  "⟦ vwb_lens x; x ♯ σ ⟧ ⟹ ⟨σ⟩⇩s x = var x"
  by (simp add: unrest_usubst_def, transfer, auto simp add: fun_eq_iff, metis vwb_lens_wb wb_lens.get_put wb_lens_weak weak_lens.put_get)

text ‹ There follows various laws about deleting variables from a substitution. ›
    
lemma subst_del_id [usubst]:
  "vwb_lens x ⟹ id -⇩s x = id"
  by (simp add: subst_del_def subst_upd_uvar_def pr_var_def, transfer, auto)

lemma subst_del_upd_same [usubst]:
  "mwb_lens x ⟹ σ(x ↦⇩s v) -⇩s x = σ -⇩s x"
  by (simp add: subst_del_def subst_upd_uvar_def)

lemma subst_del_upd_diff [usubst]:
  "x ⨝ y ⟹ σ(y ↦⇩s v) -⇩s x = (σ -⇩s x)(y ↦⇩s v)"
  by (simp add: subst_del_def subst_upd_uvar_def lens_indep_comm)

text ‹ If a variable is unrestricted in an expression, then any substitution of that variable
  has no effect on the expression .›
    
lemma subst_unrest [usubst]: "x ♯ P ⟹ σ(x ↦⇩s v) † P = σ † P"
  by (simp add: subst_upd_uvar_def, transfer, auto)

lemma subst_unrest_2 [usubst]: 
  fixes P :: "('a, 'α) uexpr"
  assumes "x ♯ P" "x ⨝ y"
  shows "σ(x ↦⇩s u,y ↦⇩s v) † P = σ(y ↦⇩s v) † P"
  using assms
  by (simp add: subst_upd_uvar_def, transfer, auto, metis lens_indep.lens_put_comm)

lemma subst_unrest_3 [usubst]: 
  fixes P :: "('a, 'α) uexpr"
  assumes "x ♯ P" "x ⨝ y" "x ⨝ z"
  shows "σ(x ↦⇩s u, y ↦⇩s v, z ↦⇩s w) † P = σ(y ↦⇩s v, z ↦⇩s w) † P"
  using assms
  by (simp add: subst_upd_uvar_def, transfer, auto, metis (no_types, opaque_lifting) lens_indep_comm)

lemma subst_unrest_4 [usubst]: 
  fixes P :: "('a, 'α) uexpr"
  assumes "x ♯ P" "x ⨝ y" "x ⨝ z" "x ⨝ u"
  shows "σ(x ↦⇩s e, y ↦⇩s f, z ↦⇩s g, u ↦⇩s h) † P = σ(y ↦⇩s f, z ↦⇩s g, u ↦⇩s h) † P"
  using assms
  by (simp add: subst_upd_uvar_def, transfer, auto, metis (no_types, opaque_lifting) lens_indep_comm)

lemma subst_unrest_5 [usubst]: 
  fixes P :: "('a, 'α) uexpr"
  assumes "x ♯ P" "x ⨝ y" "x ⨝ z" "x ⨝ u" "x ⨝ v"
  shows "σ(x ↦⇩s e, y ↦⇩s f, z ↦⇩s g, u ↦⇩s h, v ↦⇩s i) † P = σ(y ↦⇩s f, z ↦⇩s g, u ↦⇩s h, v ↦⇩s i) † P"
  using assms
  by (simp add: subst_upd_uvar_def, transfer, auto, metis (no_types, opaque_lifting) lens_indep_comm)

lemma subst_compose_upd [usubst]: "x ♯ σ ⟹ σ ∘ ρ(x ↦⇩s v) = (σ ∘ ρ)(x ↦⇩s v) "
  by (simp add: subst_upd_uvar_def, transfer, auto simp add: unrest_usubst_def)

text ‹ Any substitution is a monotonic function. ›
    
lemma subst_mono: "mono (subst σ)"
  by (simp add: less_eq_uexpr.rep_eq mono_def subst.rep_eq)

subsection ‹ Substitution laws ›
  
text ‹ We now prove the key laws that show how a substitution should be performed for every 
  expression operator, including the core function operators, literals, variables, and the 
  arithmetic operators. They are all added to the \emph{usubst} theorem attribute so that
  we can apply them using the substitution tactic. ›
    
lemma id_subst [usubst]: "id † v = v"
  by (transfer, simp)

lemma subst_lit [usubst]: "σ † «v» = «v»"
  by (transfer, simp)

lemma subst_var [usubst]: "σ † var x = ⟨σ⟩⇩s x"
  by (transfer, simp)

lemma usubst_ulambda [usubst]: "σ † (λ x ∙ P(x)) = (λ x ∙ σ † P(x))"
  by (transfer, simp)

lemma unrest_usubst_del [unrest]: "⟦ vwb_lens x; x ♯ (⟨σ⟩⇩s x); x ♯ σ -⇩s x ⟧ ⟹  x ♯ (σ † P)"
  by (simp add: subst_del_def subst_upd_uvar_def unrest_uexpr_def unrest_usubst_def subst.rep_eq usubst_lookup.rep_eq)
     (metis vwb_lens.put_eq)

text ‹ We add the symmetric definition of input and output variables to substitution laws
        so that the variables are correctly normalised after substitution. ›

lemma subst_uop [usubst]: "σ † uop f v = uop f (σ † v)"
  by (transfer, simp)

lemma subst_bop [usubst]: "σ † bop f u v = bop f (σ † u) (σ † v)"
  by (transfer, simp)

lemma subst_trop [usubst]: "σ † trop f u v w = trop f (σ † u) (σ † v) (σ † w)"
  by (transfer, simp)

lemma subst_qtop [usubst]: "σ † qtop f u v w x = qtop f (σ † u) (σ † v) (σ † w) (σ † x)"
  by (transfer, simp)

lemma subst_case_prod [usubst]:
  fixes P :: "'i ⇒ 'j ⇒ ('a, 'α) uexpr"  
  shows "σ † case_prod (λ x y. P x y) v = case_prod (λ x y. σ † P x y) v"
  by (simp add: case_prod_beta')

lemma subst_plus [usubst]: "σ † (x + y) = σ † x + σ † y"
  by (simp add: plus_uexpr_def subst_bop)

lemma subst_times [usubst]: "σ † (x * y) = σ † x * σ † y"
  by (simp add: times_uexpr_def subst_bop)

lemma subst_mod [usubst]: "σ † (x mod y) = σ † x mod σ † y"
  by (simp add: mod_uexpr_def usubst)

lemma subst_div [usubst]: "σ † (x div y) = σ † x div σ † y"
  by (simp add: divide_uexpr_def usubst)

lemma subst_minus [usubst]: "σ † (x - y) = σ † x - σ † y"
  by (simp add: minus_uexpr_def subst_bop)

lemma subst_uminus [usubst]: "σ † (- x) = - (σ † x)"
  by (simp add: uminus_uexpr_def subst_uop)

lemma usubst_sgn [usubst]: "σ † sgn x = sgn (σ † x)"
  by (simp add: sgn_uexpr_def subst_uop)

lemma usubst_abs [usubst]: "σ † abs x = abs (σ † x)"
  by (simp add: abs_uexpr_def subst_uop)

lemma subst_zero [usubst]: "σ † 0 = 0"
  by (simp add: zero_uexpr_def subst_lit)

lemma subst_one [usubst]: "σ † 1 = 1"
  by (simp add: one_uexpr_def subst_lit)

lemma subst_eq_upred [usubst]: "σ † (x =⇩u y) = (σ † x =⇩u σ † y)"
  by (simp add: eq_upred_def usubst)

text ‹ This laws shows the effect of applying one substitution after another -- we simply
  use function composition to compose them. ›
    
lemma subst_subst [usubst]: "σ † ρ † e = (ρ ∘ σ) † e"
  by (transfer, simp)

text ‹ The next law is similar, but shows how such a substitution is to be applied to every
  updated variable additionally. ›
    
lemma subst_upd_comp [usubst]:
  fixes x :: "('a ⟹ 'α)"
  shows "ρ(x ↦⇩s v) ∘ σ = (ρ ∘ σ)(x ↦⇩s σ † v)"
  by (rule ext, simp add:uexpr_defs subst_upd_uvar_def, transfer, simp)

lemma subst_singleton:
  fixes x :: "('a ⟹ 'α)"
  assumes "x ♯ σ"
  shows "σ(x ↦⇩s v) † P = (σ † P)⟦v/x⟧"
  using assms
  by (simp add: usubst)

lemmas subst_to_singleton = subst_singleton id_subst

subsection ‹ Ordering substitutions ›

text ‹ A simplification procedure to reorder substitutions maplets lexicographically by variable syntax ›

simproc_setup subst_order ("subst_upd_uvar (subst_upd_uvar σ x u) y v") =
  ‹(fn _ => fn ctxt => fn ct => 
        case (Thm.term_of ct) of
          Const ("utp_subst.subst_upd_uvar", _) $ (Const ("utp_subst.subst_upd_uvar", _) $ s $ x $ u) $ y $ v
            => if (YXML.content_of (Syntax.string_of_term ctxt x) > YXML.content_of(Syntax.string_of_term ctxt y))
               then SOME (mk_meta_eq @{thm usubst_upd_comm})
               else NONE  |
          _ => NONE) 
›

subsection ‹ Unrestriction laws ›

text ‹ These are the key unrestriction theorems for substitutions and expressions involving substitutions. ›
  
lemma unrest_usubst_single [unrest]:
  "⟦ mwb_lens x; x ♯ v ⟧ ⟹ x ♯ P⟦v/x⟧"
  by (transfer, auto simp add: subst_upd_uvar_def unrest_uexpr_def)

lemma unrest_usubst_id [unrest]:
  "mwb_lens x ⟹ x ♯ id"
  by (simp add: unrest_usubst_def)

lemma unrest_usubst_upd [unrest]:
  "⟦ x ⨝ y; x ♯ σ; x ♯ v ⟧ ⟹ x ♯ σ(y ↦⇩s v)"
  by (simp add: subst_upd_uvar_def unrest_usubst_def unrest_uexpr.rep_eq lens_indep_comm)

lemma unrest_subst [unrest]:
  "⟦ x ♯ P; x ♯ σ ⟧ ⟹ x ♯ (σ † P)"
  by (transfer, simp add: unrest_usubst_def)
    
subsection ‹ Conditional Substitution Laws ›
  
lemma usubst_cond_upd_1 [usubst]:
  "σ(x ↦⇩s u) ◃ b ▹⇩s ρ(x ↦⇩s v) = (σ ◃ b ▹⇩s ρ)(x ↦⇩s u ◃ b ▹ v)"
  by (simp add: cond_subst_def subst_upd_uvar_def uexpr_defs, transfer, auto)

lemma usubst_cond_upd_2 [usubst]:
  "⟦ vwb_lens x; x ♯ ρ ⟧ ⟹ σ(x ↦⇩s u) ◃ b ▹⇩s ρ = (σ ◃ b ▹⇩s ρ)(x ↦⇩s u ◃ b ▹ &x)"
  by (simp add: cond_subst_def subst_upd_uvar_def unrest_usubst_def uexpr_defs, transfer)
     (metis (full_types, opaque_lifting) id_apply pr_var_def subst_upd_uvar_def usubst_upd_pr_var_id var.rep_eq)
 
lemma usubst_cond_upd_3 [usubst]:
  "⟦ vwb_lens x; x ♯ σ ⟧ ⟹ σ ◃ b ▹⇩s ρ(x ↦⇩s v) = (σ ◃ b ▹⇩s ρ)(x ↦⇩s &x ◃ b ▹ v)"
  by (simp add: cond_subst_def subst_upd_uvar_def unrest_usubst_def uexpr_defs, transfer)
     (metis (full_types, opaque_lifting) id_apply pr_var_def subst_upd_uvar_def usubst_upd_pr_var_id var.rep_eq)
    
lemma usubst_cond_id [usubst]:
  "σ ◃ b ▹⇩s σ = σ"
  by (auto simp add: cond_subst_def)
    
subsection ‹ Parallel Substitution Laws ›
    
lemma par_subst_id [usubst]:
  "⟦ vwb_lens A; vwb_lens B ⟧ ⟹ id [A|B]⇩s id = id"
  by (simp add: par_subst_def id_def)

lemma par_subst_left_empty [usubst]:
  "⟦ vwb_lens A ⟧ ⟹ σ [∅|A]⇩s ρ = id [∅|A]⇩s ρ"
  by (simp add: par_subst_def pr_var_def)

lemma par_subst_right_empty [usubst]:
  "⟦ vwb_lens A ⟧ ⟹ σ [A|∅]⇩s ρ = σ [A|∅]⇩s id"
  by (simp add: par_subst_def pr_var_def)
    
lemma par_subst_comm:
  "⟦ A ⨝ B ⟧ ⟹ σ [A|B]⇩s ρ = ρ [B|A]⇩s σ"
  by (simp add: par_subst_def lens_override_def lens_indep_comm)
      
lemma par_subst_upd_left_in [usubst]:
  "⟦ vwb_lens A; A ⨝ B; x ⊆⇩L A ⟧ ⟹ σ(x ↦⇩s v) [A|B]⇩s ρ = (σ [A|B]⇩s ρ)(x ↦⇩s v)"
  by (simp add: par_subst_def subst_upd_uvar_def lens_override_put_right_in)
     (simp add: lens_indep_comm lens_override_def sublens_pres_indep)

lemma par_subst_upd_left_out [usubst]:
  "⟦ vwb_lens A; x ⨝ A ⟧ ⟹ σ(x ↦⇩s v) [A|B]⇩s ρ = (σ [A|B]⇩s ρ)"
  by (simp add: par_subst_def subst_upd_uvar_def lens_override_put_right_out)
     
lemma par_subst_upd_right_in [usubst]:
  "⟦ vwb_lens B; A ⨝ B; x ⊆⇩L B ⟧ ⟹ σ [A|B]⇩s ρ(x ↦⇩s v) = (σ [A|B]⇩s ρ)(x ↦⇩s v)"
  using lens_indep_sym par_subst_comm par_subst_upd_left_in by fastforce

lemma par_subst_upd_right_out [usubst]:
  "⟦ vwb_lens B; A ⨝ B; x ⨝ B ⟧ ⟹ σ [A|B]⇩s ρ(x ↦⇩s v) = (σ [A|B]⇩s ρ)"
  by (simp add: par_subst_comm par_subst_upd_left_out)
    
end