Theory Renaming

section Renaming

text ‹Similar to the bound variables of lambda calculus, location and revision identifiers are meaningless
  names. This theory contains all of the definitions and results required for renaming data structures
  and proving renaming-equivalence.›

theory Renaming
  imports Occurrences
begin

subsection Definitions

abbreviation rename_val :: "('r ⇒ 'r) ⇒ ('l ⇒ 'l) ⇒ ('r,'l,'v) val ⇒ ('r,'l,'v) val" (‹ℛ⇩V›) where
  "ℛ⇩V α β v ≡ map_val α β id v"

abbreviation rename_expr :: "('r ⇒ 'r) ⇒ ('l ⇒ 'l) ⇒ ('r,'l,'v) expr ⇒ ('r,'l,'v) expr" (‹ℛ⇩E›) where
  "ℛ⇩E α β e ≡ map_expr α β id e"

abbreviation rename_cntxt :: "('r ⇒ 'r) ⇒ ('l ⇒ 'l) ⇒ ('r,'l,'v) cntxt ⇒ ('r,'l,'v) cntxt" (‹ℛ⇩C›) where
  "ℛ⇩C α β ℰ ≡ map_cntxt α β id ℰ"

definition is_store_renaming :: "('r ⇒ 'r) ⇒ ('l ⇒ 'l) ⇒ ('r,'l,'v) store ⇒ ('r,'l,'v) store ⇒ bool" where 
  "is_store_renaming α β σ σ' ≡ ∀l. case σ l of None ⇒ σ' (β l) = None | Some v ⇒ σ' (β l) = Some (ℛ⇩V α β v)"

notation Option.bind (infixl ‹⤜› 80)

fun ℛ⇩S :: "('r ⇒ 'r) ⇒ ('l ⇒ 'l) ⇒ ('r,'l,'v) store ⇒ ('r,'l,'v) store" where
  "ℛ⇩S α β σ l = σ (inv β l) ⤜ (λv. Some (ℛ⇩V α β v))"

lemma ℛ⇩S_implements_renaming: "bij β ⟹ is_store_renaming α β σ (ℛ⇩S α β σ)"
proof -
  assume "bij β"
  hence "inj β" using bij_def by auto
  thus ?thesis by (auto simp add: is_store_renaming_def option.case_eq_if)
qed

fun ℛ⇩L :: "('r ⇒ 'r) ⇒ ('l ⇒ 'l) ⇒ ('r,'l,'v) local_state ⇒ ('r,'l,'v) local_state" where
  "ℛ⇩L α β (σ,τ,e) = (ℛ⇩S α β σ, ℛ⇩S α β τ, ℛ⇩E α β e)"

definition is_global_renaming :: "('r ⇒ 'r) ⇒ ('l ⇒ 'l) ⇒ ('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" where 
  "is_global_renaming α β s s' ≡ ∀r. case s r of None ⇒ s' (α r) = None | Some ls ⇒ s' (α r) = Some (ℛ⇩L α β ls)"

fun ℛ⇩G :: "('r ⇒ 'r) ⇒ ('l ⇒ 'l) ⇒ ('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state" where
  "ℛ⇩G α β s r = s (inv α r) ⤜ (λls. Some (ℛ⇩L α β ls))"

lemma ℛ⇩G_implements_renaming: "bij α ⟹ is_global_renaming α β s (ℛ⇩G α β s)"
proof -
  assume "bij α"
  hence "inj α" using bij_def by auto
  thus ?thesis by (auto simp add: is_global_renaming_def option.case_eq_if)
qed

subsection ‹Introduction rules›

lemma ℛ⇩SI [intro]:
  assumes
    bij_β: "bij β" and
    none_case: "⋀l. σ l = None ⟹ σ' (β l) = None" and
    some_case: "⋀l v. σ l = Some v ⟹ σ' (β l) = Some (ℛ⇩V α β v)"
  shows
    "ℛ⇩S α β σ = σ'"
proof (rule ext, subst ℛ⇩S.simps)
  fix l
  show "σ (inv β l) ⤜ (λv. Some (ℛ⇩V α β v)) = σ' l" (is "?lhs = σ' l")
  proof (cases "σ (inv β l) = None")
    case True
    have lhs_none: "?lhs = None" by (simp add: True)
    have "σ' (β (inv β l)) = None" by (simp add: none_case True)
    hence rhs_none: "σ' l = None" by (simp add: bij_β bijection.intro bijection.inv_right)
    show ?thesis by (simp add: lhs_none rhs_none)
  next
    case False
    from this obtain v where is_some: "σ (inv β l) = Some v" by blast
    hence lhs_some: "?lhs = Some (ℛ⇩V α β v)" by auto
    have "σ' (β (inv β l)) = Some (ℛ⇩V α β v)" by (simp add: is_some some_case)
    hence rhs_some: "σ' l = Some (ℛ⇩V α β v)" by (simp add: bij_β bijection.intro bijection.inv_right)
    then show ?thesis by (simp add: lhs_some)
  qed
