renamed `> to o_m
authornipkow
Wed May 12 08:14:29 2004 +0200 (2004-05-12)
changeset 1473986c6f272ef79
parent 14738 83f1a514dcb4
child 14740 c8e1937110c2
renamed `> to o_m
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.thy	Tue May 11 20:11:08 2004 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed May 12 08:14:29 2004 +0200
     1.3 @@ -16,7 +16,6 @@
     1.4  consts
     1.5  chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
     1.6  map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
     1.7 -map_image::"('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixr "`>" 90)
     1.8  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_|'__" [90, 91] 90)
     1.9  dom	:: "('a ~=> 'b) => 'a set"
    1.10  ran	:: "('a ~=> 'b) => 'b set"
    1.11 @@ -29,6 +28,11 @@
    1.12  	    ('a ~=> 'b)"			 ("_/'(_~>_/')"    [900,0,0]900)
    1.13  map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    1.14  
    1.15 +syntax
    1.16 +  fun_map_comp :: "('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
    1.17 +translations
    1.18 +  "f o_m m" == "option_map f o m"
    1.19 +
    1.20  nonterminals
    1.21    maplets maplet
    1.22  
    1.23 @@ -42,10 +46,13 @@
    1.24    "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
    1.25  
    1.26  syntax (xsymbols)
    1.27 +  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
    1.28 +
    1.29 +  fun_map_comp :: "('b => 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
    1.30 +
    1.31    "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
    1.32    "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
    1.33  
    1.34 -  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
    1.35    restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<lfloor>_" [90, 91] 90)
    1.36    map_upd_s  :: "('a ~=> 'b) => 'a set => 'b => ('a ~=> 'b)"
    1.37  				    		 ("_/'(_/{\<mapsto>}/_')" [900,0,0]900)
    1.38 @@ -71,7 +78,6 @@
    1.39  chg_map_def:  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    1.40  
    1.41  map_add_def:   "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    1.42 -map_image_def: "f`>m == option_map f o m"
    1.43  restrict_map_def: "m|_A == %x. if x : A then m x else None"
    1.44  
    1.45  map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    1.46 @@ -272,15 +278,6 @@
    1.47  done
    1.48  declare fun_upd_apply [simp]
    1.49  
    1.50 -subsection {* @{term map_image} *}
    1.51 -
    1.52 -lemma map_image_empty [simp]: "f`>empty = empty" 
    1.53 -by (auto simp: map_image_def empty_def)
    1.54 -
    1.55 -lemma map_image_upd [simp]: "f`>m(a|->b) = (f`>m)(a|->f b)" 
    1.56 -apply (auto simp: map_image_def fun_upd_def)
    1.57 -by (rule ext, auto)
    1.58 -
    1.59  subsection {* @{term restrict_map} *}
    1.60  
    1.61  lemma restrict_map_to_empty[simp]: "m\<lfloor>{} = empty"