Quelle  utp_usedby.thy

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