src/HOL/Map.thy
changeset 34941 156925dd67af
parent 33635 dcaada178c6f
child 34979 8cb6e7a42e9c
     1.1 --- a/src/HOL/Map.thy	Sat Jan 16 17:15:27 2010 +0100
     1.2 +++ b/src/HOL/Map.thy	Sat Jan 16 17:15:28 2010 +0100
     1.3 @@ -51,10 +51,6 @@
     1.4    map_le :: "('a ~=> 'b) => ('a ~=> 'b) => bool"  (infix "\<subseteq>\<^sub>m" 50) where
     1.5    "(m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2) = (\<forall>a \<in> dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a)"
     1.6  
     1.7 -consts
     1.8 -  map_of :: "('a * 'b) list => 'a ~=> 'b"
     1.9 -  map_upds :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    1.10 -
    1.11  nonterminals
    1.12    maplets maplet
    1.13  
    1.14 @@ -73,25 +69,27 @@
    1.15  translations
    1.16    "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    1.17    "_MapUpd m (_maplet  x y)"    == "m(x:=Some y)"
    1.18 -  "_MapUpd m (_maplets x y)"    == "map_upds m x y"
    1.19    "_Map ms"                     == "_MapUpd (CONST empty) ms"
    1.20    "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
    1.21    "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    1.22  
    1.23  primrec
    1.24 -  "map_of [] = empty"
    1.25 -  "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    1.26 +  map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
    1.27 +    "map_of [] = empty"
    1.28 +  | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
    1.29  
    1.30 -declare map_of.simps [code del]
    1.31 +definition
    1.32 +  map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b" where
    1.33 +  "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
    1.34 +
    1.35 +translations
    1.36 +  "_MapUpd m (_maplets x y)"    == "CONST map_upds m x y"
    1.37  
    1.38  lemma map_of_Cons_code [code]: 
    1.39    "map_of [] k = None"
    1.40    "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
    1.41    by simp_all
    1.42  
    1.43 -defs
    1.44 -  map_upds_def [code]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
    1.45 -
    1.46  
    1.47  subsection {* @{term [source] empty} *}
    1.48