src/HOL/Map.thy
changeset 3981 b4f93a8da835
child 5183 89f162de39cf
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Map.thy	Fri Oct 24 10:31:31 1997 +0200
     1.3 @@ -0,0 +1,44 @@
     1.4 +(*  Title:      HOL/Map.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow, based on a theory by David von Oheimb
     1.7 +    Copyright   1997 TU Muenchen
     1.8 +
     1.9 +The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
    1.10 +*)
    1.11 +
    1.12 +Map = List + Option +
    1.13 +
    1.14 +types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
    1.15 +
    1.16 +consts
    1.17 +empty   :: "'a ~=> 'b"
    1.18 +update  :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.19 +           ("_/[_/|->/_]" [900,0,0] 900)
    1.20 +override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    1.21 +dom     :: "('a ~=> 'b) => 'a set"
    1.22 +ran     :: "('a ~=> 'b) => 'b set"
    1.23 +map_of  :: "('a * 'b)list => 'a ~=> 'b"
    1.24 +
    1.25 +syntax (symbols)
    1.26 +  "~=>"     :: [type, type] => type
    1.27 +               (infixr "\\<leadsto>" 0)
    1.28 +  update    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.29 +               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
    1.30 +  override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
    1.31 +               (infixl "\\<oplus>" 100)
    1.32 +
    1.33 +defs
    1.34 +empty_def "empty == %x. None"
    1.35 +
    1.36 +update_def "m[a|->b] == %x. if x=a then Some b else m x"
    1.37 +
    1.38 +override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.39 +
    1.40 +dom_def "dom(m) == {a. m a ~= None}"
    1.41 +ran_def "ran(m) == {b. ? a. m a = Some b}"
    1.42 +
    1.43 +primrec map_of list
    1.44 +"map_of [] = empty"
    1.45 +"map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
    1.46 +
    1.47 +end