Theory Substitutions

section ‹ Substitutions ›

theory Substitutions
  imports Unrestriction
begin

subsection ‹ Types and Constants ›

text ‹ A substitution is simply a function between two state spaces. Typically,
  they are used to express mappings from variables to values (e.g. assignments). ›

type_synonym ('s⇩1, 's⇩2) psubst = "'s⇩1 ⇒ 's⇩2"
type_synonym 's subst = "'s ⇒ 's"

text ‹ There are different ways of constructing an empty substitution. ›

definition subst_id :: "'s subst" ("[↝]") 
  where [expr_defs, code_unfold]: "subst_id = (λs. s)"

definition subst_nil :: "('s⇩1, 's⇩2) psubst" ("⦇↝⦈") 
  where [expr_defs, code_unfold]: "⦇↝⦈ = (λ s. undefined)"

definition subst_default :: "('s⇩1, 's⇩2::default) psubst" ("⦉↝⦊") 
  where [expr_defs, code_unfold]: "⦉↝⦊ = (λ s. default)"

text ‹ We can update a substitution by adding a new variable maplet. ›

definition subst_upd :: "('s⇩1, 's⇩2) psubst ⇒ ('a ⟹ 's⇩2) ⇒ ('a, 's⇩1) expr ⇒ ('s⇩1, 's⇩2) psubst"
  where [expr_defs, code_unfold]: "subst_upd σ x e = (λ s. put⇘x⇙ (σ s) (e s))"

text ‹ The next two operators extend and restrict the alphabet of a substitution. ›

definition subst_ext :: "('s⇩1 ⟹ 's⇩2) ⇒ ('s⇩2, 's⇩1) psubst" ("_⇧↑" [999] 999) where
[expr_defs, code_unfold]: "subst_ext a = get⇘a⇙"

definition subst_res :: "('s⇩1 ⟹ 's⇩2) ⇒ ('s⇩1, 's⇩2) psubst" ("_⇩↓" [999] 999) where
[expr_defs, code_unfold]: "subst_res a = create⇘a⇙"

text ‹ Application of a substitution to an expression is effectively function composition. ›

definition subst_app :: "('s⇩1, 's⇩2) psubst ⇒ ('a, 's⇩2) expr ⇒ ('a, 's⇩1) expr" 
  where [expr_defs]: "subst_app σ e = (λ s. e (σ s))"

abbreviation "aext P a ≡ subst_app (a⇧↑) P"
abbreviation "ares P a ≡ subst_app (a⇩↓) P"

text ‹ We can also lookup the expression a variable is mapped to. ›

definition subst_lookup :: "('s⇩1, 's⇩2) psubst ⇒ ('a ⟹ 's⇩2) ⇒ ('a, 's⇩1) expr" ("⟨_⟩⇩s")
  where [expr_defs, code_unfold]: "⟨σ⟩⇩s x = (λ s. get⇘x⇙ (σ s))"

definition subst_comp :: "('s⇩1, 's⇩2) psubst ⇒ ('s⇩3, 's⇩1) psubst ⇒ ('s⇩3, 's⇩2) psubst" (infixl "∘⇩s" 55) 
    where [expr_defs, code_unfold]: "subst_comp = comp"

definition unrest_usubst :: "'s scene ⇒ 's subst ⇒ bool" 
  where [expr_defs]: "unrest_usubst a σ = (∀ s s'. σ (s ⊕⇩S s' on a) = (σ s) ⊕⇩S s' on a)"

definition par_subst :: "'s subst ⇒ 's scene ⇒ 's scene ⇒ 's subst ⇒ 's subst"
  where [expr_defs]: "par_subst σ⇩1 A B σ⇩2 = (λ s. (s ⊕⇩S (σ⇩1 s) on A) ⊕⇩S (σ⇩2 s) on B)"

definition subst_restrict :: "'s subst ⇒ 's scene ⇒ 's subst" where 
[expr_defs]: "subst_restrict σ a = (λ s. s ⊕⇩S σ s on a)"

text ‹ Create a substitution that copies the region from the given scene from a given state.
  This is used primarily in calculating unrestriction conditions. ›

definition sset :: "'s scene ⇒ 's ⇒ 's subst" 
  where [expr_defs, code_unfold]: "sset a s' = (λ s. s ⊕⇩S s' on a)"

