Theory Unrestriction

section ‹ Unrestriction ›

theory Unrestriction
  imports Expressions
begin

text ‹ Unrestriction means that an expression does not depend on the value of the state space
  described by the given scene (i.e. set of variables) for its valuation. It is a semantic
  characterisation of fresh variables. ›

consts unrest :: "'s scene ⇒ 'p ⇒ bool"

definition unrest_expr :: "'s scene ⇒ ('b, 's) expr ⇒ bool" where
[expr_defs]: "unrest_expr a e = (∀ s s'. e (s ⊕⇩S s' on a) = e s)"

adhoc_overloading unrest ⇌ unrest_expr

syntax
  "_unrest" :: "salpha ⇒ logic ⇒ logic ⇒ logic" (infix "♯" 20)

translations
  "_unrest x p" == "CONST unrest x p"                                           

named_theorems unrest

lemma unrest_empty [unrest]: "∅ ♯ P"
  by (simp add: expr_defs lens_defs)

lemma unrest_var_union [unrest]:
  "⟦ A ♯ P; B ♯ P ⟧ ⟹ A ∪ B ♯ P"
  by (simp add: expr_defs lens_defs)
     (metis scene_override_union scene_override_unit scene_union_incompat)

lemma unrest_neg_union:
  assumes "A ##⇩S B" "- A ♯ P" "- B ♯ P"
  shows "(- (A ∪ B)) ♯ P"
  using assms by (simp add: unrest_expr_def scene_override_commute scene_override_union)

text ‹ The following two laws greatly simplify proof when reasoning about unrestricted lens,
  and so we add them to the expression simplification set. ›

lemma unrest_lens [expr_simps]:
  "mwb_lens x ⟹ ($x ♯ e) = (∀ s v. e (put⇘x⇙ s v) = e s)"
  by (simp add: unrest_expr_def var_alpha_def comp_mwb_lens lens_override_def)
     (metis mwb_lens.put_put)

lemma unrest_compl_lens [expr_simps]:
  "mwb_lens x ⟹ (- $x ♯ e) = (∀s s'. e (put⇘x⇙ s' (get⇘x⇙ s)) = e s)"
  by (simp add: unrest_expr_def var_alpha_def comp_mwb_lens lens_override_def scene_override_commute)

lemma unrest_subscene: "⟦ idem_scene a; a ♯ e; b ⊆⇩S a ⟧ ⟹ b ♯ e"
  by (metis subscene_eliminate unrest_expr_def)

lemma unrest_lens_comp [unrest]: "⟦ mwb_lens x; mwb_lens y; $x ♯ e ⟧ ⟹ $x:y ♯ e"
  by (simp add: unrest_lens, simp add: lens_comp_def ns_alpha_def)

lemma unrest_expr [unrest]: "x ♯ e ⟹ x ♯ (e)⇩e"
  by (simp add: expr_defs)

lemma unrest_lit [unrest]: "x ♯ («v»)⇩e"
  by (simp add: expr_defs)

lemma unrest_var [unrest]: 
  "⟦ vwb_lens x; idem_scene a; var_alpha x ⨝⇩S a ⟧ ⟹ a ♯ ($x)⇩e"
  by (auto simp add: unrest_expr_def scene_indep_override var_alpha_def)
     (metis lens_override_def lens_override_idem mwb_lens_weak vwb_lens_mwb weak_lens_def)

lemma unrest_var_single [unrest]:
  "⟦ mwb_lens x; x ⨝ y ⟧ ⟹ $x ♯ ($y)⇩e"
  by (simp add: expr_defs lens_indep.lens_put_irr2 lens_indep_sym lens_override_def var_alpha_def)

lemma unrest_sublens:
  assumes "mwb_lens x" "$x ♯ P" "y ⊆⇩L x"
  shows "$y ♯ P"
  by (metis assms sublens_pres_mwb sublens_put_put unrest_lens)

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:
  assumes "mwb_lens y" "x ≈⇩L y" "$x ♯ P"
  shows "$y ♯ P"
  using assms lens_equiv_def sublens_pres_mwb unrest_sublens by blast

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:
  assumes "bij_lens x" "$x ♯ P"
  shows "Σ ♯ P"
  by (metis assms bij_lens_vwb lens_scene_top_iff_bij_lens univ_alpha_def var_alpha_def vwb_lens_iff_mwb_UNIV_src)

lemma bij_lens_unrest_all_eq:
  assumes "bij_lens x"
  shows "(Σ ♯ P) ⟷ ($x ♯ P)"
  by (metis assms bij_lens_vwb lens_scene_top_iff_bij_lens univ_alpha_def var_alpha_def vwb_lens_mwb)

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

lemma unrest_all_var:
  assumes "Σ ♯ e"
  shows "$x ♯ e"
  by (metis assms scene_top_greatest top_idem_scene univ_alpha_def unrest_subscene)

lemma unrest_pair [unrest]:
  assumes "mwb_lens x" "mwb_lens y" "$x ♯ P" "$y ♯ P"
  shows "$(x, y) ♯ P"
  using assms
  by expr_simp (simp add: lens_override_def lens_scene.rep_eq scene_override.rep_eq)

lemma unrest_pair_split:
  assumes "x ⨝ y" "vwb_lens x" "vwb_lens y"
  shows "($(x, y) ♯ P) = (($x ♯ P) ∧ ($y ♯ P))"
  using assms
  by (metis lens_equiv_scene lens_indep_sym lens_plus_comm lens_plus_right_sublens plus_vwb_lens sublens_refl unrest_pair unrest_sublens var_alpha_def var_pair_def vwb_lens_def)

lemma unrest_get [unrest]: "⟦ mwb_lens x; x ⨝ y ⟧ ⟹ $x ♯ get⇘y⇙"
  by (expr_simp, simp add: lens_indep.lens_put_irr2)

lemma unrest_conj [unrest]:
  "⟦ x ♯ P; x ♯ Q ⟧ ⟹ x ♯ (P ∧ Q)⇩e"
  by (auto simp add: expr_defs)

lemma unrest_not [unrest]:
  "⟦ x ♯ P ⟧ ⟹ x ♯ (¬ P)⇩e"
  by (auto simp add: expr_defs)

lemma unrest_disj [unrest]:
  "⟦ x ♯ P; x ♯ Q ⟧ ⟹ x ♯ (P ∨ Q)⇩e"
  by (auto simp add: expr_defs)

lemma unrest_implies [unrest]:
  "⟦ x ♯ P; x ♯ Q ⟧ ⟹ x ♯ (P ⟶ Q)⇩e"
  by (auto simp add: expr_defs)

lemma unrest_expr_if [unrest]:
  assumes "a ♯ P" "a ♯ Q" "a ♯ (e)⇩e"
  shows "a ♯ (P ◃ e ▹ Q)"
  using assms by expr_simp

lemma unrest_uop:
  "⟦ x ♯ e ⟧ ⟹ x ♯ («f» e)⇩e"
  by (auto simp add: expr_defs)

lemma unrest_bop:
  "⟦ x ♯ e⇩1; x ♯ e⇩2 ⟧ ⟹ x ♯ («f» e⇩1 e⇩2)⇩e"
  by (auto simp add: expr_defs)

lemma unrest_trop:
  "⟦ x ♯ e⇩1; x ♯ e⇩2; x ♯ e⇩3 ⟧ ⟹ x ♯ («f» e⇩1 e⇩2 e⇩3)⇩e"
  by (auto simp add: expr_defs)

end