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)" and
    lid_inf: "infinite (UNIV :: 'l set)" and
    rid_inf: "infinite (UNIV :: 'r set)"
  shows
    "∃s3 s3'. s3 ≈ s3' ∧ s2 ↝= s3 ∧ s2' ↝= s3'"
proof -
  from s1s2 obtain r where l: "revision_step r s1 s2" by auto
  from s1s2' obtain r' where r: "revision_step r' s1 s2'" by auto
  obtain s3 s3' where 
    s3_eq_s3': "s3 ≈ s3'" and
    l_join: "revision_step r' s2 s3 ∨ s2 = s3" and
    r_join: "revision_step r s2' s3' ∨ s2' = s3'"
    using l r reach lid_inf rid_inf strong_local_confluence by metis
  have s2s3: "s2 ↝= s3" using l_join steps_def by auto
  have s2's3: "s2' ↝= s3'" using r_join steps_def by auto
  show ?thesis using s2's3 s2s3 s3_eq_s3' by blast
qed

lemma SLC_top_relaxed:
  assumes
    s1s2: "s1 ↝= s2" and
    s1s2': "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' ∧ s2 ↝= s3 ∧ s2' ↝= s3'"
proof -
  have 1: "s1 ↝ s2 ⟹ s1 ↝ s2' ⟹ ?thesis" using SLC lid_inf reach rid_inf by blast
  have 2: "s1 = s2 ⟹ s1 ↝ s2' ⟹ ?thesis" 
    by (rule exI[where x="s2'"], rule exI[where x="s2'"]) (auto simp add: αβ_refl)
  show ?thesis using assms 1 2 by auto
qed

subsubsection ‹Mimicking diagrams›

declare bind_eq_None_conv [simp]
declare bind_eq_Some_conv [simp]

lemma in_renamed_in_unlabelled_val: 
  "bij α ⟹ (α r ∈ RIDV (ℛV α β v)) = (r ∈ RIDV v)"
  "bij β ⟹ (β l ∈ LIDV (ℛV α β v)) = (l ∈ LIDV v)"
  by (auto simp add: bij_is_inj inj_image_mem_iff val.set_map(1-2))

lemma in_renamed_in_unlabelled_expr:
  "bij α ⟹ (α r ∈ RIDE (ℛE α β v)) = (r ∈ RIDE v)"
  "bij β ⟹ (β l ∈ LIDE (ℛE α β v)) = (l ∈ LIDE v)"
  by (auto simp add: bij_is_inj inj_image_mem_iff expr.set_map(1-2))

lemma in_renamed_in_unlabelled_store:
  assumes 
    bij_α: "bij α" and
    bij_β: "bij β"
  shows
    "(α r ∈ RIDS (ℛS α β σ)) = (r ∈ RIDS σ)"
    "(β l ∈ LIDS (ℛS α β σ)) = (l ∈ LIDS σ)"
