Theory Substitution

section Substitution

text ‹This theory introduces the substitution operation using a locale, and provides two models.›

theory Substitution
  imports Renaming
begin

subsection Definition

locale substitution =
  fixes subst :: "('r,'l,'v) expr ⇒ 'v ⇒ ('r,'l,'v) expr ⇒ ('r,'l,'v) expr"
  assumes 
    renaming_distr_subst: "ℛ⇩E α β (subst e x e') = subst (ℛ⇩E α β e) x (ℛ⇩E α β e')" and (* needed in mimicking *)
    subst_introduces_no_rids: "RID⇩E (subst e x e') ⊆ RID⇩E e ∪ RID⇩E e'" and
    subst_introduces_no_lids: "LID⇩E (subst e x e') ⊆ LID⇩E e ∪ LID⇩E e'"
begin

lemma rid_substE [dest]: "r ∈ RID⇩E (subst (VE v) x e) ⟹ r ∉ RID⇩E e ⟹ r ∈ RID⇩V v"
  using subst_introduces_no_rids by fastforce

lemma lid_substE [dest]: "l ∈ LID⇩E (subst (VE v) x e) ⟹ l ∉ LID⇩E e ⟹ l ∈ LID⇩V v"
  using subst_introduces_no_lids by fastforce

end (* substitution locale *)

subsection ‹Trivial model›

fun constant_function :: "('r,'l,'v) expr ⇒ 'v ⇒ ('r,'l,'v) expr ⇒ ('r,'l,'v) expr" where 
  "constant_function e x e' = VE (CV Unit)"

lemma constant_function_models_substitution: 
  "substitution constant_function" by (auto simp add: substitution_def)

subsection ‹Example model›

subsubsection Preliminaries

notation set3_val ("𝒱⇩V")
notation set3_expr ("𝒱⇩E")

abbreviation rename_vars_val :: "('v ⇒ 'v) ⇒ ('r,'l,'v) val ⇒ ('r,'l,'v) val" ("ℛ𝒱⇩V") where
  "ℛ𝒱⇩V ζ ≡ map_val id id ζ"

abbreviation rename_vars_expr :: "('v ⇒ 'v) ⇒ ('r,'l,'v) expr ⇒ ('r,'l,'v) expr" ("ℛ𝒱⇩E") where
  "ℛ𝒱⇩E ζ ≡ map_expr id id ζ"

lemma var_renaming_preserves_size: (* for termination proof *)
  fixes 
    v :: "('r,'l,'v) val" and
    e :: "('r,'l,'v) expr" and
    α :: "'r ⇒ 'r'" and
    β :: "'l ⇒ 'l'" and
    ζ :: "'v ⇒ 'v'"
  shows
  "size (map_val α β ζ v) = size v"
  "size (map_expr α β ζ e) = size e"