qed

lemma ℛ⇩GI [intro]: 
  assumes
    bij_α: "bij α" and
    none_case: "⋀r. s r = None ⟹ s' (α r) = None" and
    some_case: "⋀r σ τ e. s r = Some (σ,τ,e) ⟹ s' (α r) = Some (ℛ⇩L α β (σ,τ,e))"
  shows
    "ℛ⇩G α β s = s'"
proof (rule ext, subst ℛ⇩G.simps)
  fix r
  show "s (inv α r) ⤜ (λls. Some (ℛ⇩L α β ls)) = s' r" (is "?lhs = s' r")
  proof (cases "s (inv α r) = None")
    case True
    have lhs_none: "?lhs = None" by (simp add: True)
    have "s' (α (inv α r)) = None" by (simp add: none_case True)
    hence rhs_none: "s' r = None" by (simp add: bij_α bijection.intro bijection.inv_right)
    show ?thesis by (simp add: lhs_none rhs_none)
  next
    case False
    from this obtain ls where "s (inv α r) = Some ls" by blast
    from this obtain σ τ e where is_some: "s (inv α r) = Some (σ, τ, e)" by (cases ls) blast
    hence lhs_some: "?lhs = Some (ℛ⇩L α β (σ, τ, e))" by auto
    have "s' (α (inv α r)) = Some (ℛ⇩L α β (σ, τ, e))" by (simp add: is_some some_case)
    hence rhs_some: "s' r = Some (ℛ⇩L α β (σ, τ, e))" by (simp add: bij_α bijection.intro bijection.inv_right)
    then show ?thesis by (simp add: lhs_some)
  qed
qed

subsection ‹Renaming-equivalence›

subsubsection Identity

declare val.map_id [simp]
declare expr.map_id [simp]
declare cntxt.map_id [simp]
lemma ℛ⇩S_id [simp]: "ℛ⇩S id id σ = σ" by auto
lemma ℛ⇩L_id [simp]: "ℛ⇩L id id ls = ls" by (cases ls) simp
lemma ℛ⇩G_id [simp]: "ℛ⇩G id id s = s" by auto

subsubsection Composition

declare val.map_comp [simp]
declare expr.map_comp [simp]
declare cntxt.map_comp [simp]
lemma ℛ⇩S_comp [simp]: "⟦ bij β; bij β' ⟧ ⟹ ℛ⇩S α' β' (ℛ⇩S α β s) = ℛ⇩S (α' ∘ α) (β' ∘ β) s"
  by (auto simp add: o_inv_distrib)
lemma ℛ⇩L_comp [simp]: "⟦ bij β; bij β' ⟧ ⟹ ℛ⇩L α' β' (ℛ⇩L α β ls) = ℛ⇩L (α' ∘ α) (β' ∘ β) ls"
  by (cases ls) simp
lemma ℛ⇩G_comp [simp]: "⟦ bij α; bij α'; bij β; bij β' ⟧ ⟹ ℛ⇩G α' β' (ℛ⇩G α β s) = ℛ⇩G (α' ∘ α) (β' ∘ β) s"
  by (rule ext) (auto simp add: o_inv_distrib)

subsubsection Inverse

lemma ℛ⇩V_inv [simp]: "⟦ bij α; bij β ⟧ ⟹ (ℛ⇩V (inv α) (inv β) v' = v) = (ℛ⇩V α β v = v')"
  by (auto simp add: bijection.intro bijection.inv_comp_right bijection.inv_comp_left)
lemma ℛ⇩E_inv [simp]: "⟦ bij α; bij β ⟧ ⟹ (ℛ⇩E (inv α) (inv β) e' = e) = (ℛ⇩E α β e = e')"
  by (auto simp add: bijection.intro bijection.inv_comp_right bijection.inv_comp_left)
lemma ℛ⇩C_inv [simp]: "⟦ bij α; bij β ⟧ ⟹ (ℛ⇩C (inv α) (inv β) ℰ' = ℰ) = (ℛ⇩C α β ℰ = ℰ')"
  by (auto simp add: bijection.intro bijection.inv_comp_right bijection.inv_comp_left)
lemma ℛ⇩S_inv [simp]: "⟦ bij α; bij β ⟧ ⟹ (ℛ⇩S (inv α) (inv β) σ' = σ) = (ℛ⇩S α β σ = σ')"
  by (auto simp add: bij_imp_bij_inv bijection.intro bijection.inv_comp_right bijection.inv_comp_left)
