--- a/src/HOL/Map.thy Wed Aug 12 15:40:47 1998 +0200
+++ b/src/HOL/Map.thy Wed Aug 12 16:04:27 1998 +0200
@@ -11,26 +11,38 @@
types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
consts
-empty :: "'a ~=> 'b"
-map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
- ("_/[_/|->/_]" [900,0,0] 900)
+empty :: "'a ~=> 'b"
+chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
-dom :: "('a ~=> 'b) => 'a set"
-ran :: "('a ~=> 'b) => 'b set"
-map_of :: "('a * 'b)list => 'a ~=> 'b"
+dom :: "('a ~=> 'b) => 'a set"
+ran :: "('a ~=> 'b) => 'b set"
+map_of :: "('a * 'b)list => 'a ~=> 'b"
+map_upds:: "('a ~=> 'b) => 'a list => 'b list =>
+ ('a ~=> 'b)" ("_/'(_[|->]_/')" [900,0,0]900)
+
+
+syntax
+map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
+ ("_/'(_/|->_')" [900,0,0]900)
syntax (symbols)
- "~=>" :: [type, type] => type
- (infixr "\\<leadsto>" 0)
- map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
- ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
+ "~=>" :: [type, type] => type (infixr "\\<leadsto>" 0)
+ map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
+ ("_/'(_/\\<mapsto>/_')" [900,0,0]900)
+ map_upds :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
+ ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
override :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
- (infixl "\\<oplus>" 100)
+ (infixl "\\<oplus>" 100)
+
+translations
+
+ "m(a|->b)" == "m(a:=Some b)"
defs
-empty_def "empty == %x. None"
-map_upd_def "m[a|->b] == %x. if x=a then Some b else m x"
+empty_def "empty == %x. None"
+
+chg_map_def "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
@@ -39,6 +51,9 @@
primrec
"map_of [] = empty"
- "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
+ "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
+
+primrec "t([] [|->]bs) = t"
+ "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
end