3981

1 
(* Title: HOL/Map.thy


2 
ID: $Id$


3 
Author: Tobias Nipkow, based on a theory by David von Oheimb


4 
Copyright 1997 TU Muenchen


5 


6 
The datatype of `maps' (written ~=>); strongly resembles maps in VDM.


7 
*)


8 


9 
Map = List + Option +


10 


11 
types ('a,'b) "~=>" = 'a => 'b option (infixr 0)


12 


13 
consts

5300

14 
empty :: "'a ~=> 'b"


15 
chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"

3981

16 
override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)

5300

17 
dom :: "('a ~=> 'b) => 'a set"


18 
ran :: "('a ~=> 'b) => 'b set"


19 
map_of :: "('a * 'b)list => 'a ~=> 'b"


20 
map_upds:: "('a ~=> 'b) => 'a list => 'b list =>


21 
('a ~=> 'b)" ("_/'(_[>]_/')" [900,0,0]900)


22 
syntax


23 
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"


24 
("_/'(_/>_')" [900,0,0]900)

3981

25 


26 
syntax (symbols)

5300

27 
"~=>" :: [type, type] => type (infixr "\\<leadsto>" 0)


28 
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"


29 
("_/'(_/\\<mapsto>/_')" [900,0,0]900)


30 
map_upds :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"


31 
("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)


32 


33 
translations


34 


35 
"m(a>b)" == "m(a:=Some b)"

3981

36 


37 
defs


38 

5300

39 
empty_def "empty == %x. None"


40 


41 
chg_map_def "chg_map f a m == case m a of None => m  Some b => m(a>f b)"

3981

42 


43 
override_def "m1++m2 == %x. case m2 x of None => m1 x  Some y => Some y"


44 


45 
dom_def "dom(m) == {a. m a ~= None}"


46 
ran_def "ran(m) == {b. ? a. m a = Some b}"


47 

5183

48 
primrec


49 
"map_of [] = empty"

5300

50 
"map_of (p#ps) = (map_of ps)(fst p > snd p)"


51 


52 
primrec "t([] [>]bs) = t"


53 
"t(a#as[>]bs) = t(a>hd bs)(as[>]tl bs)"

3981

54 


55 
end
