src/HOL/Map.thy
author oheimb
Wed Aug 12 16:04:27 1998 +0200 (1998-08-12)
changeset 5300 2b1ca524ace8
parent 5195 277831ae7eac
child 7958 f531589c9fc1
permissions -rw-r--r--
defined map_upd by translation via fun_upd
changed syntax of map_upd to be consistent with that of fun_upd
added chg_map, map_upds
     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 
    23 
    24 syntax
    25 map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    26 					         ("_/'(_/|->_')"   [900,0,0]900)
    27 
    28 syntax (symbols)
    29   "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
    30   map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
    31 					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
    32   map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    33 				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
    34   override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
    35 				         (infixl "\\<oplus>" 100)
    36 
    37 translations
    38 
    39   "m(a|->b)" == "m(a:=Some b)"
    40 
    41 defs
    42 
    43 empty_def    "empty == %x. None"
    44 
    45 chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    46 
    47 override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    48 
    49 dom_def "dom(m) == {a. m a ~= None}"
    50 ran_def "ran(m) == {b. ? a. m a = Some b}"
    51 
    52 primrec
    53   "map_of [] = empty"
    54   "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    55 
    56 primrec "t([]  [|->]bs) = t"
    57         "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
    58 
    59 end