9 Map = List + |
9 Map = List + |
10 |
10 |
11 types ('a,'b) "~=>" = 'a => 'b option (infixr 0) |
11 types ('a,'b) "~=>" = 'a => 'b option (infixr 0) |
12 |
12 |
13 consts |
13 consts |
14 empty :: "'a ~=> 'b" |
|
15 chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" |
14 chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" |
16 override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100) |
15 override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100) |
17 dom :: "('a ~=> 'b) => 'a set" |
16 dom :: "('a ~=> 'b) => 'a set" |
18 ran :: "('a ~=> 'b) => 'b set" |
17 ran :: "('a ~=> 'b) => 'b set" |
19 map_of :: "('a * 'b)list => 'a ~=> 'b" |
18 map_of :: "('a * 'b)list => 'a ~=> 'b" |
20 map_upds:: "('a ~=> 'b) => 'a list => 'b list => |
19 map_upds:: "('a ~=> 'b) => 'a list => 'b list => |
21 ('a ~=> 'b)" ("_/'(_[|->]_/')" [900,0,0]900) |
20 ('a ~=> 'b)" ("_/'(_[|->]_/')" [900,0,0]900) |
22 syntax |
21 syntax |
|
22 empty :: "'a ~=> 'b" |
23 map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)" |
23 map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)" |
24 ("_/'(_/|->_')" [900,0,0]900) |
24 ("_/'(_/|->_')" [900,0,0]900) |
25 |
25 |
26 syntax (xsymbols) |
26 syntax (xsymbols) |
27 "~=>" :: [type, type] => type (infixr "\\<leadsto>" 0) |
27 "~=>" :: [type, type] => type (infixr "\\<leadsto>" 0) |
29 ("_/'(_/\\<mapsto>/_')" [900,0,0]900) |
29 ("_/'(_/\\<mapsto>/_')" [900,0,0]900) |
30 map_upds :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)" |
30 map_upds :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)" |
31 ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900) |
31 ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900) |
32 |
32 |
33 translations |
33 translations |
|
34 "empty" => "_K None" |
|
35 "empty" <= "%x. None" |
34 |
36 |
35 "m(a|->b)" == "m(a:=Some b)" |
37 "m(a|->b)" == "m(a:=Some b)" |
36 |
38 |
37 defs |
39 defs |
38 |
|
39 empty_def "empty == %x. None" |
|
40 |
40 |
41 chg_map_def "chg_map f a m == case m a of None => m | Some b => m(a|->f b)" |
41 chg_map_def "chg_map f a m == case m a of None => m | Some b => m(a|->f b)" |
42 |
42 |
43 override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y" |
43 override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y" |
44 |
44 |