Theory OperationalSemantics

section ‹Operational Semantics›

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

theory OperationalSemantics
  imports Substitution
begin

context substitution
begin

subsection Definition

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

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

subsection ‹Introduction lemmas for identifiers›

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

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

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

subsection ‹Domain subsumption›

subsubsection Definitions

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

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

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

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

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

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

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

subsubsection ‹The theorem›

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

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

subsection ‹Relaxed definition of the operational semantics›

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

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

end (* substitution locale *)

end (* theory *)