src/HOL/Map.thy
author oheimb
Wed Oct 27 19:32:19 1999 +0200 (1999-10-27)
changeset 7958 f531589c9fc1
parent 5300 2b1ca524ace8
child 10137 d1c2bef01e2f
permissions -rw-r--r--
added various little lemmas
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
syntax
oheimb@5300
    23
map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
oheimb@5300
    24
					         ("_/'(_/|->_')"   [900,0,0]900)
nipkow@3981
    25
nipkow@3981
    26
syntax (symbols)
oheimb@5300
    27
  "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
oheimb@5300
    28
  map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
oheimb@5300
    29
					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
oheimb@5300
    30
  map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
oheimb@5300
    31
				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
nipkow@3981
    32
  override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
oheimb@5300
    33
				         (infixl "\\<oplus>" 100)
oheimb@5300
    34
oheimb@5300
    35
translations
oheimb@5300
    36
oheimb@5300
    37
  "m(a|->b)" == "m(a:=Some b)"
nipkow@3981
    38
nipkow@3981
    39
defs
nipkow@3981
    40
oheimb@5300
    41
empty_def    "empty == %x. None"
oheimb@5300
    42
oheimb@5300
    43
chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
nipkow@3981
    44
nipkow@3981
    45
override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
nipkow@3981
    46
nipkow@3981
    47
dom_def "dom(m) == {a. m a ~= None}"
nipkow@3981
    48
ran_def "ran(m) == {b. ? a. m a = Some b}"
nipkow@3981
    49
berghofe@5183
    50
primrec
berghofe@5183
    51
  "map_of [] = empty"
oheimb@5300
    52
  "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
oheimb@5300
    53
oheimb@5300
    54
primrec "t([]  [|->]bs) = t"
oheimb@5300
    55
        "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
nipkow@3981
    56
nipkow@3981
    57
end