Session Concurrent_Revisions

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 (RIDV: 'r, LIDV: 'l,'v) val = 
  CV const
| Var 'v
| Loc 'l
| Rid 'r
| Lambda 'v "('r,'l,'v) expr"
and (RIDE: 'r, LIDE: '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"
| Read "('r,'l,'v) expr"
| Assign "('r,'l,'v) expr" "('r,'l,'v) expr"
| Rfork "('r,'l,'v) expr"
| Rjoin "('r,'l,'v) expr"

datatype (RIDC: 'r, LIDC: '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"
| Read "('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)"
| "Read   e = Read (  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))"
| read: "redex (Read (VE (Loc l)))"
| 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 e1 e2); decompose e1  r   decompose (Apply e1 e2) (ApplyL  e2) r"
| rapply: " ¬redex (Apply (VE v) e); decompose e  r   decompose (Apply (VE v) e) (ApplyR v ) r"
| ite: " ¬redex (Ite e1 e2 e3); decompose e1  r   decompose (Ite e1 e2 e3) (Ite  e2 e3) r"
| ref: " ¬redex (Ref e); decompose e  r   decompose (Ref e) (Ref ) r"
| read: " ¬redex (Read e); decompose e  r   decompose (Read e) (Read ) r"
| lassign: " ¬redex (Assign e1 e2); decompose e1  r   decompose (Assign e1 e2) (AssignL  e2) r"
| rassign: " ¬redex (Assign (VE (Loc l)) e2); decompose e2  r   decompose (Assign (VE (Loc l)) e2) (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 e1 e2  r)
    have "(ApplyL  e2) [r] = Apply ([r]) e2" by simp
    also have "... = Apply e1 e2" using [r] = e1 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 r1  decompose e 2 r2  1 = 2  r1 = r2"
  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 RIDS :: "('r,'l,'v) store  'r set" where
  "RIDS σ   (RIDV ` ran σ)"

definition RIDL :: "('r,'l,'v) local_state  'r set" where
  "RIDL s  case s of (σ, τ, e)  RIDS σ  RIDS τ  RIDE e"

definition RIDG :: "('r,'l,'v) global_state  'r set" where
  "RIDG s  dom s   (RIDL ` ran s)"

subsubsection ‹Location identifiers›

definition LIDS :: "('r,'l,'v) store  'l set" where
  "LIDS σ  dom σ   (LIDV ` ran σ)"

definition LIDL :: "('r,'l,'v) local_state  'l set" where
  "LIDL s  case s of (σ, τ, e)  LIDS σ  LIDS τ  LIDE e"

definition LIDG :: "('r,'l,'v) global_state  'l set" where
  "LIDG s   (LIDL ` ran s)"

subsection ‹Inference rules›

subsubsection ‹Introduction and elimination rules›

lemma RIDSI [intro]: "σ l = Some v  r  RIDV v  r  RIDS σ"
  by (auto simp add: RIDS_def ran_def)

lemma RIDSE [elim]: "r  RIDS σ  (l v. σ l = Some v  r  RIDV v  P)  P"
  by (auto simp add: RIDS_def ran_def)

lemma RIDLI [intro, consumes 1]:
  assumes "s = (σ, τ, e)"
  shows
    "r  RIDS σ  r  RIDL s"
    "r  RIDS τ  r  RIDL s"
    "r  RIDE e  r  RIDL s"
  by (auto simp add: RIDL_def assms)

lemma RIDLE [elim]:
  " r  RIDL s; (σ τ e. s = (σ, τ, e)  (r  RIDS σ  P)  (r  RIDS τ  P)  (r  RIDE e  P)  P)  P   P" 
  by (cases s) (auto simp add: RIDL_def)

lemma RIDGI [intro]:
  "s r = Some v  r  RIDG s"
  "s r' = Some ls  r  RIDL ls  r  RIDG s"
   apply (simp add: RIDG_def domI)
  by (metis (no_types, lifting) RIDG_def UN_I UnI2 ranI)

lemma RIDGE [elim]:
  assumes
    "r  RIDG s"
    "r  dom s  P"
    "r' ls. s r' = Some ls  r  RIDL ls  P"
  shows P
  using assms by (auto simp add: RIDG_def ran_def)

lemma LIDSI [intro]:
  "σ l = Some v  l  LIDS σ"
  "σ l' = Some v  l  LIDV v  l  LIDS σ"
  by (auto simp add: LIDS_def ran_def)

lemma LIDSE [elim]:
  assumes 
    "l  LIDS σ"
    "l  dom σ  P"
    "l' v. σ l' = Some v  l  LIDV v  P"
  shows P
  using assms by (auto simp add: LIDS_def ran_def)

lemma LIDLI [intro]:
  assumes "s = (σ, τ, e)"
  shows
    "r  LIDS σ  r  LIDL s" 
    "r  LIDS τ  r  LIDL s" 
    "r  LIDE e  r  LIDL s"
  by (auto simp add: LIDL_def assms)

lemma LIDLE [elim]:
  " l  LIDL s; (σ τ e. s = (σ, τ, e)  (l  LIDS σ  P)  (l  LIDS τ  P)  (l  LIDE e  P)  P)  P   P" 
  by (cases s) (auto simp add: LIDL_def)

lemma LIDGI [intro]: "s r = Some ls  l  LIDL ls  l  LIDG s"
  by (auto simp add: LIDG_def LIDL_def ran_def)

lemma LIDGE [elim]: "l  LIDG s  (r ls. s r = Some ls  l  LIDL ls  P)  P"
  by (auto simp add: LIDG_def ran_def)

subsubsection ‹Distributive laws›

lemma ID_distr_completion [simp]: 
  "RIDE ([e]) = RIDC   RIDE e"
  "LIDE ([e]) = LIDC   LIDE e"
  by (induct rule: plug.induct) auto

lemma ID_restricted_store_subset_store: 
  "RIDS (σ(l := None))  RIDS σ"
  "LIDS (σ(l := None))  LIDS σ"
proof -
  show "RIDS (σ(l := None))  RIDS σ"
  proof (rule subsetI)
    fix r
    assume "r  RIDS (σ(l := None))"
    then obtain l' v where "(σ(l := None)) l' = Some v" and r_v: "r  RIDV 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  RIDS σ" using r_v by blast
  qed
next
  show "LIDS (σ(l := None))  LIDS σ"
  proof (rule subsetI)
    fix l'
    assume "l'  LIDS (σ(l := None))"
    hence "l'  dom (σ(l := None))  (l'' v. (σ(l := None)) l'' = Some v  l'  LIDV v)" by blast
    thus "l'  LIDS σ"
    proof (rule disjE)
      assume "l'  dom (σ(l := None))"
      thus "l'  LIDS σ" by auto
    next
      assume "l'' v. (σ(l := None)) l'' = Some v  l'  LIDV v"
      then obtain l'' v where "(σ(l := None)) l'' = Some v" and l'_in_v: "l'  LIDV v" by blast
      hence "σ l'' = Some v" by (cases "l = l''", auto)
      thus "l'  LIDS σ" using l'_in_v by blast
    qed
  qed
qed

lemma in_restricted_store_in_unrestricted_store [intro]: 
  "r  RIDS (σ(l := None))  r  RIDS σ"
  "l'  LIDS (σ(l := None))  l'  LIDS σ" 
  by (meson contra_subsetD ID_restricted_store_subset_store)+

lemma in_restricted_store_in_updated_store [intro]: 
  "r  RIDS (σ(l := None))  r  RIDS (σ(l  v))" 
  "l'  LIDS (σ(l := None))  l'  LIDS (σ(l  v))"
proof -
  assume "r  RIDS (σ(l := None))"
  hence "r  RIDS (σ |` (- {l}))" by (simp add: restrict_complement_singleton_eq)
  hence "r  RIDS (σ(l  v) |` (- {l}))" by simp
  hence "r  RIDS (σ(l := Some v, l := None))" by (simp add: restrict_complement_singleton_eq)
  thus "r  RIDS (σ(l  v))" by blast
next
  assume "l'  LIDS (σ(l := None))"
  hence "l'  LIDS (σ |` (- {l}))" by (simp add: restrict_complement_singleton_eq)
  hence "l'  LIDS (σ(l  v) |` (- {l}))" by simp
  hence "l'  LIDS (σ(l := Some v, l := None))" by (simp add: restrict_complement_singleton_eq)
  thus "l'  LIDS (σ(l  v))" by blast
qed

lemma ID_distr_store [simp]:
  "RIDS (τ(l  v)) = RIDS (τ(l := None))  RIDV v"
  "LIDS (τ(l  v)) = insert l (LIDS (τ(l := None))  LIDV v)"
proof -
  show "RIDS (τ(l  v)) = RIDS (τ(l := None))  RIDV v"
  proof (rule set_eqI, rule iffI)
    fix r
    assume "r  RIDS (τ(l  v))"
    then obtain l' v' where "(τ(l  v)) l' = Some v'" "r  RIDV v'" by blast
    thus "r  RIDS (τ(l := None))  RIDV v" by (cases "l' = l") auto
  qed auto
next
  show "LIDS (τ(l  v)) = insert l (LIDS (τ(l := None))  LIDV v)"
  proof (rule set_eqI, rule iffI)
    fix l'
    assume "l'  LIDS (τ(l  v))"
    hence "l'  dom (τ(l  v))  (l'' v'. (τ(l  v)) l'' = Some v'  l'  LIDV v')" by blast
    thus "l'  insert l (LIDS (τ(l := None))  LIDV v)"
    proof (rule disjE)
      assume "l'  dom (τ(l  v))"
      thus "l'  insert l (LIDS (τ(l := None))  LIDV v)" by (cases "l' = l") auto
    next
      assume "l'' v'. (τ(l  v)) l'' = Some v'  l'  LIDV v'"
      then obtain l'' v' where "(τ(l  v)) l'' = Some v'" "l'  LIDV v'" by blast
      thus "l'  insert l (LIDS (τ(l := None))  LIDV v)" by (cases "l = l''") auto
    qed
  qed auto
qed

lemma ID_distr_local [simp]: 
  "LIDL (σ,τ,e) = LIDS σ  LIDS τ  LIDE e"
  "RIDL (σ,τ,e) = RIDS σ  RIDS τ  RIDE e"
  by (simp add: LIDL_def RIDL_def)+

lemma ID_restricted_global_subset_unrestricted:
  "LIDG (s(r := None))  LIDG s"
  "RIDG (s(r := None))  RIDG s"
proof -
  show "LIDG (s(r := None))  LIDG s"
  proof (rule subsetI)
    fix l
    assume "l  LIDG (s(r := None))"
    then obtain r'' ls where "(s(r := None)) r'' = Some ls" and l_in_ls: "l  LIDL 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  LIDG s" using l_in_ls by blast
  qed
next
  show "RIDG (s(r := None))  RIDG s"
  proof (rule subsetI)
    fix r'
    assume "r'  RIDG (s(r := None))"
    hence "r'  dom (s(r := None))  (r'' ls. (s(r := None)) r'' = Some ls  r'  RIDL ls)" by blast
    thus "r'  RIDG s"
    proof (rule disjE)
      assume "r'' ls. (s(r := None)) r'' = Some ls  r'  RIDL ls"
      then obtain r'' ls where "(s(r := None)) r'' = Some ls" and r'_in_ls: "r'  RIDL 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'  RIDG s" using r'_in_ls by blast
    qed auto
  qed
qed

lemma in_restricted_global_in_unrestricted_global [intro]: 
  "r'  RIDG (s(r := None))  r'  RIDG s"
  "l  LIDG (s(r := None))  l  LIDG s"
  by (simp add: ID_restricted_global_subset_unrestricted rev_subsetD)+

lemma in_restricted_global_in_updated_global [intro]: 
  "r'  RIDG (s(r := None))  r'  RIDG (s(r  ls))" 
  "l  LIDG (s(r := None))  l  LIDG (s(r  ls))"
proof -
  assume "r'  RIDG (s(r := None))"
  hence "r'  RIDG (s |` (- {r}))" by (simp add: restrict_complement_singleton_eq)
  hence "r'  RIDG (s(r  ls) |` (- {r}))" by simp
  hence "r'  RIDG (s(r := Some ls, r := None))" by (simp add: restrict_complement_singleton_eq)
  thus "r'  RIDG (s(r  ls))" by blast
next
  assume "l  LIDG (s(r := None))"
  hence "l  LIDG (s |` (- {r}))" by (simp add: restrict_complement_singleton_eq)
  hence "l  LIDG (s(r  ls) |` (- {r}))" by simp
  hence "l  LIDG (s(r := Some ls, r := None))" by (simp add: restrict_complement_singleton_eq)
  thus "l  LIDG (s(r  ls))" by blast
qed

lemma ID_distr_global [simp]:
  "RIDG (s(r  ls)) = insert r (RIDG (s(r := None))  RIDL ls)"
  "LIDG (s(r  ls)) = LIDG (s(r := None))  LIDL ls"
proof -
  show "LIDG (s(r  ls)) = LIDG (s(r := None))  LIDL ls"
  proof (rule set_eqI)
    fix l
    show "(l  LIDG (s(r  ls))) = (l  LIDG (s(r := None))  LIDL ls)"
    proof (rule iffI)
      assume "l  LIDG (s(r  ls))"
      from this obtain r' ls' where "(s(r  ls)) r' = Some ls'" "l  LIDL ls'" by auto
      thus "l  LIDG (s(r := None))  LIDL ls" by (cases "r = r'") auto
    qed auto
  qed
  show "RIDG (s(r  ls)) = insert r (RIDG (s(r := None))  RIDL ls)"
  proof (rule set_eqI)
    fix r'
    show "(r'  RIDG (s(r  ls))) = (r'  insert r (RIDG (s(r := None))  RIDL ls))"
    proof (rule iffI, clarsimp)
      assume r'_g: "r'  RIDG (s(r  ls))" and neq: "r'  r" and r'_l: "r'  RIDL ls"
      show "r'  RIDG (s(r := None))"
      proof (rule RIDGE[OF r'_g])
        assume "r'  dom (s(r  ls))"
        thus ?thesis by (simp add: RIDG_def neq)
      next
        fix ls' r''
        assume r'_in_range:"(s(r  ls)) r'' = Some ls'" "r'  RIDL 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]:
  "RIDS (σ;;τ)  RIDS σ  RIDS τ"
  "LIDS (σ;;τ)  LIDS σ  LIDS τ"
proof -
  show "RIDS (σ;;τ)  RIDS σ  RIDS τ"
  proof (rule subsetI)
    fix r
    assume "r  RIDS (σ;;τ)"
    from this obtain l v where "(σ;;τ) l = Some v" and "r  RIDV v" by blast
    thus "r  RIDS σ  RIDS τ" by (cases "l  dom τ") auto
  qed
  show "LIDS (σ;;τ)  LIDS σ  LIDS τ"
  proof (rule subsetI)
    fix l
    assume "l  LIDS (σ;;τ)"
    hence "l  dom (σ;;τ)  (l' v. (σ;;τ) l' = Some v  l  LIDV v)" by blast
    thus "l  LIDS σ  LIDS τ"
    proof (rule disjE)
      assume "l  dom (σ;;τ)"
      thus "l  LIDS σ  LIDS τ" by (cases "l  dom τ") auto
    next 
      assume "l' v. (σ;;τ) l' = Some v  l  LIDV v"
      from this obtain l' v where "(σ;;τ) l' = Some v" "l  LIDV v" by blast
      thus "l  LIDS σ  LIDS τ" by (cases "l'  dom τ") auto
    qed
  qed
qed

lemma in_combination_in_component [intro]: 
  "r  RIDS (σ;;τ)  r  RIDS σ  r  RIDS τ"
  "r  RIDS (σ;;τ)  r  RIDS τ  r  RIDS σ"
  "l  LIDS (σ;;τ)  l  LIDS σ  l  LIDS τ"
  "l  LIDS (σ;;τ)  l  LIDS τ  l  LIDS σ"
  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'  LIDV v"
  shows
    "l'  LIDS τ  l'  LIDS σ"
    "l'  LIDS σ  l'  LIDS τ"
  by (metis LIDSI(2) combine.simps l'_in_v maps_to_v)+

lemma elim_trivial_restriction [simp]: "l  LIDS τ  (τ(l := None)) = τ" 
  by (simp add: LIDS_def domIff fun_upd_idem)

lemma ID_distr_global_conditional:
  "s r = Some ls  RIDG s = insert r (RIDG (s(r := None))  RIDL ls)"
  "s r = Some ls  LIDG s = LIDG (s(r := None))  LIDL ls"
proof -
  assume "s r = Some ls"
  hence s_as_upd: "s = (s(r  ls))" by (simp add: fun_upd_idem)
  show "RIDG s = insert r (RIDG (s(r := None))  RIDL ls)" by (subst s_as_upd, simp)
  show "LIDG s = LIDG (s(r := None))  LIDL 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))"

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

lemmaG_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›

lemmaSI [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, substS.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

lemmaGI [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, substG.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]
lemmaS_id [simp]: "ℛS id id σ = σ" by auto
lemmaL_id [simp]: "ℛL id id ls = ls" by (cases ls) simp
lemmaG_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]
lemmaS_comp [simp]: " bij β; bij β'  S α' β' (S α β s) =S (α'  α) (β'  β) s"
  by (auto simp add: o_inv_distrib)
lemmaL_comp [simp]: " bij β; bij β'  L α' β' (L α β ls) =L (α'  α) (β'  β) ls"
  by (cases ls) simp
lemmaG_comp [simp]: " bij α; bij α'; bij β; bij β'  G α' β' (G α β s) =G (α'  α) (β'  β) s"
  by (rule ext) (auto simp add: o_inv_distrib)

subsubsection Inverse

lemmaV_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)
lemmaE_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)
lemmaC_inv [simp]: " bij α; bij β   (C (inv α) (inv β) ℰ' = ) = (C α β  = ℰ')"
  by (auto simp add: bijection.intro bijection.inv_comp_right bijection.inv_comp_left)
lemmaS_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)
lemmaL_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)
lemmaG_inv [simp]: " bij α; bij β   (G (inv α) (inv β) s' = s) = (G α β s = s')"
  by (auto simp add: bij_imp_bij_inv bijection.intro bijection.inv_comp_right bijection.inv_comp_left)

