src/HOL/Map.thy
changeset 19656 09be06943252
parent 19378 6cc9ac729eb5
child 19947 29b376397cd5
     1.1 --- a/src/HOL/Map.thy	Tue May 16 21:32:56 2006 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue May 16 21:33:01 2006 +0200
     1.3 @@ -15,14 +15,20 @@
     1.4  types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
     1.5  translations (type) "a ~=> b " <= (type) "a => b option"
     1.6  
     1.7 +syntax (xsymbols)
     1.8 +  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
     1.9 +
    1.10  abbreviation
    1.11    empty     ::  "'a ~=> 'b"
    1.12    "empty == %x. None"
    1.13  
    1.14 -constdefs
    1.15 +definition
    1.16    map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
    1.17    "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    1.18  
    1.19 +const_syntax (xsymbols)
    1.20 +  map_comp  (infixl "\<circ>\<^sub>m" 55)
    1.21 +
    1.22  consts
    1.23  map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    1.24  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`"  110)
    1.25 @@ -32,6 +38,9 @@
    1.26  map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    1.27  map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    1.28  
    1.29 +const_syntax (latex output)
    1.30 +  restrict_map  ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
    1.31 +
    1.32  nonterminals
    1.33    maplets maplet
    1.34  
    1.35 @@ -44,17 +53,9 @@
    1.36    "_Map"     :: "maplets => 'a ~=> 'b"            ("(1[_])")
    1.37  
    1.38  syntax (xsymbols)
    1.39 -  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
    1.40 -
    1.41 -  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "\<circ>\<^sub>m" 55)
    1.42 -
    1.43    "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
    1.44    "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
    1.45  
    1.46 -syntax (latex output)
    1.47 -  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
    1.48 -  --"requires amssymb!"
    1.49 -
    1.50  translations
    1.51    "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    1.52    "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"