src/HOL/Map.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10137 d1c2bef01e2f
child 12114 a8e860c86252
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Map.thy
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow, based on a theory by David von Oheimb
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     4
    Copyright   1997 TU Muenchen
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     5
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     6
The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     7
*)
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     8
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
     9
Map = List + Option +
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    10
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    11
types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    12
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    13
consts
5300
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    14
empty	::  "'a ~=> 'b"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    15
chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    16
override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
5300
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    17
dom	:: "('a ~=> 'b) => 'a set"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    18
ran	:: "('a ~=> 'b) => 'b set"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    19
map_of	:: "('a * 'b)list => 'a ~=> 'b"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    20
map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    21
	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    22
syntax
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    23
map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    24
					         ("_/'(_/|->_')"   [900,0,0]900)
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    25
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    26
syntax (symbols)
5300
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    27
  "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    28
  map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    29
					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    30
  map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    31
				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    32
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    33
translations
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    34
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    35
  "m(a|->b)" == "m(a:=Some b)"
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    36
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    37
defs
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    38
5300
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    39
empty_def    "empty == %x. None"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    40
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    41
chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    42
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    43
override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    44
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    45
dom_def "dom(m) == {a. m a ~= None}"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    46
ran_def "ran(m) == {b. ? a. m a = Some b}"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    47
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 3981
diff changeset
    48
primrec
89f162de39cf Adapted to new datatype package.
berghofe
parents: 3981
diff changeset
    49
  "map_of [] = empty"
5300
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    50
  "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    51
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    52
primrec "t([]  [|->]bs) = t"
2b1ca524ace8 defined map_upd by translation via fun_upd
oheimb
parents: 5195
diff changeset
    53
        "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
3981
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    54
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    55
end