src/HOL/Map.thy
author berghofe
Fri Jul 24 13:03:20 1998 +0200 (1998-07-24)
changeset 5183 89f162de39cf
parent 3981 b4f93a8da835
child 5195 277831ae7eac
permissions -rw-r--r--
Adapted to new datatype package.
     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
    14 empty   :: "'a ~=> 'b"
    15 update  :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    16            ("_/[_/|->/_]" [900,0,0] 900)
    17 override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    18 dom     :: "('a ~=> 'b) => 'a set"
    19 ran     :: "('a ~=> 'b) => 'b set"
    20 map_of  :: "('a * 'b)list => 'a ~=> 'b"
    21 
    22 syntax (symbols)
    23   "~=>"     :: [type, type] => type
    24                (infixr "\\<leadsto>" 0)
    25   update    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    26                ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
    27   override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
    28                (infixl "\\<oplus>" 100)
    29 
    30 defs
    31 empty_def "empty == %x. None"
    32 
    33 update_def "m[a|->b] == %x. if x=a then Some b else m x"
    34 
    35 override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    36 
    37 dom_def "dom(m) == {a. m a ~= None}"
    38 ran_def "ran(m) == {b. ? a. m a = Some b}"
    39 
    40 primrec
    41   "map_of [] = empty"
    42   "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
    43 
    44 end