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)
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
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