src/HOL/Map.thy
changeset 14376 9fe787a90a48
parent 14300 bf8b8c9425c3
child 14537 e95ba267e3d5
equal deleted inserted replaced
14375:a545da363b23 14376:9fe787a90a48
    79 map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    79 map_subst_def: "m(a~>b)     == %x. if m x = Some a then Some b else m x"
    80 
    80 
    81 dom_def: "dom(m) == {a. m a ~= None}"
    81 dom_def: "dom(m) == {a. m a ~= None}"
    82 ran_def: "ran(m) == {b. EX a. m a = Some b}"
    82 ran_def: "ran(m) == {b. EX a. m a = Some b}"
    83 
    83 
    84 map_le_def: "m1 \<subseteq>\<^sub>m m2  ==  ALL a : dom m1. m1 a = m2 a"
    84 map_le_def: "m\<^isub>1 \<subseteq>\<^sub>m m\<^isub>2  ==  ALL a : dom m\<^isub>1. m\<^isub>1 a = m\<^isub>2 a"
    85 
    85 
    86 primrec
    86 primrec
    87   "map_of [] = empty"
    87   "map_of [] = empty"
    88   "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    88   "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    89 
    89