syntax "_sset" :: "salpha ⇒ logic ⇒ logic" ("sset[_, _]")
translations "_sset a P" == "CONST sset a P"

subsection ‹ Syntax Translations ›

nonterminal uexprs and smaplet and smaplets

syntax
  "_subst_app" :: "logic ⇒ logic ⇒ logic" (infix "†" 65)
  "_smaplet"        :: "[svid, logic] => smaplet" ("_ ↝ _")
  ""                :: "smaplet => smaplets" ("_")
  "_SMaplets"       :: "[smaplet, smaplets] => smaplets" ("_,/ _")
  ― ‹ A little syntax utility to extract a list of variable identifiers from a substitution ›
  "_smaplets_svids" :: "smaplets ⇒ logic"
  "_SubstUpd"       :: "[logic, smaplets] => logic" ("_/'(_')" [900,0] 900)
  "_Subst"          :: "smaplets => logic" ("(1[_])")
  "_PSubst"         :: "smaplets => logic" ("(1⦇_⦈)")
  "_DSubst"         :: "smaplets ⇒ logic" ("(1⦉_⦊)")
  "_psubst"         :: "[logic, svids, uexprs] ⇒ logic"
  "_subst"          :: "logic ⇒ uexprs ⇒ svids ⇒ logic" ("(_⟦_'/_⟧)" [990,0,0] 991)
  "_uexprs"         :: "[logic, uexprs] => uexprs" ("_,/ _")
  ""                :: "logic => uexprs" ("_")
  "_par_subst"      :: "logic ⇒ salpha ⇒ salpha ⇒ logic ⇒ logic" ("_ [_|_]⇩s _" [100,0,0,101] 101)
  "_subst_restrict" :: "logic ⇒ salpha ⇒ logic" (infixl "↾⇩s" 85)
  "_unrest_usubst"  :: "salpha ⇒ logic ⇒ logic ⇒ logic" (infix "♯⇩s" 20)

translations
  "_subst_app σ e"                    == "CONST subst_app σ e"
  "_subst_app σ e"                    <= "_subst_app σ (e)⇩e"
  "_SubstUpd m (_SMaplets xy ms)"     == "_SubstUpd (_SubstUpd m xy) ms"
  "_SubstUpd m (_smaplet x y)"        == "CONST subst_upd m x (y)⇩e"
  "_Subst ms"                         == "_SubstUpd [↝] ms"
  "_Subst (_SMaplets ms1 ms2)"        <= "_SubstUpd (_Subst ms1) ms2"
  "_PSubst ms"                        == "_SubstUpd ⦇↝⦈ ms"
  "_PSubst (_SMaplets ms1 ms2)"       <= "_SubstUpd (_PSubst ms1) ms2"
  "_DSubst ms"                        == "_SubstUpd ⦉↝⦊ ms"
  "_DSubst (_SMaplets ms1 ms2)"       <= "_SubstUpd (_DSubst ms1) ms2"
  "_SMaplets ms1 (_SMaplets ms2 ms3)" <= "_SMaplets (_SMaplets ms1 ms2) ms3"
  "_smaplets_svids (_SMaplets (_smaplet x e) ms)" => "x +⇩L (_smaplets_svids ms)"
  "_smaplets_svids (_smaplet x e)" => "x"
  "_subst P es vs" => "CONST subst_app (_psubst [↝] vs es) P"
  "_psubst m (_svid_list x xs) (_uexprs v vs)" => "_psubst (_psubst m x v) xs vs"
  "_psubst m x v"  => "CONST subst_upd m x (v)⇩e"
  "_subst P v x" <= "CONST subst_app (CONST subst_upd [↝] x (v)⇩e) P"
  "_subst P v x" <= "_subst_app (_Subst (_smaplet x v)) P"
  "_subst P v x" <= "_subst (_sexp_quote P)  v x"
  "_subst P v (_svid_tuple (_of_svid_list (x +⇩L y)))" <= "_subst P v (x +⇩L y)"
  "_par_subst σ⇩1 A B σ⇩2" == "CONST par_subst σ⇩1 A B σ⇩2"
  "_subst_restrict σ a" == "CONST subst_restrict σ a"
  "_unrest_usubst x p" == "CONST unrest_usubst x p"
  "_unrest_usubst (_salphaset (_salphamk (x +⇩L y))) P"  <= "_unrest_usubst (x +⇩L y) P"

