src/HOL/Library/RBT_Impl.thy
changeset 60500 903bb1495239
parent 59575 55f5e1cbf2a7
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -3,18 +3,18 @@
     1.4      Author:     Alexander Krauss, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Implementation of Red-Black Trees *}
     1.8 +section \<open>Implementation of Red-Black Trees\<close>
     1.9  
    1.10  theory RBT_Impl
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16    For applications, you should use theory @{text RBT} which defines
    1.17    an abstract type of red-black tree obeying the invariant.
    1.18 -*}
    1.19 +\<close>
    1.20  
    1.21 -subsection {* Datatype of RB trees *}
    1.22 +subsection \<open>Datatype of RB trees\<close>
    1.23  
    1.24  datatype color = R | B
    1.25  datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
    1.26 @@ -29,9 +29,9 @@
    1.27    case (Branch c) with that show thesis by (cases c) blast+
    1.28  qed
    1.29  
    1.30 -subsection {* Tree properties *}
    1.31 +subsection \<open>Tree properties\<close>
    1.32  
    1.33 -subsubsection {* Content of a tree *}
    1.34 +subsubsection \<open>Content of a tree\<close>
    1.35  
    1.36  primrec entries :: "('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
    1.37  where 
    1.38 @@ -66,7 +66,7 @@
    1.39    "t \<noteq> rbt.Empty \<Longrightarrow> keys t \<noteq> []"
    1.40    by (cases t) simp_all
    1.41  
    1.42 -subsubsection {* Search tree properties *}
    1.43 +subsubsection \<open>Search tree properties\<close>
    1.44  
    1.45  context ord begin
    1.46  
    1.47 @@ -129,7 +129,7 @@
    1.48    by (simp add: distinct_entries keys_def)
    1.49  
    1.50  
    1.51 -subsubsection {* Tree lookup *}
    1.52 +subsubsection \<open>Tree lookup\<close>
    1.53  
    1.54  primrec (in ord) rbt_lookup :: "('a, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
    1.55  where
    1.56 @@ -288,7 +288,7 @@
    1.57  
    1.58  end
    1.59  
    1.60 -subsubsection {* Red-black properties *}
    1.61 +subsubsection \<open>Red-black properties\<close>
    1.62  
    1.63  primrec color_of :: "('a, 'b) rbt \<Rightarrow> color"
    1.64  where
    1.65 @@ -305,7 +305,7 @@
    1.66    "inv1 Empty = True"
    1.67  | "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
    1.68  
    1.69 -primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- {* Weaker version *}
    1.70 +primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- \<open>Weaker version\<close>
    1.71  where
    1.72    "inv1l Empty = True"
    1.73  | "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
    1.74 @@ -329,7 +329,7 @@
    1.75  
    1.76  end
    1.77  
    1.78 -subsection {* Insertion *}
    1.79 +subsection \<open>Insertion\<close>
    1.80  
    1.81  fun (* slow, due to massive case splitting *)
    1.82    balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
    1.83 @@ -549,7 +549,7 @@
    1.84  
    1.85  end
    1.86  
    1.87 -subsection {* Deletion *}
    1.88 +subsection \<open>Deletion\<close>
    1.89  
    1.90  lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
    1.91  by (cases t rule: rbt_cases) auto
    1.92 @@ -894,9 +894,9 @@
    1.93      assume "xx = yy"
    1.94      with 2 show ?thesis proof (cases "xx = k")
    1.95        case True
    1.96 -      from 2 `xx = yy` `xx = k` have "rbt_sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
    1.97 +      from 2 \<open>xx = yy\<close> \<open>xx = k\<close> have "rbt_sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
    1.98        hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: rbt_less_nit rbt_greater_prop)
    1.99 -      with `xx = yy` 2 `xx = k` show ?thesis by (simp add: combine_in_tree)
   1.100 +      with \<open>xx = yy\<close> 2 \<open>xx = k\<close> show ?thesis by (simp add: combine_in_tree)
   1.101      qed (simp add: combine_in_tree)
   1.102    qed simp+
   1.103  next    
   1.104 @@ -917,7 +917,7 @@
   1.105      case True
   1.106      with "4_1" have "yy \<guillemotleft>| bb \<and> k < yy" by simp
   1.107      hence "k \<guillemotleft>| bb" by (blast dest: rbt_greater_trans)
   1.108 -    with "4_1" `xx = k` 
   1.109 +    with "4_1" \<open>xx = k\<close> 
   1.110     have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: rbt_greater_nit)
   1.111      thus ?thesis by auto
   1.112    qed simp+
   1.113 @@ -947,7 +947,7 @@
   1.114      case True
   1.115      with "6_1" have "aa |\<guillemotleft> yy \<and> k > yy" by simp
   1.116      hence "aa |\<guillemotleft> k" by (blast dest: rbt_less_trans)
   1.117 -    with "6_1" `xx = k` show ?thesis by (auto simp: rbt_less_nit)
   1.118 +    with "6_1" \<open>xx = k\<close> show ?thesis by (auto simp: rbt_less_nit)
   1.119    qed simp
   1.120  next
   1.121    case ("6_2" xx aa yy ss vaa vbb vdd vc)
   1.122 @@ -997,7 +997,7 @@
   1.123  
   1.124  end
   1.125  
   1.126 -subsection {* Modifying existing entries *}
   1.127 +subsection \<open>Modifying existing entries\<close>
   1.128  
   1.129  context ord begin
   1.130  
   1.131 @@ -1028,7 +1028,7 @@
   1.132    "rbt_lookup (rbt_map_entry k f t) = (rbt_lookup t)(k := map_option f (rbt_lookup t k))"
   1.133    by (induct t) (auto split: option.splits simp add: fun_eq_iff)
   1.134  
   1.135 -subsection {* Mapping all entries *}
   1.136 +subsection \<open>Mapping all entries\<close>
   1.137  
   1.138  primrec
   1.139    map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'c) rbt"
   1.140 @@ -1064,7 +1064,7 @@
   1.141  
   1.142  hide_const (open) map
   1.143  
   1.144 -subsection {* Folding over entries *}
   1.145 +subsection \<open>Folding over entries\<close>
   1.146  
   1.147  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
   1.148    "fold f t = List.fold (case_prod f) (entries t)"
   1.149 @@ -1094,7 +1094,7 @@
   1.150        s
   1.151    )"
   1.152  
   1.153 -subsection {* Bulkloading a tree *}
   1.154 +subsection \<open>Bulkloading a tree\<close>
   1.155  
   1.156  definition (in ord) rbt_bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" where
   1.157    "rbt_bulkload xs = foldr (\<lambda>(k, v). rbt_insert k v) xs Empty"
   1.158 @@ -1114,7 +1114,7 @@
   1.159        by (induct ys) (simp_all add: rbt_bulkload_def rbt_lookup_rbt_insert case_prod_beta)
   1.160    from this Empty_is_rbt have
   1.161      "rbt_lookup (List.fold (case_prod rbt_insert) (rev xs) Empty) = rbt_lookup Empty ++ map_of xs"
   1.162 -     by (simp add: `ys = rev xs`)
   1.163 +     by (simp add: \<open>ys = rev xs\<close>)
   1.164    then show ?thesis by (simp add: rbt_bulkload_def rbt_lookup_Empty foldr_conv_fold)
   1.165  qed
   1.166  
   1.167 @@ -1122,12 +1122,12 @@
   1.168  
   1.169  
   1.170  
   1.171 -subsection {* Building a RBT from a sorted list *}
   1.172 +subsection \<open>Building a RBT from a sorted list\<close>
   1.173  
   1.174 -text {* 
   1.175 +text \<open>
   1.176    These functions have been adapted from 
   1.177    Andrew W. Appel, Efficient Verified Red-Black Trees (September 2011) 
   1.178 -*}
   1.179 +\<close>
   1.180  
   1.181  fun rbtreeify_f :: "nat \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt \<times> ('a \<times> 'b) list"
   1.182    and rbtreeify_g :: "nat \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a, 'b) rbt \<times> ('a \<times> 'b) list"
   1.183 @@ -1264,15 +1264,15 @@
   1.184        hence "length (snd (rbtreeify_f n kvs)) = 
   1.185          length (snd (rbtreeify_f (Suc (2 * (n div 2))) kvs))"
   1.186          by (simp add: mod_eq_0_iff_dvd)
   1.187 -      also from "1.prems" `\<not> n \<le> 1` obtain k v kvs' 
   1.188 +      also from "1.prems" \<open>\<not> n \<le> 1\<close> obtain k v kvs' 
   1.189          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   1.190 -      also have "0 < n div 2" using `\<not> n \<le> 1` by(simp) 
   1.191 +      also have "0 < n div 2" using \<open>\<not> n \<le> 1\<close> by(simp) 
   1.192        note rbtreeify_f_simps(4)[OF this]
   1.193        also note kvs[symmetric] 
   1.194        also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
   1.195        from "1.prems" have "n div 2 \<le> length kvs" by simp
   1.196        with False have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
   1.197 -      with "1.prems" `\<not> n \<le> 1` obtain t1 k' v' kvs''
   1.198 +      with "1.prems" \<open>\<not> n \<le> 1\<close> obtain t1 k' v' kvs''
   1.199          where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
   1.200          by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
   1.201        note this also note prod.case also note list.simps(5)
   1.202 @@ -1290,7 +1290,7 @@
   1.203    case (2 n kvs)
   1.204    show ?case
   1.205    proof(cases "n > 1")
   1.206 -    case False with `0 < n` show ?thesis
   1.207 +    case False with \<open>0 < n\<close> show ?thesis
   1.208        by(cases n kvs rule: nat.exhaust[case_product list.exhaust]) simp_all
   1.209    next
   1.210      case True
   1.211 @@ -1304,11 +1304,11 @@
   1.212          by(metis minus_nat.diff_0 mult_div_cancel)
   1.213        also from "2.prems" True obtain k v kvs' 
   1.214          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   1.215 -      also have "0 < n div 2" using `1 < n` by(simp) 
   1.216 +      also have "0 < n div 2" using \<open>1 < n\<close> by(simp) 
   1.217        note rbtreeify_g_simps(3)[OF this]
   1.218        also note kvs[symmetric] 
   1.219        also let ?rest1 = "snd (rbtreeify_g (n div 2) kvs)"
   1.220 -      from "2.prems" `1 < n`
   1.221 +      from "2.prems" \<open>1 < n\<close>
   1.222        have "0 < n div 2" "n div 2 \<le> Suc (length kvs)" by simp_all
   1.223        with True have len: "length ?rest1 = Suc (length kvs) - n div 2" by(rule IH)
   1.224        with "2.prems" obtain t1 k' v' kvs''
   1.225 @@ -1318,7 +1318,7 @@
   1.226        also note prod.case also note snd_apfst
   1.227        also have "n div 2 \<le> Suc (length kvs'')" 
   1.228          using len "2.prems" unfolding kvs'' by simp
   1.229 -      with True kvs''[symmetric] refl refl `0 < n div 2`
   1.230 +      with True kvs''[symmetric] refl refl \<open>0 < n div 2\<close>
   1.231        have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
   1.232          by(rule IH)
   1.233        finally show ?thesis using len[unfolded kvs''] "2.prems" True
   1.234 @@ -1328,22 +1328,22 @@
   1.235        hence "length (snd (rbtreeify_g n kvs)) = 
   1.236          length (snd (rbtreeify_g (Suc (2 * (n div 2))) kvs))"
   1.237          by (simp add: mod_eq_0_iff_dvd)
   1.238 -      also from "2.prems" `1 < n` obtain k v kvs'
   1.239 +      also from "2.prems" \<open>1 < n\<close> obtain k v kvs'
   1.240          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
   1.241 -      also have "0 < n div 2" using `1 < n` by(simp)
   1.242 +      also have "0 < n div 2" using \<open>1 < n\<close> by(simp)
   1.243        note rbtreeify_g_simps(4)[OF this]
   1.244        also note kvs[symmetric] 
   1.245        also let ?rest1 = "snd (rbtreeify_f (n div 2) kvs)"
   1.246        from "2.prems" have "n div 2 \<le> length kvs" by simp
   1.247        with False have len: "length ?rest1 = length kvs - n div 2" by(rule IH)
   1.248 -      with "2.prems" `1 < n` False obtain t1 k' v' kvs'' 
   1.249 +      with "2.prems" \<open>1 < n\<close> False obtain t1 k' v' kvs'' 
   1.250          where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
   1.251          by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm, arith)
   1.252        note this also note prod.case also note list.simps(5) 
   1.253        also note prod.case also note snd_apfst
   1.254        also have "n div 2 \<le> Suc (length kvs'')" 
   1.255          using len "2.prems" False unfolding kvs'' by simp arith
   1.256 -      with False kvs''[symmetric] refl refl `0 < n div 2`
   1.257 +      with False kvs''[symmetric] refl refl \<open>0 < n div 2\<close>
   1.258        have "length (snd (rbtreeify_g (n div 2) kvs'')) = Suc (length kvs'') - n div 2"
   1.259          by(rule IH)
   1.260        finally show ?thesis using len[unfolded kvs''] "2.prems" False
   1.261 @@ -1597,103 +1597,103 @@
   1.262    \<Longrightarrow> rbt_sorted (fst (rbtreeify_g n kvs))"
   1.263  proof(induction n kvs and n kvs rule: rbtreeify_induct)
   1.264    case (f_even n kvs t k v kvs')
   1.265 -  from rbtreeify_fD[OF `rbtreeify_f n kvs = (t, (k, v) # kvs')` `n \<le> length kvs`]
   1.266 +  from rbtreeify_fD[OF \<open>rbtreeify_f n kvs = (t, (k, v) # kvs')\<close> \<open>n \<le> length kvs\<close>]
   1.267    have "entries t = take n kvs"
   1.268      and kvs': "drop n kvs = (k, v) # kvs'" by simp_all
   1.269    hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   1.270 -  from `sorted (map fst kvs)` kvs'
   1.271 +  from \<open>sorted (map fst kvs)\<close> kvs'
   1.272    have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   1.273      by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   1.274 -  moreover from `distinct (map fst kvs)` kvs'
   1.275 +  moreover from \<open>distinct (map fst kvs)\<close> kvs'
   1.276    have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   1.277      by(subst (asm) unfold)(auto intro: rev_image_eqI)
   1.278    ultimately have "(\<forall>(x, y) \<in> set (take n kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   1.279      by fastforce
   1.280    hence "fst (rbtreeify_f n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_g n kvs')"
   1.281 -    using `n \<le> Suc (length kvs')` `n \<le> length kvs` set_take_subset[of "n - 1" kvs']
   1.282 +    using \<open>n \<le> Suc (length kvs')\<close> \<open>n \<le> length kvs\<close> set_take_subset[of "n - 1" kvs']
   1.283      by(auto simp add: ord.rbt_greater_prop ord.rbt_less_prop take_map split_def)
   1.284 -  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.285 +  moreover from \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
   1.286    have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule f_even.IH)
   1.287    moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   1.288 -    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.289 +    using \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
   1.290      by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   1.291    hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule f_even.IH)
   1.292    ultimately show ?case
   1.293 -    using `0 < n` `rbtreeify_f n kvs = (t, (k, v) # kvs')` by simp
   1.294 +    using \<open>0 < n\<close> \<open>rbtreeify_f n kvs = (t, (k, v) # kvs')\<close> by simp
   1.295  next
   1.296    case (f_odd n kvs t k v kvs')
   1.297 -  from rbtreeify_fD[OF `rbtreeify_f n kvs = (t, (k, v) # kvs')` `n \<le> length kvs`]
   1.298 +  from rbtreeify_fD[OF \<open>rbtreeify_f n kvs = (t, (k, v) # kvs')\<close> \<open>n \<le> length kvs\<close>]
   1.299    have "entries t = take n kvs" 
   1.300      and kvs': "drop n kvs = (k, v) # kvs'" by simp_all
   1.301    hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   1.302 -  from `sorted (map fst kvs)` kvs'
   1.303 +  from \<open>sorted (map fst kvs)\<close> kvs'
   1.304    have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   1.305      by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   1.306 -  moreover from `distinct (map fst kvs)` kvs'
   1.307 +  moreover from \<open>distinct (map fst kvs)\<close> kvs'
   1.308    have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   1.309      by(subst (asm) unfold)(auto intro: rev_image_eqI)
   1.310    ultimately have "(\<forall>(x, y) \<in> set (take n kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   1.311      by fastforce
   1.312    hence "fst (rbtreeify_f n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_f n kvs')"
   1.313 -    using `n \<le> length kvs'` `n \<le> length kvs` set_take_subset[of n kvs']
   1.314 +    using \<open>n \<le> length kvs'\<close> \<open>n \<le> length kvs\<close> set_take_subset[of n kvs']
   1.315      by(auto simp add: rbt_greater_prop rbt_less_prop take_map split_def)
   1.316 -  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.317 +  moreover from \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
   1.318    have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule f_odd.IH)
   1.319    moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   1.320 -    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.321 +    using \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
   1.322      by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   1.323    hence "rbt_sorted (fst (rbtreeify_f n kvs'))" by(rule f_odd.IH)
   1.324    ultimately show ?case 
   1.325 -    using `0 < n` `rbtreeify_f n kvs = (t, (k, v) # kvs')` by simp
   1.326 +    using \<open>0 < n\<close> \<open>rbtreeify_f n kvs = (t, (k, v) # kvs')\<close> by simp
   1.327  next
   1.328    case (g_even n kvs t k v kvs')
   1.329 -  from rbtreeify_gD[OF `rbtreeify_g n kvs = (t, (k, v) # kvs')` `n \<le> Suc (length kvs)`]
   1.330 +  from rbtreeify_gD[OF \<open>rbtreeify_g n kvs = (t, (k, v) # kvs')\<close> \<open>n \<le> Suc (length kvs)\<close>]
   1.331    have t: "entries t = take (n - 1) kvs" 
   1.332      and kvs': "drop (n - 1) kvs = (k, v) # kvs'" by simp_all
   1.333    hence unfold: "kvs = take (n - 1) kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   1.334 -  from `sorted (map fst kvs)` kvs'
   1.335 +  from \<open>sorted (map fst kvs)\<close> kvs'
   1.336    have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   1.337      by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   1.338 -  moreover from `distinct (map fst kvs)` kvs'
   1.339 +  moreover from \<open>distinct (map fst kvs)\<close> kvs'
   1.340    have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   1.341      by(subst (asm) unfold)(auto intro: rev_image_eqI)
   1.342    ultimately have "(\<forall>(x, y) \<in> set (take (n - 1) kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   1.343      by fastforce
   1.344    hence "fst (rbtreeify_g n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_g n kvs')"
   1.345 -    using `n \<le> Suc (length kvs')` `n \<le> Suc (length kvs)` set_take_subset[of "n - 1" kvs']
   1.346 +    using \<open>n \<le> Suc (length kvs')\<close> \<open>n \<le> Suc (length kvs)\<close> set_take_subset[of "n - 1" kvs']
   1.347      by(auto simp add: rbt_greater_prop rbt_less_prop take_map split_def)
   1.348 -  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.349 +  moreover from \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
   1.350    have "rbt_sorted (fst (rbtreeify_g n kvs))" by(rule g_even.IH)
   1.351    moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   1.352 -    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.353 +    using \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
   1.354      by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   1.355    hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule g_even.IH)
   1.356 -  ultimately show ?case using `0 < n` `rbtreeify_g n kvs = (t, (k, v) # kvs')` by simp
   1.357 +  ultimately show ?case using \<open>0 < n\<close> \<open>rbtreeify_g n kvs = (t, (k, v) # kvs')\<close> by simp
   1.358  next
   1.359    case (g_odd n kvs t k v kvs')
   1.360 -  from rbtreeify_fD[OF `rbtreeify_f n kvs = (t, (k, v) # kvs')` `n \<le> length kvs`]
   1.361 +  from rbtreeify_fD[OF \<open>rbtreeify_f n kvs = (t, (k, v) # kvs')\<close> \<open>n \<le> length kvs\<close>]
   1.362    have "entries t = take n kvs"
   1.363      and kvs': "drop n kvs = (k, v) # kvs'" by simp_all
   1.364    hence unfold: "kvs = take n kvs @ (k, v) # kvs'" by(metis append_take_drop_id)
   1.365 -  from `sorted (map fst kvs)` kvs'
   1.366 +  from \<open>sorted (map fst kvs)\<close> kvs'
   1.367    have "(\<forall>(x, y) \<in> set (take n kvs). x \<le> k) \<and> (\<forall>(x, y) \<in> set kvs'. k \<le> x)"
   1.368      by(subst (asm) unfold)(auto simp add: sorted_append sorted_Cons)
   1.369 -  moreover from `distinct (map fst kvs)` kvs'
   1.370 +  moreover from \<open>distinct (map fst kvs)\<close> kvs'
   1.371    have "(\<forall>(x, y) \<in> set (take n kvs). x \<noteq> k) \<and> (\<forall>(x, y) \<in> set kvs'. x \<noteq> k)"
   1.372      by(subst (asm) unfold)(auto intro: rev_image_eqI)
   1.373    ultimately have "(\<forall>(x, y) \<in> set (take n kvs). x < k) \<and> (\<forall>(x, y) \<in> set kvs'. k < x)"
   1.374      by fastforce
   1.375    hence "fst (rbtreeify_f n kvs) |\<guillemotleft> k" "k \<guillemotleft>| fst (rbtreeify_g n kvs')"
   1.376 -    using `n \<le> Suc (length kvs')` `n \<le> length kvs` set_take_subset[of "n - 1" kvs']
   1.377 +    using \<open>n \<le> Suc (length kvs')\<close> \<open>n \<le> length kvs\<close> set_take_subset[of "n - 1" kvs']
   1.378      by(auto simp add: rbt_greater_prop rbt_less_prop take_map split_def)
   1.379 -  moreover from `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.380 +  moreover from \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
   1.381    have "rbt_sorted (fst (rbtreeify_f n kvs))" by(rule g_odd.IH)
   1.382    moreover have "sorted (map fst kvs')" "distinct (map fst kvs')"
   1.383 -    using `sorted (map fst kvs)` `distinct (map fst kvs)`
   1.384 +    using \<open>sorted (map fst kvs)\<close> \<open>distinct (map fst kvs)\<close>
   1.385      by(subst (asm) (1 2) unfold, simp add: sorted_append sorted_Cons)+
   1.386    hence "rbt_sorted (fst (rbtreeify_g n kvs'))" by(rule g_odd.IH)
   1.387    ultimately show ?case
   1.388 -    using `0 < n` `rbtreeify_f n kvs = (t, (k, v) # kvs')` by simp
   1.389 +    using \<open>0 < n\<close> \<open>rbtreeify_f n kvs = (t, (k, v) # kvs')\<close> by simp
   1.390  qed simp_all
   1.391  
   1.392  lemma rbt_sorted_rbtreeify: 
   1.393 @@ -1712,10 +1712,10 @@
   1.394  
   1.395  end
   1.396  
   1.397 -text {* 
   1.398 +text \<open>
   1.399    Functions to compare the height of two rbt trees, taken from 
   1.400    Andrew W. Appel, Efficient Verified Red-Black Trees (September 2011)
   1.401 -*}
   1.402 +\<close>
   1.403  
   1.404  fun skip_red :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   1.405  where
   1.406 @@ -1761,7 +1761,7 @@
   1.407    skip_black_def
   1.408    compare_height_def compare_height.simps
   1.409  
   1.410 -subsection {* union and intersection of sorted associative lists *}
   1.411 +subsection \<open>union and intersection of sorted associative lists\<close>
   1.412  
   1.413  context ord begin
   1.414  
   1.415 @@ -1995,7 +1995,7 @@
   1.416  end
   1.417  
   1.418  
   1.419 -subsection {* Code generator setup *}
   1.420 +subsection \<open>Code generator setup\<close>
   1.421  
   1.422  lemmas [code] =
   1.423    ord.rbt_less_prop
   1.424 @@ -2022,7 +2022,7 @@
   1.425    ord.rbt_map_entry.simps
   1.426    ord.rbt_bulkload_def
   1.427  
   1.428 -text {* More efficient implementations for @{term entries} and @{term keys} *}
   1.429 +text \<open>More efficient implementations for @{term entries} and @{term keys}\<close>
   1.430  
   1.431  definition gen_entries :: 
   1.432    "(('a \<times> 'b) \<times> ('a, 'b) rbt) list \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
   1.433 @@ -2052,8 +2052,8 @@
   1.434    "keys = gen_keys []"
   1.435  by(simp add: gen_keys_def fun_eq_iff)
   1.436  
   1.437 -text {* Restore original type constraints for constants *}
   1.438 -setup {*
   1.439 +text \<open>Restore original type constraints for constants\<close>
   1.440 +setup \<open>
   1.441    fold Sign.add_const_constraint
   1.442      [(@{const_name rbt_less}, SOME @{typ "('a :: order) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"}),
   1.443       (@{const_name rbt_greater}, SOME @{typ "('a :: order) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"}),
   1.444 @@ -2073,7 +2073,7 @@
   1.445       (@{const_name rbt_union}, SOME @{typ "('a\<Colon>linorder,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
   1.446       (@{const_name rbt_map_entry}, SOME @{typ "'a\<Colon>linorder \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"}),
   1.447       (@{const_name rbt_bulkload}, SOME @{typ "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder,'b) rbt"})]
   1.448 -*}
   1.449 +\<close>
   1.450  
   1.451  hide_const (open) R B Empty entries keys fold gen_keys gen_entries
   1.452