Theory Data

section ‹Data›

text ‹This theory defines the data types and notations, and some preliminary results about them.›

theory Data
imports Main
begin

subsection ‹Function notations›

abbreviation ε :: "'a ⇀ 'b" where
"ε ≡ λx. None"

fun combine :: "('a ⇀ 'b) ⇒ ('a  ⇀ 'b) ⇒ ('a ⇀ 'b)" ("_;;_" 20) where
"(f ;; g) x = (if g x = None then f x else g x)"

lemma dom_combination_dom_union: "dom (τ;;τ') = dom τ ∪ dom τ'"
by auto

subsection ‹Values, expressions and execution contexts›

datatype const = Unit | F | T

datatype (RID⇩V: 'r, LID⇩V: 'l,'v) val =
CV const
| Var 'v
| Loc 'l
| Rid 'r
| Lambda 'v "('r,'l,'v) expr"
and (RID⇩E: 'r, LID⇩E: 'l,'v) expr =
VE "('r,'l,'v) val"
| Apply "('r,'l,'v) expr" "('r,'l,'v) expr"
| Ite "('r,'l,'v) expr" "('r,'l,'v) expr" "('r,'l,'v) expr"
| Ref "('r,'l,'v) expr"
| Assign "('r,'l,'v) expr" "('r,'l,'v) expr"
| Rfork "('r,'l,'v) expr"
| Rjoin "('r,'l,'v) expr"

datatype (RID⇩C: 'r, LID⇩C: 'l,'v) cntxt =
Hole ("□")
| ApplyL⇩ℰ "('r,'l,'v) cntxt" "('r,'l,'v) expr"
| ApplyR⇩ℰ "('r,'l,'v) val" "('r,'l,'v) cntxt"
| Ite⇩ℰ "('r,'l,'v) cntxt" "('r,'l,'v) expr" "('r,'l,'v) expr"
| Ref⇩ℰ "('r,'l,'v) cntxt"
| AssignL⇩ℰ "('r,'l,'v) cntxt" "('r,'l,'v) expr"
| AssignR⇩ℰ 'l "('r,'l,'v) cntxt"
| Rjoin⇩ℰ "('r,'l,'v) cntxt"

subsection ‹Plugging and decomposing›

fun plug :: "('r,'l,'v) cntxt ⇒ ('r,'l,'v) expr ⇒ ('r,'l,'v) expr" (infix "⊲" 60) where
"□ ⊲ e = e"
| "ApplyL⇩ℰ ℰ e1 ⊲ e = Apply (ℰ ⊲ e) e1"
| "ApplyR⇩ℰ val ℰ ⊲ e = Apply (VE val) (ℰ ⊲ e)"
| "Ite⇩ℰ ℰ e1 e2 ⊲ e = Ite (ℰ ⊲ e) e1 e2"
| "Ref⇩ℰ ℰ ⊲ e = Ref (ℰ ⊲ e)"
| "AssignL⇩ℰ ℰ e1 ⊲ e = Assign (ℰ ⊲ e) e1"
| "AssignR⇩ℰ l ℰ ⊲ e = Assign (VE (Loc l)) (ℰ ⊲ e)"
| "Rjoin⇩ℰ ℰ ⊲ e = Rjoin (ℰ ⊲ e)"

translations
"ℰ[x]" ⇌ "ℰ ⊲ x"

lemma injective_cntxt [simp]: "(ℰ[e1] = ℰ[e2]) = (e1 = e2)" by (induction ℰ) auto

lemma VE_empty_cntxt [simp]: "(VE v = ℰ[e]) = (ℰ = □ ∧ VE v = e)" by (cases ℰ, auto)

inductive redex :: "('r,'l,'v) expr ⇒ bool" where
app: "redex (Apply (VE (Lambda x e)) (VE v))"
| iteTrue: "redex (Ite (VE (CV T)) e1 e2)"
| iteFalse: "redex (Ite (VE (CV F)) e1 e2)"
| ref: "redex (Ref (VE v))"
| assign: "redex (Assign (VE (Loc l)) (VE v))"
| rfork: "redex (Rfork e)"
| rjoin: "redex (Rjoin (VE (Rid r)))"

inductive_simps redex_simps [simp]: "redex e"
inductive_cases redexE [elim]: "redex e"

lemma plugged_redex_not_val [simp]: "redex r ⟹ (ℰ ⊲ r) ≠ (VE t)" by (cases ℰ) auto

inductive decompose :: "('r,'l,'v) expr ⇒ ('r,'l,'v) cntxt ⇒ ('r,'l,'v) expr ⇒ bool" where
top_redex: "redex e ⟹ decompose e □ e"
| lapply: "⟦ ¬redex (Apply e⇩1 e⇩2); decompose e⇩1 ℰ r ⟧ ⟹ decompose (Apply e⇩1 e⇩2) (ApplyL⇩ℰ ℰ e⇩2) r"
| rapply: "⟦ ¬redex (Apply (VE v) e); decompose e ℰ r ⟧ ⟹ decompose (Apply (VE v) e) (ApplyR⇩ℰ v ℰ) r"
| ite: "⟦ ¬redex (Ite e⇩1 e⇩2 e⇩3); decompose e⇩1 ℰ r ⟧ ⟹ decompose (Ite e⇩1 e⇩2 e⇩3) (Ite⇩ℰ ℰ e⇩2 e⇩3) r"
| ref: "⟦ ¬redex (Ref e); decompose e ℰ r ⟧ ⟹ decompose (Ref e) (Ref⇩ℰ ℰ) r"
| lassign: "⟦ ¬redex (Assign e⇩1 e⇩2); decompose e⇩1 ℰ r ⟧ ⟹ decompose (Assign e⇩1 e⇩2) (AssignL⇩ℰ ℰ e⇩2) r"
| rassign: "⟦ ¬redex (Assign (VE (Loc l)) e⇩2); decompose e⇩2 ℰ r ⟧ ⟹ decompose (Assign (VE (Loc l)) e⇩2) (AssignR⇩ℰ l ℰ) r"
| rjoin:  "⟦ ¬redex (Rjoin e); decompose e ℰ r ⟧ ⟹ decompose (Rjoin e) (Rjoin⇩ℰ ℰ) r"

inductive_cases decomposeE [elim]: "decompose e ℰ r"

lemma plug_decomposition_equivalence: "redex r ⟹ decompose e ℰ r = (ℰ[r] = e)"
proof (rule iffI)
assume x: "decompose e ℰ r"
show "ℰ[r] = e"
proof (use x in ‹induct rule: decompose.induct›)
case (top_redex e)
thus "□[e] = e" by simp
next
case (lapply e⇩1 e⇩2 ℰ r)
have "(ApplyL⇩ℰ ℰ e⇩2) [r] = Apply (ℰ[r]) e⇩2" by simp
also have "... = Apply e⇩1 e⇩2" using ‹ℰ[r] = e⇩1› by simp
then show ?case by simp
qed simp+
next
assume red: "redex r" and  eq: "ℰ[r] = e"
have "decompose (ℰ[r]) ℰ r" by (induct ℰ) (use red in ‹auto intro: decompose.intros›)
thus "decompose e ℰ r" by (simp add: eq)
qed

lemma unique_decomposition: "decompose e ℰ⇩1 r⇩1 ⟹ decompose e ℰ⇩2 r⇩2 ⟹ ℰ⇩1 = ℰ⇩2 ∧ r⇩1 = r⇩2"
by (induct arbitrary: ℰ⇩2 rule: decompose.induct) auto

lemma completion_eq [simp]:
assumes
red_e: "redex r" and
red_e': "redex r'"
shows "(ℰ[r] = ℰ'[r']) = (ℰ = ℰ' ∧ r = r')"
proof (rule iffI)
show "ℰ[r] = ℰ'[r'] ⟹ ℰ = ℰ' ∧ r = r'"
proof (rule conjI)
assume eq: "ℰ[r] = ℰ'[r']"
have "decompose (ℰ[r]) ℰ r" using plug_decomposition_equivalence red_e by blast
hence fst_decomp:"decompose (ℰ'[r']) ℰ r" by (simp add: eq)
have snd_decomp: "decompose (ℰ'[r']) ℰ' r'" using plug_decomposition_equivalence red_e' by blast
show cntxts_eq: "ℰ = ℰ'" using fst_decomp snd_decomp unique_decomposition by blast
show "r = r'" using cntxts_eq eq by simp
qed
qed simp

subsection ‹Stores and states›

type_synonym ('r,'l,'v) store = "'l ⇀ ('r,'l,'v) val"
type_synonym ('r,'l,'v) local_state = "('r,'l,'v) store × ('r,'l,'v) store × ('r,'l,'v) expr"
type_synonym ('r,'l,'v) global_state = "'r ⇀ ('r,'l,'v) local_state"

fun doms :: "('r,'l,'v) local_state ⇒ 'l set" where
"doms (σ,τ,e) = dom σ ∪ dom τ"

fun LID_snapshot :: "('r,'l,'v) local_state ⇒ ('r,'l,'v) store" ("_⇩σ" 200) where
"LID_snapshot (σ,τ,e) = σ"

fun LID_local_store :: "('r,'l,'v) local_state ⇒ ('r,'l,'v) store" ("_⇩τ" 200) where
"LID_local_store (σ,τ,e) = τ"

fun LID_expression :: "('r,'l,'v) local_state ⇒ ('r,'l,'v) expr" ("_⇩e" 200) where
"LID_expression (σ,τ,e) = e"

end


Theory Occurrences

section Occurrences

text ‹This theory contains all of the definitions and laws required for reasoning about
identifiers that occur in the data structures of the concurrent revisions model.›

theory Occurrences
imports Data
begin

subsection Definitions

subsubsection ‹Revision identifiers›

definition RID⇩S :: "('r,'l,'v) store ⇒ 'r set" where
"RID⇩S σ ≡ ⋃ (RID⇩V  ran σ)"

definition RID⇩L :: "('r,'l,'v) local_state ⇒ 'r set" where
"RID⇩L s ≡ case s of (σ, τ, e) ⇒ RID⇩S σ ∪ RID⇩S τ ∪ RID⇩E e"

definition RID⇩G :: "('r,'l,'v) global_state ⇒ 'r set" where
"RID⇩G s ≡ dom s ∪ ⋃ (RID⇩L  ran s)"

subsubsection ‹Location identifiers›

definition LID⇩S :: "('r,'l,'v) store ⇒ 'l set" where
"LID⇩S σ ≡ dom σ ∪ ⋃ (LID⇩V  ran σ)"

definition LID⇩L :: "('r,'l,'v) local_state ⇒ 'l set" where
"LID⇩L s ≡ case s of (σ, τ, e) ⇒ LID⇩S σ ∪ LID⇩S τ ∪ LID⇩E e"

definition LID⇩G :: "('r,'l,'v) global_state ⇒ 'l set" where
"LID⇩G s ≡ ⋃ (LID⇩L  ran s)"

subsection ‹Inference rules›

subsubsection ‹Introduction and elimination rules›

lemma RID⇩SI [intro]: "σ l = Some v ⟹ r ∈ RID⇩V v ⟹ r ∈ RID⇩S σ"
by (auto simp add: RID⇩S_def ran_def)

lemma RID⇩SE [elim]: "r ∈ RID⇩S σ ⟹ (⋀l v. σ l = Some v ⟹ r ∈ RID⇩V v ⟹ P) ⟹ P"
by (auto simp add: RID⇩S_def ran_def)

lemma RID⇩LI [intro, consumes 1]:
assumes "s = (σ, τ, e)"
shows
"r ∈ RID⇩S σ ⟹ r ∈ RID⇩L s"
"r ∈ RID⇩S τ ⟹ r ∈ RID⇩L s"
"r ∈ RID⇩E e ⟹ r ∈ RID⇩L s"
by (auto simp add: RID⇩L_def assms)

lemma RID⇩LE [elim]:
"⟦ r ∈ RID⇩L s; (⋀σ τ e. s = (σ, τ, e) ⟹ (r ∈ RID⇩S σ ⟹ P) ⟹ (r ∈ RID⇩S τ ⟹ P) ⟹ (r ∈ RID⇩E e ⟹ P) ⟹ P) ⟹ P ⟧ ⟹ P"
by (cases s) (auto simp add: RID⇩L_def)

lemma RID⇩GI [intro]:
"s r = Some v ⟹ r ∈ RID⇩G s"
"s r' = Some ls ⟹ r ∈ RID⇩L ls ⟹ r ∈ RID⇩G s"
by (metis (no_types, lifting) RID⇩G_def UN_I UnI2 ranI)

lemma RID⇩GE [elim]:
assumes
"r ∈ RID⇩G s"
"r ∈ dom s ⟹ P"
"⋀r' ls. s r' = Some ls ⟹ r ∈ RID⇩L ls ⟹ P"
shows P
using assms by (auto simp add: RID⇩G_def ran_def)

lemma LID⇩SI [intro]:
"σ l = Some v ⟹ l ∈ LID⇩S σ"
"σ l' = Some v ⟹ l ∈ LID⇩V v ⟹ l ∈ LID⇩S σ"
by (auto simp add: LID⇩S_def ran_def)

lemma LID⇩SE [elim]:
assumes
"l ∈ LID⇩S σ"
"l ∈ dom σ ⟹ P"
"⋀l' v. σ l' = Some v ⟹ l ∈ LID⇩V v ⟹ P"
shows P
using assms by (auto simp add: LID⇩S_def ran_def)

lemma LID⇩LI [intro]:
assumes "s = (σ, τ, e)"
shows
"r ∈ LID⇩S σ ⟹ r ∈ LID⇩L s"
"r ∈ LID⇩S τ ⟹ r ∈ LID⇩L s"
"r ∈ LID⇩E e ⟹ r ∈ LID⇩L s"
by (auto simp add: LID⇩L_def assms)

lemma LID⇩LE [elim]:
"⟦ l ∈ LID⇩L s; (⋀σ τ e. s = (σ, τ, e) ⟹ (l ∈ LID⇩S σ ⟹ P) ⟹ (l ∈ LID⇩S τ ⟹ P) ⟹ (l ∈ LID⇩E e ⟹ P) ⟹ P) ⟹ P ⟧ ⟹ P"
by (cases s) (auto simp add: LID⇩L_def)

lemma LID⇩GI [intro]: "s r = Some ls ⟹ l ∈ LID⇩L ls ⟹ l ∈ LID⇩G s"
by (auto simp add: LID⇩G_def LID⇩L_def ran_def)

lemma LID⇩GE [elim]: "l ∈ LID⇩G s ⟹ (⋀r ls. s r = Some ls ⟹ l ∈ LID⇩L ls ⟹ P) ⟹ P"
by (auto simp add: LID⇩G_def ran_def)

subsubsection ‹Distributive laws›

lemma ID_distr_completion [simp]:
"RID⇩E (ℰ[e]) = RID⇩C ℰ ∪ RID⇩E e"
"LID⇩E (ℰ[e]) = LID⇩C ℰ ∪ LID⇩E e"
by (induct rule: plug.induct) auto

lemma ID_restricted_store_subset_store:
"RID⇩S (σ(l := None)) ⊆ RID⇩S σ"
"LID⇩S (σ(l := None)) ⊆ LID⇩S σ"
proof -
show "RID⇩S (σ(l := None)) ⊆ RID⇩S σ"
proof (rule subsetI)
fix r
assume "r ∈ RID⇩S (σ(l := None))"
then obtain l' v where "(σ(l := None)) l' = Some v" and r_v: "r ∈ RID⇩V v" by blast
have "l' ≠ l" using ‹(σ(l := None)) l' = Some v› by auto
hence "σ l' = Some v" using ‹(σ(l := None)) l' = Some v› by auto
thus "r ∈ RID⇩S σ" using r_v by blast
qed
next
show "LID⇩S (σ(l := None)) ⊆ LID⇩S σ"
proof (rule subsetI)
fix l'
assume "l' ∈ LID⇩S (σ(l := None))"
hence "l' ∈ dom (σ(l := None)) ∨ (∃l'' v. (σ(l := None)) l'' = Some v ∧ l' ∈ LID⇩V v)" by blast
thus "l' ∈ LID⇩S σ"
proof (rule disjE)
assume "l' ∈ dom (σ(l := None))"
thus "l' ∈ LID⇩S σ" by auto
next
assume "∃l'' v. (σ(l := None)) l'' = Some v ∧ l' ∈ LID⇩V v"
then obtain l'' v where "(σ(l := None)) l'' = Some v" and l'_in_v: "l' ∈ LID⇩V v" by blast
hence "σ l'' = Some v" by (cases "l = l''", auto)
thus "l' ∈ LID⇩S σ" using l'_in_v by blast
qed
qed
qed

lemma in_restricted_store_in_unrestricted_store [intro]:
"r ∈ RID⇩S (σ(l := None)) ⟹ r ∈ RID⇩S σ"
"l' ∈ LID⇩S (σ(l := None)) ⟹ l' ∈ LID⇩S σ"
by (meson contra_subsetD ID_restricted_store_subset_store)+

lemma in_restricted_store_in_updated_store [intro]:
"r ∈ RID⇩S (σ(l := None)) ⟹ r ∈ RID⇩S (σ(l ↦ v))"
"l' ∈ LID⇩S (σ(l := None)) ⟹ l' ∈ LID⇩S (σ(l ↦ v))"
proof -
assume "r ∈ RID⇩S (σ(l := None))"
hence "r ∈ RID⇩S (σ | (- {l}))" by (simp add: restrict_complement_singleton_eq)
hence "r ∈ RID⇩S (σ(l ↦ v) | (- {l}))" by simp
hence "r ∈ RID⇩S (σ(l := Some v, l := None))" by (simp add: restrict_complement_singleton_eq)
thus "r ∈ RID⇩S (σ(l ↦ v))" by blast
next
assume "l' ∈ LID⇩S (σ(l := None))"
hence "l' ∈ LID⇩S (σ | (- {l}))" by (simp add: restrict_complement_singleton_eq)
hence "l' ∈ LID⇩S (σ(l ↦ v) | (- {l}))" by simp
hence "l' ∈ LID⇩S (σ(l := Some v, l := None))" by (simp add: restrict_complement_singleton_eq)
thus "l' ∈ LID⇩S (σ(l ↦ v))" by blast
qed

lemma ID_distr_store [simp]:
"RID⇩S (τ(l ↦ v)) = RID⇩S (τ(l := None)) ∪ RID⇩V v"
"LID⇩S (τ(l ↦ v)) = insert l (LID⇩S (τ(l := None)) ∪ LID⇩V v)"
proof -
show "RID⇩S (τ(l ↦ v)) = RID⇩S (τ(l := None)) ∪ RID⇩V v"
proof (rule set_eqI, rule iffI)
fix r
assume "r ∈ RID⇩S (τ(l ↦ v))"
then obtain l' v' where "(τ(l ↦ v)) l' = Some v'" "r ∈ RID⇩V v'" by blast
thus "r ∈ RID⇩S (τ(l := None)) ∪ RID⇩V v" by (cases "l' = l") auto
qed auto
next
show "LID⇩S (τ(l ↦ v)) = insert l (LID⇩S (τ(l := None)) ∪ LID⇩V v)"
proof (rule set_eqI, rule iffI)
fix l'
assume "l' ∈ LID⇩S (τ(l ↦ v))"
hence "l' ∈ dom (τ(l ↦ v)) ∨ (∃l'' v'. (τ(l ↦ v)) l'' = Some v' ∧ l' ∈ LID⇩V v')" by blast
thus "l' ∈ insert l (LID⇩S (τ(l := None)) ∪ LID⇩V v)"
proof (rule disjE)
assume "l' ∈ dom (τ(l ↦ v))"
thus "l' ∈ insert l (LID⇩S (τ(l := None)) ∪ LID⇩V v)" by (cases "l' = l") auto
next
assume "∃l'' v'. (τ(l ↦ v)) l'' = Some v' ∧ l' ∈ LID⇩V v'"
then obtain l'' v' where "(τ(l ↦ v)) l'' = Some v'" "l' ∈ LID⇩V v'" by blast
thus "l' ∈ insert l (LID⇩S (τ(l := None)) ∪ LID⇩V v)" by (cases "l = l''") auto
qed
qed auto
qed

lemma ID_distr_local [simp]:
"LID⇩L (σ,τ,e) = LID⇩S σ ∪ LID⇩S τ ∪ LID⇩E e"
"RID⇩L (σ,τ,e) = RID⇩S σ ∪ RID⇩S τ ∪ RID⇩E e"

lemma ID_restricted_global_subset_unrestricted:
"LID⇩G (s(r := None)) ⊆ LID⇩G s"
"RID⇩G (s(r := None)) ⊆ RID⇩G s"
proof -
show "LID⇩G (s(r := None)) ⊆ LID⇩G s"
proof (rule subsetI)
fix l
assume "l ∈ LID⇩G (s(r := None))"
then obtain r'' ls where "(s(r := None)) r'' = Some ls" and l_in_ls: "l ∈ LID⇩L ls" by blast
have "r'' ≠ r " using ‹(s(r := None)) r'' = Some ls› by auto
hence "s r'' = Some ls" using ‹(s(r := None)) r'' = Some ls› by auto
thus "l ∈ LID⇩G s" using l_in_ls by blast
qed
next
show "RID⇩G (s(r := None)) ⊆ RID⇩G s"
proof (rule subsetI)
fix r'
assume "r' ∈ RID⇩G (s(r := None))"
hence "r' ∈ dom (s(r := None)) ∨ (∃r'' ls. (s(r := None)) r'' = Some ls ∧ r' ∈ RID⇩L ls)" by blast
thus "r' ∈ RID⇩G s"
proof (rule disjE)
assume "∃r'' ls. (s(r := None)) r'' = Some ls ∧ r' ∈ RID⇩L ls"
then obtain r'' ls where "(s(r := None)) r'' = Some ls" and r'_in_ls: "r' ∈ RID⇩L ls" by blast
have neq: "r'' ≠ r" using ‹(s(r := None)) r'' = Some ls› by auto
hence "s r'' = Some ls" using ‹(s(r := None)) r'' = Some ls› by auto
thus "r' ∈ RID⇩G s" using r'_in_ls by blast
qed auto
qed
qed

lemma in_restricted_global_in_unrestricted_global [intro]:
"r' ∈ RID⇩G (s(r := None)) ⟹ r' ∈ RID⇩G s"
"l ∈ LID⇩G (s(r := None)) ⟹ l ∈ LID⇩G s"

lemma in_restricted_global_in_updated_global [intro]:
"r' ∈ RID⇩G (s(r := None)) ⟹ r' ∈ RID⇩G (s(r ↦ ls))"
"l ∈ LID⇩G (s(r := None)) ⟹ l ∈ LID⇩G (s(r ↦ ls))"
proof -
assume "r' ∈ RID⇩G (s(r := None))"
hence "r' ∈ RID⇩G (s | (- {r}))" by (simp add: restrict_complement_singleton_eq)
hence "r' ∈ RID⇩G (s(r ↦ ls) | (- {r}))" by simp
hence "r' ∈ RID⇩G (s(r := Some ls, r := None))" by (simp add: restrict_complement_singleton_eq)
thus "r' ∈ RID⇩G (s(r ↦ ls))" by blast
next
assume "l ∈ LID⇩G (s(r := None))"
hence "l ∈ LID⇩G (s | (- {r}))" by (simp add: restrict_complement_singleton_eq)
hence "l ∈ LID⇩G (s(r ↦ ls) | (- {r}))" by simp
hence "l ∈ LID⇩G (s(r := Some ls, r := None))" by (simp add: restrict_complement_singleton_eq)
thus "l ∈ LID⇩G (s(r ↦ ls))" by blast
qed

lemma ID_distr_global [simp]:
"RID⇩G (s(r ↦ ls)) = insert r (RID⇩G (s(r := None)) ∪ RID⇩L ls)"
"LID⇩G (s(r ↦ ls)) = LID⇩G (s(r := None)) ∪ LID⇩L ls"
proof -
show "LID⇩G (s(r ↦ ls)) = LID⇩G (s(r := None)) ∪ LID⇩L ls"
proof (rule set_eqI)
fix l
show "(l ∈ LID⇩G (s(r ↦ ls))) = (l ∈ LID⇩G (s(r := None)) ∪ LID⇩L ls)"
proof (rule iffI)
assume "l ∈ LID⇩G (s(r ↦ ls))"
from this obtain r' ls' where "(s(r ↦ ls)) r' = Some ls'" "l ∈ LID⇩L ls'" by auto
thus "l ∈ LID⇩G (s(r := None)) ∪ LID⇩L ls" by (cases "r = r'") auto
qed auto
qed
show "RID⇩G (s(r ↦ ls)) = insert r (RID⇩G (s(r := None)) ∪ RID⇩L ls)"
proof (rule set_eqI)
fix r'
show "(r' ∈ RID⇩G (s(r ↦ ls))) = (r' ∈ insert r (RID⇩G (s(r := None)) ∪ RID⇩L ls))"
proof (rule iffI, clarsimp)
assume r'_g: "r' ∈ RID⇩G (s(r ↦ ls))" and neq: "r' ≠ r" and r'_l: "r' ∉ RID⇩L ls"
show "r' ∈ RID⇩G (s(r := None))"
proof (rule RID⇩GE[OF r'_g])
assume "r' ∈ dom (s(r ↦ ls))"
thus ?thesis by (simp add: RID⇩G_def neq)
next
fix ls' r''
assume r'_in_range:"(s(r ↦ ls)) r'' = Some ls'" "r' ∈ RID⇩L ls'"
thus ?thesis by (cases "r'' = r") (use neq r'_l in auto)
qed
qed auto
qed
qed

lemma restrictions_inwards [simp]:
"x ≠ x' ⟹ f(x := Some y, x' := None) = (f(x':= None, x := Some y))"
by (rule fun_upd_twist)

subsubsection ‹Miscellaneous laws›

lemma ID_combination_subset_union [intro]:
"RID⇩S (σ;;τ) ⊆ RID⇩S σ ∪ RID⇩S τ"
"LID⇩S (σ;;τ) ⊆ LID⇩S σ ∪ LID⇩S τ"
proof -
show "RID⇩S (σ;;τ) ⊆ RID⇩S σ ∪ RID⇩S τ"
proof (rule subsetI)
fix r
assume "r ∈ RID⇩S (σ;;τ)"
from this obtain l v where "(σ;;τ) l = Some v" and "r ∈ RID⇩V v" by blast
thus "r ∈ RID⇩S σ ∪ RID⇩S τ" by (cases "l ∈ dom τ") auto
qed
show "LID⇩S (σ;;τ) ⊆ LID⇩S σ ∪ LID⇩S τ"
proof (rule subsetI)
fix l
assume "l ∈ LID⇩S (σ;;τ)"
hence "l ∈ dom (σ;;τ) ∨ (∃l' v. (σ;;τ) l' = Some v ∧ l ∈ LID⇩V v)" by blast
thus "l ∈ LID⇩S σ ∪ LID⇩S τ"
proof (rule disjE)
assume "l ∈ dom (σ;;τ)"
thus "l ∈ LID⇩S σ ∪ LID⇩S τ" by (cases "l ∈ dom τ") auto
next
assume "∃l' v. (σ;;τ) l' = Some v ∧ l ∈ LID⇩V v"
from this obtain l' v where "(σ;;τ) l' = Some v" "l ∈ LID⇩V v" by blast
thus "l ∈ LID⇩S σ ∪ LID⇩S τ" by (cases "l' ∈ dom τ") auto
qed
qed
qed

lemma in_combination_in_component [intro]:
"r ∈ RID⇩S (σ;;τ) ⟹ r ∉ RID⇩S σ ⟹ r ∈ RID⇩S τ"
"r ∈ RID⇩S (σ;;τ) ⟹ r ∉ RID⇩S τ ⟹ r ∈ RID⇩S σ"
"l ∈ LID⇩S (σ;;τ) ⟹ l ∉ LID⇩S σ ⟹ l ∈ LID⇩S τ"
"l ∈ LID⇩S (σ;;τ) ⟹ l ∉ LID⇩S τ ⟹ l ∈ LID⇩S σ"
by (meson Un_iff ID_combination_subset_union subsetCE)+

lemma in_mapped_in_component_of_combination [intro]:
assumes
maps_to_v: "(σ;;τ) l = Some v" and
l'_in_v: "l' ∈ LID⇩V v"
shows
"l' ∉ LID⇩S τ ⟹ l' ∈ LID⇩S σ"
"l' ∉ LID⇩S σ ⟹ l' ∈ LID⇩S τ"
by (metis LID⇩SI(2) combine.simps l'_in_v maps_to_v)+

lemma elim_trivial_restriction [simp]: "l ∉ LID⇩S τ ⟹ (τ(l := None)) = τ"
by (simp add: LID⇩S_def domIff fun_upd_idem)

lemma ID_distr_global_conditional:
"s r = Some ls ⟹ RID⇩G s = insert r (RID⇩G (s(r := None)) ∪ RID⇩L ls)"
"s r = Some ls ⟹ LID⇩G s = LID⇩G (s(r := None)) ∪ LID⇩L ls"
proof -
assume "s r = Some ls"
hence s_as_upd: "s = (s(r ↦ ls))" by (simp add: fun_upd_idem)
show "RID⇩G s = insert r (RID⇩G (s(r := None)) ∪ RID⇩L ls)" by (subst s_as_upd, simp)
show "LID⇩G s = LID⇩G (s(r := None)) ∪ LID⇩L ls" by (subst s_as_upd, simp)
qed

end


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


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

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


Theory OperationalSemantics

section ‹Operational Semantics›

text ‹This theory defines the operational semantics of the concurrent revisions model. It also
introduces a relaxed formulation of the operational semantics, and proves the main result required
for establishing their equivalence.›

theory OperationalSemantics
imports Substitution
begin

context substitution
begin

subsection Definition

inductive revision_step :: "'r ⇒ ('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" where
app: "s r = Some (σ, τ, ℰ[Apply (VE (Lambda x e)) (VE v)]) ⟹ revision_step r s (s(r ↦ (σ, τ, ℰ[subst (VE v) x e])))"
| ifTrue: "s r = Some (σ, τ, ℰ[Ite (VE (CV T)) e1 e2]) ⟹ revision_step r s (s(r ↦ (σ, τ, ℰ[e1])))"
| ifFalse: "s r = Some (σ, τ, ℰ[Ite (VE (CV F)) e1 e2]) ⟹ revision_step r s (s(r ↦ (σ, τ, ℰ[e2])))"
(* store operations *)
| new: "s r = Some (σ, τ, ℰ[Ref (VE v)]) ⟹ l ∉ LID⇩G s ⟹ revision_step r s (s(r ↦ (σ, τ(l ↦ v), ℰ[VE (Loc l)])))"
| get: "s r = Some (σ, τ, ℰ[Read (VE (Loc l))]) ⟹ l ∈ dom (σ;;τ) ⟹ revision_step r s (s(r ↦ (σ, τ, ℰ[VE (the ((σ;;τ) l))])))"
| set: "s r = Some (σ, τ, ℰ[Assign (VE (Loc l)) (VE v)]) ⟹ l ∈ dom (σ;;τ) ⟹ revision_step r s (s(r ↦ (σ, τ(l ↦ v), ℰ[VE (CV Unit)])))"
(* synchronization operations *)
| fork: "s r = Some (σ, τ, ℰ[Rfork e]) ⟹ r' ∉ RID⇩G s ⟹ revision_step r s (s(r ↦ (σ, τ, ℰ[VE (Rid r')]), r' ↦ (σ;;τ, ε, e)))"
| join: "s r = Some (σ, τ, ℰ[Rjoin (VE (Rid r'))]) ⟹ s r' = Some (σ', τ', VE v) ⟹ revision_step r s (s(r := Some (σ, (τ;;τ'), ℰ[VE (CV Unit)]), r' := None))"
| join⇩ε: "s r = Some (σ, τ, ℰ[Rjoin (VE (Rid r'))]) ⟹ s r' = None ⟹ revision_step r s ε"

inductive_cases revision_stepE [elim, consumes 1, case_names app ifTrue ifFalse new get set fork join join⇩ε]:
"revision_step r s s'"

subsection ‹Introduction lemmas for identifiers›

lemma only_new_introduces_lids [intro, dest]:
assumes
step: "revision_step r s s'" and
not_new: "⋀σ τ ℰ v. s r ≠ Some (σ,τ,ℰ[Ref (VE v)])"
shows "LID⇩G s' ⊆ LID⇩G s"
proof (use step in ‹cases rule: revision_stepE›)
case fork
thus ?thesis by (auto simp add: fun_upd_twist ID_distr_global_conditional)
next
case (join _ _ _ r' _ _ _)
hence "r ≠ r'" by auto
thus ?thesis using join by (auto simp add: fun_upd_twist dest!: in_combination_in_component)
qed (auto simp add: not_new fun_upd_twist ID_distr_global_conditional dest: LID⇩SI(2))

lemma only_fork_introduces_rids [intro, dest]:
assumes
step: "revision_step r s s'" and
not_fork: "⋀σ τ ℰ e. s r ≠ Some (σ,τ,ℰ[Rfork e])"
shows "RID⇩G s' ⊆ RID⇩G s"
proof (use step in ‹cases rule: revision_stepE›)
next
case get
then show ?thesis by (auto simp add: ID_distr_global_conditional)
next
case fork
then show ?thesis by (simp add: not_fork)
next
case (join _ _ _r' _ _ _)
hence "r ≠ r'" by auto
then show ?thesis using join by (auto simp add: fun_upd_twist dest!: in_combination_in_component)

lemma only_fork_introduces_rids' [dest]:
assumes
step: "revision_step r s s'" and
not_fork: "⋀σ τ ℰ e. s r ≠ Some (σ,τ,ℰ[Rfork e])"
shows "r' ∉ RID⇩G s ⟹ r' ∉ RID⇩G s'"
using assms by blast

lemma only_new_introduces_lids' [dest]:
assumes
step: "revision_step r s s'" and
not_new: "⋀σ τ ℰ v. s r ≠ Some (σ,τ,ℰ[Ref (VE v)])"
shows "l ∉ LID⇩G s ⟹ l ∉ LID⇩G s'"
using assms by blast

subsection ‹Domain subsumption›

subsubsection Definitions

definition domains_subsume :: "('r,'l,'v) local_state ⇒ bool" ("𝒮") where
"𝒮 ls = (LID⇩L ls ⊆ doms ls)"

definition domains_subsume_globally :: "('r,'l,'v) global_state ⇒ bool" ("𝒮⇩G") where
"𝒮⇩G s = (∀r ls. s r = Some ls ⟶ 𝒮 ls)"

lemma domains_subsume_globallyI [intro]:
"(⋀r σ τ e. s r = Some (σ,τ,e) ⟹ 𝒮 (σ,τ,e)) ⟹ domains_subsume_globally s"
using domains_subsume_globally_def by auto

definition subsumes_accessible :: "'r ⇒ 'r ⇒ ('r,'l,'v) global_state ⇒ bool" ("𝒜") where
"𝒜 r⇩1 r⇩2 s = (r⇩2 ∈ RID⇩L (the (s r⇩1)) ⟶ (LID⇩S ((the (s r⇩2))⇩σ) ⊆ doms (the (s r⇩1))))"

lemma subsumes_accessibleI [intro]:
"(r⇩2 ∈ RID⇩L (the (s r⇩1)) ⟹ LID⇩S ((the (s r⇩2))⇩σ) ⊆ doms (the (s r⇩1))) ⟹ 𝒜 r⇩1 r⇩2 s"
using subsumes_accessible_def by auto

definition subsumes_accessible_globally :: "('r,'l,'v) global_state ⇒ bool" ("𝒜⇩G") where
"𝒜⇩G s = (∀r⇩1 r⇩2. r⇩1 ∈ dom s ⟶ r⇩2 ∈ dom s ⟶ 𝒜 r⇩1 r⇩2 s)"

lemma subsumes_accessible_globallyI [intro]:
"(⋀r⇩1 σ⇩1 τ⇩1 e⇩1 r⇩2 σ⇩2 τ⇩2 e⇩2. s r⇩1 = Some (σ⇩1,τ⇩1,e⇩1) ⟹ s r⇩2 = Some (σ⇩2,τ⇩2,e⇩2) ⟹ 𝒜 r⇩1 r⇩2 s) ⟹ 𝒜⇩G s"
using subsumes_accessible_globally_def by auto

subsubsection ‹The theorem›

lemma 𝒮⇩G_imp_𝒜_refl:
assumes
𝒮⇩G_s: "𝒮⇩G s" and
r_in_dom: "r ∈ dom s"
shows "𝒜 r r s"
using assms by (auto simp add: domains_subsume_def domains_subsume_globally_def subsumes_accessibleI)

lemma step_preserves_𝒮⇩G_and_𝒜⇩G:
assumes
step: "revision_step r s s'" and
𝒮⇩G_s: "𝒮⇩G s" and
𝒜⇩G_s: "𝒜⇩G s"
shows "𝒮⇩G s'" "𝒜⇩G s'"
proof -
show "𝒮⇩G s'"
proof (rule domains_subsume_globallyI)
fix r' σ τ e
assume s'_r: "s' r' = Some (σ,τ,e)"
show "𝒮 (σ,τ,e)"
proof (cases "s' r' = s r'")
case True
then show ?thesis using 𝒮⇩G_s domains_subsume_globally_def s'_r by auto
next
case r'_was_updated: False
show ?thesis
proof (use step in ‹cases rule: revision_stepE›)
case (app σ' τ' ℰ' _ e' v')
have "r = r'" by (metis fun_upd_apply app(1) r'_was_updated)
have "LID⇩L (the (s' r)) ⊆ LID⇩S σ' ∪ LID⇩S τ' ∪ LID⇩C ℰ' ∪ LID⇩E e' ∪ LID⇩V v'" using app(1) by auto
also have "... = LID⇩L (the (s r))" using app(2) by auto
also have "... ⊆ doms (the (s r))"
by (metis 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def local.app(2) option.sel)
also have "... = doms (the (s' r))" using app by simp
finally have "𝒮 (the (s' r))" by (simp add: domains_subsume_def)
thus ?thesis by (simp add: ‹r = r'› s'_r)
next
case ifTrue
have "r = r'" by (metis fun_upd_apply ifTrue(1) r'_was_updated)
have "LID⇩L (the (s' r)) ⊆ LID⇩L (the (s r))" using ifTrue by auto
also have "... ⊆ doms (the (s r))"
by (metis 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def ifTrue(2) option.sel)
also have "... = doms (the (s' r))" by (simp add: ifTrue)
finally have "𝒮 (the (s' r))" by (simp add: domains_subsume_def)
thus ?thesis by (simp add: ‹r = r'› s'_r)
next
case ifFalse
have "r = r'" by (metis fun_upd_apply ifFalse(1) r'_was_updated)
have "LID⇩L (the (s' r)) ⊆ LID⇩L (the (s r))" using ifFalse by auto
also have "... ⊆ doms (the (s r))"
by (metis 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def ifFalse(2) option.sel)
also have "... = doms (the (s' r))" by (simp add: ifFalse)
finally have "𝒮 (the (s' r))" by (simp add: domains_subsume_def)
thus ?thesis by (simp add: ‹r = r'› s'_r)
next
case (new σ' τ' ℰ' v' l')
have "r = r'" by (metis fun_upd_apply new(1) r'_was_updated)
have "LID⇩L (the (s' r)) = insert l' (LID⇩S σ' ∪ LID⇩S τ' ∪ LID⇩V v' ∪ LID⇩C ℰ')"
proof -
have "l' ∉ LID⇩S τ'" using new(2-3) by auto
thus ?thesis using new(1) by auto
qed
also have "... = insert l' (LID⇩L (the (s r)))" using new by auto
also have "... ⊆ insert l' (doms (the (s r)))"
by (metis 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def insert_mono new(2) option.sel)
also have "... = doms (the (s' r))" using new by auto
finally have "𝒮 (the (s' r))" by (simp add: domains_subsume_def)
thus ?thesis by (simp add: ‹r = r'› s'_r)
next
case get
have "r = r'" by (metis fun_upd_apply get(1) r'_was_updated)
have "LID⇩L (the (s' r)) = LID⇩L (the (s r))" using get by auto
also have "... ⊆ doms (the (s r))"
by (metis 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def get(2) option.sel)
also have "... = doms (the (s' r))" by (simp add: get(1-2))
finally have "𝒮 (the (s' r))" by (simp add: domains_subsume_def)
thus ?thesis by (simp add: ‹r = r'› s'_r)
next
case set
have "r = r'" by (metis fun_upd_apply set(1) r'_was_updated)
have "LID⇩L (the (s' r)) ⊆ LID⇩L (the (s r))" using set(1-2) by auto
also have "... ⊆ doms (the (s r))"
by (metis 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def set(2) option.sel)
also have "... ⊆ doms (the (s' r))" using set(1-2) by auto
finally have "𝒮 (the (s' r))" by (simp add: domains_subsume_def)
thus ?thesis by (simp add: ‹r = r'› s'_r)
next
case (fork σ' τ' _ _ r'')
have "r = r' ∨ r'' = r'" using fork r'_was_updated by auto
then show ?thesis
proof (rule disjE)
assume "r = r'"
have "LID⇩L (the (s' r)) ⊆ LID⇩L (the (s r))" using fork(1-2) by auto
also have "... ⊆ doms (the (s r))"
by (metis 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def fork(2) option.sel)
also have "... = doms (the (s' r))" using fork by auto
finally have "𝒮 (the (s' r))" by (simp add: domains_subsume_def)
thus ?thesis by (simp add: ‹r = r'› s'_r)
next
assume "r'' = r'"
have "LID⇩L (the (s' r'')) ⊆ LID⇩L (the (s r))" using fork(1-2) by auto
also have "... ⊆ doms (the (s r))"
by (metis 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def fork(2) option.sel)
also have "... = dom σ' ∪ dom τ'" using fork by simp
also have "... = dom (σ';;τ')"  by (simp add: dom_combination_dom_union)
also have "... = doms (the (s' r''))" using fork by simp
finally have "𝒮 (the (s' r''))" by (simp add: domains_subsume_def)
thus ?thesis by (simp add: ‹r'' = r'› s'_r)
qed
next
case (join σ' τ' _ r'' σ'' τ'' _)
have "r' = r" by (metis fun_upd_def join(1) option.simps(3) r'_was_updated s'_r)
have "LID⇩L (the (s' r)) ⊆ LID⇩L (the (s r)) ∪ LID⇩S τ''" using join by auto
also have "... ⊆ doms (the (s r)) ∪ LID⇩S τ''"
by (metis Un_mono 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def join(2) option.sel subset_refl)
also have "... ⊆ doms (the (s r)) ∪ LID⇩L (the (s r''))" using join(3) by auto
also have "... ⊆ doms (the (s r)) ∪ doms (the (s r''))"
by (metis (no_types, lifting) Un_absorb 𝒮⇩G_s domains_subsume_def domains_subsume_globally_def join(3) option.sel sup.orderI sup_mono)
also have "... = dom σ' ∪ dom τ' ∪ dom σ'' ∪ dom τ''" using join by auto
also have "... ⊆ dom σ' ∪ dom τ' ∪ LID⇩S σ'' ∪ dom τ''" by auto
also have "... ⊆ dom σ' ∪ dom τ' ∪ dom σ' ∪ dom τ' ∪ dom τ''"
proof -
have r_r'': "𝒜 r r'' s" using 𝒜⇩G_s join(2-3) subsumes_accessible_globally_def by auto
have r_accesses_r'': "r'' ∈ RID⇩L (the (s r))" using join by auto
have "LID⇩S σ'' ⊆ dom σ' ∪ dom τ'" using join subsumes_accessible_def r_r'' r_accesses_r'' by auto
thus ?thesis by auto
qed
also have "... = dom σ' ∪ dom τ' ∪ dom τ''" by auto
also have "... = dom σ' ∪ dom (τ';;τ'')" by (auto simp add: dom_combination_dom_union)
also have "... = doms (the (s' r))" using join by auto
finally have "𝒮 (the (s' r))" by (simp add: domains_subsume_def)
thus ?thesis using ‹r' = r› s'_r by auto
next
case join⇩ε
then show ?thesis using s'_r by blast
qed
qed
qed
show "𝒜⇩G s'"
proof (rule subsumes_accessible_globallyI)
fix r⇩1 σ⇩1 τ⇩1 e⇩1 r⇩2 σ⇩2 τ⇩2 e⇩2
assume
s'_r⇩1: "s' r⇩1 = Some (σ⇩1, τ⇩1, e⇩1)" and
s'_r⇩2: "s' r⇩2 = Some (σ⇩2, τ⇩2, e⇩2)"
show "𝒜 r⇩1 r⇩2 s'"
proof (cases "r⇩1 = r⇩2")
case True
then show ?thesis using 𝒮⇩G_imp_𝒜_refl ‹𝒮⇩G s'› s'_r⇩1 by blast
next
case r⇩1_neq_r⇩2: False
have r⇩1_nor_r⇩2_updated_implies_thesis: "s' r⇩1 = s r⇩1 ⟹ s' r⇩2 = s r⇩2 ⟹ ?thesis"
proof -
assume r⇩1_unchanged: "s' r⇩1 = s r⇩1" and r⇩2_unchanged: "s' r⇩2 = s r⇩2"
have "𝒜 r⇩1 r⇩2 s"
by (metis 𝒜⇩G_s domIff option.discI r⇩1_unchanged r⇩2_unchanged s'_r⇩1 s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩1_unchanged r⇩2_unchanged subsumes_accessible_def by auto
qed
have r⇩1_or_r⇩2_updated_implies_thesis: "s' r⇩1 ≠ s r⇩1 ∨ s' r⇩2 ≠ s r⇩2 ⟹ ?thesis"
proof -
assume r⇩1_or_r⇩2_updated: "s' r⇩1 ≠ s r⇩1 ∨ s' r⇩2 ≠ s r⇩2"
show ?thesis
proof (use step in ‹cases rule: revision_stepE›)
case app
have "r⇩1 = r ∨ r⇩2 = r" by (metis fun_upd_other app(1) r⇩1_or_r⇩2_updated)
then show ?thesis
proof (rule disjE)
assume r⇩1_eq_r: "r⇩1 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S ((the (s' r⇩2))⇩σ) ⊆ LID⇩S ((the (s r⇩2))⇩σ)" using app by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using app r⇩2_in_s'_r⇩1 r⇩1_eq_r by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis 𝒜⇩G_s domI fun_upd_other app r⇩1_eq_r s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" using app by auto
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
next
assume r⇩2_eq_r: "r⇩2 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S (the (s' r⇩2)⇩σ) = LID⇩S (the (s r⇩2)⇩σ)" using app by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using app(1) r⇩1_neq_r⇩2 r⇩2_eq_r r⇩2_in_s'_r⇩1 by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis (no_types, lifting) 𝒜⇩G_s domIff fun_upd_other app option.discI r⇩2_eq_r s'_r⇩1 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" by (simp add: app)
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
qed
next
case ifTrue
have "r⇩1 = r ∨ r⇩2 = r" by (metis fun_upd_other ifTrue(1) r⇩1_or_r⇩2_updated)
then show ?thesis
proof (rule disjE)
assume r⇩1_eq_r: "r⇩1 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S ((the (s' r⇩2))⇩σ) ⊆ LID⇩S ((the (s r⇩2))⇩σ)" using ifTrue by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using ifTrue r⇩2_in_s'_r⇩1 r⇩1_eq_r by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis 𝒜⇩G_s domI fun_upd_other ifTrue r⇩1_eq_r s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" using ifTrue by auto
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
next
assume r⇩2_eq_r: "r⇩2 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S (the (s' r⇩2)⇩σ) = LID⇩S (the (s r⇩2)⇩σ)" using ifTrue by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using ifTrue(1) r⇩1_neq_r⇩2 r⇩2_eq_r r⇩2_in_s'_r⇩1 by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis (no_types, lifting) 𝒜⇩G_s domIff fun_upd_other ifTrue option.discI r⇩2_eq_r s'_r⇩1 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" by (simp add: ifTrue)
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
qed
next
case ifFalse
have "r⇩1 = r ∨ r⇩2 = r" by (metis fun_upd_other ifFalse(1) r⇩1_or_r⇩2_updated)
then show ?thesis
proof (rule disjE)
assume r⇩1_eq_r: "r⇩1 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S ((the (s' r⇩2))⇩σ) ⊆ LID⇩S ((the (s r⇩2))⇩σ)" using ifFalse by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using ifFalse r⇩2_in_s'_r⇩1 r⇩1_eq_r by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis 𝒜⇩G_s domI fun_upd_other ifFalse r⇩1_eq_r s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" using ifFalse by auto
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
next
assume r⇩2_eq_r: "r⇩2 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S (the (s' r⇩2)⇩σ) = LID⇩S (the (s r⇩2)⇩σ)" using ifFalse by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using ifFalse(1) r⇩1_neq_r⇩2 r⇩2_eq_r r⇩2_in_s'_r⇩1 by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis (no_types, lifting) 𝒜⇩G_s domIff fun_upd_other ifFalse option.discI r⇩2_eq_r s'_r⇩1 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" by (simp add: ifFalse)
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
qed
next
case new
have "r⇩1 = r ∨ r⇩2 = r" by (metis fun_upd_other new(1) r⇩1_or_r⇩2_updated)
then show ?thesis
proof (rule disjE)
assume r⇩1_eq_r: "r⇩1 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S ((the (s' r⇩2))⇩σ) ⊆ LID⇩S ((the (s r⇩2))⇩σ)" using new by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using new r⇩2_in_s'_r⇩1 r⇩1_eq_r by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis 𝒜⇩G_s domI fun_upd_other new(1-2) r⇩1_eq_r s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" using new by auto
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
next
assume r⇩2_eq_r: "r⇩2 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S (the (s' r⇩2)⇩σ) = LID⇩S (the (s r⇩2)⇩σ)" using new by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using new(1) r⇩1_neq_r⇩2 r⇩2_eq_r r⇩2_in_s'_r⇩1 by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis (no_types, lifting) 𝒜⇩G_s domIff fun_upd_other new(1-2) option.discI r⇩2_eq_r s'_r⇩1 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" by (auto simp add: new)
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
qed
next
case get
have "r⇩1 = r ∨ r⇩2 = r" by (metis fun_upd_other get(1) r⇩1_or_r⇩2_updated)
then show ?thesis
proof (rule disjE)
assume r⇩1_eq_r: "r⇩1 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S ((the (s' r⇩2))⇩σ) ⊆ LID⇩S ((the (s r⇩2))⇩σ)" using get by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using get r⇩2_in_s'_r⇩1 r⇩1_eq_r apply auto
by (meson RID⇩SI) (* by (auto 1 3) *)
have "𝒜 r⇩1 r⇩2 s"
by (metis 𝒜⇩G_s domI fun_upd_other get(1-2) r⇩1_eq_r s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" using get by auto
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
next
assume r⇩2_eq_r: "r⇩2 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S (the (s' r⇩2)⇩σ) = LID⇩S (the (s r⇩2)⇩σ)" using get by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using get(1) r⇩1_neq_r⇩2 r⇩2_eq_r r⇩2_in_s'_r⇩1 by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis (no_types, lifting) 𝒜⇩G_s domIff fun_upd_other get(1-2) option.discI r⇩2_eq_r s'_r⇩1 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" by (simp add: get)
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
qed
next
case set
have "r⇩1 = r ∨ r⇩2 = r" by (metis fun_upd_other set(1) r⇩1_or_r⇩2_updated)
then show ?thesis
proof (rule disjE)
assume r⇩1_eq_r: "r⇩1 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S ((the (s' r⇩2))⇩σ) ⊆ LID⇩S ((the (s r⇩2))⇩σ)" using set by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using set r⇩2_in_s'_r⇩1 r⇩1_eq_r by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis 𝒜⇩G_s domI fun_upd_other set(1-2) r⇩1_eq_r s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" using set by auto
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
next
assume r⇩2_eq_r: "r⇩2 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S (the (s' r⇩2)⇩σ) = LID⇩S (the (s r⇩2)⇩σ)" using set by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using set(1) r⇩1_neq_r⇩2 r⇩2_eq_r r⇩2_in_s'_r⇩1 by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis (no_types, lifting) 𝒜⇩G_s domIff fun_upd_other set(1-2) option.discI r⇩2_eq_r s'_r⇩1 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" by (auto simp add: set)
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
qed
next
case (fork σ τ ℰ e r')
have s'_r: "s' r = Some (σ, τ, ℰ [VE (Rid r')])" using fork by auto
have s'_r': "s' r' = Some (σ;;τ, ε, e)"
have case1: "r⇩1 = r ⟹ r⇩2 ≠ r ⟹ r⇩2 ≠ r' ⟹ ?thesis"
proof (rule subsumes_accessibleI)
assume "r⇩1 = r" "r⇩2 ≠ r" "r⇩2 ≠ r'"
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S ((the (s' r⇩2))⇩σ) ⊆ LID⇩S ((the (s r⇩2))⇩σ)" using fork(1-2) by (simp add: ‹r⇩2 ≠ r'›)
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using fork ‹r⇩1 = r› ‹r⇩2 ≠ r'› r⇩2_in_s'_r⇩1 s'_r by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis (no_types, lifting) 𝒜⇩G_s ‹r⇩1 = r› ‹r⇩2 ≠ r'› domIff fun_upd_other fork(1-2) option.discI s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))" by (simp add: ‹r⇩1 = r› fork(2) s'_r)
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
have case2: "r⇩1 ≠ r ⟹ r⇩1 ≠ r' ⟹ r⇩2 = r ⟹ ?thesis"
proof (rule subsumes_accessibleI)
assume "r⇩1 ≠ r" "r⇩1 ≠ r'" "r⇩2 = r"
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S ((the (s' r⇩2))⇩σ) ⊆ LID⇩S ((the (s r⇩2))⇩σ)"
using ‹r⇩1 ≠ r'› ‹r⇩1 ≠ r› fork r⇩2_in_s'_r⇩1 s'_r⇩1 by auto
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))" using ‹r⇩1 ≠ r'› ‹r⇩1 ≠ r› fork(1) r⇩2_in_s'_r⇩1 by auto
have "𝒜 r⇩1 r⇩2 s"
by (metis (no_types, lifting) 𝒜⇩G_s ‹r⇩1 ≠ r'› ‹r⇩2 = r› domIff fun_upd_other fork(1-2) option.discI s'_r⇩1 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by auto
qed
also have "... ⊆ doms (the (s' r⇩1))" by (simp add: ‹r⇩1 ≠ r'› ‹r⇩1 ≠ r› fork(1))
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
have case3: "r⇩1 = r' ⟹ r⇩2 ≠ r ⟹ r⇩2 ≠ r' ⟹ ?thesis"
proof (rule subsumes_accessibleI)
fix l
assume "r⇩1 = r'" "r⇩2 ≠ r" "r⇩2 ≠ r'"
assume "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
hence "r⇩2 ∈ RID⇩L (the (s r))" using RID⇩LI(3) ‹r⇩1 = r'› fork(2) s'_r' by auto
have "s r⇩2 = s' r⇩2" by (simp add: ‹r⇩2 ≠ r'› ‹r⇩2 ≠ r› fork(1))
hence "𝒜 r r⇩2 s" using 𝒜⇩G_s fork(2) s'_r⇩2 subsumes_accessible_globally_def by auto
hence "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s r))"
by (simp add: ‹r⇩2 ∈ RID⇩L (the (s r))› ‹s r⇩2 = s' r⇩2› subsumes_accessible_def)
also have "... = dom σ ∪ dom τ" by (simp add: fork(2))
also have "... = dom (σ;;τ)" by (simp add: dom_combination_dom_union)
also have "... = doms (the (s' r'))" by (simp add: s'_r')
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" using ‹r⇩1 = r'› by blast
qed
have case4: "r⇩1 ≠ r ⟹ r⇩1 ≠ r' ⟹ r⇩2 = r' ⟹ ?thesis"
proof -
assume "r⇩1 ≠ r" "r⇩1 ≠ r'" "r⇩2 = r'"
have "r⇩2 ∉ RID⇩L (the (s r⇩1))" using ‹r⇩1 ≠ r'› ‹r⇩1 ≠ r› ‹r⇩2 = r'› fork(1,3) s'_r⇩1 by auto
hence "r⇩2 ∉ RID⇩L (the (s' r⇩1))" by (simp add: ‹r⇩1 ≠ r'› ‹r⇩1 ≠ r› fork(1))
thus ?thesis by blast
qed
have case5: "r⇩1 = r ⟹ r⇩2 = r' ⟹ ?thesis"
proof (rule subsumes_accessibleI)
assume "r⇩1 = r" "r⇩2 = r'"
have "LID⇩S ((the (s' r⇩2))⇩σ) = LID⇩S (σ;;τ)" by (simp add: ‹r⇩2 = r'› s'_r')
also have "... ⊆ LID⇩S σ ∪ LID⇩S τ" by auto
also have "... ⊆ LID⇩L (the (s' r⇩1))" by (simp add: ‹r⇩1 = r› s'_r)
also have "... ⊆ doms (the (s' r⇩1))"
by (metis ‹𝒮⇩G s'› ‹r⇩1 = r› domains_subsume_def domains_subsume_globally_def option.sel s'_r)
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
have case6: "r⇩1 = r' ⟹ r⇩2 = r ⟹ ?thesis"
proof (rule subsumes_accessibleI)
assume "r⇩1 = r'" "r⇩2 = r" "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S (the (s' r⇩2)⇩σ) ⊆ LID⇩L (the (s' r⇩2))" by (simp add: s'_r⇩2 subsetI)
also have "... ⊆ doms (the (s' r⇩2))"
using ‹𝒮⇩G s'› domains_subsume_def domains_subsume_globally_def s'_r⇩2 by auto
also have "... = dom σ ∪ dom τ" by (simp add: ‹r⇩2 = r› s'_r)
also have "... = dom (σ;;τ)" by (simp add: dom_combination_dom_union)
finally show " LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))"
using ‹r⇩1 = r'› s'_r' by auto
qed
show ?thesis using case1 case2 case3 case4 case5 case6 fork(1) r⇩1_neq_r⇩2 r⇩1_nor_r⇩2_updated_implies_thesis by fastforce
next
case (join σ τ ℰ r' σ' τ' v)
have "r⇩1 = r ∨ r⇩2 = r" by (metis fun_upd_def join(1) option.simps(3) r⇩1_or_r⇩2_updated s'_r⇩1 s'_r⇩2)
then show ?thesis
proof (rule disjE)
assume "r⇩1 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))"
proof (cases "r⇩2 ∈ RID⇩S τ'")
case r⇩2_in_τ': True
have "LID⇩S (the (s' r⇩2)⇩σ) = LID⇩S (the (s r⇩2)⇩σ)"
by (metis ‹r⇩1 = r› fun_upd_def join(1) option.distinct(1) r⇩1_neq_r⇩2 s'_r⇩2)
also have "... ⊆ doms (the (s r'))"
proof -
have r⇩2_in_s_r': "r⇩2 ∈ RID⇩L (the (s r'))" by (simp add: join(3) r⇩2_in_τ')
have "𝒜 r' r⇩2 s"
by (metis 𝒜⇩G_s ‹r⇩1 = r› domI fun_upd_def join(1) join(3) r⇩1_neq_r⇩2 s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r' r⇩2 s› r⇩2_in_s_r' subsumes_accessible_def by blast
qed
also have "... = dom σ' ∪ dom τ'" by (simp add: join(3))
also have "... ⊆ LID⇩S σ' ∪ dom τ'" by auto
also have "... ⊆ dom σ ∪ dom τ ∪ dom τ'"
proof -
have "r' ∈ RID⇩L (the (s r))" by (simp add: join(2))
have "𝒜 r r' s" using 𝒜⇩G_s join(2-3) subsumes_accessible_globally_def by auto
show ?thesis using ‹𝒜 r r' s› join(2-3) subsumes_accessible_def by auto
qed
also have "... = dom σ ∪ dom (τ;;τ')" by (auto simp add: dom_combination_dom_union)
also have "... = doms (the (s' r⇩1))" using join by (auto simp add: ‹r⇩1 = r›)
finally show ?thesis by simp
next
case r⇩2_nin_τ': False
have "LID⇩S (the (s' r⇩2)⇩σ) = LID⇩S (the (s r⇩2)⇩σ)"
by (metis ‹r⇩1 = r› fun_upd_def join(1) option.distinct(1) r⇩1_neq_r⇩2 s'_r⇩2)
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r))"
proof -
have "RID⇩L (the (s' r⇩1)) = RID⇩S σ ∪ RID⇩S (τ;;τ') ∪ RID⇩C ℰ"
by (metis (no_types, lifting) ID_distr_completion(1) ID_distr_local(2) ‹r⇩1 = r› expr.simps(153) fun_upd_apply local.join(1) option.discI option.sel s'_r⇩1 sup_bot.right_neutral val.simps(66))
hence "r⇩2 ∈ RID⇩S σ ∪ RID⇩S τ ∪ RID⇩C ℰ" using r⇩2_in_s'_r⇩1 r⇩2_nin_τ' by auto
thus ?thesis by (simp add: join(2))
qed
have "𝒜 r⇩1 r⇩2 s" by (metis (no_types, lifting) 𝒜⇩G_s ‹r⇩1 = r› join(1-2) domIff fun_upd_def option.discI s'_r⇩2 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def ‹r⇩1 = r› by blast
qed
also have "... = dom σ ∪ dom τ" by (simp add: ‹r⇩1 = r› join(2))
also have "... ⊆ dom σ ∪ dom (τ;;τ')" by (auto simp add: dom_combination_dom_union)
also have "... = doms (the (s' r⇩1))" using join ‹r⇩1 = r› by auto
finally show ?thesis by simp
qed
qed
next
assume "r⇩2 = r"
show "𝒜 r⇩1 r⇩2 s'"
proof (rule subsumes_accessibleI)
assume r⇩2_in_s'_r⇩1: "r⇩2 ∈ RID⇩L (the (s' r⇩1))"
have "LID⇩S (the (s' r⇩2)⇩σ) = LID⇩S (the (s r⇩2)⇩σ)"
by (metis (no_types, lifting) LID_snapshot.simps fun_upd_apply join(1-2) option.discI option.sel s'_r⇩2)
also have "... ⊆ doms (the (s r⇩1))"
proof -
have r⇩2_in_s_r⇩1: "r⇩2 ∈ RID⇩L (the (s r⇩1))"
by (metis ‹r⇩2 = r› fun_upd_apply local.join(1) option.discI r⇩1_neq_r⇩2 r⇩2_in_s'_r⇩1 s'_r⇩1)
have "𝒜 r⇩1 r⇩2 s"
by (metis (no_types, lifting) 𝒜⇩G_s ‹r⇩2 = r› domIff fun_upd_apply join(1-2) option.discI s'_r⇩1 subsumes_accessible_globally_def)
show ?thesis using ‹𝒜 r⇩1 r⇩2 s› r⇩2_in_s_r⇩1 subsumes_accessible_def by blast
qed
also have "... ⊆ doms (the (s' r⇩1))"
by (metis ‹r⇩2 = r› eq_refl fun_upd_def local.join(1) option.distinct(1) r⇩1_neq_r⇩2 s'_r⇩1)
finally show "LID⇩S (the (s' r⇩2)⇩σ) ⊆ doms (the (s' r⇩1))" by simp
qed
qed
next
case join⇩ε
thus ?thesis using s'_r⇩1 by blast
qed
qed
show "𝒜 r⇩1 r⇩2 s'" using r⇩1_nor_r⇩2_updated_implies_thesis r⇩1_or_r⇩2_updated_implies_thesis by blast
qed
qed
qed

subsection ‹Relaxed definition of the operational semantics›

inductive revision_step_relaxed :: "'r ⇒ ('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" where
app: "s r = Some (σ, τ, ℰ[Apply (VE (Lambda x e)) (VE v)]) ⟹ revision_step_relaxed r s (s(r ↦ (σ, τ, ℰ[subst (VE v) x e])))"
| ifTrue: "s r = Some (σ, τ, ℰ[Ite (VE (CV T)) e1 e2]) ⟹ revision_step_relaxed r s (s(r ↦ (σ, τ, ℰ[e1])))"
| ifFalse: "s r = Some (σ, τ, ℰ[Ite (VE (CV F)) e1 e2]) ⟹ revision_step_relaxed r s (s(r ↦ (σ, τ, ℰ[e2])))"
(* store operations *)
| new: "s r = Some (σ, τ, ℰ[Ref (VE v)]) ⟹ l ∉ ⋃ { doms ls | ls. ls ∈ ran s } ⟹ revision_step_relaxed r s (s(r ↦ (σ, τ(l ↦ v), ℰ[VE (Loc l)])))"
| get: "s r = Some (σ, τ, ℰ[Read (VE (Loc l))]) ⟹ revision_step_relaxed r s (s(r ↦ (σ, τ, ℰ[VE (the ((σ;;τ) l))])))"
| set: "s r = Some (σ, τ, ℰ[Assign (VE (Loc l)) (VE v)]) ⟹ revision_step_relaxed r s (s(r ↦ (σ, τ(l ↦ v), ℰ[VE (CV Unit)])))"
(* synchronization operations *)
| fork: "s r = Some (σ, τ, ℰ[Rfork e]) ⟹ r' ∉ RID⇩G s ⟹ revision_step_relaxed r s (s(r ↦ (σ, τ, ℰ[VE (Rid r')]), r' ↦ (σ;;τ, ε, e)))"
| join: "s r = Some (σ, τ, ℰ[Rjoin (VE (Rid r'))]) ⟹ s r' = Some (σ', τ', VE v) ⟹ revision_step_relaxed r s (s(r := Some (σ, (τ;;τ'), ℰ[VE (CV Unit)]), r' := None))"
| join⇩ε: "s r = Some (σ, τ, ℰ[Rjoin (VE (Rid r'))]) ⟹ s r' = None ⟹ revision_step_relaxed r s ε"

inductive_cases revision_step_relaxedE [elim, consumes 1, case_names app ifTrue ifFalse new get set fork join join⇩ε]:
"revision_step_relaxed r s s'"

end (* substitution locale *)

end (* theory *)


Theory Executions

section Executions

text ‹This section contains all definitions required for reasoning about executions in the concurrent
revisions model. It also contains a number of proofs for inductive variants. One of these
proves the equivalence of the two definitions of the operational semantics. The others are
required for proving determinacy.›

theory Executions
imports OperationalSemantics
begin

context substitution
begin

subsection ‹Generalizing the original transition›

subsubsection Definition

definition steps :: "('r,'l,'v) global_state rel" ("[↝]") where
"steps = { (s,s') | s s'. ∃r. revision_step r s s' }"

abbreviation valid_step :: "('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" (infix "↝" 60) where
"s ↝ s' ≡ (s,s') ∈ [↝]"

lemma valid_stepI [intro]:
"revision_step r s s' ⟹ s ↝ s'"
using steps_def by auto

lemma valid_stepE [dest]:
"s ↝ s' ⟹ ∃r. revision_step r s s'"

subsubsection Closures

abbreviation refl_trans_step_rel :: "('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool"(infix "↝⇧*" 60) where
"s ↝⇧* s' ≡ (s,s') ∈ [↝]⇧*"

abbreviation refl_step_rel :: "('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" (infix "↝⇧=" 60) where
"s ↝⇧= s' ≡ (s,s') ∈ [↝]⇧="

lemma refl_rewritesI [intro]: "s ↝ s' ⟹ s ↝⇧= s'" by blast

subsection Properties

abbreviation program_expr :: "('r,'l,'v) expr ⇒ bool" where
"program_expr e ≡ LID⇩E e = {} ∧ RID⇩E e = {}"

abbreviation initializes :: "('r,'l,'v) global_state ⇒ ('r,'l,'v) expr ⇒ bool" where
"initializes s e ≡ ∃r. s = (ε(r ↦(ε,ε,e))) ∧ program_expr e"

abbreviation initial_state :: "('r,'l,'v) global_state ⇒ bool" where
"initial_state s ≡ ∃e. initializes s e"

definition execution :: "('r,'l,'v) expr ⇒ ('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" where
"execution e s s' ≡ initializes s e ∧ s ↝⇧* s'"

definition maximal_execution :: "('r,'l,'v) expr ⇒ ('r,'l,'v) global_state ⇒ ('r,'l,'v) global_state ⇒ bool" where
"maximal_execution e s s' ≡ execution e s s' ∧ (∄s''. s' ↝ s'')"

definition reachable :: "('r,'l,'v) global_state ⇒ bool" where
"reachable s ≡ ∃e s'. execution e s' s"

definition terminates_in :: "('r,'l,'v) expr ⇒ ('r,'l,'v) global_state ⇒ bool" (infix "↓" 60) where
"e ↓ s' ≡ ∃s. maximal_execution e s s'"

subsection Invariants

subsubsection ‹Inductive invariance›

definition inductive_invariant :: "(('r,'l,'v) global_state ⇒ bool) ⇒ bool" where
"inductive_invariant P ≡ (∀s. initial_state s ⟶ P s) ∧ (∀s s'. s ↝ s' ⟶ P s ⟶ P s')"

lemma inductive_invariantI [intro]:
"(⋀s. initial_state s ⟹ P s) ⟹ (⋀s s'. s ↝ s' ⟹ P s ⟹ P s') ⟹ inductive_invariant P"

lemma inductive_invariant_is_execution_invariant: "reachable s ⟹ inductive_invariant P ⟹ P s"
proof -
assume reach: "reachable s" and ind_inv: "inductive_invariant P"
then obtain e initial n where initializes: "initializes initial e" and trace: "(initial,s) ∈ [↝]^^n"
by (metis execution_def reachable_def rtrancl_power)
thus "P s"
proof (induct n arbitrary: s)
case 0
have "initial = s"   using "0.prems"(2) by auto
hence "initial_state s" using initializes by blast
then show ?case using ind_inv inductive_invariant_def by auto
next
case (Suc n)
obtain s' where nfold: "(initial, s') ∈ [↝]^^n" and step: "s' ↝ s" using Suc.prems(2) by auto
have "P s'" using Suc(1) nfold initializes by blast
then show ?case using ind_inv step inductive_invariant_def by auto
qed
qed

subsubsection ‹Subsumption is invariant›

lemma nice_ind_inv_is_inductive_invariant: "inductive_invariant (λs. 𝒮⇩G s ∧ 𝒜⇩G s)"
proof (rule inductive_invariantI)
fix s
assume "initial_state s"
then obtain e r where s: "s = ε(r ↦ (ε, ε, e))" and prog_expr_e: "program_expr e" by blast
show "𝒮⇩G s ∧ 𝒜⇩G s"
proof (rule conjI)
show "𝒮⇩G s"
proof (rule domains_subsume_globallyI)
fix r' σ' τ' e'
assume s_r': "s r' = Some (σ',τ',e')"
have "r' = r" using s s_r' prog_expr_e by (meson domI domIff fun_upd_other)
hence "LID⇩L (σ',τ',e') = LID⇩L (ε, ε, e)" using s s_r' by auto
also have "... = {}" using prog_expr_e by auto
also have "... = dom σ' ∪ dom τ'" using ‹r' = r› s s_r' by auto
finally show "𝒮 (σ', τ', e')" by (simp add: domains_subsume_def)
qed
show "𝒜⇩G s"
proof (rule subsumes_accessible_globallyI)
fix r⇩1 σ⇩1 τ⇩1 e⇩1 r⇩2 σ⇩2 τ⇩2 e⇩2
assume s_r1: "s r⇩1 = Some (σ⇩1, τ⇩1, e⇩1)" and s_r2: "s r⇩2 = Some (σ⇩2, τ⇩2, e⇩2)"
have "r⇩2 = r" using s s_r2 prog_expr_e  by (meson domI domIff fun_upd_other)
hence "σ⇩2 = ε" using s s_r2 by auto
hence "LID⇩S σ⇩2 = {}" by auto
thus "𝒜 r⇩1 r⇩2 s" using s_r2 by auto
qed
qed
qed (use step_preserves_𝒮⇩G_and_𝒜⇩G in auto)

corollary reachable_imp_𝒮⇩G: "reachable s ⟹ 𝒮⇩G s"
proof -
assume reach: "reachable s"
have "𝒮⇩G s ∧ 𝒜⇩G s" by (rule inductive_invariant_is_execution_invariant[OF reach nice_ind_inv_is_inductive_invariant])
thus ?thesis by auto
qed

lemma transition_relations_equivalent: "reachable s ⟹ revision_step r s s' = revision_step_relaxed r s s'"
proof -
assume reach: "reachable s"
have doms_sub_local: "𝒮⇩G s" by (rule reachable_imp_𝒮⇩G[OF reach])
show "revision_step r s s' = revision_step_relaxed r s s'"
proof (rule iffI)
assume step: "revision_step r s s'"
show "revision_step_relaxed r s s'"
proof (use step in ‹induct rule: revision_stepE›)
case (new σ τ ℰ v l)
have "revision_step_relaxed r s (s(r ↦ (σ, τ(l ↦ v), ℰ [VE (Loc l)])))"
proof (rule revision_step_relaxed.new)
show "l ∉ ⋃ { doms ls | ls. ls ∈ ran s}"
proof
assume "l ∈ ⋃ { doms ls | ls. ls ∈ ran s}"
then obtain ls where in_ran: "ls ∈ ran s" and in_doms: "l ∈ doms ls" by blast
from in_doms have "l ∈ LID⇩L ls" by (cases ls) auto
have "l ∈ LID⇩G s"
proof -
have "ls ∈ {ls. ∃r. s r = Some ls}" by (metis (full_types) in_ran ran_def)
then show ?thesis using ‹l ∈ LID⇩L ls› by blast
qed
thus False using new by auto
qed
thus ?thesis using new.hyps(1) by blast
qed (use revision_step_relaxed.intros in simp)+
next
assume step: "revision_step_relaxed r s s'"
show "revision_step r s s'"
proof (use step in ‹induct rule: revision_step_relaxedE›)
case (new σ τ ℰ v l)
have "revision_step r s (s(r ↦ (σ, τ(l ↦ v), ℰ [VE (Loc l)])))"
proof (rule revision_step.new)
show "s r = Some (σ, τ, ℰ [Ref (VE v)])" by (simp add: new.hyps(2))
show "l ∉ LID⇩G s"
proof
assume "l ∈ LID⇩G s"
then obtain r' σ' τ' e' where s_r': "s r' = Some (σ',τ',e')" and l_in_local: "l ∈ LID⇩L (σ',τ',e')" by auto
hence "l ∈ dom σ' ∪ dom τ'"
by (metis (no_types, lifting) domains_subsume_def domains_subsume_globally_def doms.simps doms_sub_local rev_subsetD)
thus False by (meson s_r' new.hyps(3) ranI)
qed
qed
then show ?case using new.hyps(1) by blast
next
case (get σ τ ℰ l)
have "revision_step r s (s(r ↦ (σ, τ, ℰ [VE (the ((σ;;τ) l))])))"
proof
show "s r = Some (σ, τ, ℰ [Read (VE (Loc l))])" by (simp add: get.hyps(2))
show "l ∈ dom (σ;;τ)"
proof -
have "l ∈ LID⇩L (σ, τ, ℰ [Read (VE (Loc l))])"  by simp
hence "l ∈ dom σ ∪ dom τ"
using domains_subsume_def domains_subsume_globally_def doms_sub_local get.hyps(2) by fastforce
thus "l ∈ dom (σ;;τ)" by (simp add: dom_combination_dom_union)
qed
qed
then show ?case using get.hyps(1) by auto
next
case (set σ τ ℰ l v)
have "revision_step r s (s(r ↦ (σ, τ(l ↦ v), ℰ [VE (CV Unit)])))"
proof
show "s r = Some (σ, τ, ℰ [Assign (VE (Loc l)) (VE v)])" by (simp add: set.hyps(2))
show "l ∈ dom (σ;;τ)"
proof -
have "l ∈ LID⇩L (σ, τ, ℰ [Assign (VE (Loc l)) (VE v)])"  by simp
hence "l ∈ dom σ ∪ dom τ"
using domains_subsume_def domains_subsume_globally_def doms_sub_local set.hyps(2) by fastforce
thus "l ∈ dom (σ;;τ)" by (simp add: dom_combination_dom_union)
qed
qed
then show ?case using set.hyps(1) by blast
qed
qed

subsubsection ‹Finitude is invariant›

lemma finite_occurrences_val_expr [simp]:
fixes
v :: "('r,'l,'v) val" and
e :: "('r,'l,'v) expr"
shows
"finite (RID⇩V v)"
"finite (RID⇩E e)"
"finite (LID⇩V v)"
"finite (LID⇩E e)"
proof -
have "(finite (RID⇩V v) ∧ finite (LID⇩V v)) ∧ finite (RID⇩E e) ∧ finite (LID⇩E e)"
by (induct rule: val_expr.induct) auto
thus
"finite (RID⇩V v)"
"finite (RID⇩E e)"
"finite (LID⇩V v)"
"finite (LID⇩E e)"
by auto
qed

lemma store_finite_upd [intro]:
"finite (RID⇩S τ) ⟹ finite (RID⇩S (τ(l := None)))"
"finite (LID⇩S τ) ⟹ finite (LID⇩S (τ(l := None)))"
apply (meson ID_restricted_store_subset_store(1) finite_subset)

lemma finite_state_imp_restriction_finite [intro]:
"finite (RID⇩G s) ⟹ finite (RID⇩G (s(r := None)))"
"finite (LID⇩G s) ⟹ finite (LID⇩G (s(r := None)))"
proof -
assume "finite (RID⇩G s)"
thus "finite (RID⇩G (s(r := None)))" by (meson infinite_super ID_restricted_global_subset_unrestricted)
next
assume fin: "finite (LID⇩G s)"
have "LID⇩G (s(r := None)) ⊆ LID⇩G s" by auto
thus "finite (LID⇩G (s(r := None)))" using fin finite_subset by auto
qed

lemma local_state_of_finite_restricted_global_state_is_finite [intro]:
"s r' = Some ls ⟹ finite (RID⇩G (s(r := None))) ⟹ r ≠ r' ⟹ finite (RID⇩L ls)"
"s r' = Some ls ⟹ finite (LID⇩G (s(r := None))) ⟹ r ≠ r' ⟹ finite (LID⇩L ls)"
apply (metis (no_types, lifting) ID_distr_global(1) finite_Un finite_insert fun_upd_triv fun_upd_twist)
by (metis ID_distr_global(2) finite_Un fun_upd_triv fun_upd_twist)

lemma empty_map_finite [simp]:
"finite (RID⇩S ε)"
"finite (LID⇩S ε)"
"finite (RID⇩G ε)"
"finite (LID⇩G ε)"
by (simp add: RID⇩S_def LID⇩S_def RID⇩G_def LID⇩G_def)+

lemma finite_combination [intro]:
"finite (RID⇩S σ) ⟹ finite (RID⇩S τ) ⟹ finite (RID⇩S (σ;;τ))"
"finite (LID⇩S σ) ⟹ finite (LID⇩S τ) ⟹ finite (LID⇩S (σ;;τ))"
by (meson finite_UnI rev_finite_subset ID_combination_subset_union)+

lemma RID⇩G_finite_invariant:
assumes
step: "revision_step r s s'" and
fin: "finite (RID⇩G s)"
shows
"finite (RID⇩G s')"
proof (use step in ‹cases rule: revision_stepE›)
case (join σ τ ℰ r' σ' τ' v)
hence "r ≠ r'" by auto
then show ?thesis
by (metis (mono_tags, lifting) ID_distr_global(1) ID_distr_local(2) fin finite_Un finite_combination(1) finite_insert finite_occurrences_val_expr(2) finite_state_imp_restriction_finite(1) join local_state_of_finite_restricted_global_state_is_finite(1))
qed (use fin in ‹auto simp add: ID_distr_global_conditional›)

lemma RID⇩L_finite_invariant:
assumes
step: "revision_step r s s'" and
fin: "finite (LID⇩G s)"
shows
"finite (LID⇩G s')"
proof (use step in ‹cases rule: revision_stepE›)
case (join σ τ ℰ r' σ' τ' v)
hence "r ≠ r'" by auto
then show ?thesis
using join assms
by (metis (mono_tags, lifting) ID_distr_global(2) ID_distr_local(1) fin finite_Un finite_combination(2) finite_occurrences_val_expr(4) finite_state_imp_restriction_finite(2) join local_state_of_finite_restricted_global_state_is_finite(2))
qed (use fin in ‹auto simp add: ID_distr_global_conditional›)

lemma reachable_imp_identifiers_finite:
assumes reach: "reachable s"
shows
"finite (RID⇩G s)"
"finite (LID⇩G s)"
proof -
from reach obtain e r where exec: "execution e (ε(r ↦ (ε,ε,e))) s" using reachable_def execution_def by auto
hence prog_exp: "program_expr e" by (meson execution_def)
obtain n where n_reachable: "(ε(r ↦ (ε,ε,e)), s) ∈ [↝]^^n" using exec by (meson execution_def rtrancl_imp_relpow)
hence "finite (RID⇩G s) ∧ finite (LID⇩G s)"
proof (induct n arbitrary: s)
case 0
hence s: "s = ε(r ↦ (ε, ε, e))" by auto
hence rid_dom: "dom s = {r}" by auto
hence rid_ran: "⋃ (RID⇩L  ran s) = {}" using s by (auto simp add: prog_exp)
have rids: "RID⇩G s = {r}" by (unfold RID⇩G_def, use rid_dom rid_ran in auto)
have lid_ran: "⋃ (LID⇩L  ran s) = {}" using s by (auto simp add: prog_exp)
hence lids: "LID⇩G s = {}" by (unfold LID⇩G_def, simp)
thus ?case using rids lids by simp
next
case (Suc n)
then obtain s' where
n_steps: "(ε(r ↦ (ε, ε, e)), s') ∈ [↝]^^n" and
step: "s' ↝ s"
by (meson relpow_Suc_E)
have fin_rid: "finite (RID⇩G s')" using Suc.hyps n_steps by blast
have fin_lid: "finite (LID⇩G s')" using Suc.hyps n_steps by blast
thus ?case by (meson RID⇩G_finite_invariant RID⇩L_finite_invariant fin_rid local.step valid_stepE)
qed
thus "finite (RID⇩G s)" "finite (LID⇩G s)" by auto
qed

lemma reachable_imp_identifiers_available:
assumes
"reachable (s :: ('r,'l,'v) global_state)"
shows
"infinite (UNIV :: 'r set) ⟹ ∃r. r ∉ RID⇩G s"
"infinite (UNIV :: 'l set) ⟹ ∃l. l ∉ LID⇩G s"
by (simp add: assms ex_new_if_finite reachable_imp_identifiers_finite)+

subsubsection ‹Reachability is invariant›

lemma initial_state_reachable:
assumes "program_expr e"
shows "reachable (ε(r ↦ (ε,ε,e)))"
proof -
have "initializes (ε(r ↦ (ε,ε,e))) e" using assms by auto
hence "execution e (ε(r ↦ (ε,ε,e))) (ε(r ↦ (ε,ε,e)))" by (simp add: execution_def)
thus ?thesis using reachable_def by blast
qed

lemma reachability_closed_under_execution_step:
assumes
reach: "reachable s" and
step: "revision_step r s s'"
shows "reachable s'"
proof -
obtain init e where exec: "execution e init s" using reach reachable_def by blast
hence init_s:"init ↝⇧* s" by (simp add: execution_def)
have s_s': "s ↝ s'" using step by blast
have "init ↝⇧* s'" using init_s s_s' by auto
hence "execution e init s'" using exec by (simp add: execution_def)
thus ?thesis using reachable_def by auto
qed

lemma reachability_closed_under_execution: "reachable s ⟹ s ↝⇧* s' ⟹ reachable s'"
proof -
assume reach: "reachable s" and "s ↝⇧* s'"
then obtain n where "(s, s') ∈ [↝]^^n" using rtrancl_imp_relpow by blast
thus "reachable s'"
proof (induct n arbitrary: s')
case 0
thus ?case using reach by auto
next
case (Suc n)
obtain s'' where "(s,s'') ∈ [↝]^^n" "s'' ↝ s'" using Suc.prems by auto
have "reachable s''" by (simp add: Suc.hyps ‹(s, s'') ∈ [↝]^^n›)
then show ?case using ‹s'' ↝ s'› reachability_closed_under_execution_step by blast
qed
qed

end (* substitution locale *)

end (* theory *)


Theory Determinacy

section Determinacy

text ‹This section proves that the concurrent revisions model is determinate modulo renaming-equivalence.›

theory Determinacy
imports Executions
begin

context substitution
begin

subsection ‹Rule determinism›

lemma app_deterministic [simp]:
assumes
s_r: "s r = Some (σ, τ, ℰ [Apply (VE (Lambda x e)) (VE v)])"
shows "(revision_step r s s') = (s' = (s(r ↦ (σ, τ, ℰ [subst (VE v) x e]))))" (is "?l = ?r")
proof (rule iffI)
assume ?l
thus ?r by (cases rule: revision_stepE) (use s_r in auto)

lemma ifTrue_deterministic [simp]:
assumes
s_r: "s r = Some (σ, τ, ℰ [Ite (VE (CV T)) e1 e2])"
shows "(revision_step r s s') = (s' = (s(r ↦ (σ, τ, ℰ [e1]))))" (is "?l = ?r")
proof (rule iffI)
assume ?l
thus ?r by (cases rule: revision_stepE) (use s_r in auto)

lemma ifFalse_deterministic [simp]:
assumes
s_r: "s r = Some (σ, τ, ℰ [Ite (VE (CV F)) e1 e2])"
shows "(revision_step r s s') = (s' = (s(r ↦ (σ, τ, ℰ [e2]))))" (is "?l = ?r")
proof (rule iffI)
assume ?l
thus ?r by (cases rule: revision_stepE) (use s_r in auto)

lemma new_pseudodeterministic [simp]:
assumes
s_r: "s r = Some (σ, τ, ℰ [Ref (VE v)])"
shows "(revision_step r s s') = (∃l. l ∉ LID⇩G s ∧ s' = (s(r ↦ (σ, τ(l ↦ v), ℰ [VE (Loc l)]))))" (is "?l = ?r")
proof (rule iffI)
assume ?l
thus ?r by (cases rule: revision_stepE) (use s_r in auto)
qed (auto simp add: s_r revision_step.new)

lemma get_deterministic [simp]:
assumes
s_r: "s r = Some (σ, τ, ℰ [Read (VE (Loc l))])"
shows "(revision_step r s s') = (l ∈ dom (σ;;τ) ∧ s' = (s(r ↦ (σ, τ, ℰ [VE (the ((σ;;τ) l))]))))" (is "?l = ?r")
proof (rule iffI)
assume ?l
thus ?r by (cases rule: revision_stepE) (use s_r in auto)
qed (use revision_step.get in ‹auto simp add: s_r›)

lemma set_deterministic [simp]:
assumes
s_r: "s r = Some (σ, τ, ℰ [Assign (VE (Loc l)) (VE v)])"
shows "(revision_step r s s') = (l ∈ dom (σ;;τ) ∧ s' = (s(r ↦ (σ, τ(l ↦ v), ℰ [VE (CV Unit)]))))" (is "?l = ?r")
proof (rule iffI)
assume ?l
thus ?r by (cases rule: revision_stepE) (use s_r in auto)
qed (auto simp add: s_r revision_step.set)

lemma fork_pseudodeterministic [simp]:
assumes
s_r: "s r = Some (σ, τ, ℰ [Rfork e])"
shows "(revision_step r s s') = (∃r'. r' ∉ RID⇩G (s(r ↦ (σ, τ, ℰ [Rfork e]))) ∧ s' = (s(r ↦ (σ, τ, ℰ [VE (Rid r')]), r' ↦ (σ;;τ, ε, e))))" (is "?l = ?r")
proof (rule iffI)
assume step: ?l
show ?r
proof (use step in ‹cases rule: revision_stepE›)
case (fork σ τ ℰ e r')
show ?thesis by (rule exI[where x=r']) (use fork s_r in auto)
qed (auto simp add: s_r revision_step.fork map_upd_triv)

lemma rjoin_deterministic [simp]:
assumes
s_r: "s r = Some (σ, τ, ℰ [Rjoin (VE (Rid r'))])" and
s_r': "s r' = Some (σ', τ', VE v)"
shows "(revision_step r s s') = (s' = (s(r := Some (σ, τ;;τ', ℰ [VE (CV Unit)]), r' := None)))" (is "?l = ?r")
proof (rule iffI)
assume step: ?l
show ?r by (cases rule: revision_stepE[OF step]) (use s_r s_r' in auto)
qed (meson s_r s_r' revision_step.join)

lemma rjoin⇩ε_deterministic [simp]:
assumes
s_r: "s r = Some (σ, τ, ℰ [Rjoin (VE (Rid r'))])" and
s_r': "s r' = None"
shows "(revision_step r s s') = (s' = ε)" (is "?l = ?r")
proof (rule iffI)
assume step: ?l
show ?r by (cases rule: revision_stepE[OF step]) (use s_r s_r' in auto)
qed (simp add: revision_step.join⇩ε s_r s_r')

subsection ‹Strong local confluence›

subsubsection ‹Local determinism›

lemma local_determinism:
assumes
left: "revision_step r s⇩1 s⇩2" and
right: "revision_step r s⇩1 s⇩2'"
shows "s⇩2 ≈ s⇩2'"
proof (use left in ‹induct rule:revision_stepE›)
case (new σ τ ℰ v l)
from new(2) right obtain l' where
side: "l' ∉ LID⇩G s⇩1" and
s⇩2': "s⇩2' = s⇩1(r ↦ (σ, τ(l' ↦ v), ℰ[VE (Loc l')]))"
by auto
let "?β" = "id(l := l', l' := l)"
have bij_β: "bij ?β" by (rule swap_bij)
have renaming: "ℛ⇩G id ?β s⇩2 = s⇩2'"
by (use new side s⇩2' bij_β in ‹auto simp add: ID_distr_global_conditional›)
show ?case by (rule eq_statesI[OF renaming bij_id bij_β])
next
case (fork σ τ ℰ e r')
from fork(2) right obtain r'' where
side: "r'' ∉ RID⇩G s⇩1" and
s⇩2': "s⇩2' = s⇩1(r ↦ (σ, τ, ℰ [VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e))"
let "?α" = "id(r' := r'', r'' := r')"
have bij_α: "bij ?α" by (rule swap_bij)
have renaming: "ℛ⇩G ?α id s⇩2 = s⇩2'"
by (use fork side s⇩2' bij_α in ‹auto simp add: ID_distr_global_conditional›)
show ?case by (rule eq_statesI[OF renaming bij_α bij_id])
qed ((rule eq_statesI[of id id], use assms in auto)[1])+

subsubsection ‹General principles›

lemma SLC_sym:
"∃s⇩3' s⇩3. s⇩3' ≈ s⇩3 ∧ (revision_step r' s⇩2 s⇩3' ∨ s⇩2 = s⇩3') ∧ (revision_step r s⇩2' s⇩3 ∨ s⇩2' = s⇩3) ⟹
∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r s⇩2' s⇩3 ∨ s⇩2' = s⇩3) ∧ (revision_step r' s⇩2 s⇩3' ∨ s⇩2 = s⇩3')"
by (metis αβ_sym)

lemma SLC_commute:
"⟦ s⇩3 = s⇩3'; revision_step r' s⇩2 s⇩3; revision_step r s⇩2' s⇩3' ⟧ ⟹
s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
using αβ_refl by auto

subsubsection ‹Case join-epsilon›

lemma SLC_join⇩ε:
assumes
s⇩1_r: "s⇩1 r = Some (σ, τ, ℰ[Rjoin (VE (Rid r''))])" and
s⇩2: "s⇩2 = ε" and
side: "s⇩1 r'' = None" and
right: "revision_step r' s⇩1 s⇩2'" and
neq: "r ≠ r'"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof -
have right_collapsed_case: "s⇩2' = ε ⟹ ?thesis"
by (rule exI[where x=ε], rule exI[where x=ε], use s⇩2 in auto)
have left_step_still_available_case: "s⇩2' ≠ ε ⟹ s⇩2' r = s⇩1 r ⟹ s⇩2' r'' = None ⟹ ?thesis"
by (rule exI[where x=ε], rule exI[where x=ε]) (use assms in auto)
show ?thesis
proof (use right in ‹cases rule: revision_stepE›)
case (join _ _ _ right_joinee)
have r_unchanged_left: "s⇩2' r = s⇩1 r" using join assms by auto
have r'_unchanged_right: "s⇩2' r'' = None" using join assms by auto
have "right_joinee ≠ r'" using join(2-3) by auto
hence s⇩2'_nonempty: "s⇩2' ≠ ε" using assms join by (auto simp add: fun_upd_twist)
show ?thesis by (rule left_step_still_available_case[OF s⇩2'_nonempty r_unchanged_left r'_unchanged_right])
next
case join⇩ε
show ?thesis by (rule right_collapsed_case, use join⇩ε(2-3) right in auto)
qed ((rule left_step_still_available_case, use side neq s⇩1_r right in auto)[1])+
qed

subsubsection ‹Case join›

lemma join_and_local_commute:
assumes
"s⇩2 = s⇩1(r := Some (σ, τ;;τ', ℰ[VE (CV Unit)]), r'' := None)"
"s⇩2' = s⇩1(r' ↦ ls)"
"r ≠ r'"
"r' ≠ r''"
"revision_step r' s⇩2 (s⇩1(r := Some (σ, τ;;τ', ℰ[VE (CV Unit)]), r'' := None, r' := Some ls))"
"s⇩2' r = Some (σ, τ, ℰ [Rjoin (VE (Rid r''))])"
"s⇩2' r'' = Some (σ', τ', VE v)"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
apply (rule exI[where x="s⇩1(r := Some (σ, τ;;τ', ℰ[VE (CV Unit)]), r'' := None, r' := Some ls)"])
apply (rule exI[where x="s⇩1(r' := Some ls, r := Some (σ, τ;;τ', ℰ[VE (CV Unit)]), r'' := None)"])
by (rule SLC_commute, use assms in auto)

lemma SLC_join:
assumes
s⇩1_r: "s⇩1 r = Some (σ, τ, ℰ[Rjoin (VE (Rid r''))])" and
s⇩2: "s⇩2 = (s⇩1(r := Some (σ, (τ;;τ'), ℰ[VE (CV Unit)]), r'' := None))" and
side: "s⇩1 r'' = Some (σ', τ', VE v)" and
right: "revision_step r' s⇩1 s⇩2'" and
neq: "r ≠ r'"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof -
have left_step: "revision_step r s⇩1 s⇩2" using s⇩1_r s⇩2 side by auto
have r'_not_joined: "r' ≠ r''" using right side by auto
show ?thesis
proof (use right in ‹cases rule: revision_stepE›)
case (new _ _ _ _ l)
have l_fresh_left: "l ∉ LID⇩G s⇩2" by (rule only_new_introduces_lids'[OF left_step]) (use new right s⇩1_r in auto)
show ?thesis by (rule join_and_local_commute, use assms r'_not_joined new l_fresh_left in auto)
next
case (fork _ _ _ _ r''')
have r'_unchanged_left: "s⇩2 r' = s⇩1 r'" using fork assms by auto
have r'''_fresh_left: "r''' ∉ RID⇩G s⇩2" using left_step fork(3) only_fork_introduces_rids' s⇩1_r by auto
have r_unchanged_right: "s⇩2' r = s⇩1 r" using fork assms by auto
have r''_unchanged_right: "s⇩2' r'' = s⇩1 r''" using fork assms by auto
let "?s⇩3" = "s⇩2(r' := s⇩2' r', r''' := s⇩2' r''')"
let "?s⇩3'" = "s⇩2'(r := s⇩2 r, r'' := None)"
show ?thesis
proof (rule exI[where x="?s⇩3"],rule exI[where x="?s⇩3'"], rule SLC_commute)
show "?s⇩3 = ?s⇩3'" using fork(1) fork(3) neq r'_not_joined s⇩1_r s⇩2 by (auto simp add: ID_distr_global_conditional)
show "revision_step r' s⇩2 ?s⇩3" using fork(1-2) r'_unchanged_left r'''_fresh_left by (auto simp add: ID_distr_global_conditional)
show "revision_step r s⇩2' ?s⇩3'" using r''_unchanged_right r_unchanged_right s⇩1_r s⇩2 side by auto
qed
next
case (join _ _ _ r''')
have r'_unchanged_left: "s⇩2 r' = s⇩1 r'" using join(2) neq r'_not_joined s⇩2 by auto
have r_unchanged_right: "s⇩2' r = s⇩1 r" using join(1,3) neq s⇩1_r by auto
show ?thesis
proof (cases "r'' = r'''")
case True
have r'''_none_left: "s⇩2 r''' = None" by (simp add: True s⇩2)
have r''_none_right: "s⇩2' r'' = None" by (simp add: True join(1))
show ?thesis
proof (rule exI[where x=ε], rule exI[where x=ε], rule SLC_commute)
show "ε = ε" by (rule refl)
show "revision_step r' s⇩2 ε" using r'_unchanged_left r'''_none_left join(2) by auto
show "revision_step r s⇩2' ε" using r_unchanged_right r''_none_right s⇩1_r by auto
qed
next
case False
have r'''_unchanged_left: "s⇩2 r''' = s⇩1 r'''" using False join(1,3) s⇩2 r_unchanged_right by auto
have r''_unchanged_right': "s⇩2' r'' = s⇩1 r''" using False join(1) r'_not_joined side by auto
let "?s⇩3" = "s⇩2(r' := s⇩2' r', r''' := None)"
let "?s⇩3'" = "s⇩2'(r := s⇩2 r, r'' := None)"
show ?thesis
proof (rule exI[where x="?s⇩3"], rule exI[where x="?s⇩3'"], rule SLC_commute)
show "?s⇩3 = ?s⇩3'" using join(1) neq r'_not_joined r_unchanged_right s⇩1_r s⇩2 s⇩1_r by fastforce
show "revision_step r' s⇩2 ?s⇩3" by (simp add: join r'''_unchanged_left r'_unchanged_left)
show "revision_step r s⇩2' ?s⇩3'" using r''_unchanged_right' r_unchanged_right s⇩1_r side s⇩2 by auto
qed
qed
next
case join⇩ε
show ?thesis by (rule SLC_sym, rule SLC_join⇩ε, use left_step neq right join⇩ε in auto)
qed ((rule join_and_local_commute, use assms r'_not_joined in auto)[1])+
qed

subsubsection ‹Case local›

lemma local_steps_commute:
assumes
"s⇩2 = s⇩1(r ↦ x)"
"s⇩2' = s⇩1(r' ↦ y)"
"revision_step r' (s⇩1(r ↦ x)) (s⇩1(r ↦ x, r' ↦ y))"
"revision_step r (s⇩1(r' ↦ y)) (s⇩1(r' ↦ y, r ↦ x))"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
by (metis (no_types, lifting) assms fun_upd_twist fun_upd_upd local_determinism)

lemma local_and_fork_commute:
assumes
"s⇩2 = s⇩1(r ↦ x)"
"s⇩2' = s⇩1(r' ↦ (σ, τ, ℰ [VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e))"
"s⇩2 r' = Some (σ, τ, ℰ[Rfork e])"
"r'' ∉ RID⇩G s⇩2"
"revision_step r s⇩2' (s⇩1(r' ↦ (σ, τ, ℰ [VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e), r ↦ x))"
"r ≠ r'"
"r ≠ r''"
shows
"∃s⇩3 s⇩3'. (s⇩3 ≈ s⇩3') ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof(rule exI[where x="s⇩1(r ↦ x, r' ↦ (σ, τ, ℰ [VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e))"],
rule exI[where x="s⇩1(r' ↦ (σ, τ, ℰ [VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e), r ↦ x)"],
rule SLC_commute)
show "s⇩1(r ↦ x, r' ↦ (σ, τ, ℰ [VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e)) =
s⇩1(r' ↦ (σ, τ, ℰ [VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e), r ↦ x)"
using assms revision_step.fork by auto
show "revision_step r' s⇩2 (s⇩1(r ↦ x, r' ↦ (σ, τ, ℰ [VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e)))"
using assms(1) assms(3) assms(4) revision_step.fork by blast
show "revision_step r s⇩2' (s⇩1(r' ↦ (σ, τ, ℰ [VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e), r ↦ x))"
using assms(5) by blast
qed

lemma SLC_app:
assumes
s⇩1_r: "s⇩1 r = Some (σ, τ, ℰ[Apply (VE (Lambda x e)) (VE v)])" and
s⇩2: "s⇩2 = s⇩1(r ↦ (σ, τ, ℰ[subst (VE v) x e]))" and
right: "revision_step r' s⇩1 s⇩2'" and
neq: "r ≠ r'"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof -
have left_step: "revision_step r s⇩1 s⇩2" using s⇩1_r s⇩2 by auto
show ?thesis
proof (use right in ‹cases rule: revision_stepE›)
case new: (new _ _ _ _ l)
have l_fresh_left: "l ∉ LID⇩G s⇩2"
by (rule only_new_introduces_lids'[OF left_step]) (simp add: s⇩1_r new(3))+
show ?thesis by (rule local_steps_commute) (use new l_fresh_left assms in auto)
next
case (fork _ _ _ _ r'')
have r''_fresh_left: "r'' ∉ RID⇩G s⇩2"
by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s⇩1_r fork(3))+
show ?thesis by (rule local_and_fork_commute[OF s⇩2 fork(1)]) (use fork neq s⇩2 r''_fresh_left s⇩1_r in auto)
next
case join
show ?thesis by (rule SLC_sym, rule SLC_join, use join left_step right neq in auto)
next
case join⇩ε
show ?thesis by (rule SLC_sym, rule SLC_join⇩ε, use join⇩ε left_step right neq in auto)
qed ((rule local_steps_commute[OF s⇩2], use assms in auto)[1])+
qed

lemma SLC_ifTrue:
assumes
s⇩1_r: "s⇩1 r = Some (σ, τ, ℰ[Ite (VE (CV T)) e1 e2])" and
s⇩2: "s⇩2 = s⇩1(r ↦ (σ, τ, ℰ[e1]))" and
right: "revision_step r' s⇩1 s⇩2'" and
neq: "r ≠ r'"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof -
have left_step: "revision_step r s⇩1 s⇩2" using s⇩1_r s⇩2 by auto
show ?thesis
proof (use right in ‹cases rule: revision_stepE›)
case (new _ _ _ _ l)
have l_fresh_left: "l ∉ LID⇩G s⇩2"
by (rule only_new_introduces_lids'[OF left_step]) (simp add: s⇩1_r new(3))+
show ?thesis by (rule local_steps_commute) (use new l_fresh_left assms in auto)
next
case (fork _ _ _ _ r'')
have r''_fresh_left: "r'' ∉ RID⇩G s⇩2"
by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s⇩1_r fork(3))+
show ?thesis by (rule local_and_fork_commute[OF s⇩2 fork(1)]) (use fork neq s⇩2 r''_fresh_left s⇩1_r in auto)
next
case join
show ?thesis by (rule SLC_sym, rule SLC_join, use join left_step right neq in auto)
next
case join⇩ε
show ?thesis by (rule SLC_sym, rule SLC_join⇩ε, use join⇩ε left_step right neq in auto)
qed ((rule local_steps_commute[OF s⇩2], use assms in auto)[1])+
qed

lemma SLC_ifFalse:
assumes
s⇩1_r: "s⇩1 r = Some (σ, τ, ℰ[Ite (VE (CV F)) e1 e2])" and
s⇩2: "s⇩2 = s⇩1(r ↦ (σ, τ, ℰ[e2]))" and
right: "revision_step r' s⇩1 s⇩2'" and
neq: "r ≠ r'"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof -
have left_step: "revision_step r s⇩1 s⇩2" using s⇩1_r s⇩2 by auto
show ?thesis
proof (use right in ‹cases rule: revision_stepE›)
next
case (new _ _ _ _ l)
have l_fresh_left: "l ∉ LID⇩G s⇩2"
by (rule only_new_introduces_lids'[OF left_step]) (simp add: s⇩1_r new(3))+
show ?thesis by (rule local_steps_commute) (use new l_fresh_left assms in auto)
next
case (fork _ _ _ _ r'')
have r''_fresh_left: "r'' ∉ RID⇩G s⇩2"
by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s⇩1_r fork(3))+
show ?thesis by (rule local_and_fork_commute[OF s⇩2 fork(1)]) (use fork neq s⇩2 r''_fresh_left s⇩1_r in auto)
next
case join
show ?thesis by (rule SLC_sym, rule SLC_join, use join left_step right neq in auto)
next
case join⇩ε
show ?thesis by (rule SLC_sym, rule SLC_join⇩ε, use join⇩ε left_step right neq in auto)
qed ((rule local_steps_commute[OF s⇩2], use assms in auto)[1])+
qed

lemma SLC_set:
assumes
s⇩1_r: "s⇩1 r = Some (σ, τ, ℰ[Assign (VE (Loc l)) (VE v)])" and
s⇩2: "s⇩2 = s⇩1(r ↦ (σ, τ(l ↦ v), ℰ[VE (CV Unit)]))" and
side: "l ∈ dom (σ;;τ)" and
right: "revision_step r' s⇩1 s⇩2'" and
neq: "r ≠ r'"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof -
have left_step: "revision_step r s⇩1 s⇩2" using s⇩1_r s⇩2 side by auto
show ?thesis
proof (use right in ‹cases rule: revision_stepE›)
case (new _ _ _ _ l)
have l_fresh_left: "l ∉ LID⇩G s⇩2"
by (rule only_new_introduces_lids'[OF left_step]) (simp add: s⇩1_r new(3))+
show ?thesis by (rule local_steps_commute) (use new l_fresh_left assms in auto)
next
case (fork _ _ _ _ r'')
have r''_fresh_left: "r'' ∉ RID⇩G s⇩2"
by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s⇩1_r fork(3))+
show ?thesis by (rule local_and_fork_commute[OF s⇩2 fork(1)]) (use fork neq s⇩2 r''_fresh_left s⇩1_r side in auto)
next
case join
show ?thesis by (rule SLC_sym, rule SLC_join, use join left_step neq in auto)
next
case join⇩ε
show ?thesis by (rule SLC_sym, rule SLC_join⇩ε, use join⇩ε left_step neq in auto)
qed ((rule local_steps_commute[OF s⇩2], use assms in auto)[1])+
qed

lemma SLC_get:
assumes
s⇩1_r: "s⇩1 r = Some (σ, τ, ℰ [Read (VE (Loc l))])" and
s⇩2: "s⇩2 = s⇩1(r ↦ (σ, τ, ℰ[VE (the ((σ;;τ) l))]))" and
side: "l ∈ dom (σ;;τ)" and
right: "revision_step r' s⇩1 s⇩2'" and
neq: "r ≠ r'"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof -
have left_step: "revision_step r s⇩1 s⇩2" using s⇩1_r s⇩2 side by auto
show ?thesis
proof (use right in ‹cases rule: revision_stepE›)
case (new _ _ _ _ l)
have l_fresh_left: "l ∉ LID⇩G s⇩2"
by (rule only_new_introduces_lids'[OF left_step]) (simp add: s⇩1_r new(3))+
show ?thesis by (rule local_steps_commute) (use new l_fresh_left assms in auto)
next
case (fork _ _ _ _ r'')
have r''_fresh_left: "r'' ∉ RID⇩G s⇩2"
by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s⇩1_r fork(3))+
show ?thesis by (rule local_and_fork_commute[OF s⇩2 fork(1)]) (use fork neq s⇩2 r''_fresh_left s⇩1_r side in auto)
next
case join
show ?thesis by (rule SLC_sym, rule SLC_join, use join left_step neq in auto)
next
case join⇩ε
show ?thesis by (rule SLC_sym, rule SLC_join⇩ε, use join⇩ε left_step neq in auto)
qed ((rule local_steps_commute[OF s⇩2], use assms in auto)[1])+
qed

subsubsection ‹Case new›

lemma SLC_new:
assumes
s⇩1_r: "s⇩1 r = Some (σ, τ, ℰ[Ref (VE v)])" and
s⇩2: "s⇩2 = s⇩1(r ↦ (σ, τ(l ↦ v), ℰ [VE (Loc l)]))" and
side: "l ∉ LID⇩G s⇩1" and
right: "revision_step r' s⇩1 s⇩2'" and
neq: "r ≠ r'" and
reach: "reachable (s⇩1 :: ('r,'l,'v) global_state)" and
lid_inf: "infinite (UNIV :: 'l set)"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof -
have left_step: "revision_step r s⇩1 s⇩2" using s⇩1_r s⇩2 side by auto
show ?thesis
proof (use right in ‹cases rule: revision_stepE›)
case app
show ?thesis by (rule SLC_sym, rule SLC_app) (use app assms(1-5) in auto)
next
case ifTrue
show ?thesis by (rule SLC_sym, rule SLC_ifTrue) (use ifTrue assms(1-5) in auto)
next
case ifFalse
show ?thesis by (rule SLC_sym, rule SLC_ifFalse) (use ifFalse assms(1-5) in auto)
next
case (new σ' τ' ℰ' v' l')
have r'_unchanged_left: "s⇩2 r' = s⇩1 r'" using new(2) neq s⇩2 by auto
have r_unchanged_right: "s⇩2' r = s⇩1 r" by (simp add: new(1) neq s⇩1_r)
show ?thesis
proof (cases "l = l'")
case True
obtain l'' where l''_fresh_left: "l'' ∉ LID⇩G s⇩2"
by (meson ex_new_if_finite left_step lid_inf reach RID⇩L_finite_invariant reachable_imp_identifiers_finite(2))
hence l_l'': "l ≠ l''" by (auto simp add: s⇩2)
have l''_fresh_s⇩1: "l'' ∉ LID⇩G s⇩1" using assms True new l''_fresh_left by (auto simp add: ID_distr_global_conditional)
hence l''_fresh_right': "l'' ∉ LID⇩G s⇩2'" using True l_l'' new(1-2) by auto
let "?β" = "id(l := l'', l'' := l)"
have bij_β: "bij ?β" by (simp add: swap_bij)
let "?s⇩3" = "s⇩2(r' ↦ (σ', τ'(l'' ↦ v'), ℰ' [VE (Loc l'')]))"
have left_convergence: "revision_step r' s⇩2 ?s⇩3"
using l''_fresh_left new(2) r'_unchanged_left by auto
let "?s⇩3'" = "s⇩2'(r ↦ (σ, τ(l'' ↦ v), ℰ [VE (Loc l'')]))"
have right_convergence: "revision_step r s⇩2' ?s⇩3'"
using l''_fresh_right' new(1) neq s⇩1_r by auto
have equiv: "?s⇩3 ≈ ?s⇩3'"
proof (rule eq_statesI[of id ?β])
show "ℛ⇩G id ?β ?s⇩3 = ?s⇩3'"
proof -
have s⇩1: "ℛ⇩G id ?β s⇩1 = s⇩1" using l''_fresh_s⇩1 side by auto
have σ: "ℛ⇩S id ?β σ = σ" using l''_fresh_s⇩1 s⇩1_r side by auto
have ℰ: "ℛ⇩C id ?β ℰ = ℰ"
proof
show "l ∉ LID⇩C ℰ" using s⇩1_r side by auto
show "l'' ∉ LID⇩C ℰ" using l''_fresh_left s⇩2 by auto
qed
have τlv: "ℛ⇩S id (id(l := l'', l'' := l)) (τ(l ↦ v)) = (τ(l'' ↦ v))"
proof -
have τ: "ℛ⇩S id ?β τ = τ" using l''_fresh_s⇩1 s⇩1_r side by auto
have v: "ℛ⇩V id ?β v = v"
proof
show "l ∉ LID⇩V v" using s⇩1_r side by auto
show "l'' ∉ LID⇩V v" using l''_fresh_s⇩1 s⇩1_r by auto
qed
show ?thesis by (simp add: τ v bij_β)
qed
have σ': "ℛ⇩S id ?β σ' = σ'" using l''_fresh_s⇩1 new(2-3) by (auto simp add: True ID_distr_global_conditional)
have ℰ': "ℛ⇩C id ?β ℰ' = ℰ'" using l''_fresh_s⇩1 new(2-3) by (auto simp add: True ID_distr_global_conditional)
have τl''v: "ℛ⇩S id (id(l := l'', l'' := l)) (τ'(l'' ↦ v')) = (τ'(l ↦ v'))"
proof -
have τ': "ℛ⇩S id ?β τ' = τ'" using new(2-3) l''_fresh_s⇩1 by (auto simp add: True ID_distr_global_conditional)
have v': "ℛ⇩V id ?β v' = v'" using new(2-3) l''_fresh_s⇩1 by (auto simp add: True ID_distr_global_conditional)
show ?thesis by (simp add: τ' v' bij_β)
qed
show ?thesis using True neq s⇩1 σ ℰ τlv σ' ℰ' τl''v s⇩2 l_l'' new(1) by auto
qed
show ?thesis using left_convergence right_convergence equiv by blast
next
case False
have l_fresh_left: "l ∉ LID⇩G s⇩2'"
by (rule revision_stepE[OF left_step]) (use False side new(1-2) in ‹auto simp add: s⇩1_r›)
have l'_fresh_right: "l' ∉ LID⇩G s⇩2"
by (rule revision_stepE[OF right]) (use False new(3) assms(1-3) in ‹auto simp add: new(2)›)
show ?thesis by (rule local_steps_commute[OF s⇩2 new(1)]) (use new assms l_fresh_left l'_fresh_right s⇩2 in auto)
qed
next
case get
show ?thesis by (rule SLC_sym, rule SLC_get) (use get assms(1-5) in auto)
next
case set
show ?thesis by (rule SLC_sym, rule SLC_set) (use set assms(1-5) in auto)
next
case (fork _ _ _ _ r'')
have r''_fresh_left: "r'' ∉ RID⇩G s⇩2"
by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s⇩1_r fork(3))+
have l_fresh_right: "l ∉ LID⇩G s⇩2'"
by (rule only_new_introduces_lids'[OF right]) (simp add: side fork(2))+
show ?thesis by (rule local_and_fork_commute[OF s⇩2 fork(1)]) (use fork(1-2) neq s⇩2 l_fresh_right r''_fresh_left s⇩1_r in auto)
next
case join
show ?thesis by (rule SLC_sym, rule SLC_join, use join left_step neq in auto)
next
case join⇩ε
show ?thesis by (rule SLC_sym, rule SLC_join⇩ε, use join⇩ε left_step neq in auto)
qed
qed

subsubsection ‹Case fork›

lemma SLC_fork:
assumes
s⇩1_r: "s⇩1 r = Some (σ, τ, ℰ [Rfork e])" and
s⇩2: "s⇩2 = (s⇩1(r ↦ (σ, τ, ℰ[VE (Rid left_forkee)]), left_forkee ↦ (σ;;τ, ε, e)))" and
side: "left_forkee ∉ RID⇩G s⇩1" and
right: "revision_step r' s⇩1 s⇩2'" and
neq: "r ≠ r'" and
reach: "reachable (s⇩1 :: ('r,'l,'v) global_state)" and
rid_inf: "infinite (UNIV :: 'r set)"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof -
have left_step: "revision_step r s⇩1 s⇩2" using s⇩1_r s⇩2 side by (auto simp add: ID_distr_global_conditional)
show ?thesis
proof (use right in ‹cases rule: revision_stepE›)
case app
show ?thesis by (rule SLC_sym, rule SLC_app) (use assms(1-5) app in ‹auto simp add: ID_distr_global_conditional›)
next
case ifTrue
show ?thesis by (rule SLC_sym, rule SLC_ifTrue) (use assms(1-5) ifTrue in ‹auto simp add: ID_distr_global_conditional›)
next
case ifFalse
show ?thesis by (rule SLC_sym, rule SLC_ifFalse) (use assms(1-5) ifFalse in ‹auto simp add: ID_distr_global_conditional›)
next
case (new _ _ _ _ l) (* symmetry is intentionally not exploited: this would require the lid_inf assumption *)
have l_fresh_left: "l ∉ LID⇩G s⇩2"
by (rule only_new_introduces_lids'[OF left_step]) (simp add: s⇩1_r new(3))+
have r''_fresh_right: "left_forkee ∉ RID⇩G s⇩2'"
by (rule only_fork_introduces_rids'[OF right]) (simp add: side new(2))+
show ?thesis by (rule SLC_sym, rule local_and_fork_commute[OF new(1) s⇩2]) (use new(1-2) neq s⇩1_r r''_fresh_right l_fresh_left s⇩2 in auto)
next
case get
show ?thesis by (rule SLC_sym, rule SLC_get) (use assms(1-5) get in ‹auto simp add: ID_distr_global_conditional›)
next
case set
show ?thesis by (rule SLC_sym, rule SLC_set) (use assms(1-5) set in ‹auto simp add: ID_distr_global_conditional›)
next
case (fork σ' τ' ℰ' e' right_forkee)
have r'_unchanged_left: "s⇩2 r' = s⇩1 r'" using side fork(2) neq s⇩2 by auto
have r_unchanged_right: "s⇩2' r = s⇩1 r" using fork(1,3) neq s⇩1_r by auto
have "r ≠ left_forkee" using s⇩1_r side by auto
have "r ≠ right_forkee" using fork(3) s⇩1_r by auto
have "r' ≠ left_forkee" using fork(2) side by auto
have "r' ≠ right_forkee" using fork(2) fork(3) by auto
show ?thesis
proof (cases "left_forkee = right_forkee")
case True
obtain r'' where r''_fresh_left: "r'' ∉ RID⇩G s⇩2"
using RID⇩G_finite_invariant ex_new_if_finite left_step reach reachable_imp_identifiers_finite(1) rid_inf by blast
hence "r'' ≠ left_forkee" using assms(2) by auto
have "r'' ≠ r" using r''_fresh_left s⇩2 by auto
have "r'' ≠ r'" using fork(2) r''_fresh_left r'_unchanged_left by auto
have "r'' ∉ RID⇩G (s⇩1(r ↦ (σ, τ, ℰ[VE (Rid left_forkee)])))"
by (metis (mono_tags, lifting) RID⇩G_def True UnI1 ‹r ≠ right_forkee› domIff fun_upd_other fun_upd_triv in_restricted_global_in_updated_global(1) fork(3) r''_fresh_left s⇩2)
hence "r'' ∉ RID⇩G (s⇩1(r := None))" by blast
have r''_fresh_s⇩1: "r'' ∉ RID⇩G s⇩1"
using ‹r ≠ left_forkee› s⇩2 r''_fresh_left s⇩1_r ‹r'' ≠ r› ‹r'' ∉ RID⇩G (s⇩1(r := None))›
have r''_fresh_right: "r'' ∉ RID⇩G s⇩2'"
using True ‹r'' ≠ left_forkee› ‹r' ≠ right_forkee› ‹r'' ≠ r'› r''_fresh_s⇩1 fork(2) r''_fresh_s⇩1
by (auto simp add: fork(1) ID_distr_global_conditional fun_upd_twist)
let ?α = "id(left_forkee := r'', r'' := left_forkee)"
have bij_α: "bij ?α" by (simp add: swap_bij)
let "?s⇩3" = "s⇩2(r' ↦ (σ', τ', ℰ' [VE (Rid r'')]), r'' ↦ (σ';;τ', ε, e'))"
have left_convergence: "revision_step r' s⇩2 ?s⇩3"
using fork(2) r''_fresh_left r'_unchanged_left revision_step.fork by auto
let "?s⇩3'" = "s⇩2'(r ↦ (σ, τ, ℰ[VE (Rid r'')]), r'' ↦ (σ;;τ, ε, e))"
have right_convergence: "revision_step r s⇩2' ?s⇩3'"
using r''_fresh_right r_unchanged_right revision_step.fork s⇩1_r by auto
have equiv: "?s⇩3 ≈ ?s⇩3'"
proof (rule eq_statesI[of ?α id])
show "ℛ⇩G ?α id ?s⇩3 = ?s⇩3'"
proof -
have s⇩1: "ℛ⇩G ?α id s⇩1 = s⇩1" using r''_fresh_s⇩1 side by auto
have σ: "ℛ⇩S ?α id σ = σ" using r''_fresh_s⇩1 s⇩1_r True fork(3) by auto
have τ: "ℛ⇩S ?α id τ = τ" using r''_fresh_s⇩1 s⇩1_r True fork(3) by auto
have ℰ: "ℛ⇩C ?α id ℰ = ℰ"
proof
show "left_forkee ∉ RID⇩C ℰ" using s⇩1_r side by auto
show "r'' ∉ RID⇩C ℰ" using True ‹r ≠ right_forkee› r''_fresh_left s⇩2 by auto
qed
have e: "ℛ⇩E ?α id e = e"
proof
show "left_forkee ∉ RID⇩E e" using s⇩1_r side by auto
show "r'' ∉ RID⇩E e" using True ‹r ≠ right_forkee› r''_fresh_left s⇩2 by auto
qed
have σ': "ℛ⇩S ?α id σ' = σ'" using fork(2) r''_fresh_s⇩1 side by auto
have τ': "ℛ⇩S ?α id τ' = τ'" using fork(2) r''_fresh_s⇩1 side by auto
have ℰ': "ℛ⇩C ?α id ℰ' = ℰ'"
proof
show "left_forkee ∉ RID⇩C ℰ'" using fork(2) side by auto
show "r'' ∉ RID⇩C ℰ'" using fork(2) r''_fresh_s⇩1 by auto
qed
have e': "ℛ⇩E ?α id e' = e'"
proof
show "left_forkee ∉ RID⇩E e'" using fork(2) side by auto
show "r'' ∉ RID⇩E e'" using fork(2) r''_fresh_s⇩1 by auto
qed
show ?thesis using True fork(1) neq σ τ ℰ e  σ' τ' ℰ' e' s⇩1 s⇩2
bij_α ‹r'' ≠ left_forkee› ‹r' ≠ left_forkee› ‹r ≠ left_forkee› ‹r'' ≠ r› ‹r'' ≠ r'›
by auto
qed
show ?thesis using equiv left_convergence right_convergence by blast
next
case False
have right_forkee_fresh_left: "right_forkee ∉ RID⇩G s⇩2"
using False ‹r ≠ left_forkee› ‹r ≠ right_forkee› fork(3) s⇩1_r
by (auto simp add: s⇩2 ID_distr_global_conditional, auto)
have left_forkee_fresh_right: "left_forkee ∉ RID⇩G s⇩2'"
using False ‹r' ≠ right_forkee› ‹r' ≠ left_forkee› side fork(2)
by (auto simp add: fork(1) ID_distr_global_conditional fun_upd_twist)
show ?thesis
proof(rule exI[where x="s⇩2(r' := s⇩2' r', right_forkee := s⇩2' right_forkee)"],
rule exI[where x="s⇩2'(r := s⇩2 r, left_forkee := s⇩2 left_forkee)"],
rule SLC_commute)
show "s⇩2(r' := s⇩2' r', right_forkee := s⇩2' right_forkee) = s⇩2'(r := s⇩2 r, left_forkee := s⇩2 left_forkee)"
using False ‹r ≠ right_forkee› ‹r' ≠ left_forkee› ‹r' ≠ right_forkee› fork(1) neq s⇩2 by auto
show "revision_step r' s⇩2 (s⇩2(r' := s⇩2' r', right_forkee := s⇩2' right_forkee))"
using fork(1-2) r'_unchanged_left revision_step.fork right_forkee_fresh_left by auto
show "revision_step r s⇩2' (s⇩2'(r := s⇩2 r, left_forkee := s⇩2 left_forkee))"
using left_forkee_fresh_right r_unchanged_right revision_step.fork s⇩1_r s⇩2 by auto
qed
qed
next
case join
show ?thesis by (rule SLC_sym, rule SLC_join, use join left_step assms(3-5) in auto)
next
case join⇩ε
show ?thesis by (rule SLC_sym, rule SLC_join⇩ε, use join⇩ε left_step assms(3-5) in auto)
qed
qed

subsubsection ‹The theorem›

theorem strong_local_confluence:
assumes
l: "revision_step r s⇩1 s⇩2" and
r: "revision_step r' s⇩1 s⇩2'" and
reach: "reachable (s⇩1 :: ('r,'l,'v) global_state)" and
lid_inf: "infinite (UNIV :: 'l set)" and
rid_inf: "infinite (UNIV :: 'r set)"
shows
"∃s⇩3 s⇩3'. s⇩3 ≈ s⇩3' ∧ (revision_step r' s⇩2 s⇩3 ∨ s⇩2 = s⇩3) ∧ (revision_step r s⇩2' s⇩3' ∨ s⇩2' = s⇩3')"
proof (cases "r = r'")
case True
thus ?thesis by (metis l local_determinism r)
next
case neq: False
thus ?thesis by (cases rule: revision_stepE[OF l]) (auto simp add: assms SLC_app SLC_ifTrue
SLC_ifFalse SLC_new SLC_get SLC_set SLC_fork SLC_join SLC_join⇩ε)
qed

subsection ‹Diagram Tiling›

subsubsection ‹Strong local confluence diagrams›

lemma SLC:
assumes
s⇩1s⇩2: "s⇩1 ↝ s⇩2" and
s⇩1s⇩2': "s⇩1 ↝ s⇩2'" and
reach: "reachable (s⇩1 :: ('r,'l,'v) global_state)