-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathLem_map_extra.thy
executable file
·68 lines (45 loc) · 2.49 KB
/
Lem_map_extra.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
chapter {* Generated by Lem from map_extra.lem. *}
theory "Lem_map_extra"
imports
Main
"Lem_bool"
"Lem_basic_classes"
"Lem_function"
"Lem_assert_extra"
"Lem_maybe"
"Lem_list"
"Lem_num"
"Lem_set"
"Lem_map"
begin
(*open import Bool Basic_classes Function Assert_extra Maybe List Num Set Map*)
(* -------------------------------------------------------------------------- *)
(* find *)
(* -------------------------------------------------------------------------- *)
(*val find : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> 'v*)
(*let find k m= match (lookup k m) with Just x -> x | Nothing -> failwith Map_extra.find end*)
(* -------------------------------------------------------------------------- *)
(* from sets / domain / range *)
(* -------------------------------------------------------------------------- *)
(*val fromSet : forall 'k 'v. MapKeyType 'k => ('k -> 'v) -> set 'k -> map 'k 'v*)
definition fromSet :: "('k \<Rightarrow> 'v)\<Rightarrow> 'k set \<Rightarrow>('k,'v)Map.map " where
" fromSet f s = ( Finite_Set.fold (\<lambda> k m . map_update k (f k) m) Map.empty s )"
(*
assert fromSet_0: (fromSet succ (Set.empty : set nat) = Map.empty)
assert fromSet_1: (fromSet succ {(2:nat); 3; 4}) = Map.fromList [(2,3); (3, 4); (4, 5)]
*)
(* -------------------------------------------------------------------------- *)
(* fold *)
(* -------------------------------------------------------------------------- *)
(*val fold : forall 'k 'v 'r. MapKeyType 'k, SetType 'k, SetType 'v => ('k -> 'v -> 'r -> 'r) -> map 'k 'v -> 'r -> 'r*)
definition fold :: "('k \<Rightarrow> 'v \<Rightarrow> 'r \<Rightarrow> 'r)\<Rightarrow>('k,'v)Map.map \<Rightarrow> 'r \<Rightarrow> 'r " where
" fold f m v = ( Finite_Set.fold (\<lambda> (k, v) r . f k v r) v (map_to_set m))"
(*
assert fold_1: (fold (fun k v a -> (a+k)) (Map.fromList [((2:nat),(3:nat)); (3, 4); (4, 5)]) 0 = 9)
assert fold_2: (fold (fun k v a -> (a+v)) (Map.fromList [((2:nat),(3:nat)); (3, 4); (4, 5)]) 0 = 12)
*)
(*val toList: forall 'k 'v. MapKeyType 'k => map 'k 'v -> list ('k * 'v)*)
(* more 'map' functions *)
(* TODO: this function is in map_extra rather than map just for implementation reasons *)
(*val mapMaybe : forall 'a 'b 'c. MapKeyType 'a => ('a -> 'b -> maybe 'c) -> map 'a 'b -> map 'a 'c*)
end