proof -
  show "(α r ∈ RIDS (ℛS α β σ)) = (r ∈ RIDS σ)"
  proof (rule iffI)
    assume "α r ∈ RIDS (ℛS α β σ)"
    thus "r ∈ RIDS σ"
    proof (rule RIDSE)
      fix l v
      assume map: "ℛS α β σ l = Some v" and αr: "α r ∈ RIDV v" 
      hence "σ (inv β l) = Some (ℛV (inv α) (inv β) v)"
        using bij_α bij_β by (auto simp add: bij_is_inj)
      have "r ∈ RIDV (ℛV (inv α) (inv β) v)"
        using bij_α bij_β αr map by (auto simp add: bij_is_inj in_renamed_in_unlabelled_val(1))
      show "r ∈ RIDS σ"
        using ‹σ (inv β l) = Some (ℛV (inv α) (inv β) v)› ‹r ∈ RIDV (ℛV (inv α) (inv β) v)› by blast
    qed
  next
    assume "r ∈ RIDS σ"
    thus "α r ∈ RIDS (ℛS α β σ)" 
      by (metis (mono_tags, lifting) RIDSE RIDSI bij_α bij_β fun_upd_same fun_upd_triv 
      in_renamed_in_unlabelled_val(1) renaming_distr_store)
  qed
  show "(β l ∈ LIDS (ℛS α β σ)) = (l ∈ LIDS σ)"
  proof (rule iffI)
    assume "β l ∈ LIDS (ℛS α β σ)"
    thus "l ∈ LIDS σ"
    proof (rule LIDSE)
      assume "β l ∈ dom (ℛS α β σ)"
      thus "l ∈ LIDS σ" by (auto simp add: LIDSI(1) bij_β bijection.intro bijection.inv_left)
    next
      fix v l'
      assume "ℛS α β σ l' = Some v" "β l ∈ LIDV v"
      thus "l ∈ LIDS σ" using bij_β by (auto simp add: LIDSI(2) in_renamed_in_unlabelled_val(2))
    qed
  next
    assume "l ∈ LIDS σ" 
    thus "β l ∈ LIDS (ℛS α β σ)"
    proof (rule LIDSE)
      assume "l ∈ dom σ"
      hence "∃σ' v. σ = (σ'(l ↦ v))" by fastforce
      hence "β l ∈ dom (ℛS α β σ)" using bij_β by auto
      thus "β l ∈ LIDS (ℛS α β σ)" by auto
    next
      fix v l'
      assume "σ l' = Some v" and l_in_v: "l ∈ LIDV v"
      hence "∃σ'. σ = (σ'(l' ↦ v))" by force
      thus "β l ∈ LIDS (ℛS α β σ)" 
        using l_in_v bij_β by (auto simp add: LIDSI(2) in_renamed_in_unlabelled_val(2))
    qed
  qed
qed

lemma in_renamed_in_unlabelled_local:
  assumes
    bij_α: "bij α" and
    bij_β: "bij β"
  shows
    "(α r ∈ RIDL (ℛL α β ls)) = (r ∈ RIDL ls)"
    "(β l ∈ LIDL (ℛL α β ls)) = (l ∈ LIDL ls)"
  by (cases ls, simp add: assms in_renamed_in_unlabelled_expr in_renamed_in_unlabelled_store)+

lemma in_renamed_in_unlabelled_global:
  assumes
    bij_α: "bij α" and
    bij_β: "bij β"
  shows
    "(α r ∈ RIDG (ℛG α β s)) = (r ∈ RIDG s)"
    "(β l ∈ LIDG (ℛG α β s)) = (l ∈ LIDG s)"
