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