expr_constructor subst_app (1) ― ‹ Only the second parameter (1) should be treated as a lifted expression. › 
expr_constructor subst_id
expr_constructor subst_nil
expr_constructor subst_default
expr_constructor subst_upd
expr_constructor subst_lookup

ML_file ‹Expr_Util.ML›

subsection ‹ Substitution Laws ›

named_theorems usubst and usubst_eval

lemma subst_id_apply [usubst]: "[↝] † P = P"
  by (expr_auto)

lemma subst_unrest [usubst]:
  "⟦ vwb_lens x; $x ♯ v ⟧ ⟹ σ(x ↝ e) † v = σ † v"
  by expr_auto

lemma subst_lookup_id [usubst]: "⟨[↝]⟩⇩s x = [var x]⇩e"
  by expr_simp

lemma subst_lookup_aext [usubst]: "⟨a⇧↑⟩⇩s x = [get⇘ns_alpha a x⇙]⇩e"
  by expr_auto

lemma subst_id_var: "[↝] = ($❙v)⇩e"
  by expr_simp

lemma subst_upd_id_lam [usubst]: "subst_upd ($❙v)⇩e x v = subst_upd [↝] x v"
  by expr_simp

lemma subst_id [simp]: "[↝] ∘⇩s σ = σ" "σ ∘⇩s [↝] = σ"
  by expr_auto+

lemma subst_default_id [simp]: "⦉↝⦊ ∘⇩s σ = ⦉↝⦊"
  by (simp add: expr_defs comp_def)

lemma subst_lookup_one_lens [usubst]: "⟨σ⟩⇩s 1⇩L = σ"
  by expr_simp

text ‹ The following law can break expressions abstraction, so it is not by default a 
  "usubst" law. ›

lemma subst_apply_SEXP: "subst_app σ [e]⇩e = [subst_app σ e]⇩e"
  by expr_simp

lemma subst_apply_twice [usubst]: 
  "ρ † (σ † e) = (σ ∘⇩s ρ) † e"
  by expr_simp

lemma subst_apply_twice_SEXP [usubst]: 
  "ρ † [σ † e]⇩e = (σ ∘⇩s ρ) † [e]⇩e"
  by expr_simp

(* FIXME: Figure out how to make laws like this parse and simplify *)

term "(f (σ † e))⇩e"

term "(∀ x. x + $y > $z)⇩e"

term "(∀ k. P⟦«k»/x⟧)⇩e"

lemma subst_get [usubst]: "σ † get⇘x⇙ = ⟨σ⟩⇩s x"
  by (simp add: expr_defs)

lemma subst_var [usubst]: "σ † ($x)⇩e = ⟨σ⟩⇩s x"
  by (simp add: expr_defs)

text ‹ We can't use this as simplification unfortunately as the expression structure is too
  ambiguous to support automatic rewriting. ›

lemma subst_uop: "σ † («f» e)⇩e = («f» (σ † e))⇩e"
  by (simp add: expr_defs)

lemma subst_bop: "σ † («f» e⇩1 e⇩2)⇩e = («f» (σ † e⇩1) (σ † e⇩2))⇩e"
  by (simp add: expr_defs)

lemma subst_lit [usubst]: "σ † («v»)⇩e = («v»)⇩e"
  by (expr_simp)

lemmas subst_basic_ops [usubst] =
  subst_bop[where f=conj] 
  subst_bop[where f=disj] 
  subst_bop[where f=implies] 
  subst_uop[where f=Not]
  subst_bop[where f=HOL.eq] 
  subst_bop[where f=less]
  subst_bop[where f=less_eq]
  subst_bop[where f=Set.member] 
  subst_bop[where f=inf]
  subst_bop[where f=sup]
  subst_bop[where f=Pair]

text ‹ A substitution update naturally yields the given expression. ›
    
lemma subst_lookup_upd [usubst]:
  assumes "weak_lens x"
  shows "⟨σ(x ↝ v)⟩⇩s x = (v)⇩e"
  using assms by (simp add: expr_defs)

lemma subst_lookup_upd_diff [usubst]:
  assumes "x ⨝ y"
  shows "⟨σ(y ↝ v)⟩⇩s x = ⟨σ⟩⇩s x"
  using assms by (simp add: expr_defs)