lemma ℛ⇩L_inv [simp]: "⟦ bij α; bij β ⟧ ⟹ (ℛ⇩L (inv α) (inv β) ls' = ls) = (ℛ⇩L α β ls = ls')"
  by (auto simp add: bij_imp_bij_inv bijection.intro bijection.inv_comp_right bijection.inv_comp_left)
lemma ℛ⇩G_inv [simp]: "⟦ bij α; bij β ⟧ ⟹ (ℛ⇩G (inv α) (inv β) s' = s) = (ℛ⇩G α β s = s')"
  by (auto simp add: bij_imp_bij_inv bijection.intro bijection.inv_comp_right bijection.inv_comp_left)

subsubsection Equivalence

definition eq_states :: "('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" (‹_ ≈ _› [100, 100]) where
  "s ≈ s' ≡ ∃α β. bij α ∧ bij β ∧ ℛ⇩G α β s = s'"

lemma eq_statesI [intro]:
  "ℛ⇩G α β s = s' ⟹ bij α ⟹ bij β ⟹ s ≈ s'"
  using eq_states_def by auto

lemma eq_statesE [elim]:
  "s ≈ s' ⟹ (⋀α β. ℛ⇩G α β s = s' ⟹ bij α ⟹ bij β ⟹ P) ⟹ P"
  using eq_states_def by blast

lemma αβ_refl: "s ≈ s" by (rule eq_statesI[of id id s]) auto
 
lemma αβ_trans: "s ≈ s' ⟹ s' ≈ s'' ⟹ s ≈ s''"
proof -
  assume "s ≈ s'"
  from this obtain α β where s_s': "bij α" "bij β" "ℛ⇩G α β s = s'" by blast
  assume "s' ≈ s''"
  from this obtain α' β' where s'_s'': "bij α'" "bij β'" "ℛ⇩G α' β' s' = s''" by blast
  show "s ≈ s''" by (rule eq_statesI[of "α' ∘ α" "β' ∘ β"]) (use s_s' s'_s'' in ‹auto simp add: bij_comp›)
qed

lemma αβ_sym: "s ≈ s' ⟹ s' ≈ s"
proof -
  assume "s ≈ s'"
  from this obtain α β where s_s': "bij α" "bij β" "ℛ⇩G α β s = s'" by blast
  show "s' ≈ s" by (rule eq_statesI[of "inv α" "inv β"]) (use s_s' in ‹auto simp add: bij_imp_bij_inv›)
qed

subsection ‹Distributive laws›

subsubsection Expression

lemma renaming_distr_completion [simp]:
  "ℛ⇩E α β (ℰ[e]) = ((ℛ⇩C α β ℰ)[ℛ⇩E α β e])"
  by (induct ℰ) simp+

subsubsection Store

lemma renaming_distr_combination [simp]: 
  "ℛ⇩S α β (σ;;τ) = (ℛ⇩S α β σ;;ℛ⇩S α β τ)"
  by (rule ext) auto

lemma renaming_distr_store [simp]:
  "bij β ⟹ ℛ⇩S α β (σ(l ↦ v)) = (ℛ⇩S α β σ)(β l ↦ ℛ⇩V α β v)"
  by (auto simp add: bijection.intro bijection.inv_left_eq_iff)

(* distribution law for local follows from the definition *)

subsubsection Global 

lemma renaming_distr_global [simp]:
  "bij α ⟹ ℛ⇩G α β (s(r ↦ ls)) = (ℛ⇩G α β s)(α r ↦ ℛ⇩L α β ls)"
  "bij α ⟹ ℛ⇩G α β (s(r := None)) = (ℛ⇩G α β s)(α r := None)"
  by (auto simp add: bijection.intro bijection.inv_left_eq_iff)

subsection ‹Miscellaneous laws›

lemma rename_empty [simp]:
  "ℛ⇩S α β ε = ε"
  "ℛ⇩G α β ε = ε"
  by auto

subsection Swaps

lemma swap_bij: 
  "bij (id(x := x', x' := x))" (is "bij ?f")
proof (rule bijI)
  show "inj ?f" by (simp add: inj_on_def)
  show "surj ?f"
  proof
    show "UNIV ⊆ range (id(x := x', x' := x))"
    proof (rule subsetI)
      fix y
      assume "y ∈ (UNIV :: 'a set)"
      show "y ∈ range (id(x := x', x' := x))" by (cases "y = x"; cases "y = x'") auto
    qed
  qed simp
qed

lemma id_trivial_update [simp]: "id(x := x) = id" by auto (* for solving trivial peaks *)

lemma eliminate_renaming_val_expr [simp]:
  fixes
    v :: "('r,'l,'v) val" and
    e :: "('r,'l,'v) expr"
  shows
    "l ∉ LID⇩V v ⟹ ℛ⇩V α (β(l := l')) v = ℛ⇩V α β v"
    "l ∉ LID⇩E e ⟹ ℛ⇩E α (β(l := l')) e = ℛ⇩E α β e"
    "r ∉ RID⇩V v ⟹ ℛ⇩V (α(r := r')) β v = ℛ⇩V α β v"
    "r ∉ RID⇩E e ⟹ ℛ⇩E (α(r := r')) β e = ℛ⇩E α β e"
proof -
  have "(∀α β r r'. r ∉ RID⇩V v ⟶ ℛ⇩V (α(r := r')) β v = ℛ⇩V α β v) ∧
    (∀α β r r'. r ∉ RID⇩E e ⟶ ℛ⇩E (α(r := r')) β e = ℛ⇩E α β e)"
    by (induct rule: val_expr.induct) simp+
  thus 
    "r ∉ RID⇩V v ⟹ ℛ⇩V (α(r := r')) β v = ℛ⇩V α β v" 
    "r ∉ RID⇩E e ⟹ ℛ⇩E (α(r := r')) β e = ℛ⇩E α β e"
    by simp+
  have "(∀α β l l'. l ∉ LID⇩V v ⟶ ℛ⇩V α (β(l := l')) v = ℛ⇩V α β v) ∧
    (∀α β l l'. l ∉ LID⇩E e ⟶ ℛ⇩E α (β(l := l')) e = ℛ⇩E α β e)"
    by (induct rule: val_expr.induct) simp+
  thus 
    "l ∉ LID⇩V v ⟹ ℛ⇩V α (β(l := l')) v = ℛ⇩V α β v" and
    "l ∉ LID⇩E e ⟹ ℛ⇩E α (β(l := l')) e = ℛ⇩E α β e"
    by simp+
