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  LIDV v  V α (β(l := l')) v = V α β v"
    "l  LIDE e  E α (β(l := l')) e = E α β e"
    "r  RIDV v  V (α(r := r')) β v = V α β v"
    "r  RIDE e  E (α(r := r')) β e = E α β e"
proof -
  have "(α β r r'. r  RIDV v  V (α(r := r')) β v = V α β v) 
    (α β r r'. r  RIDE e  E (α(r := r')) β e = E α β e)"
    by (induct rule: val_expr.induct) simp+
  thus 
    "r  RIDV v  V (α(r := r')) β v = V α β v" 
    "r  RIDE e  E (α(r := r')) β e = E α β e"
    by simp+
  have "(α β l l'. l  LIDV v  V α (β(l := l')) v = V α β v) 
    (α β l l'. l  LIDE e  E α (β(l := l')) e = E α β e)"
    by (induct rule: val_expr.induct) simp+
  thus 
    "l  LIDV v  V α (β(l := l')) v = V α β v" and
    "l  LIDE e  E α (β(l := l')) e = E α β e"
    by simp+
qed

lemma eliminate_renaming_cntxt [simp]:
  "r  RIDC   C (α(r := r')) β  = C α β "
  "l  LIDC   C α (β(l := l'))  = C α β "
  by (induct  rule: cntxt.induct) auto

lemma eliminate_swap_val [simp, intro]:
  "r  RIDV v  r'  RIDV v  V (id(r := r', r' := r)) id v = v"
  "l  LIDV v  l'  LIDV v  V id (id(l := l', l' := l)) v = v"
  by simp+

lemma eliminate_swap_expr [simp, intro]:
  "r  RIDE e  r'  RIDE e  E (id(r := r', r' := r)) id e = e"
  "l  LIDE e  l'  LIDE e  E id (id(l := l', l' := l)) e = e"
  by simp+

lemma eliminate_swap_cntxt [simp, intro]:
  "r  RIDC   r'  RIDC   C (id(r := r', r' := r)) id  = "
  "l  LIDC   l'  LIDC   C id (id(l := l', l' := l))  = "
  by simp+

lemma eliminate_swap_store_rid [simp, intro]:
  "r  RIDS σ  r'  RIDS σ  S (id(r := r', r' := r)) id σ = σ"
  by (rule SI) (auto simp add: swap_bij RIDS_def domIff ranI)

lemma eliminate_swap_store_lid [simp, intro]:
  "l  LIDS σ  l'  LIDS σ  S id (id(l := l', l' := l)) σ = σ"
  by (rule SI) (auto simp add: swap_bij LIDS_def domIff ranI)

lemma eliminate_swap_global_rid [simp, intro]:
  "r  RIDG s  r'  RIDG 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  LIDG s  l'  LIDG s  G id (id(l := l', l' := l)) s = s"
  by (rule GI) (auto simp add: ID_distr_global_conditional)

end