Theory utp_usedby

section ‹ Used-by ›

theory utp_usedby
  imports utp_unrest
begin

text ‹ The used-by predicate is the dual of unrestriction. It states that the given lens is an 
  upper-bound on the size of state space the given expression depends on. It is similar to stating
  that the lens is a valid alphabet for the predicate. For convenience, and because the predicate
  uses a similar form, we will reuse much of unrestriction's infrastructure. ›
  
consts
  usedBy :: "'a ⇒ 'b ⇒ bool"

syntax
  "_usedBy" :: "salpha ⇒ logic ⇒ logic ⇒ logic" (infix ‹♮› 20)

syntax_consts
  "_usedBy" == usedBy

translations
  "_usedBy x p" == "CONST usedBy x p"                                           
  "_usedBy (_salphaset (_salphamk (x +⇩L y))) P"  <= "_usedBy (x +⇩L y) P"

lift_definition usedBy_uexpr :: "('b ⟹ 'α) ⇒ ('a, 'α) uexpr ⇒ bool" 
is "λ x e. (∀ b b'. e (b' ⊕⇩L b on x) = e b)" .

adhoc_overloading usedBy usedBy_uexpr
  
lemma usedBy_lit [unrest]: "x ♮ «v»"
  by (transfer, simp)

lemma usedBy_sublens:
  fixes P :: "('a, 'α) uexpr"
  assumes "x ♮ P" "x ⊆⇩L y" "vwb_lens y"
  shows "y ♮ P"
  using assms 
  by (transfer, auto, metis Lens_Order.lens_override_idem lens_override_def sublens_obs_get vwb_lens_mwb)

lemma usedBy_svar [unrest]: "x ♮ P ⟹ &x ♮ P"
  by (transfer, simp add: lens_defs)
    
lemma usedBy_lens_plus_1 [unrest]: "x ♮ P ⟹ x;y ♮ P"
  by (transfer, simp add: lens_defs)

lemma usedBy_lens_plus_2 [unrest]: "⟦ x ⨝ y; y ♮ P ⟧ ⟹ x;y ♮ P"
  by (transfer, auto simp add: lens_defs lens_indep_comm)
    
text ‹ Linking used-by to unrestriction: if x is used-by P, and x is independent of y, then
  P cannot depend on any variable in y. ›
    
lemma usedBy_indep_uses:
  fixes P :: "('a, 'α) uexpr"
  assumes "x ♮ P" "x ⨝ y"
  shows "y ♯ P"
  using assms by (transfer, auto, metis lens_indep_get lens_override_def)

lemma usedBy_var [unrest]:
  assumes "vwb_lens x" "y ⊆⇩L x"
  shows "x ♮ var y"
  using assms
  by (transfer, simp add: uexpr_defs pr_var_def)
     (metis lens_override_def sublens_obs_get vwb_lens_def wb_lens.get_put)    
  
lemma usedBy_uop [unrest]: "x ♮ e ⟹ x ♮ uop f e"
  by (transfer, simp)

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

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

lemma usedBy_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 used-by rules for the bespoke operators on equality,
  numbers, arithmetic etc. ›
    
lemma usedBy_eq [unrest]: "⟦ x ♮ u; x ♮ v ⟧ ⟹ x ♮ u =⇩u v"
  by (simp add: eq_upred_def, transfer, simp)

lemma usedBy_zero [unrest]: "x ♮ 0"
  by (simp add: usedBy_lit zero_uexpr_def)

lemma usedBy_one [unrest]: "x ♮ 1"
  by (simp add: one_uexpr_def usedBy_lit)

lemma usedBy_numeral [unrest]: "x ♮ (numeral n)"
  by (simp add: numeral_uexpr_simp usedBy_lit)

lemma usedBy_sgn [unrest]: "x ♮ u ⟹ x ♮ sgn u"
  by (simp add: sgn_uexpr_def usedBy_uop)

lemma usedBy_abs [unrest]: "x ♮ u ⟹ x ♮ abs u"
  by (simp add: abs_uexpr_def usedBy_uop)

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

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

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

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

lemma usedBy_divide [unrest]: "⟦ x ♮ u; x ♮ v ⟧ ⟹ x ♮ u / v"
  by (simp add: divide_uexpr_def unrest)
    
lemma usedBy_ulambda [unrest]:
  "⟦ ⋀ x. v ♮ F x ⟧ ⟹ v ♮ (λ x ∙ F x)"
  by (transfer, simp)      

lemma unrest_var_sep [unrest]:
  "vwb_lens x ⟹ x ♮ &x:y"
  by (transfer, simp add: lens_defs)
    
end