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
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
oheimb@5300
    14
empty	::  "'a ~=> 'b"
oheimb@5300
    15
chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
nipkow@3981
    16
override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
oheimb@5300
    17
dom	:: "('a ~=> 'b) => 'a set"
oheimb@5300
    18
ran	:: "('a ~=> 'b) => 'b set"
oheimb@5300
    19
map_of	:: "('a * 'b)list => 'a ~=> 'b"
oheimb@5300
    20
map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
oheimb@5300
    21
	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
oheimb@5300
    22
oheimb@5300
    23
oheimb@5300
    24
syntax
oheimb@5300
    25
map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
oheimb@5300
    26
					         ("_/'(_/|->_')"   [900,0,0]900)
nipkow@3981
    27
nipkow@3981
    28
syntax (symbols)
oheimb@5300
    29
  "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
oheimb@5300
    30
  map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
oheimb@5300
    31
					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
oheimb@5300
    32
  map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
oheimb@5300
    33
				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
nipkow@3981
    34
  override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
oheimb@5300
    35
				         (infixl "\\<oplus>" 100)
oheimb@5300
    36
oheimb@5300
    37
translations
oheimb@5300
    38
oheimb@5300
    39
  "m(a|->b)" == "m(a:=Some b)"
nipkow@3981
    40
nipkow@3981
    41
defs
nipkow@3981
    42
oheimb@5300
    43
empty_def    "empty == %x. None"
oheimb@5300
    44
oheimb@5300
    45
chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
nipkow@3981
    46
nipkow@3981
    47
override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
nipkow@3981
    48
nipkow@3981
    49
dom_def "dom(m) == {a. m a ~= None}"
nipkow@3981
    50
ran_def "ran(m) == {b. ? a. m a = Some b}"
nipkow@3981
    51
berghofe@5183
    52
primrec
berghofe@5183
    53
  "map_of [] = empty"
oheimb@5300
    54
  "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
oheimb@5300
    55
oheimb@5300
    56
primrec "t([]  [|->]bs) = t"
oheimb@5300
    57
        "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
nipkow@3981
    58
nipkow@3981
    59
end