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 ('s1, 's2) psubst = "'s1  's2"
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 :: "('s1, 's2) psubst" ("⦇↝⦈") 
  where [expr_defs, code_unfold]: "⦇↝⦈ = (λ s. undefined)"

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

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

definition subst_upd :: "('s1, 's2) psubst  ('a  's2)  ('a, 's1) expr  ('s1, 's2) psubst"
  where [expr_defs, code_unfold]: "subst_upd σ x e = (λ s. putx(σ s) (e s))"

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

definition subst_ext :: "('s1  's2)  ('s2, 's1) psubst" ("_" [999] 999) where
[expr_defs, code_unfold]: "subst_ext a = geta⇙"

definition subst_res :: "('s1  's2)  ('s1, 's2) psubst" ("_" [999] 999) where
[expr_defs, code_unfold]: "subst_res a = createa⇙"

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

definition subst_app :: "('s1, 's2) psubst  ('a, 's2) expr  ('a, 's1) 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 :: "('s1, 's2) psubst  ('a  's2)  ('a, 's1) expr" ("_s")
  where [expr_defs, code_unfold]: "σs x = (λ s. getx(σ s))"

definition subst_comp :: "('s1, 's2) psubst  ('s3, 's1) psubst  ('s3, 's2) 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]: "as x = [getns_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 1L = σ"
  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]: "σ  getx= σ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» e1 e2)e = («f» (σ  e1) (σ  e2))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" "PTrue/x = QTrue/x" "PFalse/x = QFalse/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. σ (putxs v) = putx(σ 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  PTrue/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  QFalse/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]: "getx([↝] s) = getxs"
  by (simp add: subst_id_def)

lemma get_subst_upd_same [usubst_eval]: "weak_lens x  getx((σ(x  e)) s) = e s"
  by (simp add: subst_upd_def SEXP_def)

lemma get_subst_upd_indep [usubst_eval]: 
  "x  y  getx((σ(y  e)) s) = getx(σ 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   getx(sset a s' s) = getxs"
  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   getx(sset a s' s) = getxs'"
  by (simp add: get_scene_override_le sset_def var_alpha_def)

lemma get_subst_ext [usubst_eval]: "getx(subst_ext a s) = getns_alpha a xs"
  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   getx((σ s $a) s) = getxs"
  by (expr_simp)

lemma get_subst_restrict_in [usubst_eval]: " vwb_lens a; x L a   getx((σ s $a) s) = getx(σ 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