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" ("_,/ _")
"_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)
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
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