Theory MapOps

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory MapOps
imports Main
begin
(*>*)

subsection‹Finite map operations›

text‹

\label{sec:kbps-theory-map-ops}

The algorithm represents an automaton as a pair of maps, which we
capture abstractly with a record and a predicate:

›

record ('m, 'k, 'e) MapOps =
  empty :: "'m"
  lookup :: "'m ⇒ 'k ⇀ 'e"
  update :: "'k ⇒ 'e ⇒ 'm ⇒ 'm"

definition
  MapOps :: "('k ⇒ 'kabs) ⇒ 'kabs set ⇒ ('m, 'k, 'e) MapOps ⇒ bool"
where
  "MapOps α d ops ≡
      (∀k. α k ∈ d ⟶ lookup ops (empty ops) k = None)
    ∧ (∀e k k' M. α k ∈ d ∧ α k' ∈ d
        ⟶ lookup ops (update ops k e M) k'
          = (if α k' = α k then Some e else lookup ops M k'))"
(*<*)

lemma MapOpsI[intro]:
  "⟦ ⋀k. α k ∈ d ⟹ lookup ops (empty ops) k = None;
     ⋀e k k' M. ⟦ α k ∈ d; α k' ∈ d ⟧ ⟹
                 lookup ops (update ops k e M) k'
              = (if α k' = α k then Some e else lookup ops M k') ⟧
     ⟹ MapOps α d ops"
  unfolding MapOps_def by blast

lemma MapOps_emptyD:
  "⟦ α k ∈ d; MapOps α d ops ⟧ ⟹ lookup ops (empty ops) k = None"
  unfolding MapOps_def by simp

lemma MapOps_lookup_updateD:
  "⟦ α k ∈ d; α k' ∈ d; MapOps α d ops ⟧ ⟹ lookup ops (update ops k e M) k' = (if α k' = α k then Some e else lookup ops M k')"
  unfolding MapOps_def by simp

(*>*)

text‹

The function @{term "α"} abstracts concrete keys of type @{typ "'k"},
and the parameter @{term "d"} specifies the valid abstract keys.

This approach has the advantage over a locale that we can pass records
to functions, while for a locale we would need to pass the three
functions separately (as in the DFS theory of \S\ref{sec:dfs}).

We use the following function to test for membership in the domain of
the map:

›

definition isSome :: "'a option ⇒ bool" where
  "isSome opt ≡ case opt of None ⇒ False | Some _ ⇒ True"
(*<*)

lemma isSome_simps[simp]:
  "⋀x. isSome (Some x)"
  "⋀x. ¬ isSome x ⟷ x = None"
  unfolding isSome_def by (auto split: option.split)

lemma isSome_eq:
  "isSome x ⟷ (∃y. x = Some y)"
  unfolding isSome_def by (auto split: option.split)

lemma isSomeE: "⟦ isSome x; ⋀s. x = Some s ⟹ Q ⟧ ⟹ Q"
  unfolding isSome_def by (cases x) auto

end
(*>*)