Theory Liberation

subsection ‹ Liberation ›

theory Liberation
  imports Extension
begin

text ‹ Liberation~\cite{Dongol19} is an operator that removes dependence on a number of variables.
  It is similar to existential quantification, but is defined over a scene (a variable set). ›

subsection ‹ Definition and Syntax ›

definition liberate :: "('s ⇒ bool) ⇒ 's scene ⇒ ('s ⇒ bool)" where
[expr_defs]: "liberate P x = (λ s. ∃ s'. P (s ⊕⇩S s' on x))"

syntax
  "_liberate" :: "logic ⇒ salpha ⇒ logic" (infixl "\\" 80)

translations
  "_liberate P x" == "CONST liberate P x"
  "_liberate P x" <= "_liberate (P)⇩e x"

expr_constructor liberate (0)

subsection ‹ Laws ›

lemma liberate_lens [expr_simps]: 
  "mwb_lens x ⟹ P \\ $x = (λs. ∃s'. P (s ◃⇘x⇙ s'))"
  by (simp add: liberate_def)

lemma liberate_lens': "mwb_lens x ⟹ P \\ $x = (λs. ∃v. P (put⇘x⇙ s v))"
  by (auto simp add: liberate_def lens_defs fun_eq_iff)
     (metis mwb_lens_weak weak_lens.put_get)

lemma liberate_as_subst: "vwb_lens x ⟹ e \\ $x = (∃ v. e⟦«v»/x⟧)⇩e"
  by (expr_simp, metis vwb_lens.put_eq)

lemma unrest_liberate: "a ♯ P \\ a"
  by (expr_simp)

lemma unrest_liberate_iff: "(a ♯ P) ⟷ (P \\ a = P)"
  by (expr_simp, metis (full_types) scene_override_overshadow_left)

lemma liberate_none [simp]: "P \\ ∅ = P"
  by (expr_simp)

lemma liberate_idem [simp]: "P \\ a \\ a = P \\ a"
  by (expr_simp)

lemma liberate_commute [simp]: "a ⨝⇩S b ⟹ P \\ a \\ b = P \\ b \\ a"
  using scene_override_commute_indep by (expr_auto, fastforce+)

lemma liberate_true [simp]: "(True)⇩e \\ a = (True)⇩e"
  by (expr_simp)

lemma liberate_false [simp]: "(False)⇩e \\ a = (False)⇩e"
  by (expr_simp)

lemma liberate_disj [simp]: "(P ∨ Q)⇩e \\ a = (P \\ a ∨ Q \\ a)⇩e"
  by (expr_auto)

end