lemma subst_lookup_pair [usubst]: 
  "⟨σ⟩⇩s (x +⇩L y) = ((⟨σ⟩⇩s x, ⟨σ⟩⇩s y))⇩e"
  by (expr_simp)

text ‹ Substitution update is idempotent. ›

lemma usubst_upd_idem [usubst]:
  assumes "mwb_lens x"
  shows "σ(x ↝ u, x ↝ v) = σ(x ↝ v)"
  using assms by (simp add: expr_defs)

lemma usubst_upd_idem_sub [usubst]:
  assumes "x ⊆⇩L y" "mwb_lens y"
  shows "σ(x ↝ u, y ↝ v) = σ(y ↝ v)"
  using assms by (simp add: expr_defs assms fun_eq_iff sublens_put_put)

text ‹ Substitution updates commute when the lenses are independent. ›
    
lemma subst_upd_comm:
  assumes "x ⨝ y"
  shows "σ(x ↝ u, y ↝ v) = σ(y ↝ v, x ↝ u)"
  using assms unfolding subst_upd_def
  by (auto simp add: subst_upd_def assms comp_def lens_indep_comm)

lemma subst_upd_comm2:
  assumes "z ⨝ y"
  shows "σ(x ↝ u, y ↝ v, z ↝ s) = σ(x ↝ u, z ↝ s, y ↝ v)"
  using assms unfolding subst_upd_def
  by (auto simp add: subst_upd_def assms comp_def lens_indep_comm)

lemma subst_upd_var_id [usubst]:
  "vwb_lens x ⟹ [x ↝ $x] = [↝]"
  by (simp add: subst_upd_def subst_id_def id_lens_def SEXP_def)

lemma subst_upd_pair [usubst]:
  "σ((x, y) ↝ (e, f)) = σ(y ↝ f, x ↝ e)"
  by (simp add: subst_upd_def lens_defs SEXP_def fun_eq_iff)

lemma subst_upd_comp [usubst]:
  "ρ(x ↝ v) ∘⇩s σ = (ρ ∘⇩s σ)(x ↝ σ † v)"
  by (simp add: expr_defs fun_eq_iff)

lemma swap_subst_inj: "⟦ vwb_lens x; vwb_lens y; x ⨝ y ⟧ ⟹ inj [(x, y) ↝ ($y, $x)]"
  by (simp add: expr_defs lens_defs inj_on_def)
     (metis lens_indep.lens_put_irr2 lens_indep_get vwb_lens.source_determination vwb_lens_def wb_lens_weak weak_lens.put_get)

subsection ‹ Proof rules ›

text ‹ In proof, a lens can always be substituted for an arbitrary but fixed value. ›

lemma taut_substI:
  assumes "vwb_lens x" "⋀ v. `P⟦«v»/x⟧`"
  shows "`P`"
  using assms by (expr_simp, metis vwb_lens.put_eq)

lemma eq_substI:
  assumes "vwb_lens x" "⋀ v. P⟦«v»/x⟧ = Q⟦«v»/x⟧"
  shows "P = Q"
  using assms by (expr_simp, metis vwb_lens.put_eq)

lemma bool_eq_substI:
  assumes "vwb_lens x" "P⟦True/x⟧ = Q⟦True/x⟧" "P⟦False/x⟧ = Q⟦False/x⟧"
  shows "P = Q"
  by (metis (full_types) assms eq_substI)

lemma less_eq_substI:
  assumes "vwb_lens x" "⋀ v. P⟦«v»/x⟧ ≤ Q⟦«v»/x⟧"
  shows "P ≤ Q"
  using assms by (expr_simp, metis le_funE le_funI vwb_lens_def wb_lens.source_stability)

subsection ‹ Ordering substitutions ›

text ‹ A simplification procedure to reorder substitutions maplets lexicographically by variable syntax ›

simproc_setup subst_order ("subst_upd (subst_upd σ x u) y v") =
  ‹ (fn _ => fn ctx => fn ct => 
        case (Thm.term_of ct) of
          Const (@{const_name subst_upd}, _) $ (Const (@{const_name subst_upd}, _) $ s $ x $ u) $ y $ v
            => if (XML.content_of (YXML.parse_body (Syntax.string_of_term ctx x)) > XML.content_of (YXML.parse_body (Syntax.string_of_term ctx y)))
               then SOME (mk_meta_eq @{thm subst_upd_comm})
               else NONE  |
          _ => NONE) 
  ›