qed

lemma eliminate_renaming_cntxt [simp]:
  "r ∉ RID⇩C ℰ ⟹ ℛ⇩C (α(r := r')) β ℰ = ℛ⇩C α β ℰ"
  "l ∉ LID⇩C ℰ ⟹ ℛ⇩C α (β(l := l')) ℰ = ℛ⇩C α β ℰ"
  by (induct ℰ rule: cntxt.induct) auto

lemma eliminate_swap_val [simp, intro]:
  "r ∉ RID⇩V v ⟹ r' ∉ RID⇩V v ⟹ ℛ⇩V (id(r := r', r' := r)) id v = v"
  "l ∉ LID⇩V v ⟹ l' ∉ LID⇩V v ⟹ ℛ⇩V id (id(l := l', l' := l)) v = v"
  by simp+

lemma eliminate_swap_expr [simp, intro]:
  "r ∉ RID⇩E e ⟹ r' ∉ RID⇩E e ⟹ ℛ⇩E (id(r := r', r' := r)) id e = e"
  "l ∉ LID⇩E e ⟹ l' ∉ LID⇩E e ⟹ ℛ⇩E id (id(l := l', l' := l)) e = e"
  by simp+

lemma eliminate_swap_cntxt [simp, intro]:
  "r ∉ RID⇩C ℰ ⟹ r' ∉ RID⇩C ℰ ⟹ ℛ⇩C (id(r := r', r' := r)) id ℰ = ℰ"
  "l ∉ LID⇩C ℰ ⟹ l' ∉ LID⇩C ℰ ⟹ ℛ⇩C id (id(l := l', l' := l)) ℰ = ℰ"
  by simp+

lemma eliminate_swap_store_rid [simp, intro]:
  "r ∉ RID⇩S σ ⟹ r' ∉ RID⇩S σ ⟹ ℛ⇩S (id(r := r', r' := r)) id σ = σ"
  by (rule ℛ⇩SI) (auto simp add: swap_bij RID⇩S_def domIff ranI)

lemma eliminate_swap_store_lid [simp, intro]:
  "l ∉ LID⇩S σ ⟹ l' ∉ LID⇩S σ ⟹ ℛ⇩S id (id(l := l', l' := l)) σ = σ"
  by (rule ℛ⇩SI) (auto simp add: swap_bij LID⇩S_def domIff ranI)

lemma eliminate_swap_global_rid [simp, intro]:
  "r ∉ RID⇩G s ⟹ r' ∉ RID⇩G s ⟹ ℛ⇩G (id(r := r', r' := r)) id s = s"
  by (rule ℛ⇩GI[OF swap_bij], ((rule sym, auto)[1])+)

lemma eliminate_swap_global_lid [simp, intro]:
  "l ∉ LID⇩G s ⟹ l' ∉ LID⇩G s ⟹ ℛ⇩G id (id(l := l', l' := l)) s = s"
  by (rule ℛ⇩GI) (auto simp add: ID_distr_global_conditional)

end