# HG changeset patch
# User nipkow
# Date 1084342469 -7200
# Node ID 86c6f272ef794074ea8ea59e9071b7a546a4d6c7
# Parent  83f1a514dcb4648deb6c5c22aea9943e32846cca
renamed `> to o_m

diff -r 83f1a514dcb4 -r 86c6f272ef79 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue May 11 20:11:08 2004 +0200
+++ b/src/HOL/Map.thy	Wed May 12 08:14:29 2004 +0200
@@ -16,7 +16,6 @@
 consts
 chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
 map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
-map_image::"('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixr "`>" 90)
 restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_|'__" [90, 91] 90)
 dom	:: "('a ~=> 'b) => 'a set"
 ran	:: "('a ~=> 'b) => 'b set"
@@ -29,6 +28,11 @@
 	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
 map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
 
+syntax
+  fun_map_comp :: "('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
+translations
+  "f o_m m" == "option_map f o m"
+
 nonterminals
   maplets maplet
 
@@ -42,10 +46,13 @@
   "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
 
 syntax (xsymbols)
+  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
+
+  fun_map_comp :: "('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
+
   "_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_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
 				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
@@ -71,7 +78,6 @@
 chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
 
 map_add_def:   "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
-map_image_def: "f`>m == option_map f o m"
 restrict_map_def: "m|_A == %x. if x : A then m x else None"
 
 map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
@@ -272,15 +278,6 @@
 done
 declare fun_upd_apply [simp]
 
-subsection {* @{term map_image} *}
-
-lemma map_image_empty [simp]: "f`>empty = empty" 
-by (auto simp: map_image_def empty_def)
-
-lemma map_image_upd [simp]: "f`>m(a|->b) = (f`>m)(a|->f b)" 
-apply (auto simp: map_image_def fun_upd_def)
-by (rule ext, auto)
-
 subsection {* @{term restrict_map} *}
 
 lemma restrict_map_to_empty[simp]: "m\<lfloor>{} = empty"