src/HOL/Map.thy
changeset 5300 2b1ca524ace8
parent 5195 277831ae7eac
child 7958 f531589c9fc1
     1.1 --- a/src/HOL/Map.thy	Wed Aug 12 15:40:47 1998 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed Aug 12 16:04:27 1998 +0200
     1.3 @@ -11,26 +11,38 @@
     1.4  types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
     1.5  
     1.6  consts
     1.7 -empty   :: "'a ~=> 'b"
     1.8 -map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
     1.9 -           ("_/[_/|->/_]" [900,0,0] 900)
    1.10 +empty	::  "'a ~=> 'b"
    1.11 +chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
    1.12  override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    1.13 -dom     :: "('a ~=> 'b) => 'a set"
    1.14 -ran     :: "('a ~=> 'b) => 'b set"
    1.15 -map_of  :: "('a * 'b)list => 'a ~=> 'b"
    1.16 +dom	:: "('a ~=> 'b) => 'a set"
    1.17 +ran	:: "('a ~=> 'b) => 'b set"
    1.18 +map_of	:: "('a * 'b)list => 'a ~=> 'b"
    1.19 +map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
    1.20 +	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
    1.21 +
    1.22 +
    1.23 +syntax
    1.24 +map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.25 +					         ("_/'(_/|->_')"   [900,0,0]900)
    1.26  
    1.27  syntax (symbols)
    1.28 -  "~=>"     :: [type, type] => type
    1.29 -               (infixr "\\<leadsto>" 0)
    1.30 -  map_upd    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    1.31 -               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
    1.32 +  "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
    1.33 +  map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
    1.34 +					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
    1.35 +  map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    1.36 +				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
    1.37    override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
    1.38 -               (infixl "\\<oplus>" 100)
    1.39 +				         (infixl "\\<oplus>" 100)
    1.40 +
    1.41 +translations
    1.42 +
    1.43 +  "m(a|->b)" == "m(a:=Some b)"
    1.44  
    1.45  defs
    1.46 -empty_def "empty == %x. None"
    1.47  
    1.48 -map_upd_def "m[a|->b] == %x. if x=a then Some b else m x"
    1.49 +empty_def    "empty == %x. None"
    1.50 +
    1.51 +chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.52  
    1.53  override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.54  
    1.55 @@ -39,6 +51,9 @@
    1.56  
    1.57  primrec
    1.58    "map_of [] = empty"
    1.59 -  "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
    1.60 +  "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    1.61 +
    1.62 +primrec "t([]  [|->]bs) = t"
    1.63 +        "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
    1.64  
    1.65  end