Theory Extension

section ‹ Extension and Restriction ›

theory Extension
  imports Substitutions
begin

text ‹ It is often necessary to coerce an expression into a different state space using a lens,
  for example when the state space grows to add additional variables. Extension and restriction
  is provided by @{term aext} and @{term ares} respectively. Here, we provide syntax translations
  and reasoning support for these.
›

subsection ‹ Syntax ›

syntax 
  "_aext"      :: "logic ⇒ svid ⇒ logic" (infixl "↑" 80)
  "_ares"      :: "logic ⇒ svid ⇒ logic" (infixl "↓" 80)
  "_pre"       :: "logic ⇒ logic" ("_⇧<" [999] 1000)
  "_post"      :: "logic ⇒ logic" ("_⇧>" [999] 1000)
  "_drop_pre"  :: "logic ⇒ logic" ("_⇩<" [999] 1000)
  "_drop_post" :: "logic ⇒ logic" ("_⇩>" [999] 1000)

translations
  "_aext P a" == "CONST aext P a"
  "_ares P a" == "CONST ares P a"
  "_pre P" == "_aext (P)⇩e fst⇩L"
  "_post P" == "_aext (P)⇩e snd⇩L"
  "_drop_pre P" == "_ares (P)⇩e fst⇩L"
  "_drop_post P" == "_ares (P)⇩e snd⇩L"

expr_constructor aext
expr_constructor ares

named_theorems alpha

subsection ‹ Laws ›

lemma aext_var [alpha]: "($x)⇩e ↑ a = ($a:x)⇩e"
  by (simp add: expr_defs lens_defs)

lemma ares_aext [alpha]: "weak_lens a ⟹ P ↑ a ↓ a = P"
  by (simp add: expr_defs)

lemma aext_ares [alpha]: "⟦ mwb_lens a; (- $a) ♯ P ⟧ ⟹ P ↓ a ↑ a = P"
  unfolding unrest_compl_lens
  by (auto simp add: expr_defs fun_eq_iff lens_create_def)

lemma expr_pre [simp]: "e⇧< (s⇩1, s⇩2) = (e)⇩e s⇩1"
  by (simp add: subst_ext_def subst_app_def)

lemma expr_post [simp]: "e⇧> (s⇩1, s⇩2) = (@e)⇩e s⇩2"
  by (simp add: subst_ext_def subst_app_def)

lemma unrest_aext_expr_lens [unrest]: "⟦ mwb_lens x; x ⨝ a ⟧ ⟹ $x ♯ (P ↑ a)"
  by (expr_simp add: lens_indep.lens_put_irr2)

lemma unrest_init_pre [unrest]: "⟦ mwb_lens x; $x ♯ e ⟧ ⟹ $x⇧< ♯ e⇧<"
  by expr_auto

lemma unrest_init_post [unrest]: "mwb_lens x ⟹ $x⇧< ♯ e⇧>"
  by expr_auto

lemma unrest_fin_pre [unrest]: "mwb_lens x ⟹ $x⇧> ♯ e⇧<"
  by expr_auto

lemma unrest_fin_post [unrest]: "⟦ mwb_lens x; $x ♯ e ⟧ ⟹ $x⇧> ♯ e⇧>"
  by expr_auto

lemma aext_get_fst [usubst]: "aext (get⇘x⇙) fst⇩L = get⇘ns_alpha fst⇩L x⇙"
  by expr_simp

lemma aext_get_snd [usubst]: "aext (get⇘x⇙) snd⇩L = get⇘ns_alpha snd⇩L x⇙"
  by expr_simp

subsection ‹ Substitutions ›

definition subst_aext :: "'a subst ⇒ ('a ⟹ 'b) ⇒ 'b subst"
  where [expr_defs]: "subst_aext σ x = (λ s. put⇘x⇙ s (σ (get⇘x⇙ s)))"

definition subst_ares :: "'b subst ⇒ ('a ⟹ 'b) ⇒ 'a subst"
  where [expr_defs]: "subst_ares σ x = (λ s. get⇘x⇙ (σ (create⇘x⇙ s)))"

syntax 
  "_subst_aext" :: "logic ⇒ svid ⇒ logic" (infixl "↑⇩s" 80)
  "_subst_ares" :: "logic ⇒ svid ⇒ logic" (infixl "↓⇩s" 80)

translations
  "_subst_aext P a" == "CONST subst_aext P a"
  "_subst_ares P a" == "CONST subst_ares P a"

lemma unrest_subst_aext [unrest]: "x ⨝ a ⟹ $x ♯⇩s (σ ↑⇩s a)"
  by (expr_simp)
     (metis lens_indep_def lens_override_def lens_scene.rep_eq scene_override.rep_eq)

lemma subst_id_ext [usubst]:
  "vwb_lens x ⟹ [↝] ↑⇩s x = [↝]"
  by expr_auto

lemma upd_subst_ext [alpha]:
  "vwb_lens x ⟹ σ(y ↝ e) ↑⇩s x = (σ ↑⇩s x)(x:y ↝ e ↑ x)"
  by expr_auto

lemma apply_subst_ext [alpha]:
  "vwb_lens x ⟹ (σ † e) ↑ x = (σ ↑⇩s x) † (e ↑ x)"
  by (expr_auto)

lemma subst_aext_compose [alpha]: "(σ ↑⇩s x) ↑⇩s y = σ ↑⇩s y:x"
  by (expr_simp)

lemma subst_aext_comp [usubst]:
  "vwb_lens a ⟹ (σ ↑⇩s a) ∘⇩s (ρ ↑⇩s a) = (σ ∘⇩s ρ) ↑⇩s a"
  by expr_auto

lemma subst_id_res: "mwb_lens a ⟹ [↝] ↓⇩s a = [↝]"
  by expr_auto

lemma upd_subst_res_in: 
  "⟦ mwb_lens a; x ⊆⇩L a ⟧ ⟹ σ(x ↝ e) ↓⇩s a = (σ ↓⇩s a)(x ↾ a ↝ e ↓ a)"
  by (expr_simp, fastforce)

lemma upd_subst_res_out: 
  "⟦ mwb_lens a; x ⨝ a ⟧ ⟹ σ(x ↝ e) ↓⇩s a = σ ↓⇩s a"
  by (simp add: expr_defs lens_indep_sym)

lemma subst_ext_lens_apply: "⟦ mwb_lens a; -$a ♯⇩s σ ⟧ ⟹ (a⇧↑ ∘⇩s σ) † P = ((σ ↓⇩s a) † P) ↑ a"
  by (expr_simp, simp add: lens_override_def scene_override_commute)

end