src/HOL/Map.thy
changeset 67091 1393c2340eec
parent 67051 e7e54a0b9197
child 67780 7655e6369c9f
     1.1 --- a/src/HOL/Map.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Map.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -258,11 +258,11 @@
     1.4  
     1.5  subsection \<open>@{const map_option} related\<close>
     1.6  
     1.7 -lemma map_option_o_empty [simp]: "map_option f o empty = empty"
     1.8 +lemma map_option_o_empty [simp]: "map_option f \<circ> empty = empty"
     1.9  by (rule ext) simp
    1.10  
    1.11  lemma map_option_o_map_upd [simp]:
    1.12 -  "map_option f o m(a\<mapsto>b) = (map_option f o m)(a\<mapsto>f b)"
    1.13 +  "map_option f \<circ> m(a\<mapsto>b) = (map_option f \<circ> m)(a\<mapsto>f b)"
    1.14  by (rule ext) simp
    1.15  
    1.16  
    1.17 @@ -299,7 +299,7 @@
    1.18  by (rule ext) (simp add: map_add_def split: option.split)
    1.19  
    1.20  lemma map_add_Some_iff:
    1.21 -  "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)"
    1.22 +  "((m ++ n) k = Some x) = (n k = Some x \<or> n k = None \<and> m k = Some x)"
    1.23  by (simp add: map_add_def split: option.split)
    1.24  
    1.25  lemma map_add_SomeD [dest!]:
    1.26 @@ -309,7 +309,7 @@
    1.27  lemma map_add_find_right [simp]: "n k = Some xx \<Longrightarrow> (m ++ n) k = Some xx"
    1.28  by (subst map_add_Some_iff) fast
    1.29  
    1.30 -lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
    1.31 +lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None \<and> m k = None)"
    1.32  by (simp add: map_add_def split: option.split)
    1.33  
    1.34  lemma map_add_upd[simp]: "f ++ g(x\<mapsto>y) = (f ++ g)(x\<mapsto>y)"