# Theory MapOps

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

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
(*>*)