proof -
  show "(α r ∈ RIDG (ℛG α β s)) = (r ∈ RIDG s)"
  proof (rule iffI)
    assume "α r ∈ RIDG (ℛG α β s)"
    thus "r ∈ RIDG s" 
    proof (rule RIDGE)
      assume "α r ∈ dom (ℛG α β s)"
      hence "r ∈ dom s" by (metis bij_α domIff fun_upd_same fun_upd_triv renaming_distr_global(2))
      thus "r ∈ RIDG s" by auto
    next
      fix r' ls
      assume ℛsr': "ℛG α β s r' = Some ls" and αr: "α r ∈ RIDL ls"
      have s_inv_αr': "s (inv α r') = Some (ℛL (inv α) (inv β) ls)"
      proof -
        have "inv α r' ∈ dom s" using ℛsr' by auto
        then obtain ls' where s_inv_αr: "s (inv α r') = Some ls'" by blast
        hence "ℛG α β s r' = Some (ℛL α β ls')" by simp
        hence "ls = (ℛL α β ls')" using ℛsr' by auto
        thus ?thesis by (metis ℛL_inv s_inv_αr bij_α bij_β)
      qed
      have r_in: "r ∈ RIDL (ℛL (inv α) (inv β) ls)"
        by (metis bij_α bij_β bij_imp_bij_inv bijection.intro bijection.inv_left in_renamed_in_unlabelled_local(1) αr)
      show "r ∈ RIDG s"
        using r_in s_inv_αr' by blast
    qed
  next
    assume "r ∈ RIDG s"
    thus "α r ∈ RIDG (ℛG α β s)"
    proof (rule RIDGE)
      assume "r ∈ dom s"
      hence "α r ∈ dom (ℛG α β s)"
        by (metis (mono_tags, lifting) bij_α domD domI fun_upd_same fun_upd_triv renaming_distr_global(1))
      thus "α r ∈ RIDG (ℛG α β s)" by auto
    next
      fix r' ls
      assume "s r' = Some ls" "r ∈ RIDL ls"
      thus "α r ∈ RIDG (ℛG α β s)"
        by (metis ID_distr_global(1) UnI2 bij_α bij_β fun_upd_triv in_renamed_in_unlabelled_local(1) insertI2 renaming_distr_global(1))
    qed
  qed
  show "(β l ∈ LIDG (ℛG α β s)) = (l ∈ LIDG s)"
  proof (rule iffI)
    assume "β l ∈ LIDG (ℛG α β s)"
    from this obtain r ls where Rs_ls: "ℛG α β s r = Some ls" and βl_in_ls: "β l ∈ LIDL ls" by blast
    hence "l ∈ LIDL (ℛL (inv α) (inv β) ls)"
      by (metis bij_α bij_β bij_imp_bij_inv bijection.intro bijection.inv_left in_renamed_in_unlabelled_local(2))
    hence "l ∈ LIDG (ℛG (inv α) (inv β) (ℛG α β s))"
      by (metis (mono_tags, lifting) LIDGI Rs_ls bij_α bij_imp_bij_inv fun_upd_idem_iff renaming_distr_global(1))
    thus "l ∈ LIDG s" using bij_α bij_β by (metis ℛG_inv)
  next
    assume "l ∈ LIDG s"
    then obtain r s' ls where "s = (s'(r ↦ ls))" "l ∈ LIDL ls" by (metis LIDGE fun_upd_triv)
    thus "β l ∈ LIDG (ℛG α β s)" by (simp add: bij_α bij_β in_renamed_in_unlabelled_local(2))
  qed
qed

lemma mimicking:
  assumes
    step: "revision_step r s s'" and
    bij_α: "bij α" and
    bij_β: "bij β"
  shows "revision_step (α r) (ℛG α β s) (ℛG α β s')"
proof (use step in ‹cases rule: revision_stepE›)
  case app
  then show ?thesis by (auto simp add: bij_α bij_β bijection.intro bijection.inv_left renaming_distr_subst)
next
  case (new _ _ _ _ l)
  have βl_fresh: "β l ∉ LIDG (ℛG α β s)"
    by (simp add: bij_α bij_β in_renamed_in_unlabelled_global(2) new(3))
  show ?thesis using βl_fresh new by (auto simp add: bij_α bij_β bijection.intro bijection.inv_left)   