subsection ‹ Substitution Unrestriction Laws ›

lemma unrest_subst_lens [expr_simps]: "mwb_lens x ⟹ ($x ♯⇩s σ) = (∀s v. σ (put⇘x⇙ s v) = put⇘x⇙ (σ s) v)"
  by (simp add: unrest_usubst_def, metis lens_override_def mwb_lens_weak weak_lens.create_get)

lemma unrest_subst_empty [unrest]: "x ♯⇩s [↝]"
  by (expr_simp)

lemma unrest_subst_upd [unrest]: "⟦ vwb_lens x; x ⨝ y; $x ♯ (e)⇩e; $x ♯⇩s σ ⟧ ⟹ $x ♯⇩s σ(y ↝ e)"
  by (expr_auto add: lens_indep_comm)

lemma unrest_subst_upd_compl [unrest]: "⟦ vwb_lens x; y ⊆⇩L x; -$x ♯ (e)⇩e; -$x ♯⇩s σ ⟧ ⟹ -$x ♯⇩s σ(y ↝ e)"
  by (expr_auto, simp add: lens_override_def scene_override_commute)

lemma unrest_subst_apply [unrest]:
  "⟦ $x ♯ P; $x ♯⇩s σ ⟧ ⟹ $x ♯ (σ † P)"
  by (expr_auto)

lemma unrest_sset [unrest]:
  "x ⨝ y ⟹ $x ♯⇩s sset[$y, v]"
  by (expr_auto, meson lens_indep_impl_scene_indep scene_override_commute_indep)

subsection ‹ Conditional Substitution Laws ›

lemma subst_cond_upd_1 [usubst]:
  "σ(x ↝ u) ◃ b ▹ ρ(x ↝ v) = (σ ◃ b ▹ ρ)(x ↝ (u ◃ b ▹ v))"
  by expr_auto

lemma subst_cond_upd_2 [usubst]:
  "⟦ vwb_lens x; $x ♯⇩s ρ ⟧ ⟹ σ(x ↝ u) ◃ b ▹ ρ = (σ ◃ b ▹ ρ)(x ↝ (u ◃ b ▹ ($x)⇩e))"
  by (expr_auto, metis lens_override_def lens_override_idem)

lemma subst_cond_upd_3 [usubst]:
  "⟦ vwb_lens x; $x ♯⇩s σ ⟧ ⟹ σ ◃ b ▹ ρ(x ↝ v) = (σ ◃ b ▹ ρ)(x ↝ (($x)⇩e ◃ b ▹ v))"
  by (expr_auto, metis lens_override_def lens_override_idem)

lemma expr_if_bool_var_left: "vwb_lens x ⟹ P⟦True/x⟧ ◃ $x ▹ Q = P ◃ $x ▹ Q"
  by (expr_simp, metis (full_types) lens_override_def lens_override_idem)

lemma expr_if_bool_var_right: "vwb_lens x ⟹ P ◃ $x ▹ Q⟦False/x⟧ = P ◃ $x ▹ Q"
  by (expr_simp, metis (full_types) lens_override_def lens_override_idem)

lemma subst_expr_if [usubst]: "σ † (P ◃ B ▹ Q) = (σ † P) ◃ (σ † B) ▹ (σ † Q)"
  by expr_simp

subsection ‹ Substitution Restriction Laws ›

lemma subst_restrict_id [usubst]: "idem_scene a ⟹ [↝] ↾⇩s a = [↝]"
  by expr_simp

lemma subst_restrict_out [usubst]: "⟦ vwb_lens x; vwb_lens a; x ⨝ a ⟧ ⟹ σ(x ↝ e) ↾⇩s $a = σ ↾⇩s $a" 
  by (expr_simp add: lens_indep.lens_put_irr2)

lemma subst_restrict_in [usubst]: "⟦ vwb_lens x; vwb_lens y; x ⊆⇩L y ⟧ ⟹ σ(x ↝ e) ↾⇩s $y = (σ ↾⇩s $y)(x ↝ e)" 
  by (expr_auto)

