src/HOL/Map.thy
changeset 60758 d8d85a8172b5
parent 60057 86fa63ce8156
child 60838 2d7eea27ceec
     1.1 --- a/src/HOL/Map.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Map.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
     1.5  *)
     1.6  
     1.7 -section {* Maps *}
     1.8 +section \<open>Maps\<close>
     1.9  
    1.10  theory Map
    1.11  imports List
    1.12 @@ -89,13 +89,13 @@
    1.13    by simp_all
    1.14  
    1.15  
    1.16 -subsection {* @{term [source] empty} *}
    1.17 +subsection \<open>@{term [source] empty}\<close>
    1.18  
    1.19  lemma empty_upd_none [simp]: "empty(x := None) = empty"
    1.20  by (rule ext) simp
    1.21  
    1.22  
    1.23 -subsection {* @{term [source] map_upd} *}
    1.24 +subsection \<open>@{term [source] map_upd}\<close>
    1.25  
    1.26  lemma map_upd_triv: "t k = Some x ==> t(k|->x) = t"
    1.27  by (rule ext) simp
    1.28 @@ -131,7 +131,7 @@
    1.29  done
    1.30  
    1.31  
    1.32 -subsection {* @{term [source] map_of} *}
    1.33 +subsection \<open>@{term [source] map_of}\<close>
    1.34  
    1.35  lemma map_of_eq_None_iff:
    1.36    "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
    1.37 @@ -204,12 +204,12 @@
    1.38    case Nil show ?case by simp
    1.39  next
    1.40    case (Cons y ys x xs z zs)
    1.41 -  from `map_of (zip (x#xs) (y#ys)) = map_of (zip (x#xs) (z#zs))`
    1.42 +  from \<open>map_of (zip (x#xs) (y#ys)) = map_of (zip (x#xs) (z#zs))\<close>
    1.43      have map_of: "map_of (zip xs ys)(x \<mapsto> y) = map_of (zip xs zs)(x \<mapsto> z)" by simp
    1.44    from Cons have "length ys = length xs" and "length zs = length xs"
    1.45      and "x \<notin> set xs" by simp_all
    1.46    then have "map_of (zip xs ys) = map_of (zip xs zs)" using map_of by (rule map_of_zip_upd)
    1.47 -  with Cons.hyps `distinct (x # xs)` have "ys = zs" by simp
    1.48 +  with Cons.hyps \<open>distinct (x # xs)\<close> have "ys = zs" by simp
    1.49    moreover from map_of have "y = z" by (rule map_upd_eqD1)
    1.50    ultimately show ?case by simp
    1.51  qed
    1.52 @@ -254,7 +254,7 @@
    1.53    using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def)
    1.54  
    1.55  
    1.56 -subsection {* @{const map_option} related *}
    1.57 +subsection \<open>@{const map_option} related\<close>
    1.58  
    1.59  lemma map_option_o_empty [simp]: "map_option f o empty = empty"
    1.60  by (rule ext) simp
    1.61 @@ -264,7 +264,7 @@
    1.62  by (rule ext) simp
    1.63  
    1.64  
    1.65 -subsection {* @{term [source] map_comp} related *}
    1.66 +subsection \<open>@{term [source] map_comp} related\<close>
    1.67  
    1.68  lemma map_comp_empty [simp]:
    1.69    "m \<circ>\<^sub>m empty = empty"
    1.70 @@ -285,7 +285,7 @@
    1.71  by (auto simp add: map_comp_def split: option.splits)
    1.72  
    1.73  
    1.74 -subsection {* @{text "++"} *}
    1.75 +subsection \<open>@{text "++"}\<close>
    1.76  
    1.77  lemma map_add_empty[simp]: "m ++ empty = m"
    1.78  by(simp add: map_add_def)
    1.79 @@ -352,7 +352,7 @@
    1.80    by (induct ps) (auto simp add: fun_eq_iff map_add_def)
    1.81  
    1.82  
    1.83 -subsection {* @{term [source] restrict_map} *}
    1.84 +subsection \<open>@{term [source] restrict_map}\<close>
    1.85  
    1.86  lemma restrict_map_to_empty [simp]: "m|`{} = empty"
    1.87  by (simp add: restrict_map_def)
    1.88 @@ -405,7 +405,7 @@
    1.89    by (simp add: restrict_map_def fun_eq_iff)
    1.90  
    1.91  
    1.92 -subsection {* @{term [source] map_upds} *}
    1.93 +subsection \<open>@{term [source] map_upds}\<close>
    1.94  
    1.95  lemma map_upds_Nil1 [simp]: "m([] [|->] bs) = m"
    1.96  by (simp add: map_upds_def)
    1.97 @@ -485,7 +485,7 @@
    1.98  done
    1.99  
   1.100  
   1.101 -subsection {* @{term [source] dom} *}
   1.102 +subsection \<open>@{term [source] dom}\<close>
   1.103  
   1.104  lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
   1.105    by (auto simp: dom_def)
   1.106 @@ -605,14 +605,14 @@
   1.107      proof
   1.108        fix m assume "m \<in> ?S'"
   1.109        hence 1: "dom m = A" by force
   1.110 -      hence 2: "ran m \<subseteq> B" using `m \<in> ?S'` by(auto simp: dom_def ran_def)
   1.111 +      hence 2: "ran m \<subseteq> B" using \<open>m \<in> ?S'\<close> by(auto simp: dom_def ran_def)
   1.112        from 1 2 show "m \<in> ?S" by blast
   1.113      qed
   1.114    qed
   1.115    with assms show ?thesis by(simp add: finite_set_of_finite_funs)
   1.116  qed
   1.117  
   1.118 -subsection {* @{term [source] ran} *}
   1.119 +subsection \<open>@{term [source] ran}\<close>
   1.120  
   1.121  lemma ranI: "m a = Some b ==> b : ran m"
   1.122  by(auto simp: ran_def)
   1.123 @@ -644,7 +644,7 @@
   1.124  lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
   1.125  by(auto simp add: ran_def)
   1.126  
   1.127 -subsection {* @{text "map_le"} *}
   1.128 +subsection \<open>@{text "map_le"}\<close>
   1.129  
   1.130  lemma map_le_empty [simp]: "empty \<subseteq>\<^sub>m g"
   1.131  by (simp add: map_le_def)
   1.132 @@ -702,14 +702,14 @@
   1.133    assume "dom f = {x}"
   1.134    then obtain v where "f x = Some v" by auto
   1.135    hence "[x \<mapsto> v] \<subseteq>\<^sub>m f" by(auto simp add: map_le_def)
   1.136 -  moreover have "f \<subseteq>\<^sub>m [x \<mapsto> v]" using `dom f = {x}` `f x = Some v`
   1.137 +  moreover have "f \<subseteq>\<^sub>m [x \<mapsto> v]" using \<open>dom f = {x}\<close> \<open>f x = Some v\<close>
   1.138      by(auto simp add: map_le_def)
   1.139    ultimately have "f = [x \<mapsto> v]" by-(rule map_le_antisym)
   1.140    thus "\<exists>v. f = [x \<mapsto> v]" by blast
   1.141  qed
   1.142  
   1.143  
   1.144 -subsection {* Various *}
   1.145 +subsection \<open>Various\<close>
   1.146  
   1.147  lemma set_map_of_compr:
   1.148    assumes distinct: "distinct (map fst xs)"
   1.149 @@ -725,7 +725,7 @@
   1.150      {(k', v'). (map_of xs(k \<mapsto> v)) k' = Some v'}"
   1.151      by (auto split: if_splits)
   1.152    from Cons have "set xs = {(k, v). map_of xs k = Some v}" by simp
   1.153 -  with * `x = (k, v)` show ?case by simp
   1.154 +  with * \<open>x = (k, v)\<close> show ?case by simp
   1.155  qed
   1.156  
   1.157  lemma map_of_inject_set:
   1.158 @@ -733,9 +733,9 @@
   1.159    shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys" (is "?lhs \<longleftrightarrow> ?rhs")
   1.160  proof
   1.161    assume ?lhs
   1.162 -  moreover from `distinct (map fst xs)` have "set xs = {(k, v). map_of xs k = Some v}"
   1.163 +  moreover from \<open>distinct (map fst xs)\<close> have "set xs = {(k, v). map_of xs k = Some v}"
   1.164      by (rule set_map_of_compr)
   1.165 -  moreover from `distinct (map fst ys)` have "set ys = {(k, v). map_of ys k = Some v}"
   1.166 +  moreover from \<open>distinct (map fst ys)\<close> have "set ys = {(k, v). map_of ys k = Some v}"
   1.167      by (rule set_map_of_compr)
   1.168    ultimately show ?rhs by simp
   1.169  next
   1.170 @@ -744,12 +744,12 @@
   1.171      fix k
   1.172      show "map_of xs k = map_of ys k" proof (cases "map_of xs k")
   1.173        case None
   1.174 -      with `?rhs` have "map_of ys k = None"
   1.175 +      with \<open>?rhs\<close> have "map_of ys k = None"
   1.176          by (simp add: map_of_eq_None_iff)
   1.177        with None show ?thesis by simp
   1.178      next
   1.179        case (Some v)
   1.180 -      with distinct `?rhs` have "map_of ys k = Some v"
   1.181 +      with distinct \<open>?rhs\<close> have "map_of ys k = Some v"
   1.182          by simp
   1.183        with Some show ?thesis by simp
   1.184      qed