src/HOL/Map.thy
changeset 60839 422ec7a3c18a
parent 60838 2d7eea27ceec
child 60841 144523e0678e
     1.1 --- a/src/HOL/Map.thy	Tue Aug 04 14:06:24 2015 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue Aug 04 14:29:45 2015 +0200
     1.3 @@ -11,65 +11,65 @@
     1.4  imports List
     1.5  begin
     1.6  
     1.7 -type_synonym ('a, 'b) "map" = "'a => 'b option" (infixr "~=>" 0)
     1.8 +type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "~=>" 0)
     1.9  
    1.10  type_notation (xsymbols)
    1.11    "map" (infixr "\<rightharpoonup>" 0)
    1.12  
    1.13  abbreviation
    1.14    empty :: "'a \<rightharpoonup> 'b" where
    1.15 -  "empty == %x. None"
    1.16 +  "empty \<equiv> \<lambda>x. None"
    1.17  
    1.18  definition
    1.19 -  map_comp :: "('b \<rightharpoonup> 'c) => ('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> 'c)"  (infixl "o'_m" 55) where
    1.20 +  map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)"  (infixl "o'_m" 55) where
    1.21    "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    1.22  
    1.23  notation (xsymbols)
    1.24    map_comp  (infixl "\<circ>\<^sub>m" 55)
    1.25  
    1.26  definition
    1.27 -  map_add :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> 'b)"  (infixl "++" 100) where
    1.28 -  "m1 ++ m2 = (\<lambda>x. case m2 x of None => m1 x | Some y => Some y)"
    1.29 +  map_add :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)"  (infixl "++" 100) where
    1.30 +  "m1 ++ m2 = (\<lambda>x. case m2 x of None \<Rightarrow> m1 x | Some y \<Rightarrow> Some y)"
    1.31  
    1.32  definition
    1.33 -  restrict_map :: "('a \<rightharpoonup> 'b) => 'a set => ('a \<rightharpoonup> 'b)"  (infixl "|`"  110) where
    1.34 -  "m|`A = (\<lambda>x. if x : A then m x else None)"
    1.35 +  restrict_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set \<Rightarrow> ('a \<rightharpoonup> 'b)"  (infixl "|`"  110) where
    1.36 +  "m|`A = (\<lambda>x. if x \<in> A then m x else None)"
    1.37  
    1.38  notation (latex output)
    1.39    restrict_map  ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
    1.40  
    1.41  definition
    1.42 -  dom :: "('a \<rightharpoonup> 'b) => 'a set" where
    1.43 -  "dom m = {a. m a ~= None}"
    1.44 +  dom :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set" where
    1.45 +  "dom m = {a. m a \<noteq> None}"
    1.46  
    1.47  definition
    1.48 -  ran :: "('a \<rightharpoonup> 'b) => 'b set" where
    1.49 -  "ran m = {b. EX a. m a = Some b}"
    1.50 +  ran :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'b set" where
    1.51 +  "ran m = {b. \<exists>a. m a = Some b}"
    1.52  
    1.53  definition
    1.54 -  map_le :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> 'b) => bool"  (infix "\<subseteq>\<^sub>m" 50) where
    1.55 -  "(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) = (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)"
    1.56 +  map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool"  (infix "\<subseteq>\<^sub>m" 50) where
    1.57 +  "(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) \<longleftrightarrow> (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)"
    1.58  
    1.59  nonterminal maplets and maplet
    1.60  
    1.61  syntax
    1.62 -  "_maplet"  :: "['a, 'a] => maplet"             ("_ /|->/ _")
    1.63 -  "_maplets" :: "['a, 'a] => maplet"             ("_ /[|->]/ _")
    1.64 -  ""         :: "maplet => maplets"             ("_")
    1.65 -  "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
    1.66 -  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] => 'a \<rightharpoonup> 'b" ("_/'(_')" [900,0]900)
    1.67 -  "_Map"     :: "maplets => 'a \<rightharpoonup> 'b"            ("(1[_])")
    1.68 +  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /|->/ _")
    1.69 +  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[|->]/ _")
    1.70 +  ""         :: "maplet \<Rightarrow> maplets"             ("_")
    1.71 +  "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _")
    1.72 +  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [900,0]900)
    1.73 +  "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"            ("(1[_])")
    1.74  
    1.75  syntax (xsymbols)
    1.76 -  "_maplet"  :: "['a, 'a] => maplet"             ("_ /\<mapsto>/ _")
    1.77 -  "_maplets" :: "['a, 'a] => maplet"             ("_ /[\<mapsto>]/ _")
    1.78 +  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /\<mapsto>/ _")
    1.79 +  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[\<mapsto>]/ _")
    1.80  
    1.81  translations
    1.82 -  "_MapUpd m (_Maplets xy ms)"  == "_MapUpd (_MapUpd m xy) ms"
    1.83 -  "_MapUpd m (_maplet  x y)"    == "m(x := CONST Some y)"
    1.84 -  "_Map ms"                     == "_MapUpd (CONST empty) ms"
    1.85 -  "_Map (_Maplets ms1 ms2)"     <= "_MapUpd (_Map ms1) ms2"
    1.86 -  "_Maplets ms1 (_Maplets ms2 ms3)" <= "_Maplets (_Maplets ms1 ms2) ms3"
    1.87 +  "_MapUpd m (_Maplets xy ms)"  \<rightleftharpoons> "_MapUpd (_MapUpd m xy) ms"
    1.88 +  "_MapUpd m (_maplet  x y)"    \<rightleftharpoons> "m(x := CONST Some y)"
    1.89 +  "_Map ms"                     \<rightleftharpoons> "_MapUpd (CONST empty) ms"
    1.90 +  "_Map (_Maplets ms1 ms2)"     \<leftharpoondown> "_MapUpd (_Map ms1) ms2"
    1.91 +  "_Maplets ms1 (_Maplets ms2 ms3)" \<leftharpoondown> "_Maplets (_Maplets ms1 ms2) ms3"
    1.92  
    1.93  primrec
    1.94    map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
    1.95 @@ -81,9 +81,9 @@
    1.96    "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
    1.97  
    1.98  translations
    1.99 -  "_MapUpd m (_maplets x y)"    == "CONST map_upds m x y"
   1.100 +  "_MapUpd m (_maplets x y)" \<rightleftharpoons> "CONST map_upds m x y"
   1.101  
   1.102 -lemma map_of_Cons_code [code]: 
   1.103 +lemma map_of_Cons_code [code]:
   1.104    "map_of [] k = None"
   1.105    "map_of ((l, v) # ps) k = (if l = k then Some v else map_of ps k)"
   1.106    by simp_all
   1.107 @@ -92,15 +92,15 @@
   1.108  subsection \<open>@{term [source] empty}\<close>
   1.109  
   1.110  lemma empty_upd_none [simp]: "empty(x := None) = empty"
   1.111 -by (rule ext) simp
   1.112 +  by (rule ext) simp
   1.113  
   1.114  
   1.115  subsection \<open>@{term [source] map_upd}\<close>
   1.116  
   1.117 -lemma map_upd_triv: "t k = Some x ==> t(k\<mapsto>x) = t"
   1.118 -by (rule ext) simp
   1.119 +lemma map_upd_triv: "t k = Some x \<Longrightarrow> t(k\<mapsto>x) = t"
   1.120 +  by (rule ext) simp
   1.121  
   1.122 -lemma map_upd_nonempty [simp]: "t(k\<mapsto>x) ~= empty"
   1.123 +lemma map_upd_nonempty [simp]: "t(k\<mapsto>x) \<noteq> empty"
   1.124  proof
   1.125    assume "t(k \<mapsto> x) = empty"
   1.126    then have "(t(k \<mapsto> x)) k = None" by simp
   1.127 @@ -122,7 +122,7 @@
   1.128  lemma image_map_upd [simp]: "x \<notin> A \<Longrightarrow> m(x \<mapsto> y) ` A = m ` A"
   1.129  by auto
   1.130  
   1.131 -lemma finite_range_updI: "finite (range f) ==> finite (range (f(a\<mapsto>b)))"
   1.132 +lemma finite_range_updI: "finite (range f) \<Longrightarrow> finite (range (f(a\<mapsto>b)))"
   1.133  unfolding image_def
   1.134  apply (simp (no_asm_use) add:full_SetCompr_eq)
   1.135  apply (rule finite_subset)
   1.136 @@ -152,7 +152,7 @@
   1.137  
   1.138  lemma Some_eq_map_of_iff [simp]:
   1.139    "distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
   1.140 -by (auto simp del:map_of_eq_Some_iff simp add: map_of_eq_Some_iff [symmetric])
   1.141 +by (auto simp del: map_of_eq_Some_iff simp: map_of_eq_Some_iff [symmetric])
   1.142  
   1.143  lemma map_of_is_SomeI [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
   1.144      \<Longrightarrow> map_of xys x = Some y"
   1.145 @@ -200,7 +200,9 @@
   1.146      and dist: "distinct xs"
   1.147      and map_of: "map_of (zip xs ys) = map_of (zip xs zs)"
   1.148    shows "ys = zs"
   1.149 -using assms(1) assms(2)[symmetric] using dist map_of proof (induct ys xs zs rule: list_induct3)
   1.150 +  using assms(1) assms(2)[symmetric]
   1.151 +  using dist map_of
   1.152 +proof (induct ys xs zs rule: list_induct3)
   1.153    case Nil show ?case by simp
   1.154  next
   1.155    case (Cons y ys x xs z zs)
   1.156 @@ -230,11 +232,11 @@
   1.157  by (induct xs) (simp, atomize (full), auto)
   1.158  
   1.159  lemma map_of_mapk_SomeI:
   1.160 -  "inj f ==> map_of t k = Some x ==>
   1.161 -   map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
   1.162 -by (induct t) (auto simp add: inj_eq)
   1.163 +  "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>
   1.164 +   map_of (map (split (\<lambda>k. Pair (f k))) t) (f k) = Some x"
   1.165 +by (induct t) (auto simp: inj_eq)
   1.166  
   1.167 -lemma weak_map_of_SomeI: "(k, x) : set l ==> \<exists>x. map_of l k = Some x"
   1.168 +lemma weak_map_of_SomeI: "(k, x) \<in> set l \<Longrightarrow> \<exists>x. map_of l k = Some x"
   1.169  by (induct l) auto
   1.170  
   1.171  lemma map_of_filter_in:
   1.172 @@ -243,7 +245,7 @@
   1.173  
   1.174  lemma map_of_map:
   1.175    "map_of (map (\<lambda>(k, v). (k, f v)) xs) = map_option f \<circ> map_of xs"
   1.176 -  by (induct xs) (auto simp add: fun_eq_iff)
   1.177 +  by (induct xs) (auto simp: fun_eq_iff)
   1.178  
   1.179  lemma dom_map_option:
   1.180    "dom (\<lambda>k. map_option (f k) (m k)) = dom m"
   1.181 @@ -269,20 +271,20 @@
   1.182  lemma map_comp_empty [simp]:
   1.183    "m \<circ>\<^sub>m empty = empty"
   1.184    "empty \<circ>\<^sub>m m = empty"
   1.185 -by (auto simp add: map_comp_def split: option.splits)
   1.186 +by (auto simp: map_comp_def split: option.splits)
   1.187  
   1.188  lemma map_comp_simps [simp]:
   1.189    "m2 k = None \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = None"
   1.190    "m2 k = Some k' \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = m1 k'"
   1.191 -by (auto simp add: map_comp_def)
   1.192 +by (auto simp: map_comp_def)
   1.193  
   1.194  lemma map_comp_Some_iff:
   1.195    "((m1 \<circ>\<^sub>m m2) k = Some v) = (\<exists>k'. m2 k = Some k' \<and> m1 k' = Some v)"
   1.196 -by (auto simp add: map_comp_def split: option.splits)
   1.197 +by (auto simp: map_comp_def split: option.splits)
   1.198  
   1.199  lemma map_comp_None_iff:
   1.200    "((m1 \<circ>\<^sub>m m2) k = None) = (m2 k = None \<or> (\<exists>k'. m2 k = Some k' \<and> m1 k' = None)) "
   1.201 -by (auto simp add: map_comp_def split: option.splits)
   1.202 +by (auto simp: map_comp_def split: option.splits)
   1.203  
   1.204  
   1.205  subsection \<open>@{text "++"}\<close>
   1.206 @@ -304,7 +306,7 @@
   1.207    "(m ++ n) k = Some x \<Longrightarrow> n k = Some x \<or> n k = None \<and> m k = Some x"
   1.208  by (rule map_add_Some_iff [THEN iffD1])
   1.209  
   1.210 -lemma map_add_find_right [simp]: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx"
   1.211 +lemma map_add_find_right [simp]: "n k = Some xx \<Longrightarrow> (m ++ n) k = Some xx"
   1.212  by (subst map_add_Some_iff) fast
   1.213  
   1.214  lemma map_add_None [iff]: "((m ++ n) k = None) = (n k = None & m k = None)"
   1.215 @@ -328,7 +330,7 @@
   1.216  done
   1.217  
   1.218  lemma finite_range_map_of_map_add:
   1.219 -  "finite (range f) ==> finite (range (f ++ map_of l))"
   1.220 +  "finite (range f) \<Longrightarrow> finite (range (f ++ map_of l))"
   1.221  apply (induct l)
   1.222   apply (auto simp del: fun_upd_apply)
   1.223  apply (erule finite_range_updI)
   1.224 @@ -349,7 +351,7 @@
   1.225  
   1.226  lemma map_add_map_of_foldr:
   1.227    "m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m"
   1.228 -  by (induct ps) (auto simp add: fun_eq_iff map_add_def)
   1.229 +  by (induct ps) (auto simp: fun_eq_iff map_add_def)
   1.230  
   1.231  
   1.232  subsection \<open>@{term [source] restrict_map}\<close>
   1.233 @@ -358,7 +360,7 @@
   1.234  by (simp add: restrict_map_def)
   1.235  
   1.236  lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
   1.237 -by (auto simp add: restrict_map_def)
   1.238 +by (auto simp: restrict_map_def)
   1.239  
   1.240  lemma restrict_map_empty [simp]: "empty|`D = empty"
   1.241  by (simp add: restrict_map_def)
   1.242 @@ -386,7 +388,7 @@
   1.243  by (simp add: restrict_map_def fun_eq_iff)
   1.244  
   1.245  lemma fun_upd_None_restrict [simp]:
   1.246 -  "(m|`D)(x := None) = (if x:D then m|`(D - {x}) else m|`D)"
   1.247 +  "(m|`D)(x := None) = (if x \<in> D then m|`(D - {x}) else m|`D)"
   1.248  by (simp add: restrict_map_def fun_eq_iff)
   1.249  
   1.250  lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
   1.251 @@ -416,9 +418,9 @@
   1.252  lemma map_upds_Cons [simp]: "m(a#as [\<mapsto>] b#bs) = (m(a\<mapsto>b))(as[\<mapsto>]bs)"
   1.253  by (simp add:map_upds_def)
   1.254  
   1.255 -lemma map_upds_append1 [simp]: "\<And>ys m. size xs < size ys \<Longrightarrow>
   1.256 +lemma map_upds_append1 [simp]: "size xs < size ys \<Longrightarrow>
   1.257    m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
   1.258 -apply(induct xs)
   1.259 +apply(induct xs arbitrary: ys m)
   1.260   apply (clarsimp simp add: neq_Nil_conv)
   1.261  apply (case_tac ys)
   1.262   apply simp
   1.263 @@ -436,7 +438,7 @@
   1.264  
   1.265  lemma map_upd_upds_conv_if:
   1.266    "(f(x\<mapsto>y))(xs [\<mapsto>] ys) =
   1.267 -   (if x : set(take (length ys) xs) then f(xs [\<mapsto>] ys)
   1.268 +   (if x \<in> set(take (length ys) xs) then f(xs [\<mapsto>] ys)
   1.269                                      else (f(xs [\<mapsto>] ys))(x\<mapsto>y))"
   1.270  apply (induct xs arbitrary: x y ys f)
   1.271   apply simp
   1.272 @@ -445,11 +447,11 @@
   1.273  done
   1.274  
   1.275  lemma map_upds_twist [simp]:
   1.276 -  "a ~: set as ==> m(a\<mapsto>b)(as[\<mapsto>]bs) = m(as[\<mapsto>]bs)(a\<mapsto>b)"
   1.277 +  "a \<notin> set as \<Longrightarrow> m(a\<mapsto>b)(as[\<mapsto>]bs) = m(as[\<mapsto>]bs)(a\<mapsto>b)"
   1.278  using set_take_subset by (fastforce simp add: map_upd_upds_conv_if)
   1.279  
   1.280  lemma map_upds_apply_nontin [simp]:
   1.281 -  "x ~: set xs ==> (f(xs[\<mapsto>]ys)) x = f x"
   1.282 +  "x \<notin> set xs \<Longrightarrow> (f(xs[\<mapsto>]ys)) x = f x"
   1.283  apply (induct xs arbitrary: ys)
   1.284   apply simp
   1.285  apply (case_tac ys)
   1.286 @@ -490,22 +492,22 @@
   1.287  lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
   1.288    by (auto simp: dom_def)
   1.289  
   1.290 -lemma domI: "m a = Some b ==> a : dom m"
   1.291 -by(simp add:dom_def)
   1.292 +lemma domI: "m a = Some b \<Longrightarrow> a \<in> dom m"
   1.293 +  by (simp add: dom_def)
   1.294  (* declare domI [intro]? *)
   1.295  
   1.296 -lemma domD: "a : dom m ==> \<exists>b. m a = Some b"
   1.297 -by (cases "m a") (auto simp add: dom_def)
   1.298 +lemma domD: "a \<in> dom m \<Longrightarrow> \<exists>b. m a = Some b"
   1.299 +  by (cases "m a") (auto simp add: dom_def)
   1.300  
   1.301 -lemma domIff [iff, simp del]: "(a : dom m) = (m a ~= None)"
   1.302 -by(simp add:dom_def)
   1.303 +lemma domIff [iff, simp del]: "a \<in> dom m \<longleftrightarrow> m a \<noteq> None"
   1.304 +  by (simp add: dom_def)
   1.305  
   1.306  lemma dom_empty [simp]: "dom empty = {}"
   1.307 -by(simp add:dom_def)
   1.308 +  by (simp add: dom_def)
   1.309  
   1.310  lemma dom_fun_upd [simp]:
   1.311 -  "dom(f(x := y)) = (if y=None then dom f - {x} else insert x (dom f))"
   1.312 -by(auto simp add:dom_def)
   1.313 +  "dom(f(x := y)) = (if y = None then dom f - {x} else insert x (dom f))"
   1.314 +  by (auto simp: dom_def)
   1.315  
   1.316  lemma dom_if:
   1.317    "dom (\<lambda>x. if P x then f x else g x) = dom f \<inter> {x. P x} \<union> dom g \<inter> {x. \<not> P x}"
   1.318 @@ -515,36 +517,36 @@
   1.319    "dom (map_of xys) = fst ` set xys"
   1.320    by (induct xys) (auto simp add: dom_if)
   1.321  
   1.322 -lemma dom_map_of_zip [simp]: "length xs = length ys ==> dom (map_of (zip xs ys)) = set xs"
   1.323 -by (induct rule: list_induct2) (auto simp add: dom_if)
   1.324 +lemma dom_map_of_zip [simp]: "length xs = length ys \<Longrightarrow> dom (map_of (zip xs ys)) = set xs"
   1.325 +  by (induct rule: list_induct2) (auto simp: dom_if)
   1.326  
   1.327  lemma finite_dom_map_of: "finite (dom (map_of l))"
   1.328 -by (induct l) (auto simp add: dom_def insert_Collect [symmetric])
   1.329 +  by (induct l) (auto simp: dom_def insert_Collect [symmetric])
   1.330  
   1.331  lemma dom_map_upds [simp]:
   1.332 -  "dom(m(xs[\<mapsto>]ys)) = set(take (length ys) xs) Un dom m"
   1.333 +  "dom(m(xs[\<mapsto>]ys)) = set(take (length ys) xs) \<union> dom m"
   1.334  apply (induct xs arbitrary: m ys)
   1.335   apply simp
   1.336  apply (case_tac ys)
   1.337   apply auto
   1.338  done
   1.339  
   1.340 -lemma dom_map_add [simp]: "dom(m++n) = dom n Un dom m"
   1.341 -by(auto simp:dom_def)
   1.342 +lemma dom_map_add [simp]: "dom (m ++ n) = dom n \<union> dom m"
   1.343 +  by (auto simp: dom_def)
   1.344  
   1.345  lemma dom_override_on [simp]:
   1.346 -  "dom(override_on f g A) =
   1.347 -    (dom f  - {a. a : A - dom g}) Un {a. a : A Int dom g}"
   1.348 -by(auto simp: dom_def override_on_def)
   1.349 +  "dom (override_on f g A) =
   1.350 +    (dom f  - {a. a \<in> A - dom g}) \<union> {a. a \<in> A \<inter> dom g}"
   1.351 +  by (auto simp: dom_def override_on_def)
   1.352  
   1.353 -lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
   1.354 -by (rule ext) (force simp: map_add_def dom_def split: option.split)
   1.355 +lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1 ++ m2 = m2 ++ m1"
   1.356 +  by (rule ext) (force simp: map_add_def dom_def split: option.split)
   1.357  
   1.358  lemma map_add_dom_app_simps:
   1.359 -  "\<lbrakk> m\<in>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
   1.360 -  "\<lbrakk> m\<notin>dom l1 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m"
   1.361 -  "\<lbrakk> m\<notin>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l1 m"
   1.362 -by (auto simp add: map_add_def split: option.split_asm)
   1.363 +  "m \<in> dom l2 \<Longrightarrow> (l1 ++ l2) m = l2 m"
   1.364 +  "m \<notin> dom l1 \<Longrightarrow> (l1 ++ l2) m = l2 m"
   1.365 +  "m \<notin> dom l2 \<Longrightarrow> (l1 ++ l2) m = l1 m"
   1.366 +  by (auto simp add: map_add_def split: option.split_asm)
   1.367  
   1.368  lemma dom_const [simp]:
   1.369    "dom (\<lambda>x. Some (f x)) = UNIV"
   1.370 @@ -554,7 +556,7 @@
   1.371  lemma finite_map_freshness:
   1.372    "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>
   1.373     \<exists>x. f x = None"
   1.374 -by(bestsimp dest:ex_new_if_finite)
   1.375 +  by (bestsimp dest: ex_new_if_finite)
   1.376  
   1.377  lemma dom_minus:
   1.378    "f x = None \<Longrightarrow> dom f - insert x A = dom f - A"
   1.379 @@ -575,12 +577,14 @@
   1.380  proof (rule ext)
   1.381    fix k show "map_of xs k = map_of ys k"
   1.382    proof (cases "map_of xs k")
   1.383 -    case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
   1.384 +    case None
   1.385 +    then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
   1.386      with set_eq have "k \<notin> set (map fst ys)" by simp
   1.387      then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
   1.388      with None show ?thesis by simp
   1.389    next
   1.390 -    case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
   1.391 +    case (Some v)
   1.392 +    then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
   1.393      with map_eq show ?thesis by auto
   1.394    qed
   1.395  qed
   1.396 @@ -594,45 +598,48 @@
   1.397  qed
   1.398  
   1.399  lemma finite_set_of_finite_maps:
   1.400 -assumes "finite A" "finite B"
   1.401 -shows  "finite {m. dom m = A \<and> ran m \<subseteq> B}" (is "finite ?S")
   1.402 +  assumes "finite A" "finite B"
   1.403 +  shows "finite {m. dom m = A \<and> ran m \<subseteq> B}" (is "finite ?S")
   1.404  proof -
   1.405    let ?S' = "{m. \<forall>x. (x \<in> A \<longrightarrow> m x \<in> Some ` B) \<and> (x \<notin> A \<longrightarrow> m x = None)}"
   1.406    have "?S = ?S'"
   1.407    proof
   1.408 -    show "?S \<subseteq> ?S'" by(auto simp: dom_def ran_def image_def)
   1.409 +    show "?S \<subseteq> ?S'" by (auto simp: dom_def ran_def image_def)
   1.410      show "?S' \<subseteq> ?S"
   1.411      proof
   1.412        fix m assume "m \<in> ?S'"
   1.413        hence 1: "dom m = A" by force
   1.414 -      hence 2: "ran m \<subseteq> B" using \<open>m \<in> ?S'\<close> by(auto simp: dom_def ran_def)
   1.415 +      hence 2: "ran m \<subseteq> B" using \<open>m \<in> ?S'\<close> by (auto simp: dom_def ran_def)
   1.416        from 1 2 show "m \<in> ?S" by blast
   1.417      qed
   1.418    qed
   1.419    with assms show ?thesis by(simp add: finite_set_of_finite_funs)
   1.420  qed
   1.421  
   1.422 +
   1.423  subsection \<open>@{term [source] ran}\<close>
   1.424  
   1.425 -lemma ranI: "m a = Some b ==> b : ran m"
   1.426 -by(auto simp: ran_def)
   1.427 +lemma ranI: "m a = Some b \<Longrightarrow> b \<in> ran m"
   1.428 +  by (auto simp: ran_def)
   1.429  (* declare ranI [intro]? *)
   1.430  
   1.431  lemma ran_empty [simp]: "ran empty = {}"
   1.432 -by(auto simp: ran_def)
   1.433 +  by (auto simp: ran_def)
   1.434  
   1.435 -lemma ran_map_upd [simp]: "m a = None ==> ran(m(a\<mapsto>b)) = insert b (ran m)"
   1.436 -unfolding ran_def
   1.437 +lemma ran_map_upd [simp]: "m a = None \<Longrightarrow> ran(m(a\<mapsto>b)) = insert b (ran m)"
   1.438 +  unfolding ran_def
   1.439  apply auto
   1.440 -apply (subgoal_tac "aa ~= a")
   1.441 +apply (subgoal_tac "aa \<noteq> a")
   1.442   apply auto
   1.443  done
   1.444  
   1.445 -lemma ran_distinct: 
   1.446 -  assumes dist: "distinct (map fst al)" 
   1.447 +lemma ran_distinct:
   1.448 +  assumes dist: "distinct (map fst al)"
   1.449    shows "ran (map_of al) = snd ` set al"
   1.450 -using assms proof (induct al)
   1.451 -  case Nil then show ?case by simp
   1.452 +  using assms
   1.453 +proof (induct al)
   1.454 +  case Nil
   1.455 +  then show ?case by simp
   1.456  next
   1.457    case (Cons kv al)
   1.458    then have "ran (map_of al) = snd ` set al" by simp
   1.459 @@ -642,24 +649,25 @@
   1.460  qed
   1.461  
   1.462  lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
   1.463 -by(auto simp add: ran_def)
   1.464 +  by (auto simp add: ran_def)
   1.465 +
   1.466  
   1.467  subsection \<open>@{text "map_le"}\<close>
   1.468  
   1.469  lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
   1.470 -by (simp add: map_le_def)
   1.471 +  by (simp add: map_le_def)
   1.472  
   1.473  lemma upd_None_map_le [simp]: "f(x := None) \<subseteq>\<^sub>m f"
   1.474 -by (force simp add: map_le_def)
   1.475 +  by (force simp add: map_le_def)
   1.476  
   1.477  lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
   1.478 -by (fastforce simp add: map_le_def)
   1.479 +  by (fastforce simp add: map_le_def)
   1.480  
   1.481  lemma map_le_imp_upd_le [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
   1.482 -by (force simp add: map_le_def)
   1.483 +  by (force simp add: map_le_def)
   1.484  
   1.485  lemma map_le_upds [simp]:
   1.486 -  "f \<subseteq>\<^sub>m g ==> f(as [\<mapsto>] bs) \<subseteq>\<^sub>m g(as [\<mapsto>] bs)"
   1.487 +  "f \<subseteq>\<^sub>m g \<Longrightarrow> f(as [\<mapsto>] bs) \<subseteq>\<^sub>m g(as [\<mapsto>] bs)"
   1.488  apply (induct as arbitrary: f g bs)
   1.489   apply simp
   1.490  apply (case_tac bs)
   1.491 @@ -667,13 +675,13 @@
   1.492  done
   1.493  
   1.494  lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
   1.495 -by (fastforce simp add: map_le_def dom_def)
   1.496 +  by (fastforce simp add: map_le_def dom_def)
   1.497  
   1.498  lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
   1.499 -by (simp add: map_le_def)
   1.500 +  by (simp add: map_le_def)
   1.501  
   1.502  lemma map_le_trans[trans]: "\<lbrakk> m1 \<subseteq>\<^sub>m m2; m2 \<subseteq>\<^sub>m m3\<rbrakk> \<Longrightarrow> m1 \<subseteq>\<^sub>m m3"
   1.503 -by (auto simp add: map_le_def dom_def)
   1.504 +  by (auto simp add: map_le_def dom_def)
   1.505  
   1.506  lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
   1.507  unfolding map_le_def
   1.508 @@ -682,17 +690,17 @@
   1.509  apply (case_tac "x \<in> dom g", simp, fastforce)
   1.510  done
   1.511  
   1.512 -lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
   1.513 -by (fastforce simp add: map_le_def)
   1.514 +lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m g ++ f"
   1.515 +  by (fastforce simp: map_le_def)
   1.516  
   1.517 -lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
   1.518 -by(fastforce simp: map_add_def map_le_def fun_eq_iff split: option.splits)
   1.519 +lemma map_le_iff_map_add_commute: "f \<subseteq>\<^sub>m f ++ g \<longleftrightarrow> f ++ g = g ++ f"
   1.520 +  by (fastforce simp: map_add_def map_le_def fun_eq_iff split: option.splits)
   1.521  
   1.522 -lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
   1.523 -by (fastforce simp add: map_le_def map_add_def dom_def)
   1.524 +lemma map_add_le_mapE: "f ++ g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
   1.525 +  by (fastforce simp: map_le_def map_add_def dom_def)
   1.526  
   1.527 -lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
   1.528 -by (clarsimp simp add: map_le_def map_add_def dom_def split: option.splits)
   1.529 +lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h \<rbrakk> \<Longrightarrow> f ++ g \<subseteq>\<^sub>m h"
   1.530 +  by (auto simp: map_le_def map_add_def dom_def split: option.splits)
   1.531  
   1.532  lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
   1.533  proof(rule iffI)
   1.534 @@ -714,8 +722,10 @@
   1.535  lemma set_map_of_compr:
   1.536    assumes distinct: "distinct (map fst xs)"
   1.537    shows "set xs = {(k, v). map_of xs k = Some v}"
   1.538 -using assms proof (induct xs)
   1.539 -  case Nil then show ?case by simp
   1.540 +  using assms
   1.541 +proof (induct xs)
   1.542 +  case Nil
   1.543 +  then show ?case by simp
   1.544  next
   1.545    case (Cons x xs)
   1.546    obtain k v where "x = (k, v)" by (cases x) blast
   1.547 @@ -742,7 +752,8 @@
   1.548    assume ?rhs show ?lhs
   1.549    proof
   1.550      fix k
   1.551 -    show "map_of xs k = map_of ys k" proof (cases "map_of xs k")
   1.552 +    show "map_of xs k = map_of ys k"
   1.553 +    proof (cases "map_of xs k")
   1.554        case None
   1.555        with \<open>?rhs\<close> have "map_of ys k = None"
   1.556          by (simp add: map_of_eq_None_iff)