proof -
  have "(∀(α :: 'r ⇒ 'r') (β :: 'l ⇒ 'l') (ζ :: 'v ⇒ 'v'). size (map_val α β ζ v) = size v) ∧ 
        (∀(α :: 'r ⇒ 'r') (β :: 'l ⇒ 'l') (ζ :: 'v ⇒ 'v'). size (map_expr α β ζ e) = size e)"
    by (induct rule: val_expr.induct) auto
  thus 
    "size (map_val α β ζ v) = size v" 
    "size (map_expr α β ζ e) = size e" 
    by auto
qed

subsubsection Definition

function
  nat_subst⇩V :: "('r,'l,nat) expr ⇒ nat ⇒ ('r,'l,nat) val ⇒ ('r,'l,nat) expr" and
  nat_subst⇩E :: "('r,'l,nat) expr ⇒ nat ⇒ ('r,'l,nat) expr ⇒ ('r,'l,nat) expr"
  where
  "nat_subst⇩V e x (CV const) = VE (CV const)"
| "nat_subst⇩V e x (Var x') = (if x = x' then e else VE (Var x'))"
| "nat_subst⇩V e x (Loc l) = VE (Loc l)"
| "nat_subst⇩V e x (Rid r) = VE (Rid r)"
| "nat_subst⇩V e x (Lambda y e') = VE (
  if x = y then 
    Lambda y e' 
  else 
    let z = Suc (Max (𝒱⇩E e' ∪ 𝒱⇩E e)) in
    Lambda z (nat_subst⇩E e x (ℛ𝒱⇩E (id(y := z)) e')))"
| "nat_subst⇩E e x (VE v') = nat_subst⇩V e x v'"
| "nat_subst⇩E e x (Apply l r) = Apply (nat_subst⇩E e x l) (nat_subst⇩E e x r)"
| "nat_subst⇩E e x (Ite e1 e2 e3) = Ite (nat_subst⇩E e x e1) (nat_subst⇩E e x e2) (nat_subst⇩E e x e3)"
| "nat_subst⇩E e x (Ref e') = Ref (nat_subst⇩E e x e')"
| "nat_subst⇩E e x (Read e') = Read (nat_subst⇩E e x e')"
| "nat_subst⇩E e x (Assign l r) = Assign (nat_subst⇩E e x l) (nat_subst⇩E e x r)"
| "nat_subst⇩E e x (Rfork e') = Rfork (nat_subst⇩E e x e')"
| "nat_subst⇩E e x (Rjoin e')  = Rjoin (nat_subst⇩E e x e')"
  by pat_completeness auto
termination 
  by (relation "measure (λx. case x of Inl (e,x,v) ⇒ size v | Inr (e,x,e') ⇒ size e')")
     (auto simp add: var_renaming_preserves_size(2))

subsubsection ‹Proof obligations›

lemma nat_subst⇩E_distr:
  fixes e :: "('r,'l,nat) expr"
  shows "ℛ⇩E α β (nat_subst⇩E e x e') = nat_subst⇩E (ℛ⇩E α β e) x (ℛ⇩E α β e')"
proof -
  fix v' :: "('r,'l,nat) val"
  have
    "(∀α β x e ζ. ℛ⇩E α β (nat_subst⇩V e x (ℛ𝒱⇩V ζ v')) = nat_subst⇩V (ℛ⇩E α β e) x (ℛ⇩V α β (ℛ𝒱⇩V ζ v'))) ∧
     (∀α β x e ζ. ℛ⇩E α β (nat_subst⇩E e x (ℛ𝒱⇩E ζ e')) = nat_subst⇩E (ℛ⇩E α β e) x (ℛ⇩E α β (ℛ𝒱⇩E ζ e')))"
    by (induct rule: val_expr.induct) (auto simp add: expr.set_map(3) fun.map_ident)
  hence "ℛ⇩E α β (nat_subst⇩E e x (ℛ𝒱⇩E id e')) = nat_subst⇩E (ℛ⇩E α β e) x (ℛ⇩E α β (ℛ𝒱⇩E id e'))" by blast
  thus ?thesis by simp
qed

lemma nat_subst⇩E_introduces_no_rids:
  fixes e' :: "('r,'l,nat) expr"
  shows "RID⇩E (nat_subst⇩E e x e') ⊆ RID⇩E e ∪ RID⇩E e'"
proof -
  fix v' :: "('r,'l,nat) val"
  have 
    "(∀x e. ∀ζ. RID⇩E (nat_subst⇩V e x (ℛ𝒱⇩V ζ v')) ⊆ RID⇩E e ∪ RID⇩V (ℛ𝒱⇩V ζ v')) ∧
     (∀x e. ∀ζ. RID⇩E (nat_subst⇩E e x (ℛ𝒱⇩E ζ e')) ⊆ RID⇩E e ∪ RID⇩E (ℛ𝒱⇩E ζ e'))"
    by (induct rule: val_expr.induct) (auto 0 4 simp add: expr.set_map(1))
  hence "RID⇩E (nat_subst⇩E e x (ℛ𝒱⇩E id e')) ⊆ RID⇩E e ∪ RID⇩E (ℛ𝒱⇩E id e')" by blast
  thus ?thesis by simp
qed

lemma nat_subst⇩E_introduces_no_lids: 
  fixes e' :: "('r,'l,nat) expr"
  shows "LID⇩E (nat_subst⇩E e x e') ⊆ LID⇩E e ∪ LID⇩E e'"
proof -
  fix v' :: "('r,'l,nat) val"
  have 
    "(∀x e. ∀ζ. LID⇩E (nat_subst⇩V e x (ℛ𝒱⇩V ζ v')) ⊆ LID⇩E e ∪ LID⇩V (ℛ𝒱⇩V ζ v')) ∧
     (∀x e. ∀ζ. LID⇩E (nat_subst⇩E e x (ℛ𝒱⇩E ζ e')) ⊆ LID⇩E e ∪ LID⇩E (ℛ𝒱⇩E ζ e'))"
    by (induct rule: val_expr.induct) (auto 0 4 simp add: expr.set_map(2))
  hence "LID⇩E (nat_subst⇩E e x (ℛ𝒱⇩E id e')) ⊆ LID⇩E e ∪ LID⇩E (ℛ𝒱⇩E id e')" by blast
  thus ?thesis by simp
qed

lemma nat_subst⇩E_models_substitution: "substitution nat_subst⇩E"
  by (simp add: nat_subst⇩E_distr nat_subst⇩E_introduces_no_lids nat_subst⇩E_introduces_no_rids substitution_def)

end