Theory utp_unrest

section ‹ Unrestriction ›

theory utp_unrest
  imports utp_expr_insts
begin

subsection ‹ Definitions and Core Syntax ›
  
text ‹ Unrestriction is an encoding of semantic freshness that allows us to reason about the
  presence of variables in predicates without being concerned with abstract syntax trees.
  An expression $p$ is unrestricted by lens $x$, written $x \mathop{\sharp} p$, if
  altering the value of $x$ has no effect on the valuation of $p$. This is a sufficient
  notion to prove many laws that would ordinarily rely on an \emph{fv} function. 

  Unrestriction was first defined in the work of Marcel Oliveira~\<^cite>‹"Oliveira2005-PHD" and "Oliveira07"› in his
  UTP mechanisation in \emph{ProofPowerZ}. Our definition modifies his in that our variables
  are semantically characterised as lenses, and supported by the lens laws, rather than named 
  syntactic entities. We effectively fuse the ideas from both Feliachi~\<^cite>‹"Feliachi2010"› and 
  Oliveira's~\<^cite>‹"Oliveira07"› mechanisations of the UTP, the former being also purely semantic
  in nature.

  We first set up overloaded syntax for unrestriction, as several concepts will have this
  defined. ›

consts
  unrest :: "'a ⇒ 'b ⇒ bool"

syntax
  "_unrest" :: "salpha ⇒ logic ⇒ logic ⇒ logic" (infix "♯" 20)
  
translations
  "_unrest x p" == "CONST unrest x p"                                           
  "_unrest (_salphaset (_salphamk (x +⇩_L y))) P"  <= "_unrest (x +⇩_L y) P"

text ‹ Our syntax translations support both variables and variable sets such that we can write down 
  predicates like @{term "&x ♯ P"} and also @{term "{&x,&y,&z} ♯ P"}. 

  We set up a simple tactic for discharging unrestriction conjectures using a simplification set. ›
  
named_theorems unrest
method unrest_tac = (simp add: unrest)?

text ‹ Unrestriction for expressions is defined as a lifted construct using the underlying lens
  operations. It states that lens $x$ is unrestricted by expression $e$ provided that, for any
  state-space binding $b$ and variable valuation $v$, the value which the expression evaluates
  to is unaltered if we set $x$ to $v$ in $b$. In other words, we cannot effect the behaviour
  of $e$ by changing $x$. Thus $e$ does not observe the portion of state-space characterised
  by $x$. We add this definition to our overloaded constant. ›
  
lift_definition unrest_uexpr :: "('a ⟹ 'α) ⇒ ('b, 'α) uexpr ⇒ bool"
is "λ x e. ∀ b v. e (put⇘x⇙ b v) = e b" .

adhoc_overloading
  unrest unrest_uexpr

lemma unrest_expr_alt_def:
  "weak_lens x ⟹ (x ♯ P) = (∀ b b'. ⟦P⟧⇩_e (b ⊕⇩_L b' on x) = ⟦P⟧⇩_e b)"
  by (transfer, metis lens_override_def weak_lens.put_get)
  
subsection ‹ Unrestriction laws ›
  
text ‹ We now prove unrestriction laws for the key constructs of our expression model. Many
  of these depend on lens properties and so variously employ the assumptions @{term mwb_lens} and
  @{term vwb_lens}, depending on the number of assumptions from the lenses theory is required.

  Firstly, we prove a general property -- if $x$ and $y$ are both unrestricted in $P$, then their composition
  is also unrestricted in $P$. One can interpret the composition here as a union -- if the two sets
  of variables $x$ and $y$ are unrestricted, then so is their union. ›
  
lemma unrest_var_comp [unrest]:
  "⟦ x ♯ P; y ♯ P ⟧ ⟹ x;y ♯ P"
  by (transfer, simp add: lens_defs)

lemma unrest_svar [unrest]: "(&x ♯ P) ⟷ (x ♯ P)"
  by (transfer, simp add: lens_defs)

text ‹ No lens is restricted by a literal, since it returns the same value for any state binding. ›
    
lemma unrest_lit [unrest]: "x ♯ «v»"
  by (transfer, simp)

text ‹ If one lens is smaller than another, then any unrestriction on the larger lens implies
  unrestriction on the smaller. ›
    
lemma unrest_sublens:
  fixes P :: "('a, 'α) uexpr"
  assumes "x ♯ P" "y ⊆⇩_L x"
  shows "y ♯ P" 
  using assms
  by (transfer, metis (no_types, lifting) lens.select_convs(2) lens_comp_def sublens_def)
    
text ‹ If two lenses are equivalent, and thus they characterise the same state-space regions,
  then clearly unrestrictions over them are equivalent. ›
    
lemma unrest_equiv:
  fixes P :: "('a, 'α) uexpr"
  assumes "mwb_lens y" "x ≈⇩_L y" "x ♯ P"
  shows "y ♯ P"
  by (metis assms lens_equiv_def sublens_pres_mwb sublens_put_put unrest_uexpr.rep_eq)

text ‹ If we can show that an expression is unrestricted on a bijective lens, then is unrestricted
  on the entire state-space. ›

lemma bij_lens_unrest_all:
  fixes P :: "('a, 'α) uexpr"
  assumes "bij_lens X" "X ♯ P"
  shows "Σ ♯ P"
  using assms bij_lens_equiv_id lens_equiv_def unrest_sublens by blast

lemma bij_lens_unrest_all_eq:
  fixes P :: "('a, 'α) uexpr"
  assumes "bij_lens X"
  shows "(Σ ♯ P) ⟷ (X ♯ P)"
  by (meson assms bij_lens_equiv_id lens_equiv_def unrest_sublens)

