src/HOL/Map.thy
author nipkow
Fri Jul 24 17:18:15 1998 +0200 (1998-07-24)
changeset 5195 277831ae7eac
parent 5183 89f162de39cf
child 5300 2b1ca524ace8
permissions -rw-r--r--
Map.update -> map_upd, Unpdate.update -> fun_upd
Problem: macros get confused about two updates.
nipkow@3981
     1
(*  Title:      HOL/Map.thy
nipkow@3981
     2
    ID:         $Id$
nipkow@3981
     3
    Author:     Tobias Nipkow, based on a theory by David von Oheimb
nipkow@3981
     4
    Copyright   1997 TU Muenchen
nipkow@3981
     5
nipkow@3981
     6
The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
nipkow@3981
     7
*)
nipkow@3981
     8
nipkow@3981
     9
Map = List + Option +
nipkow@3981
    10
nipkow@3981
    11
types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
nipkow@3981
    12
nipkow@3981
    13
consts
nipkow@3981
    14
empty   :: "'a ~=> 'b"
nipkow@5195
    15
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
nipkow@3981
    16
           ("_/[_/|->/_]" [900,0,0] 900)
nipkow@3981
    17
override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
nipkow@3981
    18
dom     :: "('a ~=> 'b) => 'a set"
nipkow@3981
    19
ran     :: "('a ~=> 'b) => 'b set"
nipkow@3981
    20
map_of  :: "('a * 'b)list => 'a ~=> 'b"
nipkow@3981
    21
nipkow@3981
    22
syntax (symbols)
nipkow@3981
    23
  "~=>"     :: [type, type] => type
nipkow@3981
    24
               (infixr "\\<leadsto>" 0)
nipkow@5195
    25
  map_upd    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
nipkow@3981
    26
               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
nipkow@3981
    27
  override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
nipkow@3981
    28
               (infixl "\\<oplus>" 100)
nipkow@3981
    29
nipkow@3981
    30
defs
nipkow@3981
    31
empty_def "empty == %x. None"
nipkow@3981
    32
nipkow@5195
    33
map_upd_def "m[a|->b] == %x. if x=a then Some b else m x"
nipkow@3981
    34
nipkow@3981
    35
override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
nipkow@3981
    36
nipkow@3981
    37
dom_def "dom(m) == {a. m a ~= None}"
nipkow@3981
    38
ran_def "ran(m) == {b. ? a. m a = Some b}"
nipkow@3981
    39
berghofe@5183
    40
primrec
berghofe@5183
    41
  "map_of [] = empty"
berghofe@5183
    42
  "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
nipkow@3981
    43
nipkow@3981
    44
end