lemma subst_restrict_twice [simp]: "σ ↾⇩s a ↾⇩s a = σ ↾⇩s a"
  by expr_simp

subsection ‹ Evaluation ›

lemma subst_SEXP [usubst_eval]: "σ † [λ s. e s]⇩e = [λ s. e (σ s)]⇩e"
  by (simp add: SEXP_def subst_app_def fun_eq_iff)

lemma get_subst_id [usubst_eval]: "get⇘x⇙ ([↝] s) = get⇘x⇙ s"
  by (simp add: subst_id_def)

lemma get_subst_upd_same [usubst_eval]: "weak_lens x ⟹ get⇘x⇙ ((σ(x ↝ e)) s) = e s"
  by (simp add: subst_upd_def SEXP_def)

lemma get_subst_upd_indep [usubst_eval]: 
  "x ⨝ y ⟹ get⇘x⇙ ((σ(y ↝ e)) s) = get⇘x⇙ (σ s)"
  by (simp add: subst_upd_def)

lemma unrest_ssubst: "(a ♯ P) ⟷ (∀ s'. sset a s' † P = (P)⇩e)"
  by (auto simp add: expr_defs fun_eq_iff)

lemma unrest_ssubst_expr: "(a ♯ (P)⇩e) = (∀s'. sset[a, s'] † (P)⇩e = (P)⇩e)"
  by (simp add: unrest_ssubst)

lemma get_subst_sset_out [usubst_eval]: "⟦ vwb_lens x; var_alpha x ⨝⇩S a ⟧ ⟹ get⇘x⇙ (sset a s' s) = get⇘x⇙ s"
  by (simp add: expr_defs var_alpha_def get_scene_override_indep)

lemma get_subst_sset_in [usubst_eval]: "⟦ vwb_lens x; var_alpha x ≤ a ⟧ ⟹ get⇘x⇙ (sset a s' s) = get⇘x⇙ s'"
  by (simp add: get_scene_override_le sset_def var_alpha_def)

lemma get_subst_ext [usubst_eval]: "get⇘x⇙ (subst_ext a s) = get⇘ns_alpha a x⇙ s"
  by (expr_simp)

lemma unrest_sset_lens [unrest]: "⟦ mwb_lens x; mwb_lens y; x ⨝ y ⟧ ⟹ $x ♯⇩s sset[$y, s]"
  by (simp add: sset_def unrest_subst_lens lens_indep_comm lens_override_def)

lemma get_subst_restrict_out [usubst_eval]: "⟦ vwb_lens a; x ⨝ a ⟧ ⟹ get⇘x⇙ ((σ ↾⇩s $a) s) = get⇘x⇙ s"
  by (expr_simp)

lemma get_subst_restrict_in [usubst_eval]: "⟦ vwb_lens a; x ⊆⇩L a ⟧ ⟹ get⇘x⇙ ((σ ↾⇩s $a) s) = get⇘x⇙ (σ s)"
  by (expr_simp, force)

text ‹ If a variable is unrestricted in a substitution then it's application has no effect. ›

lemma subst_apply_unrest:
  "⟦ vwb_lens x; $x ♯⇩s σ ⟧ ⟹ ⟨σ⟩⇩s x = var x"
proof -
  assume 1: "vwb_lens x" and "$x ♯⇩s σ"
  hence "∀s s'. σ (s ⊕⇩L s' on x) = σ s ⊕⇩L s' on x"
    by (simp add: unrest_usubst_def)
  thus "⟨σ⟩⇩s x = var x"
    by (metis 1 lens_override_def lens_override_idem mwb_lens_weak subst_lookup_def vwb_lens_mwb weak_lens.put_get)
qed

text ‹ A tactic for proving unrestrictions by evaluating a special kind of substitution. ›

method unrest uses add = (simp add: add unrest unrest_ssubst_expr var_alpha_combine usubst usubst_eval)

text ‹ A tactic for evaluating substitutions. ›

method subst_eval uses add = (simp add: add usubst_eval usubst unrest)

text ‹ We can exercise finer grained control over substitutions with the following method. ›

declare vwb_lens_mwb [lens]
declare mwb_lens_weak [lens]

method subst_eval' = (simp only: lens usubst_eval usubst unrest SEXP_apply)

end