Theory Quantifiers

subsection ‹ Quantifying Lenses ›

theory Quantifiers
  imports Liberation
begin

text ‹ We define operators to existentially and universally quantify an expression over a lens. ›

subsection ‹ Operators and Syntax ›

definition ex_expr :: "('a ⟹ 's) ⇒ (bool, 's) expr ⇒ (bool, 's) expr" where
[expr_defs]: "ex_expr x e = (λ s. (∃ v. e (put⇘x⇙ s v)))"

definition ex1_expr :: "('a ⟹ 's) ⇒ (bool, 's) expr ⇒ (bool, 's) expr" where
[expr_defs]: "ex1_expr x e = (λ s. (∃! v. e (put⇘x⇙ s v)))"

definition all_expr :: "('a ⟹ 's) ⇒ (bool, 's) expr ⇒ (bool, 's) expr" where
[expr_defs]: "all_expr x e = (λ s. (∀ v. e (put⇘x⇙ s v)))"

expr_constructor ex_expr (1)
expr_constructor ex1_expr (1)
expr_constructor all_expr (1)

syntax 
  "_ex_expr"  :: "svid ⇒ logic ⇒ logic" ("∃ _ ⦁ _" [0, 20] 20)
  "_ex1_expr" :: "svid ⇒ logic ⇒ logic" ("∃⇩1 _ ⦁ _" [0, 20] 20)
  "_all_expr" :: "svid ⇒ logic ⇒ logic" ("∀ _ ⦁ _" [0, 20] 20)

translations
  "_ex_expr x P" == "CONST ex_expr x P"
  "_ex1_expr x P" == "CONST ex1_expr x P"
  "_all_expr x P" == "CONST all_expr x P"

subsection ‹ Laws ›

lemma ex_is_liberation: "mwb_lens x ⟹ (∃ x ⦁ P) = (P \\ $x)"
  by (expr_auto, metis mwb_lens_weak weak_lens.put_get)

lemma ex_unrest_iff: "⟦ mwb_lens x ⟧ ⟹ ($x ♯ P) ⟷ (∃ x ⦁ P) = P"
  by (simp add: ex_is_liberation unrest_liberate_iff)

lemma ex_unrest: "⟦ mwb_lens x; $x ♯ P ⟧ ⟹ (∃ x ⦁ P) = P"
  using ex_unrest_iff by blast

lemma unrest_ex_in [unrest]:
  "⟦ mwb_lens y; x ⊆⇩L y ⟧ ⟹ $x ♯ (∃ y ⦁ P)"
  by (simp add: ex_expr_def sublens_pres_mwb sublens_put_put unrest_lens)

lemma unrest_ex_out [unrest]:
  "⟦ mwb_lens x; $x ♯ P; x ⨝ y ⟧ ⟹ $x ♯ (∃ y ⦁ P)"
  by (simp add: ex_expr_def unrest_lens, metis lens_indep.lens_put_comm)

lemma subst_ex_out [usubst]: "⟦ mwb_lens x; $x ♯⇩s σ ⟧ ⟹ σ † (∃ x ⦁ P) = (∃ x ⦁ σ † P)"
  by (expr_simp)

lemma subst_lit_ex_indep [usubst]:
  "y ⨝ x ⟹ σ(y ↝ «v») † (∃ x ⦁ P) = σ † (∃ x ⦁ [y ↝ «v»] † P)"
  by (expr_simp, simp add: lens_indep.lens_put_comm)

lemma subst_ex_in [usubst]:
  "⟦ vwb_lens a; x ⊆⇩L a ⟧ ⟹ σ(x ↝ e) † (∃ a ⦁ P) = σ † (∃ a ⦁ P)"
  by (expr_simp, force)

declare lens_plus_right_sublens [simp]

lemma ex_as_subst: "vwb_lens x ⟹ (∃ x ⦁ e) = (∃ v. e⟦«v»/x⟧)⇩e"
  by expr_auto

lemma ex_twice [simp]: "mwb_lens x ⟹ (∃ x ⦁ ∃ x ⦁ P) = (∃ x ⦁ P)"
  by (expr_simp)

lemma ex_commute: "x ⨝ y ⟹ (∃ x ⦁ ∃ y ⦁ P) = (∃ y ⦁ ∃ x ⦁ P)"
  by (expr_auto, metis lens_indep_comm)+
  
lemma ex_true [simp]: "(∃ x ⦁ (True)⇩e) = (True)⇩e"
  by expr_simp

lemma ex_false [simp]: "(∃ x ⦁ (False)⇩e) = (False)⇩e"
  by (expr_simp)

lemma ex_disj [simp]: "(∃ x ⦁ (P ∨ Q)⇩e) = ((∃ x ⦁ P) ∨ (∃ x ⦁ Q))⇩e"
  by (expr_auto)

lemma ex_plus:
  "(∃ (y,x) ⦁ P) = (∃ x ⦁ ∃ y ⦁ P)"
  by (expr_auto)

lemma all_as_ex: "(∀ x ⦁ P) = (¬ (∃ x ⦁ ¬ P))⇩e"
  by (expr_auto)

lemma ex_as_all: "(∃ x ⦁ P) = (¬ (∀ x ⦁ ¬ P))⇩e"
  by (expr_auto)

subsection ‹ Cylindric Algebra ›

lemma ex_C1: "(∃ x ⦁ (False)⇩e) = (False)⇩e"
  by (expr_auto)

lemma ex_C2: "wb_lens x ⟹ `P ⟶ (∃ x ⦁ P)`"
  by (expr_simp, metis wb_lens.get_put)

lemma ex_C3: "mwb_lens x ⟹ (∃ x ⦁ (P ∧ (∃ x ⦁ Q)))⇩e = ((∃ x ⦁ P) ∧ (∃ x ⦁ Q))⇩e"
  by (expr_auto)

lemma ex_C4a: "x ≈⇩L y ⟹ (∃ x ⦁ ∃ y ⦁ P) = (∃ y ⦁ ∃ x ⦁ P)"
  by (expr_simp, metis (mono_tags, lifting) lens.select_convs(2))

lemma ex_C4b: "x ⨝ y ⟹ (∃ x ⦁ ∃ y ⦁ P) = (∃ y ⦁ ∃ x ⦁ P)"
  using ex_commute by blast

lemma ex_C5:
  fixes x :: "('a ⟹ 'α)"
  shows "($x = $x)⇩e = (True)⇩e"
  by simp

lemma ex_C6:
  assumes "wb_lens x" "x ⨝ y" "x ⨝ z"
  shows "($y = $z)⇩e = (∃ x ⦁ $y = $x ∧ $x = $z)⇩e"
  using assms
  by (expr_simp, metis lens_indep_def)

lemma ex_C7:
  assumes "weak_lens x" "x ⨝ y"
  shows "((∃ x ⦁ $x = $y ∧ P) ∧ (∃ x ⦁ $x = $y ∧ ¬ P))⇩e = (False)⇩e"
  using assms by (expr_simp, simp add: lens_indep_sym)

end