src/HOL/Map.thy
changeset 19378 6cc9ac729eb5
parent 19323 ec5cd5b1804c
child 19656 09be06943252
     1.1 --- a/src/HOL/Map.thy	Sun Apr 09 14:31:37 2006 +0200
     1.2 +++ b/src/HOL/Map.thy	Sun Apr 09 14:47:24 2006 +0200
     1.3 @@ -15,6 +15,14 @@
     1.4  types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
     1.5  translations (type) "a ~=> b " <= (type) "a => b option"
     1.6  
     1.7 +abbreviation
     1.8 +  empty     ::  "'a ~=> 'b"
     1.9 +  "empty == %x. None"
    1.10 +
    1.11 +constdefs
    1.12 +  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
    1.13 +  "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    1.14 +
    1.15  consts
    1.16  map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    1.17  restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`"  110)
    1.18 @@ -24,16 +32,6 @@
    1.19  map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    1.20  map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
    1.21  
    1.22 -constdefs
    1.23 -  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
    1.24 -  "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    1.25 -
    1.26 -syntax
    1.27 -  empty     ::  "'a ~=> 'b"
    1.28 -translations
    1.29 -  "empty"    => "%_. None"
    1.30 -  "empty"    <= "%x. None"
    1.31 -
    1.32  nonterminals
    1.33    maplets maplet
    1.34