src/HOL/Map.thy
author nipkow
Tue Apr 01 17:43:10 2003 +0200 (2003-04-01)
changeset 13890 90611b4e0054
parent 12919 d6a0d168291e
child 13908 4bdfa9f77254
permissions -rw-r--r--
Made empty a translation rather than a constant.
     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 +
    10 
    11 types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
    12 
    13 consts
    14 chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
    15 override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    16 dom	:: "('a ~=> 'b) => 'a set"
    17 ran	:: "('a ~=> 'b) => 'b set"
    18 map_of	:: "('a * 'b)list => 'a ~=> 'b"
    19 map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
    20 	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
    21 syntax
    22 empty	::  "'a ~=> 'b"
    23 map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    24 					         ("_/'(_/|->_')"   [900,0,0]900)
    25 
    26 syntax (xsymbols)
    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   "empty"    => "_K None"
    35   "empty"    <= "%x. None"
    36 
    37   "m(a|->b)" == "m(a:=Some b)"
    38 
    39 defs
    40 
    41 chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    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 
    48 primrec
    49   "map_of [] = empty"
    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)"
    54 
    55 end