src/HOL/Map.thy
author wenzelm
Fri Nov 09 00:09:47 2001 +0100 (2001-11-09)
changeset 12114 a8e860c86252
parent 10137 d1c2bef01e2f
child 12919 d6a0d168291e
permissions -rw-r--r--
eliminated old "symbols" syntax, use "xsymbols" instead;
     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 chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
    16 override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    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)
    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 
    35   "m(a|->b)" == "m(a:=Some b)"
    36 
    37 defs
    38 
    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)"
    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