src/HOL/Map.thy
author nipkow
Fri, 24 Oct 1997 10:31:31 +0200
changeset 3981 b4f93a8da835
child 5183 89f162de39cf
permissions -rw-r--r--
Added the new theory Map.
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
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    14
empty   :: "'a ~=> 'b"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    15
update  :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    16
           ("_/[_/|->/_]" [900,0,0] 900)
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    17
override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    18
dom     :: "('a ~=> 'b) => 'a set"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    19
ran     :: "('a ~=> 'b) => 'b set"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    20
map_of  :: "('a * 'b)list => 'a ~=> 'b"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    21
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    22
syntax (symbols)
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    23
  "~=>"     :: [type, type] => type
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    24
               (infixr "\\<leadsto>" 0)
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    25
  update    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    26
               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    27
  override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    28
               (infixl "\\<oplus>" 100)
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    29
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    30
defs
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    31
empty_def "empty == %x. None"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    32
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    33
update_def "m[a|->b] == %x. if x=a then Some b else m x"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    34
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    35
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
    36
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    37
dom_def "dom(m) == {a. m a ~= None}"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    38
ran_def "ran(m) == {b. ? a. m a = Some b}"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    39
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    40
primrec map_of list
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    41
"map_of [] = empty"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    42
"map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    43
b4f93a8da835 Added the new theory Map.
nipkow
parents:
diff changeset
    44
end