src/HOL/Map.thy
changeset 61955 e96292f32c3c
parent 61799 4cf66f21b764
child 62390 842917225d56
     1.1 --- a/src/HOL/Map.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Map.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -47,16 +47,16 @@
     1.4  nonterminal maplets and maplet
     1.5  
     1.6  syntax
     1.7 -  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /|->/ _")
     1.8 -  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[|->]/ _")
     1.9 +  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /\<mapsto>/ _")
    1.10 +  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[\<mapsto>]/ _")
    1.11    ""         :: "maplet \<Rightarrow> maplets"             ("_")
    1.12    "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _")
    1.13 -  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [900,0]900)
    1.14 +  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [900, 0] 900)
    1.15    "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"            ("(1[_])")
    1.16  
    1.17 -syntax (xsymbols)
    1.18 -  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /\<mapsto>/ _")
    1.19 -  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[\<mapsto>]/ _")
    1.20 +syntax (ASCII)
    1.21 +  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /|->/ _")
    1.22 +  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[|->]/ _")
    1.23  
    1.24  translations
    1.25    "_MapUpd m (_Maplets xy ms)"  \<rightleftharpoons> "_MapUpd (_MapUpd m xy) ms"
    1.26 @@ -65,15 +65,13 @@
    1.27    "_Map (_Maplets ms1 ms2)"     \<leftharpoondown> "_MapUpd (_Map ms1) ms2"
    1.28    "_Maplets ms1 (_Maplets ms2 ms3)" \<leftharpoondown> "_Maplets (_Maplets ms1 ms2) ms3"
    1.29  
    1.30 -primrec
    1.31 -  map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
    1.32 -    "map_of [] = empty"
    1.33 -  | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
    1.34 +primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b"
    1.35 +where
    1.36 +  "map_of [] = empty"
    1.37 +| "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
    1.38  
    1.39 -definition
    1.40 -  map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b" where
    1.41 -  "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
    1.42 -
    1.43 +definition map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b"
    1.44 +  where "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
    1.45  translations
    1.46    "_MapUpd m (_maplets x y)" \<rightleftharpoons> "CONST map_upds m x y"
    1.47