Theory IMAP-proof-commute

section ‹Commutativity of IMAP Commands›

text‹In this section we prove the commutativity of operations and identify the edge cases.›

theory
  "IMAP-proof-commute"
  imports
    "IMAP-def"  
begin

lemma (in imap) create_create_commute:
  shows "⟨Create i1 e1⟩ ⊳ ⟨Create i2 e2⟩ = ⟨Create i2 e2⟩ ⊳ ⟨Create i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) create_delete_commute:
  assumes "i ∉ is"
  shows "⟨Create i e1⟩ ⊳ ⟨Delete is e2⟩ = ⟨Delete is e2⟩ ⊳ ⟨Create i e1⟩"
  using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)

lemma (in imap) create_append_commute:
  shows "⟨Create i1 e1⟩ ⊳ ⟨Append i2 e2⟩ = ⟨Append i2 e2⟩ ⊳ ⟨Create i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) create_expunge_commute:
  shows "⟨Create i1 e1⟩ ⊳ ⟨Expunge e2 mo i2⟩ = ⟨Expunge e2 mo i2⟩ ⊳ ⟨Create i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) create_store_commute:
  shows "⟨Create i1 e1⟩ ⊳ ⟨Store e2 mo i2⟩ = ⟨Store e2 mo i2⟩ ⊳ ⟨Create i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) delete_delete_commute:
  shows "⟨Delete i1 e1⟩ ⊳ ⟨Delete i2 e2⟩ = ⟨Delete i2 e2⟩ ⊳ ⟨Delete i1 e1⟩"
  by(unfold interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) delete_append_commute:
  assumes "i ∉ is"
  shows "⟨Delete is e1⟩ ⊳ ⟨Append i e2⟩ = ⟨Append i e2⟩ ⊳ ⟨Delete is e1⟩"
  using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)

lemma (in imap) delete_expunge_commute:
  assumes "i ∉ is"
  shows "⟨Delete is e1⟩ ⊳ ⟨Expunge e2 mo i⟩ = ⟨Expunge e2 mo i⟩ ⊳ ⟨Delete is e1⟩"
  using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)

lemma (in imap) delete_store_commute:
  assumes "i ∉ is"
  shows "⟨Delete is e1⟩ ⊳ ⟨Store e2 mo i⟩ = ⟨Store e2 mo i⟩ ⊳ ⟨Delete is e1⟩"
  using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def, fastforce)

lemma (in imap) append_append_commute:
  shows "⟨Append i1 e1⟩ ⊳ ⟨Append i2 e2⟩ = ⟨Append i2 e2⟩ ⊳ ⟨Append i1 e1⟩"
  by(auto simp add: interpret_op_def op_elem_def kleisli_def, fastforce)

lemma (in imap) append_expunge_commute:
  assumes "i1 ≠ mo"
  shows "(⟨Append i1 e1⟩ ⊳ ⟨Expunge e2 mo i2⟩) = (⟨Expunge e2 mo i2⟩ ⊳ ⟨Append i1 e1⟩)"
proof
  fix x
  show "(⟨Append i1 e1⟩ ⊳ ⟨Expunge e2 mo i2⟩) x = (⟨Expunge e2 mo i2⟩ ⊳ ⟨Append i1 e1⟩) x"
    using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def)
qed

lemma (in imap) append_store_commute:
  assumes "i1 ≠ mo"
  shows "(⟨Append i1 e1⟩ ⊳ ⟨Store e2 mo i2⟩) = (⟨Store e2 mo i2⟩ ⊳ ⟨Append i1 e1⟩)"
proof
  fix x
  show "(⟨Append i1 e1⟩ ⊳ ⟨Store e2 mo i2⟩) x = (⟨Store e2 mo i2⟩ ⊳ ⟨Append i1 e1⟩) x"
    using assms by(auto simp add: interpret_op_def kleisli_def op_elem_def)
qed

lemma (in imap) expunge_expunge_commute:
  shows "(⟨Expunge e1 mo1 i1⟩ ⊳ ⟨Expunge e2 mo2 i2⟩) = (⟨Expunge e2 mo2 i2⟩ ⊳ ⟨Expunge e1 mo1 i1⟩)"
proof
  fix x
  show "(⟨Expunge e1 mo1 i1⟩ ⊳ ⟨Expunge e2 mo2 i2⟩) x 
       = (⟨Expunge e2 mo2 i2⟩ ⊳ ⟨Expunge e1 mo1 i1⟩) x"
    by(auto simp add: interpret_op_def kleisli_def op_elem_def) qed

lemma (in imap) expunge_store_commute:
  assumes "i1 ≠ mo2" and "i2 ≠ mo1"
  shows "(⟨Expunge e1 mo1 i1⟩ ⊳ ⟨Store e2 mo2 i2⟩) = (⟨Store e2 mo2 i2⟩ ⊳ ⟨Expunge e1 mo1 i1⟩)"
proof
  fix x
  show "(⟨Expunge e1 mo1 i1⟩ ⊳ ⟨Store e2 mo2 i2⟩) x = (⟨Store e2 mo2 i2⟩ ⊳ ⟨Expunge e1 mo1 i1⟩) x"
    unfolding  interpret_op_def kleisli_def op_elem_def using assms(2) by (simp, fastforce)
qed

lemma (in imap) store_store_commute:
  assumes "i1 ≠ mo2" and "i2 ≠ mo1"
  shows "(⟨Store e1 mo1 i1⟩ ⊳ ⟨Store e2 mo2 i2⟩) = (⟨Store e2 mo2 i2⟩ ⊳ ⟨Store e1 mo1 i1⟩)"
proof
  fix x
  show "(⟨Store e1 mo1 i1⟩ ⊳ ⟨Store e2 mo2 i2⟩) x = (⟨Store e2 mo2 i2⟩ ⊳ ⟨Store e1 mo1 i1⟩) x"
    unfolding  interpret_op_def kleisli_def op_elem_def using assms by (simp, fastforce)
qed

end