1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory DataMap
8imports Main
9begin
10
11type_synonym ('k, 'a) map = "'k \<rightharpoonup> 'a"
12
13definition
14  data_map_empty :: "('k, 'a) map"
15where
16  data_map_empty_def[simp]: "data_map_empty \<equiv> Map.empty"
17
18definition
19  data_map_insert :: "'k \<Rightarrow> 'a \<Rightarrow> ('k, 'a) map \<Rightarrow> ('k, 'a) map"
20where
21  data_map_insert_def[simp]: "data_map_insert x y m \<equiv> (m (x \<mapsto> y))"
22
23definition
24  lookupBefore :: "('k :: {linorder, finite}) \<Rightarrow> ('k, 'a) map \<Rightarrow> ('k \<times> 'a) option"
25where
26  "lookupBefore x m \<equiv>
27     let Ks = {k \<in> dom m. k \<le> x}
28     in if Ks = {} then None
29            else Some (Max Ks, the (m (Max Ks)))"
30
31definition
32  lookupAround :: "('k :: {linorder, finite}) \<Rightarrow> ('k, 'a) map
33                       \<Rightarrow> (('k \<times> 'a) option \<times> 'a option \<times> ('k \<times> 'a) option)"
34where
35  "lookupAround x m \<equiv>
36     let Bs = {k \<in> dom m. k < x};
37         As = {k \<in> dom m. k > x}
38     in (if Bs = {} then None else Some (Max Bs, the (m (Max Bs))),
39         m x,
40         if As = {} then None else Some (Min As, the (m (Min Bs))))"
41
42definition
43  data_map_filterWithKey :: "('k \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('k, 'a) map \<Rightarrow> ('k, 'a) map"
44where
45  "data_map_filterWithKey f m \<equiv> \<lambda>x. case m x of
46       None   \<Rightarrow> None
47     | Some y \<Rightarrow> if f x y then Some y else None"
48
49abbreviation(input)
50  "data_set_empty \<equiv> {}"
51
52abbreviation(input)
53  "data_set_insert \<equiv> insert"
54
55abbreviation(input)
56  "data_set_delete x S \<equiv> S - {x}"
57
58end
59