subsubsection Equivalence

definition eq_states :: "('r,'l,'v) global_state  ('r,'l,'v) global_state  bool" ("_  _" [100, 100]) where
  "s  s'  α β. bij α  bij β G α β s = s'"

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

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

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

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

subsection ‹Distributive laws›

subsubsection Expression

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

subsubsection Store

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

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

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

subsubsection Global 

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

subsection ‹Miscellaneous laws›

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

subsection Swaps

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

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

lemma eliminate_renaming_val_expr [simp]:
  fixes
    v :: "('r,'l,'v) val" and
    e :: "('r,'l,'v) expr"
  shows
    "l  LIDV v  V α (β(l := l')) v = V α β v"
    "l  LIDE e  E α (β(l := l')) e = E α β e"
    "r  RIDV v  V (α(r := r')) β v = V α β v"
    "r  RIDE e  E (α(r := r')) β e = E α β e"
proof -
  have "(α β r r'. r  RIDV v  V (α(r := r')) β v = V α β v) 
    (α β r r'. r  RIDE e  E (α(r := r')) β e = E α β e)"
    by (induct rule: val_expr.induct) simp+
  thus 
    "r  RIDV v  V (α(r := r')) β v = V α β v" 
    "r  RIDE e  E (α(r := r')) β e = E α β e"
    by simp+
  have "(α β l l'. l  LIDV v  V α (β(l := l')) v = V α β v) 
    (α β l l'. l  LIDE e  E α (β(l := l')) e = E α β e)"
    by (induct rule: val_expr.induct) simp+
  thus 
    "l  LIDV v  V α (β(l := l')) v = V α β v" and
    "l  LIDE e  E α (β(l := l')) e = E α β e"
    by simp+
