section ‹IMAP-CRDT Definitions›

text‹We begin by defining the operations on a mailbox state. In addition to the interpretation of
  operations, we define valid behaviours for the operations as assumptions for the network.
  use the \texttt{network\_with\_constrained\_ops} locale from the framework.›

theory
  "IMAP-def"
  imports
    "CRDT.Network"
begin

datatype ('id, 'a) operation = 
  Create "'id" "'a" | 
  Delete "'id set" "'a" | 
  Append "'id" "'a" | 
  Expunge "'a" "'id" "'id" | 
  Store "'a" "'id" "'id"

type_synonym ('id, 'a) state = "'a → ('id set × 'id set)"

definition op_elem :: "('id, 'a) operation → 'a" where
  "op_elem oper ≡ case oper of
    Create i e → e |
    Delete is e → e |
    Append i e → e |
    Expunge e mo i → e |
    Store e mo i → e"

definition interpret_op :: "('id, 'a) operation → ('id, 'a) state ⇀ ('id, 'a) state" 
  (‹⟨_⟩› [0] 1000) where
  "interpret_op oper state ≡
    let metadata = fst (state (op_elem oper));
        files = snd (state (op_elem oper));
        after = case oper of
          Create i e → (metadata ∪ {i}, files) |
          Delete is e → (metadata - is, files - is) |
          Append i e → (metadata, files ∪ {i}) |
          Expunge e mo i → (metadata ∪ {i}, files - {mo}) |
          Store e mo i → (metadata, insert i (files - {mo}))
    in Some (state ((op_elem oper) := after))"

text‹In the definition of the valid behaviours of the operations, we define additional assumption
  state where the operation is executed. In essence, a the tag of a \create, \append, \expunge,
  \store\ operation is identical to the message number and therefore unique. A \delete\ operation
  all metadata and the content of a folder. The \store\ and \expunge\ operations must refer
  an existing message.›

definition valid_behaviours :: "('id, 'a) state → 'id × ('id, 'a) operation → bool" where
  "valid_behaviours state msg ≡
    case msg of
      (i, Create j e) → i = j |
      (i, Delete is e) → is = fst (state e) ∪ snd (state e) |
      (i, Append j e) → i = j |
      (i, Expunge e mo j) → i = j ∧ mo ∈ snd (state e) |
      (i, Store e mo j) → i = j ∧ mo ∈ snd (state e)"

locale imap = network_with_constrained_ops _ interpret_op "λx. ({},{})" valid_behaviours

end