Quelle  MapOps.thy

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

  algorithm represents an automaton as a pair of maps, which we
  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‹

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

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

  use the following function to test for membership in the domain of
  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
(*>*)