qed

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

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

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

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

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

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

lemma eliminate_swap_global_rid [simp, intro]:
  "r  RIDG s  r'  RIDG s G (id(r := r', r' := r)) id s = s"
  by (ruleGI[OF swap_bij], ((rule sym, auto)[1])+)

lemma eliminate_swap_global_lid [simp, intro]:
  "l  LIDG s  l'  LIDG s G id (id(l := l', l' := l)) s = s"
  by (ruleGI) (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: "RIDE (subst e x e')  RIDE e  RIDE e'" and
    subst_introduces_no_lids: "LIDE (subst e x e')  LIDE e  LIDE e'"
begin

lemma rid_substE [dest]: "r  RIDE (subst (VE v) x e)  r  RIDE e  r  RIDV v"
  using subst_introduces_no_rids by fastforce

lemma lid_substE [dest]: "l  LIDE (subst (VE v) x e)  l  LIDE e  l  LIDV 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_substV :: "('r,'l,nat) expr  nat  ('r,'l,nat) val  ('r,'l,nat) expr" and
  nat_substE :: "('r,'l,nat) expr  nat  ('r,'l,nat) expr  ('r,'l,nat) expr"
  where
  "nat_substV e x (CV const) = VE (CV const)"
| "nat_substV e x (Var x') = (if x = x' then e else VE (Var x'))"
| "nat_substV e x (Loc l) = VE (Loc l)"
| "nat_substV e x (Rid r) = VE (Rid r)"
| "nat_substV 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_substE e x (ℛ𝒱E (id(y := z)) e')))"
| "nat_substE e x (VE v') = nat_substV e x v'"
| "nat_substE e x (Apply l r) = Apply (nat_substE e x l) (nat_substE e x r)"
| "nat_substE e x (Ite e1 e2 e3) = Ite (nat_substE e x e1) (nat_substE e x e2) (nat_substE e x e3)"
| "nat_substE e x (Ref e') = Ref (nat_substE e x e')"
| "nat_substE e x (Read e') = Read (nat_substE e x e')"
| "nat_substE e x (Assign l r) = Assign (nat_substE e x l) (nat_substE e x r)"
| "nat_substE e x (Rfork e') = Rfork (nat_substE e x e')"
| "nat_substE e x (Rjoin e')  = Rjoin (nat_substE e x e')"
  by pat_completeness auto
termination 
  by (relation "measure (λx. case x of Inl (e,x,v)  size v | Inr (e,x,e')  size e')")
     (auto simp add: var_renaming_preserves_size(2))

subsubsection ‹Proof obligations›

lemma nat_substE_distr:
  fixes e :: "('r,'l,nat) expr"
  shows "E α β (nat_substE e x e') = nat_substE (E α β e) x (E α β e')"
proof -
  fix v' :: "('r,'l,nat) val"
  have
    "(α β x e ζ. E α β (nat_substV e x (ℛ𝒱V ζ v')) = nat_substV (E α β e) x (V α β (ℛ𝒱V ζ v'))) 
     (α β x e ζ. E α β (nat_substE e x (ℛ𝒱E ζ e')) = nat_substE (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_substE e x (ℛ𝒱E id e')) = nat_substE (E α β e) x (E α β (ℛ𝒱E id e'))" by blast
  thus ?thesis by simp
qed

lemma nat_substE_introduces_no_rids:
  fixes e' :: "('r,'l,nat) expr"
  shows "RIDE (nat_substE e x e')  RIDE e  RIDE e'"
proof -
  fix v' :: "('r,'l,nat) val"
  have 
    "(x e. ζ. RIDE (nat_substV e x (ℛ𝒱V ζ v'))  RIDE e  RIDV (ℛ𝒱V ζ v')) 
     (x e. ζ. RIDE (nat_substE e x (ℛ𝒱E ζ e'))  RIDE e  RIDE (ℛ𝒱E ζ e'))"
    by (induct rule: val_expr.induct) (auto 0 4 simp add: expr.set_map(1))
  hence "RIDE (nat_substE e x (ℛ𝒱E id e'))  RIDE e  RIDE (ℛ𝒱E id e')" by blast
  thus ?thesis by simp
qed

lemma nat_substE_introduces_no_lids: 
  fixes e' :: "('r,'l,nat) expr"
  shows "LIDE (nat_substE e x e')  LIDE e  LIDE e'"
proof -
  fix v' :: "('r,'l,nat) val"
  have 
    "(x e. ζ. LIDE (nat_substV e x (ℛ𝒱V ζ v'))  LIDE e  LIDV (ℛ𝒱V ζ v')) 
     (x e. ζ. LIDE (nat_substE e x (ℛ𝒱E ζ e'))  LIDE e  LIDE (ℛ𝒱E ζ e'))"
    by (induct rule: val_expr.induct) (auto 0 4 simp add: expr.set_map(2))
  hence "LIDE (nat_substE e x (ℛ𝒱E id e'))  LIDE e  LIDE (ℛ𝒱E id e')" by blast
  thus ?thesis by simp
qed

lemma nat_substE_models_substitution: "substitution nat_substE"
  by (simp add: nat_substE_distr nat_substE_introduces_no_lids nat_substE_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  LIDG 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'  RIDG 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 "LIDG s'  LIDG 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: LIDSI(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 "RIDG s'  RIDG 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)
qed (auto simp add: ID_distr_global_conditional)

lemma only_fork_introduces_rids' [dest]:
  assumes 
    step: "revision_step r s s'" and
    not_fork: "σ τ  e. s r  Some (σ,τ,[Rfork e])"
  shows "r'  RIDG s  r'  RIDG 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  LIDG s  l  LIDG s'"
  using assms by blast

subsection ‹Domain subsumption›

subsubsection Definitions

definition domains_subsume :: "('r,'l,'v) local_state  bool" ("𝒮") where
  "𝒮 ls = (LIDL 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
  "𝒜 r1 r2 s = (r2  RIDL (the (s r1))  (LIDS ((the (s r2))σ)  doms (the (s r1))))"

lemma subsumes_accessibleI [intro]: 
  "(r2  RIDL (the (s r1))  LIDS ((the (s r2))σ)  doms (the (s r1)))  𝒜 r1 r2 s"
  using subsumes_accessible_def by auto

definition subsumes_accessible_globally :: "('r,'l,'v) global_state  bool" ("𝒜G") where
  "𝒜G s = (r1 r2. r1  dom s  r2  dom s  𝒜 r1 r2 s)"

lemma subsumes_accessible_globallyI [intro]:
  "(r1 σ1 τ1 e1 r2 σ2 τ2 e2. s r1 = Some (σ1,τ1,e1)  s r2 = Some (σ2,τ2,e2)  𝒜 r1 r2 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 "LIDL (the (s' r))  LIDS σ'  LIDS τ'  LIDC ℰ'  LIDE e'  LIDV v'" using app(1) by auto
        also have "... = LIDL (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 "LIDL (the (s' r))  LIDL (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 "LIDL (the (s' r))  LIDL (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 "LIDL (the (s' r)) = insert l' (LIDS σ'  LIDS τ'  LIDV v'  LIDC ℰ')"
        proof -
          have "l'  LIDS τ'" using new(2-3) by auto
          thus ?thesis using new(1) by auto
        qed
        also have "... = insert l' (LIDL (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 "LIDL (the (s' r)) = LIDL (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 "LIDL (the (s' r))  LIDL (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 "LIDL (the (s' r))  LIDL (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 "LIDL (the (s' r''))  LIDL (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 "LIDL (the (s' r))  LIDL (the (s r))  LIDS τ''" using join by auto
        also have "...  doms (the (s r))  LIDS τ''"
          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))  LIDL (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 τ'  LIDS σ''  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''  RIDL (the (s r))" using join by auto
          have "LIDS σ''  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 r1 σ1 τ1 e1 r2 σ2 τ2 e2
    assume 
      s'_r1: "s' r1 = Some (σ1, τ1, e1)" and
      s'_r2: "s' r2 = Some (σ2, τ2, e2)"
    show "𝒜 r1 r2 s'"
    proof (cases "r1 = r2")
      case True
      then show ?thesis using 𝒮G_imp_𝒜_refl 𝒮G s' s'_r1 by blast
    next
      case r1_neq_r2: False
      have r1_nor_r2_updated_implies_thesis: "s' r1 = s r1  s' r2 = s r2  ?thesis"
      proof - 
        assume r1_unchanged: "s' r1 = s r1" and r2_unchanged: "s' r2 = s r2"
        have "𝒜 r1 r2 s"
          by (metis 𝒜G_s domIff option.discI r1_unchanged r2_unchanged s'_r1 s'_r2 subsumes_accessible_globally_def)
        show ?thesis using 𝒜 r1 r2 s r1_unchanged r2_unchanged subsumes_accessible_def by auto
      qed
      have r1_or_r2_updated_implies_thesis: "s' r1  s r1  s' r2  s r2  ?thesis"
      proof -
        assume r1_or_r2_updated: "s' r1  s r1  s' r2  s r2"
        show ?thesis
        proof (use step in cases rule: revision_stepE›)
          case app
          have "r1 = r  r2 = r" by (metis fun_upd_other app(1) r1_or_r2_updated)
          then show ?thesis
          proof (rule disjE)
            assume r1_eq_r: "r1 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS ((the (s' r2))σ)  LIDS ((the (s r2))σ)" using app by auto
              also have "...  doms (the (s r1))" 
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using app r2_in_s'_r1 r1_eq_r by auto
                have "𝒜 r1 r2 s"
                  by (metis 𝒜G_s domI fun_upd_other app r1_eq_r s'_r2 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" using app by auto
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          next
            assume r2_eq_r: "r2 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS (the (s' r2)σ) = LIDS (the (s r2)σ)" using app by auto
              also have "...  doms (the (s r1))"
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using app(1) r1_neq_r2 r2_eq_r r2_in_s'_r1 by auto
                have "𝒜 r1 r2 s"
                  by (metis (no_types, lifting) 𝒜G_s domIff fun_upd_other app option.discI r2_eq_r s'_r1 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" by (simp add: app)
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          qed
        next
          case ifTrue
          have "r1 = r  r2 = r" by (metis fun_upd_other ifTrue(1) r1_or_r2_updated)
          then show ?thesis
          proof (rule disjE)
            assume r1_eq_r: "r1 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS ((the (s' r2))σ)  LIDS ((the (s r2))σ)" using ifTrue by auto
              also have "...  doms (the (s r1))" 
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using ifTrue r2_in_s'_r1 r1_eq_r by auto
                have "𝒜 r1 r2 s"
                  by (metis 𝒜G_s domI fun_upd_other ifTrue r1_eq_r s'_r2 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" using ifTrue by auto
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          next
            assume r2_eq_r: "r2 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS (the (s' r2)σ) = LIDS (the (s r2)σ)" using ifTrue by auto
              also have "...  doms (the (s r1))"
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using ifTrue(1) r1_neq_r2 r2_eq_r r2_in_s'_r1 by auto
                have "𝒜 r1 r2 s"
                  by (metis (no_types, lifting) 𝒜G_s domIff fun_upd_other ifTrue option.discI r2_eq_r s'_r1 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" by (simp add: ifTrue)
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          qed
        next
          case ifFalse
          have "r1 = r  r2 = r" by (metis fun_upd_other ifFalse(1) r1_or_r2_updated)
          then show ?thesis
          proof (rule disjE)
            assume r1_eq_r: "r1 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS ((the (s' r2))σ)  LIDS ((the (s r2))σ)" using ifFalse by auto
              also have "...  doms (the (s r1))" 
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using ifFalse r2_in_s'_r1 r1_eq_r by auto
                have "𝒜 r1 r2 s"
                  by (metis 𝒜G_s domI fun_upd_other ifFalse r1_eq_r s'_r2 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" using ifFalse by auto
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          next
            assume r2_eq_r: "r2 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS (the (s' r2)σ) = LIDS (the (s r2)σ)" using ifFalse by auto
              also have "...  doms (the (s r1))"
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using ifFalse(1) r1_neq_r2 r2_eq_r r2_in_s'_r1 by auto
                have "𝒜 r1 r2 s"
                  by (metis (no_types, lifting) 𝒜G_s domIff fun_upd_other ifFalse option.discI r2_eq_r s'_r1 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" by (simp add: ifFalse)
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          qed
        next
          case new
          have "r1 = r  r2 = r" by (metis fun_upd_other new(1) r1_or_r2_updated)
          then show ?thesis
          proof (rule disjE)
            assume r1_eq_r: "r1 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS ((the (s' r2))σ)  LIDS ((the (s r2))σ)" using new by auto
              also have "...  doms (the (s r1))" 
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using new r2_in_s'_r1 r1_eq_r by auto
                have "𝒜 r1 r2 s"
                  by (metis 𝒜G_s domI fun_upd_other new(1-2) r1_eq_r s'_r2 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" using new by auto
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          next
            assume r2_eq_r: "r2 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS (the (s' r2)σ) = LIDS (the (s r2)σ)" using new by auto
              also have "...  doms (the (s r1))"
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using new(1) r1_neq_r2 r2_eq_r r2_in_s'_r1 by auto
                have "𝒜 r1 r2 s"
                  by (metis (no_types, lifting) 𝒜G_s domIff fun_upd_other new(1-2) option.discI r2_eq_r s'_r1 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" by (auto simp add: new)
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          qed
        next
          case get
          have "r1 = r  r2 = r" by (metis fun_upd_other get(1) r1_or_r2_updated)
          then show ?thesis
          proof (rule disjE)
            assume r1_eq_r: "r1 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS ((the (s' r2))σ)  LIDS ((the (s r2))σ)" using get by auto
              also have "...  doms (the (s r1))" 
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using get r2_in_s'_r1 r1_eq_r apply auto
                  by (meson RIDSI) (* by (auto 1 3) *)
                have "𝒜 r1 r2 s"
                  by (metis 𝒜G_s domI fun_upd_other get(1-2) r1_eq_r s'_r2 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" using get by auto
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          next
            assume r2_eq_r: "r2 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS (the (s' r2)σ) = LIDS (the (s r2)σ)" using get by auto
              also have "...  doms (the (s r1))"
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using get(1) r1_neq_r2 r2_eq_r r2_in_s'_r1 by auto
                have "𝒜 r1 r2 s"
                  by (metis (no_types, lifting) 𝒜G_s domIff fun_upd_other get(1-2) option.discI r2_eq_r s'_r1 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" by (simp add: get)
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          qed
        next
          case set
          have "r1 = r  r2 = r" by (metis fun_upd_other set(1) r1_or_r2_updated)
          then show ?thesis
          proof (rule disjE)
            assume r1_eq_r: "r1 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS ((the (s' r2))σ)  LIDS ((the (s r2))σ)" using set by auto
              also have "...  doms (the (s r1))" 
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using set r2_in_s'_r1 r1_eq_r by auto
                have "𝒜 r1 r2 s"
                  by (metis 𝒜G_s domI fun_upd_other set(1-2) r1_eq_r s'_r2 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" using set by auto
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          next
            assume r2_eq_r: "r2 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS (the (s' r2)σ) = LIDS (the (s r2)σ)" using set by auto
              also have "...  doms (the (s r1))"
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))" using set(1) r1_neq_r2 r2_eq_r r2_in_s'_r1 by auto
                have "𝒜 r1 r2 s"
                  by (metis (no_types, lifting) 𝒜G_s domIff fun_upd_other set(1-2) option.discI r2_eq_r s'_r1 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))" by (auto simp add: set)
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" 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)" 
            by (simp add: local.fork(1))
          have case1: "r1 = r  r2  r  r2  r'  ?thesis"
          proof (rule subsumes_accessibleI)
            assume "r1 = r" "r2  r" "r2  r'"
            assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
            have "LIDS ((the (s' r2))σ)  LIDS ((the (s r2))σ)" using fork(1-2) by (simp add: r2  r')
            also have "...  doms (the (s r1))" 
            proof -
              have r2_in_s_r1: "r2  RIDL (the (s r1))" using fork r1 = r r2  r' r2_in_s'_r1 s'_r by auto
              have "𝒜 r1 r2 s"
                by (metis (no_types, lifting) 𝒜G_s r1 = r r2  r' domIff fun_upd_other fork(1-2) option.discI s'_r2 subsumes_accessible_globally_def)
              show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
            qed
            also have "...  doms (the (s' r1))" by (simp add: r1 = r fork(2) s'_r)
            finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
          qed
          have case2: "r1  r  r1  r'  r2 = r  ?thesis"
          proof (rule subsumes_accessibleI)
            assume "r1  r" "r1  r'" "r2 = r"
            assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
            have "LIDS ((the (s' r2))σ)  LIDS ((the (s r2))σ)"
              using r1  r' r1  r fork r2_in_s'_r1 s'_r1 by auto
            also have "...  doms (the (s r1))" 
            proof -
              have r2_in_s_r1: "r2  RIDL (the (s r1))" using r1  r' r1  r fork(1) r2_in_s'_r1 by auto
              have "𝒜 r1 r2 s"
                by (metis (no_types, lifting) 𝒜G_s r1  r' r2 = r domIff fun_upd_other fork(1-2) option.discI s'_r1 subsumes_accessible_globally_def)
              show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by auto
            qed
            also have "...  doms (the (s' r1))" by (simp add: r1  r' r1  r fork(1))
            finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
          qed
          have case3: "r1 = r'  r2  r  r2  r'  ?thesis"
          proof (rule subsumes_accessibleI)
            fix l
            assume "r1 = r'" "r2  r" "r2  r'"
            assume "r2  RIDL (the (s' r1))"
            hence "r2  RIDL (the (s r))" using RIDLI(3) r1 = r' fork(2) s'_r' by auto
            have "s r2 = s' r2" by (simp add: r2  r' r2  r fork(1))
            hence "𝒜 r r2 s" using 𝒜G_s fork(2) s'_r2 subsumes_accessible_globally_def by auto
            hence "LIDS (the (s' r2)σ)  doms (the (s r))"
              by (simp add: r2  RIDL (the (s r)) s r2 = s' r2 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 "LIDS (the (s' r2)σ)  doms (the (s' r1))" using r1 = r' by blast
          qed
          have case4: "r1  r  r1  r'  r2 = r'  ?thesis"
          proof -
            assume "r1  r" "r1  r'" "r2 = r'"
            have "r2  RIDL (the (s r1))" using r1  r' r1  r r2 = r' fork(1,3) s'_r1 by auto
            hence "r2  RIDL (the (s' r1))" by (simp add: r1  r' r1  r fork(1))
            thus ?thesis by blast
          qed
          have case5: "r1 = r  r2 = r'  ?thesis"
          proof (rule subsumes_accessibleI)
            assume "r1 = r" "r2 = r'"
            have "LIDS ((the (s' r2))σ) = LIDS (σ;;τ)" by (simp add: r2 = r' s'_r')
            also have "...  LIDS σ  LIDS τ" by auto
            also have "...  LIDL (the (s' r1))" by (simp add: r1 = r s'_r)
            also have "...  doms (the (s' r1))"
              by (metis 𝒮G s' r1 = r domains_subsume_def domains_subsume_globally_def option.sel s'_r)
            finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
          qed
          have case6: "r1 = r'  r2 = r  ?thesis"
          proof (rule subsumes_accessibleI)
            assume "r1 = r'" "r2 = r" "r2  RIDL (the (s' r1))"
            have "LIDS (the (s' r2)σ)  LIDL (the (s' r2))" by (simp add: s'_r2 subsetI)
            also have "...  doms (the (s' r2))"
              using 𝒮G s' domains_subsume_def domains_subsume_globally_def s'_r2 by auto
            also have "... = dom σ  dom τ" by (simp add: r2 = r s'_r)
            also have "... = dom (σ;;τ)" by (simp add: dom_combination_dom_union)
            finally show " LIDS (the (s' r2)σ)  doms (the (s' r1))"
              using r1 = r' s'_r' by auto
          qed
          show ?thesis using case1 case2 case3 case4 case5 case6 fork(1) r1_neq_r2 r1_nor_r2_updated_implies_thesis by fastforce
        next
          case (join σ τ  r' σ' τ' v)
          have "r1 = r  r2 = r" by (metis fun_upd_def join(1) option.simps(3) r1_or_r2_updated s'_r1 s'_r2)
          then show ?thesis
          proof (rule disjE)
            assume "r1 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              show "LIDS (the (s' r2)σ)  doms (the (s' r1))"
              proof (cases "r2  RIDS τ'")
                case r2_in_τ': True
                have "LIDS (the (s' r2)σ) = LIDS (the (s r2)σ)" 
                  by (metis r1 = r fun_upd_def join(1) option.distinct(1) r1_neq_r2 s'_r2)
                also have "...  doms (the (s r'))"
                proof -
                  have r2_in_s_r': "r2  RIDL (the (s r'))" by (simp add: join(3) r2_in_τ')
                  have "𝒜 r' r2 s"
                    by (metis 𝒜G_s r1 = r domI fun_upd_def join(1) join(3) r1_neq_r2 s'_r2 subsumes_accessible_globally_def)
                  show ?thesis using 𝒜 r' r2 s r2_in_s_r' subsumes_accessible_def by blast
                qed
                also have "... = dom σ'  dom τ'" by (simp add: join(3))
                also have "...  LIDS σ'  dom τ'" by auto
                also have "...  dom σ  dom τ  dom τ'"
                proof -
                  have "r'  RIDL (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' r1))" using join by (auto simp add: r1 = r)
                finally show ?thesis by simp
              next
                case r2_nin_τ': False
                have "LIDS (the (s' r2)σ) = LIDS (the (s r2)σ)" 
                  by (metis r1 = r fun_upd_def join(1) option.distinct(1) r1_neq_r2 s'_r2)
                also have "...  doms (the (s r1))"
                proof -
                  have r2_in_s_r1: "r2  RIDL (the (s r))"
                  proof -
                    have "RIDL (the (s' r1)) = RIDS σ  RIDS (τ;;τ')  RIDC "
                      by (metis (no_types, lifting) ID_distr_completion(1) ID_distr_local(2) r1 = r expr.simps(153) fun_upd_apply local.join(1) option.discI option.sel s'_r1 sup_bot.right_neutral val.simps(66))
                    hence "r2  RIDS σ  RIDS τ  RIDC " using r2_in_s'_r1 r2_nin_τ' by auto
                    thus ?thesis by (simp add: join(2))
                  qed
                  have "𝒜 r1 r2 s" by (metis (no_types, lifting) 𝒜G_s r1 = r join(1-2) domIff fun_upd_def option.discI s'_r2 subsumes_accessible_globally_def)
                  show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def r1 = r by blast
                qed
                also have "... = dom σ  dom τ" by (simp add: r1 = r join(2))
                also have "...  dom σ  dom (τ;;τ')" by (auto simp add: dom_combination_dom_union)
                also have "... = doms (the (s' r1))" using join r1 = r by auto
                finally show ?thesis by simp
              qed
            qed
          next
            assume "r2 = r"
            show "𝒜 r1 r2 s'"
            proof (rule subsumes_accessibleI)
              assume r2_in_s'_r1: "r2  RIDL (the (s' r1))"
              have "LIDS (the (s' r2)σ) = LIDS (the (s r2)σ)"
                by (metis (no_types, lifting) LID_snapshot.simps fun_upd_apply join(1-2) option.discI option.sel s'_r2)
              also have "...  doms (the (s r1))"
              proof -
                have r2_in_s_r1: "r2  RIDL (the (s r1))"
                  by (metis r2 = r fun_upd_apply local.join(1) option.discI r1_neq_r2 r2_in_s'_r1 s'_r1)
                have "𝒜 r1 r2 s"
                  by (metis (no_types, lifting) 𝒜G_s r2 = r domIff fun_upd_apply join(1-2) option.discI s'_r1 subsumes_accessible_globally_def)
                show ?thesis using 𝒜 r1 r2 s r2_in_s_r1 subsumes_accessible_def by blast
              qed
              also have "...  doms (the (s' r1))"
                by (metis r2 = r eq_refl fun_upd_def local.join(1) option.distinct(1) r1_neq_r2 s'_r1)
              finally show "LIDS (the (s' r2)σ)  doms (the (s' r1))" by simp
            qed
          qed
        next
          case joinε
          thus ?thesis using s'_r1 by blast
        qed
      qed
      show "𝒜 r1 r2 s'" using r1_nor_r2_updated_implies_thesis r1_or_r2_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'  RIDG 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'"
  by (simp add: steps_def)

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  LIDE e = {}  RIDE 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"
  by (auto simp add: inductive_invariant_def)

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 "LIDL (σ',τ',e') = LIDL (ε, ε, 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 r1 σ1 τ1 e1 r2 σ2 τ2 e2
      assume s_r1: "s r1 = Some (σ1, τ1, e1)" and s_r2: "s r2 = Some (σ2, τ2, e2)"
      have "r2 = r" using s s_r2 prog_expr_e  by (meson domI domIff fun_upd_other)
      hence "σ2 = ε" using s s_r2 by auto
      hence "LIDS σ2 = {}" by auto
      thus "𝒜 r1 r2 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  LIDL ls" by (cases ls) auto
          have "l  LIDG s"
          proof -
            have "ls  {ls. r. s r = Some ls}" by (metis (full_types) in_ran ran_def)
            then show ?thesis using l  LIDL ls by blast
          qed
          thus False using new by auto
        qed
      qed (simp add: new.hyps(2))
      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  LIDG s"
        proof
          assume "l  LIDG s"
          then obtain r' σ' τ' e' where s_r': "s r' = Some (σ',τ',e')" and l_in_local: "l  LIDL (σ',τ',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  LIDL (σ, τ,  [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  LIDL (σ, τ,  [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 (simp add: revision_step.intros)+
  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 (RIDV v)"
  "finite (RIDE e)"
  "finite (LIDV v)"
  "finite (LIDE e)"
proof -
  have "(finite (RIDV v)  finite (LIDV v))  finite (RIDE e)  finite (LIDE e)"
    by (induct rule: val_expr.induct) auto
  thus  
    "finite (RIDV v)"
    "finite (RIDE e)"
    "finite (LIDV v)"
    "finite (LIDE e)"
    by auto
qed

lemma store_finite_upd [intro]:
  "finite (RIDS τ)  finite (RIDS (τ(l := None)))" 
  "finite (LIDS τ)  finite (LIDS (τ(l := None)))"
  apply (meson ID_restricted_store_subset_store(1) finite_subset)
  by (simp add: ID_restricted_store_subset_store(2) rev_finite_subset)

lemma finite_state_imp_restriction_finite [intro]: 
  "finite (RIDG s)  finite (RIDG (s(r := None)))"
  "finite (LIDG s)  finite (LIDG (s(r := None)))"
proof -
  assume "finite (RIDG s)"
  thus "finite (RIDG (s(r := None)))" by (meson infinite_super ID_restricted_global_subset_unrestricted)
next
  assume fin: "finite (LIDG s)"
  have "LIDG (s(r := None))  LIDG s" by auto
  thus "finite (LIDG (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 (RIDG (s(r := None)))  r  r'  finite (RIDL ls)"
  "s r' = Some ls  finite (LIDG (s(r := None)))  r  r'  finite (LIDL 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 (RIDS ε)" 
  "finite (LIDS ε)" 
  "finite (RIDG ε)" 
  "finite (LIDG ε)" 
  by (simp add: RIDS_def LIDS_def RIDG_def LIDG_def)+

lemma finite_combination [intro]:
  "finite (RIDS σ)  finite (RIDS τ)  finite (RIDS (σ;;τ))"
  "finite (LIDS σ)  finite (LIDS τ)  finite (LIDS (σ;;τ))"
  by (meson finite_UnI rev_finite_subset ID_combination_subset_union)+

lemma RIDG_finite_invariant:
  assumes
    step: "revision_step r s s'" and
    fin: "finite (RIDG s)"
shows
    "finite (RIDG 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 RIDL_finite_invariant:
  assumes
    step: "revision_step r s s'" and
    fin: "finite (LIDG s)"
shows
    "finite (LIDG 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 (RIDG s)"
    "finite (LIDG 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 (RIDG s)  finite (LIDG 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: " (RIDL ` ran s) = {}" using s by (auto simp add: prog_exp)
    have rids: "RIDG s = {r}" by (unfold RIDG_def, use rid_dom rid_ran in auto)
    have lid_ran: " (LIDL ` ran s) = {}" using s by (auto simp add: prog_exp)
    hence lids: "LIDG s = {}" by (unfold LIDG_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 (RIDG s')" using Suc.hyps n_steps by blast
    have fin_lid: "finite (LIDG s')" using Suc.hyps n_steps by blast
    thus ?case by (meson RIDG_finite_invariant RIDL_finite_invariant fin_rid local.step valid_stepE)
  qed
  thus "finite (RIDG s)" "finite (LIDG s)" by auto
qed

lemma reachable_imp_identifiers_available:
  assumes 
    "reachable (s :: ('r,'l,'v) global_state)"
  shows 
    "infinite (UNIV :: 'r set)  r. r  RIDG s"
    "infinite (UNIV :: 'l set)  l. l  LIDG 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)
qed (simp add: s_r revision_step.app)

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)
qed (simp add: s_r revision_step.ifTrue)

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)
qed (simp add: s_r revision_step.ifFalse)

lemma new_pseudodeterministic [simp]:
  assumes
    s_r: "s r = Some (σ, τ,  [Ref (VE v)])"
  shows "(revision_step r s s') = (l. l  LIDG 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'  RIDG (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)
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 s1 s2" and
    right: "revision_step r s1 s2'"
  shows "s2  s2'"
proof (use left in induct rule:revision_stepE›)
  case (new σ τ  v l)
  from new(2) right obtain l' where 
    side: "l'  LIDG s1" and
    s2': "s2' = s1(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  s2 = s2'" 
    by (use new side s2' 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''  RIDG s1" and
    s2': "s2' = s1(r  (σ, τ,  [VE (Rid r'')]), r''  (σ;;τ, ε, e))"
    by (auto simp add: ID_distr_global_conditional)
  let "" = "id(r' := r'', r'' := r')"
  have bij_α: "bij " by (rule swap_bij)
  have renaming: "ℛG  id s2 = s2'" 
    by (use fork side s2' 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:
  "s3' s3. s3'  s3  (revision_step r' s2 s3'  s2 = s3')  (revision_step r s2' s3  s2' = s3) 
   s3 s3'. s3  s3'  (revision_step r s2' s3  s2' = s3)  (revision_step r' s2 s3'  s2 = s3')"
  by (metis αβ_sym)

lemma SLC_commute: 
  " s3 = s3'; revision_step r' s2 s3; revision_step r s2' s3'   
  s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
  using αβ_refl by auto

subsubsection ‹Case join-epsilon›

lemma SLC_joinε:
  assumes
    s1_r: "s1 r = Some (σ, τ, [Rjoin (VE (Rid r''))])" and
    s2: "s2 = ε" and
    side: "s1 r'' = None" and
    right: "revision_step r' s1 s2'" and
    neq: "r  r'"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
proof -
  have right_collapsed_case: "s2' = ε  ?thesis" 
    by (rule exI[where x=ε], rule exI[where x=ε], use s2 in auto)
  have left_step_still_available_case: "s2'  ε  s2' r = s1 r  s2' 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: "s2' r = s1 r" using join assms by auto
    have r'_unchanged_right: "s2' r'' = None" using join assms by auto
    have "right_joinee  r'" using join(2-3) by auto
    hence s2'_nonempty: "s2'  ε" using assms join by (auto simp add: fun_upd_twist)
    show ?thesis by (rule left_step_still_available_case[OF s2'_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 s1_r right in auto)[1])+
qed

subsubsection ‹Case join›

lemma join_and_local_commute:
  assumes
    "s2 = s1(r := Some (σ, τ;;τ', [VE (CV Unit)]), r'' := None)"
    "s2' = s1(r'  ls)"
    "r  r'"
    "r'  r''"
    "revision_step r' s2 (s1(r := Some (σ, τ;;τ', [VE (CV Unit)]), r'' := None, r' := Some ls))"
    "s2' r = Some (σ, τ,  [Rjoin (VE (Rid r''))])"
    "s2' r'' = Some (σ', τ', VE v)"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
  apply (rule exI[where x="s1(r := Some (σ, τ;;τ', [VE (CV Unit)]), r'' := None, r' := Some ls)"])
  apply (rule exI[where x="s1(r' := Some ls, r := Some (σ, τ;;τ', [VE (CV Unit)]), r'' := None)"])
  by (rule SLC_commute, use assms in auto)

lemma SLC_join:
  assumes
    s1_r: "s1 r = Some (σ, τ, [Rjoin (VE (Rid r''))])" and
    s2: "s2 = (s1(r := Some (σ, (τ;;τ'), [VE (CV Unit)]), r'' := None))" and
    side: "s1 r'' = Some (σ', τ', VE v)" and 
    right: "revision_step r' s1 s2'" and
    neq: "r  r'"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
proof -
  have left_step: "revision_step r s1 s2" using s1_r s2 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  LIDG s2" by (rule only_new_introduces_lids'[OF left_step]) (use new right s1_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: "s2 r' = s1 r'" using fork assms by auto
    have r'''_fresh_left: "r'''  RIDG s2" using left_step fork(3) only_fork_introduces_rids' s1_r by auto 
    have r_unchanged_right: "s2' r = s1 r" using fork assms by auto
    have r''_unchanged_right: "s2' r'' = s1 r''" using fork assms by auto
    let "?s3" = "s2(r' := s2' r', r''' := s2' r''')"
    let "?s3'" = "s2'(r := s2 r, r'' := None)"
    show ?thesis 
    proof (rule exI[where x="?s3"],rule exI[where x="?s3'"], rule SLC_commute)
      show "?s3 = ?s3'" using fork(1) fork(3) neq r'_not_joined s1_r s2 by (auto simp add: ID_distr_global_conditional)
      show "revision_step r' s2 ?s3" using fork(1-2) r'_unchanged_left r'''_fresh_left by (auto simp add: ID_distr_global_conditional) 
      show "revision_step r s2' ?s3'" using r''_unchanged_right r_unchanged_right s1_r s2 side by auto
    qed
  next
    case (join _ _ _ r''')
    have r'_unchanged_left: "s2 r' = s1 r'" using join(2) neq r'_not_joined s2 by auto
    have r_unchanged_right: "s2' r = s1 r" using join(1,3) neq s1_r by auto
    show ?thesis
    proof (cases "r'' = r'''")
      case True
      have r'''_none_left: "s2 r''' = None" by (simp add: True s2)
      have r''_none_right: "s2' 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' s2 ε" using r'_unchanged_left r'''_none_left join(2) by auto
        show "revision_step r s2' ε" using r_unchanged_right r''_none_right s1_r by auto
      qed
    next
      case False
      have r'''_unchanged_left: "s2 r''' = s1 r'''" using False join(1,3) s2 r_unchanged_right by auto
      have r''_unchanged_right': "s2' r'' = s1 r''" using False join(1) r'_not_joined side by auto
      let "?s3" = "s2(r' := s2' r', r''' := None)"
      let "?s3'" = "s2'(r := s2 r, r'' := None)"
      show ?thesis
      proof (rule exI[where x="?s3"], rule exI[where x="?s3'"], rule SLC_commute)
        show "?s3 = ?s3'" using join(1) neq r'_not_joined r_unchanged_right s1_r s2 s1_r by fastforce
        show "revision_step r' s2 ?s3" by (simp add: join r'''_unchanged_left r'_unchanged_left)
        show "revision_step r s2' ?s3'" using r''_unchanged_right' r_unchanged_right s1_r side s2 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
    "s2 = s1(r  x)"
    "s2' = s1(r'  y)"
    "revision_step r' (s1(r  x)) (s1(r  x, r'  y))"
    "revision_step r (s1(r'  y)) (s1(r'  y, r  x))"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
  by (metis (no_types, lifting) assms fun_upd_twist fun_upd_upd local_determinism)

lemma local_and_fork_commute:
  assumes
    "s2 = s1(r  x)"
    "s2' = s1(r'  (σ, τ,  [VE (Rid r'')]), r''  (σ;;τ, ε, e))"
    "s2 r' = Some (σ, τ, [Rfork e])"
    "r''  RIDG s2"
    "revision_step r s2' (s1(r'  (σ, τ,  [VE (Rid r'')]), r''  (σ;;τ, ε, e), r  x))"
    "r  r'"
    "r  r''"
  shows
    "s3 s3'. (s3  s3')  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
  proof(rule exI[where x="s1(r  x, r'  (σ, τ,  [VE (Rid r'')]), r''  (σ;;τ, ε, e))"],
        rule exI[where x="s1(r'  (σ, τ,  [VE (Rid r'')]), r''  (σ;;τ, ε, e), r  x)"],
        rule SLC_commute)
  show "s1(r  x, r'  (σ, τ,  [VE (Rid r'')]), r''  (σ;;τ, ε, e)) = 
    s1(r'  (σ, τ,  [VE (Rid r'')]), r''  (σ;;τ, ε, e), r  x)"
    using assms revision_step.fork by auto
  show "revision_step r' s2 (s1(r  x, r'  (σ, τ,  [VE (Rid r'')]), r''  (σ;;τ, ε, e)))"
    using assms(1) assms(3) assms(4) revision_step.fork by blast
  show "revision_step r s2' (s1(r'  (σ, τ,  [VE (Rid r'')]), r''  (σ;;τ, ε, e), r  x))"
    using assms(5) by blast
qed
 
lemma SLC_app:
  assumes
    s1_r: "s1 r = Some (σ, τ, [Apply (VE (Lambda x e)) (VE v)])" and
    s2: "s2 = s1(r  (σ, τ, [subst (VE v) x e]))" and
    right: "revision_step r' s1 s2'" and
    neq: "r  r'"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
proof -
  have left_step: "revision_step r s1 s2" using s1_r s2 by auto 
  show ?thesis
  proof (use right in cases rule: revision_stepE›)
    case new: (new _ _ _ _ l)
    have l_fresh_left: "l  LIDG s2"
      by (rule only_new_introduces_lids'[OF left_step]) (simp add: s1_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''  RIDG s2"
      by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s1_r fork(3))+
    show ?thesis by (rule local_and_fork_commute[OF s2 fork(1)]) (use fork neq s2 r''_fresh_left s1_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 s2], use assms in auto)[1])+
qed

lemma SLC_ifTrue:
  assumes
    s1_r: "s1 r = Some (σ, τ, [Ite (VE (CV T)) e1 e2])" and
    s2: "s2 = s1(r  (σ, τ, [e1]))" and
    right: "revision_step r' s1 s2'" and
    neq: "r  r'"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
proof -
  have left_step: "revision_step r s1 s2" using s1_r s2 by auto
  show ?thesis
  proof (use right in cases rule: revision_stepE›)
    case (new _ _ _ _ l)
    have l_fresh_left: "l  LIDG s2"
      by (rule only_new_introduces_lids'[OF left_step]) (simp add: s1_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''  RIDG s2"
      by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s1_r fork(3))+
    show ?thesis by (rule local_and_fork_commute[OF s2 fork(1)]) (use fork neq s2 r''_fresh_left s1_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 s2], use assms in auto)[1])+
qed

lemma SLC_ifFalse:
  assumes
    s1_r: "s1 r = Some (σ, τ, [Ite (VE (CV F)) e1 e2])" and
    s2: "s2 = s1(r  (σ, τ, [e2]))" and
    right: "revision_step r' s1 s2'" and
    neq: "r  r'"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
proof -
  have left_step: "revision_step r s1 s2" using s1_r s2 by auto
  show ?thesis
  proof (use right in cases rule: revision_stepE›)
  next
    case (new _ _ _ _ l)
    have l_fresh_left: "l  LIDG s2" 
      by (rule only_new_introduces_lids'[OF left_step]) (simp add: s1_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''  RIDG s2"
      by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s1_r fork(3))+
    show ?thesis by (rule local_and_fork_commute[OF s2 fork(1)]) (use fork neq s2 r''_fresh_left s1_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 s2], use assms in auto)[1])+
qed

lemma SLC_set:
  assumes
    s1_r: "s1 r = Some (σ, τ, [Assign (VE (Loc l)) (VE v)])" and
    s2: "s2 = s1(r  (σ, τ(l  v), [VE (CV Unit)]))" and
    side: "l  dom (σ;;τ)" and
    right: "revision_step r' s1 s2'" and
    neq: "r  r'"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
proof -
  have left_step: "revision_step r s1 s2" using s1_r s2 side by auto
  show ?thesis
  proof (use right in cases rule: revision_stepE›)
    case (new _ _ _ _ l)
    have l_fresh_left: "l  LIDG s2"
      by (rule only_new_introduces_lids'[OF left_step]) (simp add: s1_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''  RIDG s2"
      by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s1_r fork(3))+
    show ?thesis by (rule local_and_fork_commute[OF s2 fork(1)]) (use fork neq s2 r''_fresh_left s1_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 s2], use assms in auto)[1])+
qed

lemma SLC_get:
  assumes
    s1_r: "s1 r = Some (σ, τ,  [Read (VE (Loc l))])" and
    s2: "s2 = s1(r  (σ, τ, [VE (the ((σ;;τ) l))]))" and
    side: "l  dom (σ;;τ)" and
    right: "revision_step r' s1 s2'" and
    neq: "r  r'"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
proof -
  have left_step: "revision_step r s1 s2" using s1_r s2 side by auto
  show ?thesis
  proof (use right in cases rule: revision_stepE›)
    case (new _ _ _ _ l)
    have l_fresh_left: "l  LIDG s2"
      by (rule only_new_introduces_lids'[OF left_step]) (simp add: s1_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''  RIDG s2"
      by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s1_r fork(3))+
    show ?thesis by (rule local_and_fork_commute[OF s2 fork(1)]) (use fork neq s2 r''_fresh_left s1_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 s2], use assms in auto)[1])+
qed

subsubsection ‹Case new›

lemma SLC_new:
  assumes
    s1_r: "s1 r = Some (σ, τ, [Ref (VE v)])" and
    s2: "s2 = s1(r  (σ, τ(l  v),  [VE (Loc l)]))" and
    side: "l  LIDG s1" and
    right: "revision_step r' s1 s2'" and
    neq: "r  r'" and
    reach: "reachable (s1 :: ('r,'l,'v) global_state)" and
    lid_inf: "infinite (UNIV :: 'l set)"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
proof -
  have left_step: "revision_step r s1 s2" using s1_r s2 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: "s2 r' = s1 r'" using new(2) neq s2 by auto
    have r_unchanged_right: "s2' r = s1 r" by (simp add: new(1) neq s1_r)
    show ?thesis
    proof (cases "l = l'")
      case True
      obtain l'' where l''_fresh_left: "l''  LIDG s2"
        by (meson ex_new_if_finite left_step lid_inf reach RIDL_finite_invariant reachable_imp_identifiers_finite(2))
      hence l_l'': "l  l''" by (auto simp add: s2)
      have l''_fresh_s1: "l''  LIDG s1" using assms True new l''_fresh_left by (auto simp add: ID_distr_global_conditional)
      hence l''_fresh_right': "l''  LIDG s2'" using True l_l'' new(1-2) by auto
      let "" = "id(l := l'', l'' := l)" 
      have bij_β: "bij " by (simp add: swap_bij)
      let "?s3" = "s2(r'  (σ', τ'(l''  v'), ℰ' [VE (Loc l'')]))"
      have left_convergence: "revision_step r' s2 ?s3"
        using l''_fresh_left new(2) r'_unchanged_left by auto
      let "?s3'" = "s2'(r  (σ, τ(l''  v),  [VE (Loc l'')]))"
      have right_convergence: "revision_step r s2' ?s3'"
        using l''_fresh_right' new(1) neq s1_r by auto 
      have equiv: "?s3  ?s3'"
      proof (rule eq_statesI[of id ])
        show "ℛG id  ?s3 = ?s3'"
        proof -
          have s1: "ℛG id  s1 = s1" using l''_fresh_s1 side by auto
          have σ: "ℛS id  σ = σ" using l''_fresh_s1 s1_r side by auto
          have: "C id   = "
          proof
            show "l  LIDC " using s1_r side by auto
            show "l''  LIDC " using l''_fresh_left s2 by auto
          qed
          have τlv: "ℛS id (id(l := l'', l'' := l)) (τ(l  v)) = (τ(l''  v))"
          proof -
            have τ: "ℛS id  τ = τ" using l''_fresh_s1 s1_r side by auto
            have v: "V id  v = v"
            proof
              show "l  LIDV v" using s1_r side by auto
              show "l''  LIDV v" using l''_fresh_s1 s1_r by auto
            qed
            show ?thesis by (simp add: τ v bij_β)
          qed
          have σ': "ℛS id  σ' = σ'" using l''_fresh_s1 new(2-3) by (auto simp add: True ID_distr_global_conditional)
          have ℰ': "C id  ℰ' = ℰ'" using l''_fresh_s1 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_s1 by (auto simp add: True ID_distr_global_conditional)
            have v': "V id  v' = v'" using new(2-3) l''_fresh_s1 by (auto simp add: True ID_distr_global_conditional)
            show ?thesis by (simp add: τ' v' bij_β)
          qed
          show ?thesis using True neq s1 σ ℰ τlv σ' ℰ' τl''v s2 l_l'' new(1) by auto
        qed
      qed (simp add: bij_β)+
      show ?thesis using left_convergence right_convergence equiv by blast
    next
      case False
      have l_fresh_left: "l  LIDG s2'" 
        by (rule revision_stepE[OF left_step]) (use False side new(1-2) in auto simp add: s1_r›)
      have l'_fresh_right: "l'  LIDG s2" 
        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 s2 new(1)]) (use new assms l_fresh_left l'_fresh_right s2 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''  RIDG s2" 
      by (rule only_fork_introduces_rids'[OF left_step]) (simp add: s1_r fork(3))+
    have l_fresh_right: "l  LIDG s2'" 
      by (rule only_new_introduces_lids'[OF right]) (simp add: side fork(2))+
    show ?thesis by (rule local_and_fork_commute[OF s2 fork(1)]) (use fork(1-2) neq s2 l_fresh_right r''_fresh_left s1_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
    s1_r: "s1 r = Some (σ, τ,  [Rfork e])" and
    s2: "s2 = (s1(r  (σ, τ, [VE (Rid left_forkee)]), left_forkee  (σ;;τ, ε, e)))" and
    side: "left_forkee  RIDG s1" and
    right: "revision_step r' s1 s2'" and
    neq: "r  r'" and
    reach: "reachable (s1 :: ('r,'l,'v) global_state)" and
    rid_inf: "infinite (UNIV :: 'r set)"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
proof -
  have left_step: "revision_step r s1 s2" using s1_r s2 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  LIDG s2"
      by (rule only_new_introduces_lids'[OF left_step]) (simp add: s1_r new(3))+
    have r''_fresh_right: "left_forkee  RIDG s2'"
      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) s2]) (use new(1-2) neq s1_r r''_fresh_right l_fresh_left s2 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: "s2 r' = s1 r'" using side fork(2) neq s2 by auto
    have r_unchanged_right: "s2' r = s1 r" using fork(1,3) neq s1_r by auto
    have "r  left_forkee" using s1_r side by auto
    have "r  right_forkee" using fork(3) s1_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''  RIDG s2"
        using RIDG_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 s2 by auto
      have "r''  r'" using fork(2) r''_fresh_left r'_unchanged_left by auto
      have "r''  RIDG (s1(r  (σ, τ, [VE (Rid left_forkee)])))"
        by (metis (mono_tags, lifting) RIDG_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 s2)
      hence "r''  RIDG (s1(r := None))" by blast
      have r''_fresh_s1: "r''  RIDG s1" 
        using r  left_forkee s2 r''_fresh_left s1_r r''  r r''  RIDG (s1(r := None))
        by (auto simp add: ID_distr_global_conditional)
      have r''_fresh_right: "r''  RIDG s2'"
        using True r''  left_forkee r'  right_forkee r''  r' r''_fresh_s1 fork(2) r''_fresh_s1 
        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 "?s3" = "s2(r'  (σ', τ', ℰ' [VE (Rid r'')]), r''  (σ';;τ', ε, e'))"
      have left_convergence: "revision_step r' s2 ?s3"
        using fork(2) r''_fresh_left r'_unchanged_left revision_step.fork by auto
      let "?s3'" = "s2'(r  (σ, τ, [VE (Rid r'')]), r''  (σ;;τ, ε, e))"
      have right_convergence: "revision_step r s2' ?s3'"
        using r''_fresh_right r_unchanged_right revision_step.fork s1_r by auto
      have equiv: "?s3  ?s3'"
      proof (rule eq_statesI[of  id])
        show "ℛG  id ?s3 = ?s3'"
        proof -
          have s1: "ℛG  id s1 = s1" using r''_fresh_s1 side by auto
          have σ: "ℛS  id σ = σ" using r''_fresh_s1 s1_r True fork(3) by auto
          have τ: "ℛS  id τ = τ" using r''_fresh_s1 s1_r True fork(3) by auto
          have: "C  id  = "
          proof
            show "left_forkee  RIDC " using s1_r side by auto
            show "r''  RIDC " using True r  right_forkee r''_fresh_left s2 by auto
          qed
          have e: "E  id e = e"
          proof
            show "left_forkee  RIDE e" using s1_r side by auto
            show "r''  RIDE e" using True r  right_forkee r''_fresh_left s2 by auto
          qed
          have σ': "ℛS  id σ' = σ'" using fork(2) r''_fresh_s1 side by auto
          have τ': "ℛS  id τ' = τ'" using fork(2) r''_fresh_s1 side by auto
          have ℰ': "C  id ℰ' = ℰ'"
          proof 
            show "left_forkee  RIDC ℰ'" using fork(2) side by auto
            show "r''  RIDC ℰ'" using fork(2) r''_fresh_s1 by auto
          qed
          have e': "E  id e' = e'"
          proof 
            show "left_forkee  RIDE e'" using fork(2) side by auto
            show "r''  RIDE e'" using fork(2) r''_fresh_s1 by auto
          qed
          show ?thesis using True fork(1) neq σ τ ℰ e  σ' τ' ℰ' e' s1 s2
            bij_α r''  left_forkee r'  left_forkee r  left_forkee r''  r r''  r' 
            by auto
        qed
      qed (simp add: bij_α)+
      show ?thesis using equiv left_convergence right_convergence by blast
    next
      case False
      have right_forkee_fresh_left: "right_forkee  RIDG s2" 
        using False r  left_forkee r  right_forkee fork(3) s1_r 
        by (auto simp add: s2 ID_distr_global_conditional, auto)
      have left_forkee_fresh_right: "left_forkee  RIDG s2'" 
        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="s2(r' := s2' r', right_forkee := s2' right_forkee)"],
            rule exI[where x="s2'(r := s2 r, left_forkee := s2 left_forkee)"],
            rule SLC_commute)
        show "s2(r' := s2' r', right_forkee := s2' right_forkee) = s2'(r := s2 r, left_forkee := s2 left_forkee)"
          using False r  right_forkee r'  left_forkee r'  right_forkee fork(1) neq s2 by auto
        show "revision_step r' s2 (s2(r' := s2' r', right_forkee := s2' right_forkee))"
          using fork(1-2) r'_unchanged_left revision_step.fork right_forkee_fresh_left by auto
        show "revision_step r s2' (s2'(r := s2 r, left_forkee := s2 left_forkee))"
          using left_forkee_fresh_right r_unchanged_right revision_step.fork s1_r s2 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 s1 s2" and
    r: "revision_step r' s1 s2'" and
    reach: "reachable (s1 :: ('r,'l,'v) global_state)" and
    lid_inf: "infinite (UNIV :: 'l set)" and
    rid_inf: "infinite (UNIV :: 'r set)"
  shows
    "s3 s3'. s3  s3'  (revision_step r' s2 s3  s2 = s3)  (revision_step r s2' s3'  s2' = s3')"
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
    s1s2: "s1  s2" and
    s1s2': "s1  s2'" and
    reach: "reachable (s1 :: ('r,'l,'v) global_state)