Theory Occurrences

section Occurrences

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

theory Occurrences
  imports Data
begin

subsection Definitions

subsubsection ‹Revision identifiers›

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

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

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

subsubsection ‹Location identifiers›

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

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

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

subsection ‹Inference rules›

subsubsection ‹Introduction and elimination rules›

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

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

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

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

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

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

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

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

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

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

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

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

subsubsection ‹Distributive laws›

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

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

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

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

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

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

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

lemma in_restricted_global_in_unrestricted_global [intro]: 
  "r' ∈ RID⇩G (s(r := None)) ⟹ r' ∈ RID⇩G s"
  "l ∈ LID⇩G (s(r := None)) ⟹ l ∈ LID⇩G s"
  by (simp add: ID_restricted_global_subset_unrestricted rev_subsetD)+

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

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

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

subsubsection ‹Miscellaneous laws›

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

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

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

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

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

end