# HG changeset patch
# User nipkow
# Date 1062606057 -7200
# Node ID d2e550609c408d8056e498b822ea781f749f5239
# Parent  04f905c13502d64a4da01e33df85aab289826ebb
Introduced new syntax for maplets x |-> y

diff -r 04f905c13502 -r d2e550609c40 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Sep 01 15:07:43 2003 +0200
+++ b/src/HOL/Map.thy	Wed Sep 03 18:20:57 2003 +0200
@@ -22,25 +22,31 @@
 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)
+	    ('a ~=> 'b)"
 map_upd_s::"('a ~=> 'b) => 'a set => 'b => 
 	    ('a ~=> 'b)"			 ("_/'(_{|->}_/')" [900,0,0]900)
 map_subst::"('a ~=> 'b) => 'b => 'b => 
 	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
 map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
 
+nonterminals
+  maplets maplet
+
 syntax
-empty	::  "'a ~=> 'b"
-map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
-					 ("_/'(_/|->_')"   [900,0,0]900)
+  empty	    ::  "'a ~=> 'b"
+  "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
+  "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
+  ""         :: "maplet => maplets"             ("_")
+  "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
+  "_MapUpd"  :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
+  "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
 
 syntax (xsymbols)
+  "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
+  "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
+
   "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
   restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<lfloor>_" [90, 91] 90)
-  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)
   map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
 				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
   map_subst :: "('a ~=> 'b) => 'b => 'b => 
@@ -52,9 +58,15 @@
   "empty"    => "_K None"
   "empty"    <= "%x. None"
 
-  "m(a|->b)" == "m(a:=Some b)"
   "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
 
+  "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
+  "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
+  "_MapUpd m (_maplets x y)"    == "map_upds m x y"
+  "_Map ms"                     == "_MapUpd empty ms"
+  "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
+  "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
+
 defs
 chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"