text ‹ If an expression is unrestricted by all variables, then it is unrestricted by any variable ›

lemma unrest_all_var:
  fixes e :: "('a, 'α) uexpr"
  assumes "Σ ♯ e"
  shows "x ♯ e"
  by (metis assms id_lens_def lens.simps(2) unrest_uexpr.rep_eq)

text ‹ We can split an unrestriction composed by lens plus ›

lemma unrest_plus_split:
  fixes P :: "('a, 'α) uexpr"
  assumes "x ⨝ y" "vwb_lens x" "vwb_lens y"
  shows "unrest (x +⇩_L y) P ⟷ (x ♯ P) ∧ (y ♯ P)"
  using assms
  by (meson lens_plus_right_sublens lens_plus_ub sublens_refl unrest_sublens unrest_var_comp vwb_lens_wb)

text ‹ The following laws demonstrate the primary motivation for lens independence: a variable
  expression is unrestricted by another variable only when the two variables are independent. 
  Lens independence thus effectively allows us to semantically characterise when two variables,
  or sets of variables, are different. ›

lemma unrest_var [unrest]: "⟦ mwb_lens x; x ⨝ y ⟧ ⟹ y ♯ var x"
  by (transfer, auto)
    
lemma unrest_iuvar [unrest]: "⟦ mwb_lens x; x ⨝ y ⟧ ⟹ $y ♯ $x"
  by (simp add: unrest_var)

lemma unrest_ouvar [unrest]: "⟦ mwb_lens x; x ⨝ y ⟧ ⟹ $y´ ♯ $x´"
  by (simp add: unrest_var)

text ‹ The following laws follow automatically from independence of input and output variables. ›
    
lemma unrest_iuvar_ouvar [unrest]:
  fixes x :: "('a ⟹ 'α)"
  assumes "mwb_lens y"
  shows "$x ♯ $y´"
  by (metis prod.collapse unrest_uexpr.rep_eq var.rep_eq var_lookup_out var_update_in)

lemma unrest_ouvar_iuvar [unrest]:
  fixes x :: "('a ⟹ 'α)"
  assumes "mwb_lens y"
  shows "$x´ ♯ $y"
  by (metis prod.collapse unrest_uexpr.rep_eq var.rep_eq var_lookup_in var_update_out)

text ‹ Unrestriction distributes through the various function lifting expression constructs;
  this allows us to prove unrestrictions for the majority of the expression language. ›
    
lemma unrest_uop [unrest]: "x ♯ e ⟹ x ♯ uop f e"
  by (transfer, simp)

lemma unrest_bop [unrest]: "⟦ x ♯ u; x ♯ v ⟧ ⟹ x ♯ bop f u v"
  by (transfer, simp)

lemma unrest_trop [unrest]: "⟦ x ♯ u; x ♯ v; x ♯ w ⟧ ⟹ x ♯ trop f u v w"
  by (transfer, simp)

lemma unrest_qtop [unrest]: "⟦ x ♯ u; x ♯ v; x ♯ w; x ♯ y ⟧ ⟹ x ♯ qtop f u v w y"
  by (transfer, simp)

text ‹ For convenience, we also prove unrestriction rules for the bespoke operators on equality,
  numbers, arithmetic etc. ›
    
lemma unrest_eq [unrest]: "⟦ x ♯ u; x ♯ v ⟧ ⟹ x ♯ u =⇩_u v"
  by (simp add: eq_upred_def, transfer, simp)

lemma unrest_zero [unrest]: "x ♯ 0"
  by (simp add: unrest_lit zero_uexpr_def)

lemma unrest_one [unrest]: "x ♯ 1"
  by (simp add: one_uexpr_def unrest_lit)

lemma unrest_numeral [unrest]: "x ♯ (numeral n)"
  by (simp add: numeral_uexpr_simp unrest_lit)

lemma unrest_sgn [unrest]: "x ♯ u ⟹ x ♯ sgn u"
  by (simp add: sgn_uexpr_def unrest_uop)

lemma unrest_abs [unrest]: "x ♯ u ⟹ x ♯ abs u"
  by (simp add: abs_uexpr_def unrest_uop)

lemma unrest_plus [unrest]: "⟦ x ♯ u; x ♯ v ⟧ ⟹ x ♯ u + v"
  by (simp add: plus_uexpr_def unrest)

lemma unrest_uminus [unrest]: "x ♯ u ⟹ x ♯ - u"
  by (simp add: uminus_uexpr_def unrest)

lemma unrest_minus [unrest]: "⟦ x ♯ u; x ♯ v ⟧ ⟹ x ♯ u - v"
  by (simp add: minus_uexpr_def unrest)

lemma unrest_times [unrest]: "⟦ x ♯ u; x ♯ v ⟧ ⟹ x ♯ u * v"
  by (simp add: times_uexpr_def unrest)

lemma unrest_divide [unrest]: "⟦ x ♯ u; x ♯ v ⟧ ⟹ x ♯ u / v"
  by (simp add: divide_uexpr_def unrest)

lemma unrest_case_prod [unrest]: "⟦ ⋀ i j. x ♯ P i j ⟧ ⟹ x ♯ case_prod P v"
  by (simp add: prod.split_sel_asm)

text ‹ For a $\lambda$-term we need to show that the characteristic function expression does
  not restrict $v$ for any input value $x$. ›
    
lemma unrest_ulambda [unrest]:
  "⟦ ⋀ x. v ♯ F x ⟧ ⟹ v ♯ (λ x ∙ F x)"
  by (transfer, simp)

end