next
  case (fork σ τ ℰ e r')
  have αr'_fresh: "α r' ∉ RIDG (ℛG α β s)"
    by (simp add: bij_α bij_β in_renamed_in_unlabelled_global(1) fork(3))
  have s_r_as_upd: "s = (s(r ↦ (σ, τ, ℰ [Rfork e])))" using fork(2) by auto
  have src: "ℛG α β s (α r) = Some (ℛS α β σ, ℛS α β τ, (ℛC α β ℰ) [Rfork (ℛE α β e)])" 
    by (subst s_r_as_upd, simp add: bij_α)
  show ?thesis using αr'_fresh src revision_step.fork fork(1) bij_α by auto
qed (auto simp add: bij_α bij_β bijection.intro bijection.inv_left)

lemma mimic_single_step:
  assumes
    s1s1': "s1 ≈ s1'" and
    s1s2: "s1 ↝ s2"
  shows "∃s2'. (s2 ≈ s2') ∧ s1' ↝ s2'"
proof -
  from s1s1' obtain α β where 
    bij_α: "bij α" and 
    bij_β: "bij β" and
    R: "ℛG α β s1 = s1'" by blast
  from s1s2 obtain r where step: "revision_step r s1 s2" by auto
  have mirrored_step: "revision_step (α r) s1' (ℛG α β s2)" 
    using R bij_α bij_β step mimicking by auto
  have eq: "s2 ≈ (ℛG α β s2)" using bij_α bij_β by blast
  have s1's2': "s1' ↝ (ℛG α β s2)" using mirrored_step by auto
  from eq s1's2' show ?thesis by blast
qed

lemma mimic_trans:
  assumes
    s1_eq_s1': "s1 ≈ s1'" and
    s1s2: "s1 ↝* s2"
  shows "∃s2'. s2 ≈ s2' ∧ s1' ↝* s2'"
proof -
  from s1_eq_s1' obtain α β where
    bij_α: "bij α" and
    bij_β: "bij β" and
    R: "ℛG α β s1 = s1'"
    by blast
  from s1s2 obtain n where "(s1,s2) ∈ [↝]^^n" using rtrancl_power by blast
  thus ?thesis
  proof (induct n arbitrary: s2)
    case 0
    thus ?case using s1_eq_s1' by auto
  next
    case (Suc n)
    obtain x where n_steps: "(s1, x) ∈ [↝]^^n" and step: "x ↝ s2" using Suc.prems by auto
    obtain x' where x_eq_x': "x ≈ x'" and s1'x: "s1' ↝* x'" using Suc.hyps n_steps by blast
    obtain s2' where s2_eq_s2': "s2 ≈ s2'" and x's2': "x' ↝ s2'" 
      by (meson step mimic_single_step x_eq_x')
    show ?case using s1'x s2_eq_s2' trancl_into_rtrancl x's2' by auto
  qed
qed

subsubsection ‹Strip diagram›

lemma strip_lemma:
  assumes
    s1s2: "s1 ↝* s2" and
    s1s2': "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' ∧ s2 ↝* s3 ∧ s2' ↝* s3'"
proof -
  from s1s2 obtain n where "(s1, s2) ∈ [↝]^^n" using rtrancl_power by blast
  from reach s1s2' and this show ?thesis
  proof (induct n arbitrary: s1 s2 s2')
    case 0
    hence "s1 = s2" by simp
    hence s2s2': "s2 ↝* s2'" using "0.prems"(2) by blast
    show ?case by (rule exI[where x=s2'], rule exI[where x=s2']) (use s2s2' in ‹simp add: αβ_refl›)
  next
    case (Suc n)
    obtain a where s1a: "s1 ↝ a" and as2: "(a, s2) ∈ [↝]^^n" by (meson Suc.prems(3) relpow_Suc_D2)
    obtain b c where "b ≈ c" "a ↝= b" "s2' ↝= c"
      by (metis (mono_tags, lifting) SLC_top_relaxed Suc.prems(1) Suc.prems(2) αβ_sym lid_inf rid_inf s1a)
    obtain d e where "d ≈ e" "s2 ↝* d" "b ↝* e"
      by (meson Suc.hyps Suc.prems(1) ‹a ↝= b› as2 reachability_closed_under_execution_step s1a valid_stepE)
    obtain f where "c ↝* f" "e ≈ f"
      by (meson  ‹b ≈ c› ‹b ↝* e› mimic_trans)
    have "d ≈ f" using αβ_trans ‹d ≈ e› ‹e ≈ f› by auto
    then show ?case by (metis (no_types, lifting) ‹c ↝* f› ‹s2 ↝* d› ‹s2' ↝= c› r_into_rtrancl rtrancl_reflcl rtrancl_trans)
  qed
qed

subsubsection ‹Confluence diagram›

lemma confluence_modulo_equivalence:
  assumes
    s1s2: "s1 ↝* s2" and
    s1s2': "s1' ↝* s2'" and
    equiv: "s1 ≈ s1'" 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' ∧ s2 ↝* s3 ∧ s2' ↝* s3'"
proof -
  obtain n where "(s1, s2) ∈ [↝]^^n" using s1s2 rtrancl_power by blast
  from reach equiv s1s2' and this show ?thesis
  proof (induct n arbitrary: s1 s1' s2 s2')
    case base: 0
    hence "s1 = s2" by simp
    obtain s2'' where "s1 ↝* s2''" "s2' ≈ s2''"
      using αβ_sym base.prems(2,3) mimic_trans by blast
    have "s2 ↝* s2''" using ‹s1 = s2› ‹s1 ↝* s2''› by blast
    show ?case by (rule exI[where x=s2''], rule exI[where x=s2']) (auto simp add: αβ_sym ‹s2 ↝* s2''› ‹s2' ≈ s2''›)
  next
    case step: (Suc n)
    obtain a where s1a: "(s1, a) ∈ [↝]^^n" and as2: "a ↝ s2" using step.prems(4) by auto
    have "reachable a" using reachability_closed_under_execution relpow_imp_rtrancl s1a step.prems(1) by blast
    obtain b c where "a ↝* b" "s2' ↝* c" "b ≈ c"
      using s1a step.hyps step.prems(1-3) by blast
    have "a ↝* s2" by (simp add: as2 r_into_rtrancl)
    obtain s3 d where "s3 ≈ d" "s2 ↝* s3" "b ↝* d" 
      by (meson αβ_sym ‹a ↝* b› ‹reachable a› as2 lid_inf refl_rewritesI rid_inf strip_lemma)
    obtain s3' where "s3 ≈ s3'" "c ↝* s3'"
      by (meson αβ_trans ‹b ≈ c› ‹b ↝* d› ‹s3 ≈ d› mimic_trans)
    show ?case by (meson ‹c ↝* s3'› ‹s2 ↝* s3› ‹s2' ↝* c› ‹s3 ≈ s3'› transD trans_rtrancl)
  qed
qed

subsection ‹Determinacy›

theorem determinacy:
  assumes 
    prog_expr: "program_expr e" and
    e_terminates_in_s: "e ↓ s" and
    e_terminates_in_s': "e ↓ s'" and
    lid_inf: "infinite (UNIV :: 'l set)" and
    rid_inf: "infinite (UNIV :: 'r set)"
  shows "s ≈ s'"
proof -
  obtain r where x: "(ε(r ↦ (ε,ε,e))) ↝* s"
    by (metis e_terminates_in_s execution_def maximal_execution_def terminates_in_def)
  obtain r' where y: "(ε(r' ↦ (ε,ε,e))) ↝* s'"
    by (metis e_terminates_in_s' execution_def maximal_execution_def terminates_in_def)
  let "?α" = "id(r := r', r' := r)"
  have bij_α: "bij ?α" by (simp add: swap_bij)
  have equiv: "(ε(r ↦ (ε,ε,e))) ≈ (ε(r' ↦ (ε,ε,e)))" 
  proof (rule eq_statesI[of ?α id])
    show "ℛG ?α id (ε(r ↦ (ε, ε, e))) = ε(r' ↦ (ε, ε, e))"
      using bij_α prog_expr by auto
  qed (simp add: bij_α)+
  have reach: "reachable (ε(r ↦ (ε,ε,e)))" 
    by (simp add: initial_state_reachable prog_expr)
  have "∃a b. (a ≈ b) ∧ s ↝* a ∧ s' ↝* b"
    by (rule confluence_modulo_equivalence[OF x y equiv reach lid_inf rid_inf])
  from this obtain a b where "s ↝* a" "s' ↝* b" "a ≈ b" by blast
  have "s = a" by (meson ‹s ↝* a› e_terminates_in_s maximal_execution_def rtranclD terminates_in_def tranclD)
  have "s' = b" by (meson ‹s' ↝* b› converse_rtranclE e_terminates_in_s' maximal_execution_def terminates_in_def)
  show ?thesis using ‹a ≈ b› ‹s = a› ‹s' = b› by auto
qed

end (* substitution locale *)

end