# HG changeset patch
# User haftmann
# Date 1743358826 -7200
# Node ID f1ff9123c62ac8374b66fe251f1eec3212f535d6
# Parent  667c67b1e8f1fbca7e84373a7c1d04430ea51788
tuned

diff -r 667c67b1e8f1 -r f1ff9123c62a src/HOL/Library/Comparator.thy
--- a/src/HOL/Library/Comparator.thy	Mon Mar 31 19:17:51 2025 +0200
+++ b/src/HOL/Library/Comparator.thy	Sun Mar 30 20:20:26 2025 +0200
@@ -13,146 +13,146 @@
 datatype comp = Less | Equiv | Greater
 
 locale comparator =
-  fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
-  assumes refl [simp]: "\<And>a. cmp a a = Equiv"
-    and trans_equiv: "\<And>a b c. cmp a b = Equiv \<Longrightarrow> cmp b c = Equiv \<Longrightarrow> cmp a c = Equiv"
-  assumes trans_less: "cmp a b = Less \<Longrightarrow> cmp b c = Less \<Longrightarrow> cmp a c = Less"
-    and greater_iff_sym_less: "\<And>b a. cmp b a = Greater \<longleftrightarrow> cmp a b = Less"
+  fixes cmp :: \<open>'a \<Rightarrow> 'a \<Rightarrow> comp\<close>
+  assumes refl [simp]: \<open>\<And>a. cmp a a = Equiv\<close>
+    and trans_equiv: \<open>\<And>a b c. cmp a b = Equiv \<Longrightarrow> cmp b c = Equiv \<Longrightarrow> cmp a c = Equiv\<close>
+  assumes trans_less: \<open>cmp a b = Less \<Longrightarrow> cmp b c = Less \<Longrightarrow> cmp a c = Less\<close>
+    and greater_iff_sym_less: \<open>\<And>b a. cmp b a = Greater \<longleftrightarrow> cmp a b = Less\<close>
 begin
 
 text \<open>Dual properties\<close>
 
 lemma trans_greater:
-  "cmp a c = Greater" if "cmp a b = Greater" "cmp b c = Greater"
+  \<open>cmp a c = Greater\<close> if \<open>cmp a b = Greater\<close> \<open>cmp b c = Greater\<close>
   using that greater_iff_sym_less trans_less by blast
 
 lemma less_iff_sym_greater:
-  "cmp b a = Less \<longleftrightarrow> cmp a b = Greater"
+  \<open>cmp b a = Less \<longleftrightarrow> cmp a b = Greater\<close>
   by (simp add: greater_iff_sym_less)
 
 text \<open>The equivalence part\<close>
 
 lemma sym:
-  "cmp b a = Equiv \<longleftrightarrow> cmp a b = Equiv"
+  \<open>cmp b a = Equiv \<longleftrightarrow> cmp a b = Equiv\<close>
   by (metis (full_types) comp.exhaust greater_iff_sym_less)
 
 lemma reflp:
-  "reflp (\<lambda>a b. cmp a b = Equiv)"
+  \<open>reflp (\<lambda>a b. cmp a b = Equiv)\<close>
   by (rule reflpI) simp
 
 lemma symp:
-  "symp (\<lambda>a b. cmp a b = Equiv)"
+  \<open>symp (\<lambda>a b. cmp a b = Equiv)\<close>
   by (rule sympI) (simp add: sym)
 
 lemma transp:
-  "transp (\<lambda>a b. cmp a b = Equiv)"
+  \<open>transp (\<lambda>a b. cmp a b = Equiv)\<close>
   by (rule transpI) (fact trans_equiv)
 
 lemma equivp:
-  "equivp (\<lambda>a b. cmp a b = Equiv)"
+  \<open>equivp (\<lambda>a b. cmp a b = Equiv)\<close>
   using reflp symp transp by (rule equivpI)
 
 text \<open>The strict part\<close>
 
 lemma irreflp_less:
-  "irreflp (\<lambda>a b. cmp a b = Less)"
+  \<open>irreflp (\<lambda>a b. cmp a b = Less)\<close>
   by (rule irreflpI) simp
 
 lemma irreflp_greater:
-  "irreflp (\<lambda>a b. cmp a b = Greater)"
+  \<open>irreflp (\<lambda>a b. cmp a b = Greater)\<close>
   by (rule irreflpI) simp
 
 lemma asym_less:
-  "cmp b a \<noteq> Less" if "cmp a b = Less"
+  \<open>cmp b a \<noteq> Less\<close> if \<open>cmp a b = Less\<close>
   using that greater_iff_sym_less by force
 
 lemma asym_greater:
-  "cmp b a \<noteq> Greater" if "cmp a b = Greater"
+  \<open>cmp b a \<noteq> Greater\<close> if \<open>cmp a b = Greater\<close>
   using that greater_iff_sym_less by force
 
 lemma asymp_less:
-  "asymp (\<lambda>a b. cmp a b = Less)"
-  using irreflp_less by (auto intro: asympI dest: asym_less)
+  \<open>asymp (\<lambda>a b. cmp a b = Less)\<close>
+  using irreflp_less by (auto dest: asym_less)
 
 lemma asymp_greater:
-  "asymp (\<lambda>a b. cmp a b = Greater)"
-  using irreflp_greater by (auto intro!: asympI dest: asym_greater)
+  \<open>asymp (\<lambda>a b. cmp a b = Greater)\<close>
+  using irreflp_greater by (auto dest: asym_greater)
 
 lemma trans_equiv_less:
-  "cmp a c = Less" if "cmp a b = Equiv" and "cmp b c = Less"
+  \<open>cmp a c = Less\<close> if \<open>cmp a b = Equiv\<close> and \<open>cmp b c = Less\<close>
   using that
   by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
 
 lemma trans_less_equiv:
-  "cmp a c = Less" if "cmp a b = Less" and "cmp b c = Equiv"
+  \<open>cmp a c = Less\<close> if \<open>cmp a b = Less\<close> and \<open>cmp b c = Equiv\<close>
   using that
   by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
 
 lemma trans_equiv_greater:
-  "cmp a c = Greater" if "cmp a b = Equiv" and "cmp b c = Greater"
+  \<open>cmp a c = Greater\<close> if \<open>cmp a b = Equiv\<close> and \<open>cmp b c = Greater\<close>
   using that by (simp add: sym [of a b] greater_iff_sym_less trans_less_equiv)
 
 lemma trans_greater_equiv:
-  "cmp a c = Greater" if "cmp a b = Greater" and "cmp b c = Equiv"
+  \<open>cmp a c = Greater\<close> if \<open>cmp a b = Greater\<close> and \<open>cmp b c = Equiv\<close>
   using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less)
 
 lemma transp_less:
-  "transp (\<lambda>a b. cmp a b = Less)"
+  \<open>transp (\<lambda>a b. cmp a b = Less)\<close>
   by (rule transpI) (fact trans_less)
 
 lemma transp_greater:
-  "transp (\<lambda>a b. cmp a b = Greater)"
+  \<open>transp (\<lambda>a b. cmp a b = Greater)\<close>
   by (rule transpI) (fact trans_greater)
 
 text \<open>The reflexive part\<close>
 
 lemma reflp_not_less:
-  "reflp (\<lambda>a b. cmp a b \<noteq> Less)"
+  \<open>reflp (\<lambda>a b. cmp a b \<noteq> Less)\<close>
   by (rule reflpI) simp
 
 lemma reflp_not_greater:
-  "reflp (\<lambda>a b. cmp a b \<noteq> Greater)"
+  \<open>reflp (\<lambda>a b. cmp a b \<noteq> Greater)\<close>
   by (rule reflpI) simp
 
 lemma quasisym_not_less:
-  "cmp a b = Equiv" if "cmp a b \<noteq> Less" and "cmp b a \<noteq> Less"
+  \<open>cmp a b = Equiv\<close> if \<open>cmp a b \<noteq> Less\<close> and \<open>cmp b a \<noteq> Less\<close>
   using that comp.exhaust greater_iff_sym_less by auto
 
 lemma quasisym_not_greater:
-  "cmp a b = Equiv" if "cmp a b \<noteq> Greater" and "cmp b a \<noteq> Greater"
+  \<open>cmp a b = Equiv\<close> if \<open>cmp a b \<noteq> Greater\<close> and \<open>cmp b a \<noteq> Greater\<close>
   using that comp.exhaust greater_iff_sym_less by auto
 
 lemma trans_not_less:
-  "cmp a c \<noteq> Less" if "cmp a b \<noteq> Less" "cmp b c \<noteq> Less"
+  \<open>cmp a c \<noteq> Less\<close> if \<open>cmp a b \<noteq> Less\<close> \<open>cmp b c \<noteq> Less\<close>
   using that by (metis comp.exhaust greater_iff_sym_less trans_equiv trans_less)
 
 lemma trans_not_greater:
-  "cmp a c \<noteq> Greater" if "cmp a b \<noteq> Greater" "cmp b c \<noteq> Greater"
+  \<open>cmp a c \<noteq> Greater\<close> if \<open>cmp a b \<noteq> Greater\<close> \<open>cmp b c \<noteq> Greater\<close>
   using that greater_iff_sym_less trans_not_less by blast
 
 lemma transp_not_less:
-  "transp (\<lambda>a b. cmp a b \<noteq> Less)"
+  \<open>transp (\<lambda>a b. cmp a b \<noteq> Less)\<close>
   by (rule transpI) (fact trans_not_less)
 
 lemma transp_not_greater:
-  "transp (\<lambda>a b. cmp a b \<noteq> Greater)"
+  \<open>transp (\<lambda>a b. cmp a b \<noteq> Greater)\<close>
   by (rule transpI) (fact trans_not_greater)
 
 text \<open>Substitution under equivalences\<close>
 
 lemma equiv_subst_left:
-  "cmp z y = comp \<longleftrightarrow> cmp x y = comp" if "cmp z x = Equiv" for comp
+  \<open>cmp z y = comp \<longleftrightarrow> cmp x y = comp\<close> if \<open>cmp z x = Equiv\<close> for comp
 proof -
-  from that have "cmp x z = Equiv"
+  from that have \<open>cmp x z = Equiv\<close>
     by (simp add: sym)
   with that show ?thesis
     by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater)
 qed
 
 lemma equiv_subst_right:
-  "cmp x z = comp \<longleftrightarrow> cmp x y = comp" if "cmp z y = Equiv" for comp
+  \<open>cmp x z = comp \<longleftrightarrow> cmp x y = comp\<close> if \<open>cmp z y = Equiv\<close> for comp
 proof -
-  from that have "cmp y z = Equiv"
+  from that have \<open>cmp y z = Equiv\<close>
     by (simp add: sym)
   with that show ?thesis
     by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv)
@@ -160,10 +160,10 @@
 
 end
 
-typedef 'a comparator = "{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}"
+typedef 'a comparator = \<open>{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}\<close>
   morphisms compare Abs_comparator
 proof -
-  have "comparator (\<lambda>_ _. Equiv)"
+  have \<open>comparator (\<lambda>_ _. Equiv)\<close>
     by standard simp_all
   then show ?thesis
     by auto
@@ -171,17 +171,17 @@
 
 setup_lifting type_definition_comparator
 
-global_interpretation compare: comparator "compare cmp"
+global_interpretation compare: comparator \<open>compare cmp\<close>
   using compare [of cmp] by simp
 
-lift_definition flat :: "'a comparator"
-  is "\<lambda>_ _. Equiv" by standard simp_all
+lift_definition flat :: \<open>'a comparator\<close>
+  is \<open>\<lambda>_ _. Equiv\<close> by standard simp_all
 
 instantiation comparator :: (linorder) default
 begin
 
-lift_definition default_comparator :: "'a comparator"
-  is "\<lambda>x y. if x < y then Less else if x > y then Greater else Equiv"
+lift_definition default_comparator :: \<open>'a comparator\<close>
+  is \<open>\<lambda>x y. if x < y then Less else if x > y then Greater else Equiv\<close>
   by standard (auto split: if_splits)
 
 instance ..
@@ -193,8 +193,8 @@
 instantiation comparator :: (enum) equal
 begin
 
-lift_definition equal_comparator :: "'a comparator \<Rightarrow> 'a comparator \<Rightarrow> bool"
-  is "\<lambda>f g. \<forall>x \<in> set Enum.enum. f x = g x" .
+lift_definition equal_comparator :: \<open>'a comparator \<Rightarrow> 'a comparator \<Rightarrow> bool\<close>
+  is \<open>\<lambda>f g. \<forall>x \<in> set Enum.enum. f x = g x\<close> .
 
 instance
   by (standard; transfer) (auto simp add: enum_UNIV)
@@ -202,23 +202,23 @@
 end
 
 lemma [code]:
-  "HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)"
+  \<open>HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)\<close>
   by transfer (simp add: enum_UNIV)
 
 lemma [code nbe]:
-  "HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True"
+  \<open>HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True\<close>
   by (fact equal_refl)
 
 instantiation comparator :: ("{linorder, typerep}") full_exhaustive
 begin
 
 definition full_exhaustive_comparator ::
-  "('a comparator \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option)
-    \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
-  where "full_exhaustive_comparator f s =
+  \<open>('a comparator \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option)
+    \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option\<close>
+  where \<open>full_exhaustive_comparator f s =
     Quickcheck_Exhaustive.orelse
       (f (flat, (\<lambda>u. Code_Evaluation.Const (STR ''Comparator.flat'') TYPEREP('a comparator))))
-      (f (default, (\<lambda>u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))"
+      (f (default, (\<lambda>u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))\<close>
 
 instance ..
 
@@ -227,67 +227,67 @@
 
 subsection \<open>Fundamental comparator combinators\<close>
 
-lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
-  is "\<lambda>cmp a b. cmp b a"
+lift_definition reversed :: \<open>'a comparator \<Rightarrow> 'a comparator\<close>
+  is \<open>\<lambda>cmp a b. cmp b a\<close>
 proof -
-  fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
-  assume "comparator cmp"
+  fix cmp :: \<open>'a \<Rightarrow> 'a \<Rightarrow> comp\<close>
+  assume \<open>comparator cmp\<close>
   then interpret comparator cmp .
-  show "comparator (\<lambda>a b. cmp b a)"
+  show \<open>comparator (\<lambda>a b. cmp b a)\<close>
     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
 qed
 
-lift_definition key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator"
-  is "\<lambda>f cmp a b. cmp (f a) (f b)"
+lift_definition key :: \<open>('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator\<close>
+  is \<open>\<lambda>f cmp a b. cmp (f a) (f b)\<close>
 proof -
-  fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp" and f :: "'b \<Rightarrow> 'a"
-  assume "comparator cmp"
+  fix cmp :: \<open>'a \<Rightarrow> 'a \<Rightarrow> comp\<close> and f :: \<open>'b \<Rightarrow> 'a\<close>
+  assume \<open>comparator cmp\<close>
   then interpret comparator cmp .
-  show "comparator (\<lambda>a b. cmp (f a) (f b))"
+  show \<open>comparator (\<lambda>a b. cmp (f a) (f b))\<close>
     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
 qed
 
 
 subsection \<open>Direct implementations for linear orders on selected types\<close>
 
-definition comparator_bool :: "bool comparator"
-  where [simp, code_abbrev]: "comparator_bool = default"
+definition comparator_bool :: \<open>bool comparator\<close>
+  where [simp, code_abbrev]: \<open>comparator_bool = default\<close>
 
 lemma compare_comparator_bool [code abstract]:
-  "compare comparator_bool = (\<lambda>p q.
+  \<open>compare comparator_bool = (\<lambda>p q.
     if p then if q then Equiv else Greater
-    else if q then Less else Equiv)"
+    else if q then Less else Equiv)\<close>
   by (auto simp add: fun_eq_iff) (transfer; simp)+
 
-definition raw_comparator_nat :: "nat \<Rightarrow> nat \<Rightarrow> comp"
-  where [simp]: "raw_comparator_nat = compare default"
+definition raw_comparator_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> comp\<close>
+  where [simp]: \<open>raw_comparator_nat = compare default\<close>
 
 lemma default_comparator_nat [simp, code]:
-  "raw_comparator_nat (0::nat) 0 = Equiv"
-  "raw_comparator_nat (Suc m) 0 = Greater"
-  "raw_comparator_nat 0 (Suc n) = Less"
-  "raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n"
+  \<open>raw_comparator_nat (0::nat) 0 = Equiv\<close>
+  \<open>raw_comparator_nat (Suc m) 0 = Greater\<close>
+  \<open>raw_comparator_nat 0 (Suc n) = Less\<close>
+  \<open>raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n\<close>
   by (transfer; simp)+
 
-definition comparator_nat :: "nat comparator"
-  where [simp, code_abbrev]: "comparator_nat = default"
+definition comparator_nat :: \<open>nat comparator\<close>
+  where [simp, code_abbrev]: \<open>comparator_nat = default\<close>
 
 lemma compare_comparator_nat [code abstract]:
-  "compare comparator_nat = raw_comparator_nat"
+  \<open>compare comparator_nat = raw_comparator_nat\<close>
   by simp
 
-definition comparator_linordered_group :: "'a::linordered_ab_group_add comparator"
-  where [simp, code_abbrev]: "comparator_linordered_group = default"
+definition comparator_linordered_group :: \<open>'a::linordered_ab_group_add comparator\<close>
+  where [simp, code_abbrev]: \<open>comparator_linordered_group = default\<close>
 
 lemma comparator_linordered_group [code abstract]:
-  "compare comparator_linordered_group = (\<lambda>a b.
+  \<open>compare comparator_linordered_group = (\<lambda>a b.
     let c = a - b in if c < 0 then Less
-    else if c = 0 then Equiv else Greater)"
+    else if c = 0 then Equiv else Greater)\<close>
 proof (rule ext)+
   fix a b :: 'a
-  show "compare comparator_linordered_group a b =
+  show \<open>compare comparator_linordered_group a b =
     (let c = a - b in if c < 0 then Less
-       else if c = 0 then Equiv else Greater)"
+       else if c = 0 then Equiv else Greater)\<close>
     by (simp add: Let_def not_less) (transfer; auto)
 qed
 
diff -r 667c67b1e8f1 -r f1ff9123c62a src/HOL/Library/Sorting_Algorithms.thy
--- a/src/HOL/Library/Sorting_Algorithms.thy	Mon Mar 31 19:17:51 2025 +0200
+++ b/src/HOL/Library/Sorting_Algorithms.thy	Sun Mar 30 20:20:26 2025 +0200
@@ -8,43 +8,43 @@
 
 section \<open>Stably sorted lists\<close>
 
-abbreviation (input) stable_segment :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  where "stable_segment cmp x \<equiv> filter (\<lambda>y. compare cmp x y = Equiv)"
+abbreviation (input) stable_segment :: \<open>'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+  where \<open>stable_segment cmp x \<equiv> filter (\<lambda>y. compare cmp x y = Equiv)\<close>
 
-fun sorted :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> bool"
-  where sorted_Nil: "sorted cmp [] \<longleftrightarrow> True"
-  | sorted_single: "sorted cmp [x] \<longleftrightarrow> True"
-  | sorted_rec: "sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp y x \<noteq> Greater \<and> sorted cmp (x # xs)"
+fun sorted :: \<open>'a comparator \<Rightarrow> 'a list \<Rightarrow> bool\<close>
+  where sorted_Nil: \<open>sorted cmp [] \<longleftrightarrow> True\<close>
+  | sorted_single: \<open>sorted cmp [x] \<longleftrightarrow> True\<close>
+  | sorted_rec: \<open>sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp y x \<noteq> Greater \<and> sorted cmp (x # xs)\<close>
 
 lemma sorted_ConsI:
-  "sorted cmp (x # xs)" if "sorted cmp xs"
-    and "\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp x y \<noteq> Greater"
+  \<open>sorted cmp (x # xs)\<close> if \<open>sorted cmp xs\<close>
+    and \<open>\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp x y \<noteq> Greater\<close>
   using that by (cases xs) simp_all
 
 lemma sorted_Cons_imp_sorted:
-  "sorted cmp xs" if "sorted cmp (x # xs)"
+  \<open>sorted cmp xs\<close> if \<open>sorted cmp (x # xs)\<close>
   using that by (cases xs) simp_all
 
 lemma sorted_Cons_imp_not_less:
-  "compare cmp y x \<noteq> Greater" if "sorted cmp (y # xs)"
-    and "x \<in> set xs"
+  \<open>compare cmp y x \<noteq> Greater\<close> if \<open>sorted cmp (y # xs)\<close>
+    and \<open>x \<in> set xs\<close>
   using that by (induction xs arbitrary: y) (auto dest: compare.trans_not_greater)
 
 lemma sorted_induct [consumes 1, case_names Nil Cons, induct pred: sorted]:
-  "P xs" if "sorted cmp xs" and "P []"
-    and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P xs
-      \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) \<Longrightarrow> P (x # xs)"
+  \<open>P xs\<close> if \<open>sorted cmp xs\<close> and \<open>P []\<close>
+    and *: \<open>\<And>x xs. sorted cmp xs \<Longrightarrow> P xs
+      \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) \<Longrightarrow> P (x # xs)\<close>
 using \<open>sorted cmp xs\<close> proof (induction xs)
   case Nil
   show ?case
     by (rule \<open>P []\<close>)
 next
   case (Cons x xs)
-  from \<open>sorted cmp (x # xs)\<close> have "sorted cmp xs"
+  from \<open>sorted cmp (x # xs)\<close> have \<open>sorted cmp xs\<close>
     by (cases xs) simp_all
-  moreover have "P xs" using \<open>sorted cmp xs\<close>
+  moreover have \<open>P xs\<close> using \<open>sorted cmp xs\<close>
     by (rule Cons.IH)
-  moreover have "compare cmp x y \<noteq> Greater" if "y \<in> set xs" for y
+  moreover have \<open>compare cmp x y \<noteq> Greater\<close> if \<open>y \<in> set xs\<close> for y
   using that \<open>sorted cmp (x # xs)\<close> proof (induction xs)
     case Nil
     then show ?case
@@ -58,9 +58,9 @@
         by simp
     next
       case (Cons w ws)
-      with Cons.prems have "compare cmp z w \<noteq> Greater" "compare cmp x z \<noteq> Greater"
+      with Cons.prems have \<open>compare cmp z w \<noteq> Greater\<close> \<open>compare cmp x z \<noteq> Greater\<close>
         by auto
-      then have "compare cmp x w \<noteq> Greater"
+      then have \<open>compare cmp x w \<noteq> Greater\<close>
         by (auto dest: compare.trans_not_greater)
       with Cons show ?thesis
         using Cons.prems Cons.IH by auto
@@ -71,28 +71,28 @@
 qed
 
 lemma sorted_induct_remove1 [consumes 1, case_names Nil minimum]:
-  "P xs" if "sorted cmp xs" and "P []"
-    and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P (remove1 x xs)
+  \<open>P xs\<close> if \<open>sorted cmp xs\<close> and \<open>P []\<close>
+    and *: \<open>\<And>x xs. sorted cmp xs \<Longrightarrow> P (remove1 x xs)
       \<Longrightarrow> x \<in> set xs \<Longrightarrow> hd (stable_segment cmp x xs) = x \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater)
-    \<Longrightarrow> P xs"
+    \<Longrightarrow> P xs\<close>
 using \<open>sorted cmp xs\<close> proof (induction xs)
   case Nil
   show ?case
     by (rule \<open>P []\<close>)
 next
   case (Cons x xs)
-  then have "sorted cmp (x # xs)"
+  then have \<open>sorted cmp (x # xs)\<close>
     by (simp add: sorted_ConsI)
   moreover note Cons.IH
-  moreover have "\<And>y. compare cmp x y = Greater \<Longrightarrow> y \<in> set xs \<Longrightarrow> False"
+  moreover have \<open>\<And>y. compare cmp x y = Greater \<Longrightarrow> y \<in> set xs \<Longrightarrow> False\<close>
     using Cons.hyps by simp
   ultimately show ?case
-    by (auto intro!: * [of "x # xs" x]) blast
+    by (auto intro!: * [of \<open>x # xs\<close> x]) blast
 qed
 
 lemma sorted_remove1:
-  "sorted cmp (remove1 x xs)" if "sorted cmp xs"
-proof (cases "x \<in> set xs")
+  \<open>sorted cmp (remove1 x xs)\<close> if \<open>sorted cmp xs\<close>
+proof (cases \<open>x \<in> set xs\<close>)
   case False
   with that show ?thesis
     by (simp add: remove1_idem)
@@ -104,21 +104,21 @@
       by simp
   next
     case (Cons y ys)
-    show ?case proof (cases "x = y")
+    show ?case proof (cases \<open>x = y\<close>)
       case True
       with Cons.hyps show ?thesis
         by simp
     next
       case False
-      then have "sorted cmp (remove1 x ys)"
+      then have \<open>sorted cmp (remove1 x ys)\<close>
         using Cons.IH Cons.prems by auto
-      then have "sorted cmp (y # remove1 x ys)"
+      then have \<open>sorted cmp (y # remove1 x ys)\<close>
       proof (rule sorted_ConsI)
         fix z zs
-        assume "remove1 x ys = z # zs"
-        with \<open>x \<noteq> y\<close> have "z \<in> set ys"
+        assume \<open>remove1 x ys = z # zs\<close>
+        with \<open>x \<noteq> y\<close> have \<open>z \<in> set ys\<close>
           using notin_set_remove1 [of z ys x] by auto
-        then show "compare cmp y z \<noteq> Greater"
+        then show \<open>compare cmp y z \<noteq> Greater\<close>
           by (rule Cons.hyps(2))
       qed
       with False show ?thesis
@@ -128,7 +128,7 @@
 qed
 
 lemma sorted_stable_segment:
-  "sorted cmp (stable_segment cmp x xs)"
+  \<open>sorted cmp (stable_segment cmp x xs)\<close>
 proof (induction xs)
   case Nil
   show ?case
@@ -141,22 +141,22 @@
 
 qed
 
-primrec insort :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  where "insort cmp y [] = [y]"
-  | "insort cmp y (x # xs) = (if compare cmp y x \<noteq> Greater
+primrec insort :: \<open>'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+  where \<open>insort cmp y [] = [y]\<close>
+  | \<open>insort cmp y (x # xs) = (if compare cmp y x \<noteq> Greater
        then y # x # xs
-       else x # insort cmp y xs)"
+       else x # insort cmp y xs)\<close>
 
 lemma mset_insort [simp]:
-  "mset (insort cmp x xs) = add_mset x (mset xs)"
+  \<open>mset (insort cmp x xs) = add_mset x (mset xs)\<close>
   by (induction xs) simp_all
 
 lemma length_insort [simp]:
-  "length (insort cmp x xs) = Suc (length xs)"
+  \<open>length (insort cmp x xs) = Suc (length xs)\<close>
   by (induction xs) simp_all
 
 lemma sorted_insort:
-  "sorted cmp (insort cmp x xs)" if "sorted cmp xs"
+  \<open>sorted cmp (insort cmp x xs)\<close> if \<open>sorted cmp xs\<close>
 using that proof (induction xs)
   case Nil
   then show ?case
@@ -168,37 +168,37 @@
 qed
 
 lemma stable_insort_equiv:
-  "stable_segment cmp y (insort cmp x xs) = x # stable_segment cmp y xs"
-    if "compare cmp y x = Equiv"
+  \<open>stable_segment cmp y (insort cmp x xs) = x # stable_segment cmp y xs\<close>
+    if \<open>compare cmp y x = Equiv\<close>
 proof (induction xs)
   case Nil
   from that show ?case
     by simp
 next
   case (Cons z xs)
-  moreover from that have "compare cmp y z = Equiv \<Longrightarrow> compare cmp z x = Equiv"
+  moreover from that have \<open>compare cmp y z = Equiv \<Longrightarrow> compare cmp z x = Equiv\<close>
     by (auto intro: compare.trans_equiv simp add: compare.sym)
   ultimately show ?case
     using that by (auto simp add: compare.greater_iff_sym_less)
 qed
 
 lemma stable_insort_not_equiv:
-  "stable_segment cmp y (insort cmp x xs) = stable_segment cmp y xs"
-    if "compare cmp y x \<noteq> Equiv"
+  \<open>stable_segment cmp y (insort cmp x xs) = stable_segment cmp y xs\<close>
+    if \<open>compare cmp y x \<noteq> Equiv\<close>
   using that by (induction xs) simp_all
 
 lemma remove1_insort_same_eq [simp]:
-  "remove1 x (insort cmp x xs) = xs"
+  \<open>remove1 x (insort cmp x xs) = xs\<close>
   by (induction xs) simp_all
 
 lemma insort_eq_ConsI:
-  "insort cmp x xs = x # xs"
-    if "sorted cmp xs" "\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater"
+  \<open>insort cmp x xs = x # xs\<close>
+    if \<open>sorted cmp xs\<close> \<open>\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater\<close>
   using that by (induction xs) (simp_all add: compare.greater_iff_sym_less)
 
 lemma remove1_insort_not_same_eq [simp]:
-  "remove1 y (insort cmp x xs) = insort cmp x (remove1 y xs)"
-    if "sorted cmp xs" "x \<noteq> y"
+  \<open>remove1 y (insort cmp x xs) = insort cmp x (remove1 y xs)\<close>
+    if \<open>sorted cmp xs\<close> \<open>x \<noteq> y\<close>
 using that proof (induction xs)
   case Nil
   then show ?case
@@ -206,13 +206,13 @@
 next
   case (Cons z zs)
   show ?case
-  proof (cases "compare cmp x z = Greater")
+  proof (cases \<open>compare cmp x z = Greater\<close>)
     case True
     with Cons show ?thesis
       by simp
   next
     case False
-    then have "compare cmp x y \<noteq> Greater" if "y \<in> set zs" for y
+    then have \<open>compare cmp x y \<noteq> Greater\<close> if \<open>y \<in> set zs\<close> for y
       using that Cons.hyps
       by (auto dest: compare.trans_not_greater)
     with Cons show ?thesis
@@ -221,25 +221,25 @@
 qed
 
 lemma insort_remove1_same_eq:
-  "insort cmp x (remove1 x xs) = xs"
-    if "sorted cmp xs" and "x \<in> set xs" and "hd (stable_segment cmp x xs) = x"
+  \<open>insort cmp x (remove1 x xs) = xs\<close>
+    if \<open>sorted cmp xs\<close> and \<open>x \<in> set xs\<close> and \<open>hd (stable_segment cmp x xs) = x\<close>
 using that proof (induction xs)
   case Nil
   then show ?case
     by simp
 next
   case (Cons y ys)
-  then have "compare cmp x y \<noteq> Less"
+  then have \<open>compare cmp x y \<noteq> Less\<close>
     by (auto simp add: compare.greater_iff_sym_less)
-  then consider "compare cmp x y = Greater" | "compare cmp x y = Equiv"
-    by (cases "compare cmp x y") auto
+  then consider \<open>compare cmp x y = Greater\<close> | \<open>compare cmp x y = Equiv\<close>
+    by (cases \<open>compare cmp x y\<close>) auto
   then show ?case proof cases
     case 1
     with Cons.prems Cons.IH show ?thesis
       by auto
   next
     case 2
-    with Cons.prems have "x = y"
+    with Cons.prems have \<open>x = y\<close>
       by simp
     with Cons.hyps show ?thesis
       by (simp add: insort_eq_ConsI)
@@ -247,8 +247,8 @@
 qed
 
 lemma sorted_append_iff:
-  "sorted cmp (xs @ ys) \<longleftrightarrow> sorted cmp xs \<and> sorted cmp ys
-     \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. compare cmp x y \<noteq> Greater)" (is "?P \<longleftrightarrow> ?R \<and> ?S \<and> ?Q")
+  \<open>sorted cmp (xs @ ys) \<longleftrightarrow> sorted cmp xs \<and> sorted cmp ys
+     \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. compare cmp x y \<noteq> Greater)\<close> (is \<open>?P \<longleftrightarrow> ?R \<and> ?S \<and> ?Q\<close>)
 proof
   assume ?P
   have ?R
@@ -260,10 +260,10 @@
   moreover have ?Q
     using \<open>?P\<close> by (induction xs) (auto simp add: sorted_Cons_imp_not_less,
       simp add: sorted_Cons_imp_sorted)
-  ultimately show "?R \<and> ?S \<and> ?Q"
+  ultimately show \<open>?R \<and> ?S \<and> ?Q\<close>
     by simp
 next
-  assume "?R \<and> ?S \<and> ?Q"
+  assume \<open>?R \<and> ?S \<and> ?Q\<close>
   then have ?R ?S ?Q
     by simp_all
   then show ?P
@@ -271,65 +271,65 @@
       (auto simp add: append_eq_Cons_conv intro!: sorted_ConsI)
 qed
 
-definition sort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  where "sort cmp xs = foldr (insort cmp) xs []"
+definition sort :: \<open>'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+  where \<open>sort cmp xs = foldr (insort cmp) xs []\<close>
 
 lemma sort_simps [simp]:
-  "sort cmp [] = []"
-  "sort cmp (x # xs) = insort cmp x (sort cmp xs)"
+  \<open>sort cmp [] = []\<close>
+  \<open>sort cmp (x # xs) = insort cmp x (sort cmp xs)\<close>
   by (simp_all add: sort_def)
 
 lemma mset_sort [simp]:
-  "mset (sort cmp xs) = mset xs"
+  \<open>mset (sort cmp xs) = mset xs\<close>
   by (induction xs) simp_all
 
 lemma length_sort [simp]:
-  "length (sort cmp xs) = length xs"
+  \<open>length (sort cmp xs) = length xs\<close>
   by (induction xs) simp_all
 
 lemma sorted_sort [simp]:
-  "sorted cmp (sort cmp xs)"
+  \<open>sorted cmp (sort cmp xs)\<close>
   by (induction xs) (simp_all add: sorted_insort)
 
 lemma stable_sort:
-  "stable_segment cmp x (sort cmp xs) = stable_segment cmp x xs"
+  \<open>stable_segment cmp x (sort cmp xs) = stable_segment cmp x xs\<close>
   by (induction xs) (simp_all add: stable_insort_equiv stable_insort_not_equiv)
 
 lemma sort_remove1_eq [simp]:
-  "sort cmp (remove1 x xs) = remove1 x (sort cmp xs)"
+  \<open>sort cmp (remove1 x xs) = remove1 x (sort cmp xs)\<close>
   by (induction xs) simp_all
 
 lemma set_insort [simp]:
-  "set (insort cmp x xs) = insert x (set xs)"
+  \<open>set (insort cmp x xs) = insert x (set xs)\<close>
   by (induction xs) auto
 
 lemma set_sort [simp]:
-  "set (sort cmp xs) = set xs"
+  \<open>set (sort cmp xs) = set xs\<close>
   by (induction xs) auto
 
 lemma sort_eqI:
-  "sort cmp ys = xs"
-    if permutation: "mset ys = mset xs"
-    and sorted: "sorted cmp xs"
-    and stable: "\<And>y. y \<in> set ys \<Longrightarrow>
-      stable_segment cmp y ys = stable_segment cmp y xs"
+  \<open>sort cmp ys = xs\<close>
+    if permutation: \<open>mset ys = mset xs\<close>
+    and sorted: \<open>sorted cmp xs\<close>
+    and stable: \<open>\<And>y. y \<in> set ys \<Longrightarrow>
+      stable_segment cmp y ys = stable_segment cmp y xs\<close>
 proof -
-  have stable': "stable_segment cmp y ys =
-    stable_segment cmp y xs" for y
-  proof (cases "\<exists>x\<in>set ys. compare cmp y x = Equiv")
+  have stable': \<open>stable_segment cmp y ys =
+    stable_segment cmp y xs\<close> for y
+  proof (cases \<open>\<exists>x\<in>set ys. compare cmp y x = Equiv\<close>)
     case True
-    then obtain z where "z \<in> set ys" and "compare cmp y z = Equiv"
+    then obtain z where \<open>z \<in> set ys\<close> and \<open>compare cmp y z = Equiv\<close>
       by auto
-    then have "compare cmp y x = Equiv \<longleftrightarrow> compare cmp z x = Equiv" for x
+    then have \<open>compare cmp y x = Equiv \<longleftrightarrow> compare cmp z x = Equiv\<close> for x
       by (meson compare.sym compare.trans_equiv)
-    moreover have "stable_segment cmp z ys =
-      stable_segment cmp z xs"
+    moreover have \<open>stable_segment cmp z ys =
+      stable_segment cmp z xs\<close>
       using \<open>z \<in> set ys\<close> by (rule stable)
     ultimately show ?thesis
       by simp
   next
     case False
-    moreover from permutation have "set ys = set xs"
+    moreover from permutation have \<open>set ys = set xs\<close>
       by (rule mset_eq_setD)
     ultimately show ?thesis
       by simp
@@ -341,40 +341,40 @@
       by simp
   next
     case (minimum x xs)
-    from \<open>mset ys = mset xs\<close> have ys: "set ys = set xs"
+    from \<open>mset ys = mset xs\<close> have ys: \<open>set ys = set xs\<close>
       by (rule mset_eq_setD)
-    then have "compare cmp x y \<noteq> Greater" if "y \<in> set ys" for y
+    then have \<open>compare cmp x y \<noteq> Greater\<close> if \<open>y \<in> set ys\<close> for y
       using that minimum.hyps by simp
-    from minimum.prems have stable: "stable_segment cmp x ys = stable_segment cmp x xs"
+    from minimum.prems have stable: \<open>stable_segment cmp x ys = stable_segment cmp x xs\<close>
       by simp
-    have "sort cmp (remove1 x ys) = remove1 x xs"
+    have \<open>sort cmp (remove1 x ys) = remove1 x xs\<close>
       by (rule minimum.IH) (simp_all add: minimum.prems filter_remove1)
-    then have "remove1 x (sort cmp ys) = remove1 x xs"
+    then have \<open>remove1 x (sort cmp ys) = remove1 x xs\<close>
       by simp
-    then have "insort cmp x (remove1 x (sort cmp ys)) =
-      insort cmp x (remove1 x xs)"
+    then have \<open>insort cmp x (remove1 x (sort cmp ys)) =
+      insort cmp x (remove1 x xs)\<close>
       by simp
-    also from minimum.hyps ys stable have "insort cmp x (remove1 x (sort cmp ys)) = sort cmp ys"
+    also from minimum.hyps ys stable have \<open>insort cmp x (remove1 x (sort cmp ys)) = sort cmp ys\<close>
       by (simp add: stable_sort insort_remove1_same_eq)
-    also from minimum.hyps have "insort cmp x (remove1 x xs) = xs"
+    also from minimum.hyps have \<open>insort cmp x (remove1 x xs) = xs\<close>
       by (simp add: insort_remove1_same_eq)
     finally show ?case .
   qed
 qed
 
 lemma filter_insort:
-  "filter P (insort cmp x xs) = insort cmp x (filter P xs)"
-    if "sorted cmp xs" and "P x"
+  \<open>filter P (insort cmp x xs) = insort cmp x (filter P xs)\<close>
+    if \<open>sorted cmp xs\<close> and \<open>P x\<close>
   using that by (induction xs)
     (auto simp add: compare.trans_not_greater insort_eq_ConsI)
 
 lemma filter_insort_triv:
-  "filter P (insort cmp x xs) = filter P xs"
-    if "\<not> P x"
+  \<open>filter P (insort cmp x xs) = filter P xs\<close>
+    if \<open>\<not> P x\<close>
   using that by (induction xs) simp_all
 
 lemma filter_sort:
-  "filter P (sort cmp xs) = sort cmp (filter P xs)"
+  \<open>filter P (sort cmp xs) = sort cmp (filter P xs)\<close>
   by (induction xs) (auto simp add: filter_insort filter_insort_triv)
 
 
@@ -382,80 +382,80 @@
 
 subsection \<open>Quicksort\<close>
 
-definition quicksort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  where quicksort_is_sort [simp]: "quicksort = sort"
+definition quicksort :: \<open>'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+  where quicksort_is_sort [simp]: \<open>quicksort = sort\<close>
 
 lemma sort_by_quicksort:
-  "sort = quicksort"
+  \<open>sort = quicksort\<close>
   by simp
 
 lemma sort_by_quicksort_rec:
-  "sort cmp xs = sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Less]
+  \<open>sort cmp xs = sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Less]
     @ stable_segment cmp (xs ! (length xs div 2)) xs
-    @ sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Greater]" (is "_ = ?rhs")
+    @ sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Greater]\<close> (is \<open>_ = ?rhs\<close>)
 proof (rule sort_eqI)
-  show "mset xs = mset ?rhs"
+  show \<open>mset xs = mset ?rhs\<close>
     by (rule multiset_eqI) (auto simp add: compare.sym intro: comp.exhaust)
 next
-  show "sorted cmp ?rhs"
+  show \<open>sorted cmp ?rhs\<close>
     by (auto simp add: sorted_append_iff sorted_stable_segment compare.equiv_subst_right dest: compare.trans_greater)
 next
-  let ?pivot = "xs ! (length xs div 2)"
+  let ?pivot = \<open>xs ! (length xs div 2)\<close>
   fix l
-  have "compare cmp x ?pivot = comp \<and> compare cmp l x = Equiv
-    \<longleftrightarrow> compare cmp l ?pivot = comp \<and> compare cmp l x = Equiv" for x comp
+  have \<open>compare cmp x ?pivot = comp \<and> compare cmp l x = Equiv
+    \<longleftrightarrow> compare cmp l ?pivot = comp \<and> compare cmp l x = Equiv\<close> for x comp
   proof -
-    have "compare cmp x ?pivot = comp \<longleftrightarrow> compare cmp l ?pivot = comp"
-      if "compare cmp l x = Equiv"
+    have \<open>compare cmp x ?pivot = comp \<longleftrightarrow> compare cmp l ?pivot = comp\<close>
+      if \<open>compare cmp l x = Equiv\<close>
       using that by (simp add: compare.equiv_subst_left compare.sym)
     then show ?thesis by blast
   qed
-  then show "stable_segment cmp l xs = stable_segment cmp l ?rhs"
+  then show \<open>stable_segment cmp l xs = stable_segment cmp l ?rhs\<close>
     by (simp add: stable_sort compare.sym [of _ ?pivot])
-      (cases "compare cmp l ?pivot", simp_all)
+      (cases \<open>compare cmp l ?pivot\<close>, simp_all)
 qed
 
 context
 begin
 
-qualified definition partition :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list"
-  where "partition cmp pivot xs =
-    ([x \<leftarrow> xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \<leftarrow> xs. compare cmp x pivot = Greater])"
+qualified definition partition :: \<open>'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list\<close>
+  where \<open>partition cmp pivot xs =
+    ([x \<leftarrow> xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \<leftarrow> xs. compare cmp x pivot = Greater])\<close>
 
 qualified lemma partition_code [code]:
-  "partition cmp pivot [] = ([], [], [])"
-  "partition cmp pivot (x # xs) =
+  \<open>partition cmp pivot [] = ([], [], [])\<close>
+  \<open>partition cmp pivot (x # xs) =
     (let (lts, eqs, gts) = partition cmp pivot xs
      in case compare cmp x pivot of
        Less \<Rightarrow> (x # lts, eqs, gts)
      | Equiv \<Rightarrow> (lts, x # eqs, gts)
-     | Greater \<Rightarrow> (lts, eqs, x # gts))"
+     | Greater \<Rightarrow> (lts, eqs, x # gts))\<close>
   using comp.exhaust by (auto simp add: partition_def Let_def compare.sym [of _ pivot])
 
 lemma quicksort_code [code]:
-  "quicksort cmp xs =
+  \<open>quicksort cmp xs =
     (case xs of
       [] \<Rightarrow> []
     | [x] \<Rightarrow> xs
     | [x, y] \<Rightarrow> (if compare cmp x y \<noteq> Greater then xs else [y, x])
     | _ \<Rightarrow>
         let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs
-        in quicksort cmp lts @ eqs @ quicksort cmp gts)"
-proof (cases "length xs \<ge> 3")
+        in quicksort cmp lts @ eqs @ quicksort cmp gts)\<close>
+proof (cases \<open>length xs \<ge> 3\<close>)
   case False
-  then have "length xs \<in> {0, 1, 2}"
+  then have \<open>length xs \<in> {0, 1, 2}\<close>
     by (auto simp add: not_le le_less less_antisym)
-  then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]"
+  then consider \<open>xs = []\<close> | x where \<open>xs = [x]\<close> | x y where \<open>xs = [x, y]\<close>
     by (auto simp add: length_Suc_conv numeral_2_eq_2)
   then show ?thesis
     by cases simp_all
 next
   case True
-  then obtain x y z zs where "xs = x # y # z # zs"
+  then obtain x y z zs where \<open>xs = x # y # z # zs\<close>
     by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3)
-  moreover have "quicksort cmp xs =
+  moreover have \<open>quicksort cmp xs =
     (let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs
-    in quicksort cmp lts @ eqs @ quicksort cmp gts)"
+    in quicksort cmp lts @ eqs @ quicksort cmp gts)\<close>
     using sort_by_quicksort_rec [of cmp xs] by (simp add: partition_def)
   ultimately show ?thesis
     by simp
@@ -466,38 +466,38 @@
 
 subsection \<open>Mergesort\<close>
 
-definition mergesort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  where mergesort_is_sort [simp]: "mergesort = sort"
+definition mergesort :: \<open>'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+  where mergesort_is_sort [simp]: \<open>mergesort = sort\<close>
 
 lemma sort_by_mergesort:
-  "sort = mergesort"
+  \<open>sort = mergesort\<close>
   by simp
 
 context
-  fixes cmp :: "'a comparator"
+  fixes cmp :: \<open>'a comparator\<close>
 begin
 
-qualified function merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  where "merge [] ys = ys"
-  | "merge xs [] = xs"
-  | "merge (x # xs) (y # ys) = (if compare cmp x y = Greater
-      then y # merge (x # xs) ys else x # merge xs (y # ys))"
+qualified function merge :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> 'a list\<close>
+  where \<open>merge [] ys = ys\<close>
+  | \<open>merge xs [] = xs\<close>
+  | \<open>merge (x # xs) (y # ys) = (if compare cmp x y = Greater
+      then y # merge (x # xs) ys else x # merge xs (y # ys))\<close>
   by pat_completeness auto
 
 qualified termination by lexicographic_order
 
 lemma mset_merge:
-  "mset (merge xs ys) = mset xs + mset ys"
+  \<open>mset (merge xs ys) = mset xs + mset ys\<close>
   by (induction xs ys rule: merge.induct) simp_all
 
 lemma merge_eq_Cons_imp:
-  "xs \<noteq> [] \<and> z = hd xs \<or> ys \<noteq> [] \<and> z = hd ys"
-    if "merge xs ys = z # zs"
+  \<open>xs \<noteq> [] \<and> z = hd xs \<or> ys \<noteq> [] \<and> z = hd ys\<close>
+    if \<open>merge xs ys = z # zs\<close>
   using that by (induction xs ys rule: merge.induct) (auto split: if_splits)
 
 lemma filter_merge:
-  "filter P (merge xs ys) = merge (filter P xs) (filter P ys)"
-    if "sorted cmp xs" and "sorted cmp ys"
+  \<open>filter P (merge xs ys) = merge (filter P xs) (filter P ys)\<close>
+    if \<open>sorted cmp xs\<close> and \<open>sorted cmp ys\<close>
 using that proof (induction xs ys rule: merge.induct)
   case (1 ys)
   then show ?case
@@ -509,47 +509,47 @@
 next
   case (3 x xs y ys)
   show ?case
-  proof (cases "compare cmp x y = Greater")
+  proof (cases \<open>compare cmp x y = Greater\<close>)
     case True
-    with 3 have hyp: "filter P (merge (x # xs) ys) =
-      merge (filter P (x # xs)) (filter P ys)"
+    with 3 have hyp: \<open>filter P (merge (x # xs) ys) =
+      merge (filter P (x # xs)) (filter P ys)\<close>
       by (simp add: sorted_Cons_imp_sorted)
     show ?thesis
-    proof (cases "\<not> P x \<and> P y")
+    proof (cases \<open>\<not> P x \<and> P y\<close>)
       case False
       with \<open>compare cmp x y = Greater\<close> show ?thesis
         by (auto simp add: hyp)
     next
       case True
       from \<open>compare cmp x y = Greater\<close> "3.prems"
-      have *: "compare cmp z y = Greater" if "z \<in> set (filter P xs)" for z
+      have *: \<open>compare cmp z y = Greater\<close> if \<open>z \<in> set (filter P xs)\<close> for z
         using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less)
       from \<open>compare cmp x y = Greater\<close> show ?thesis
-        by (cases "filter P xs") (simp_all add: hyp *)
+        by (cases \<open>filter P xs\<close>) (simp_all add: hyp *)
     qed
   next
     case False
-    with 3 have hyp: "filter P (merge xs (y # ys)) =
-      merge (filter P xs) (filter P (y # ys))"
+    with 3 have hyp: \<open>filter P (merge xs (y # ys)) =
+      merge (filter P xs) (filter P (y # ys))\<close>
       by (simp add: sorted_Cons_imp_sorted)
     show ?thesis
-    proof (cases "P x \<and> \<not> P y")
+    proof (cases \<open>P x \<and> \<not> P y\<close>)
       case False
       with \<open>compare cmp x y \<noteq> Greater\<close> show ?thesis
         by (auto simp add: hyp)
     next
       case True
       from \<open>compare cmp x y \<noteq> Greater\<close> "3.prems"
-      have *: "compare cmp x z \<noteq> Greater" if "z \<in> set (filter P ys)" for z
+      have *: \<open>compare cmp x z \<noteq> Greater\<close> if \<open>z \<in> set (filter P ys)\<close> for z
         using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less)
       from \<open>compare cmp x y \<noteq> Greater\<close> show ?thesis
-        by (cases "filter P ys") (simp_all add: hyp *)
+        by (cases \<open>filter P ys\<close>) (simp_all add: hyp *)
     qed
   qed
 qed
 
 lemma sorted_merge:
-  "sorted cmp (merge xs ys)" if "sorted cmp xs" and "sorted cmp ys"
+  \<open>sorted cmp (merge xs ys)\<close> if \<open>sorted cmp xs\<close> and \<open>sorted cmp ys\<close>
 using that proof (induction xs ys rule: merge.induct)
   case (1 ys)
   then show ?case
@@ -561,15 +561,15 @@
 next
   case (3 x xs y ys)
   show ?case
-  proof (cases "compare cmp x y = Greater")
+  proof (cases \<open>compare cmp x y = Greater\<close>)
     case True
-    with 3 have "sorted cmp (merge (x # xs) ys)"
+    with 3 have \<open>sorted cmp (merge (x # xs) ys)\<close>
       by (simp add: sorted_Cons_imp_sorted)
-    then have "sorted cmp (y # merge (x # xs) ys)"
+    then have \<open>sorted cmp (y # merge (x # xs) ys)\<close>
     proof (rule sorted_ConsI)
       fix z zs
-      assume "merge (x # xs) ys = z # zs"
-      with 3(4) True show "compare cmp y z \<noteq> Greater"
+      assume \<open>merge (x # xs) ys = z # zs\<close>
+      with 3(4) True show \<open>compare cmp y z \<noteq> Greater\<close>
         by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp)
           (auto simp add: compare.asym_greater sorted_Cons_imp_not_less)
     qed
@@ -577,13 +577,13 @@
       by simp
   next
     case False
-    with 3 have "sorted cmp (merge xs (y # ys))"
+    with 3 have \<open>sorted cmp (merge xs (y # ys))\<close>
       by (simp add: sorted_Cons_imp_sorted)
-    then have "sorted cmp (x # merge xs (y # ys))"
+    then have \<open>sorted cmp (x # merge xs (y # ys))\<close>
     proof (rule sorted_ConsI)
       fix z zs
-      assume "merge xs (y # ys) = z # zs"
-      with 3(3) False show "compare cmp x z \<noteq> Greater"
+      assume \<open>merge xs (y # ys) = z # zs\<close>
+      with 3(3) False show \<open>compare cmp x z \<noteq> Greater\<close>
         by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp)
           (auto simp add: compare.asym_greater sorted_Cons_imp_not_less)
     qed
@@ -593,45 +593,45 @@
 qed
 
 lemma merge_eq_appendI:
-  "merge xs ys = xs @ ys"
-    if "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set ys \<Longrightarrow> compare cmp x y \<noteq> Greater"
+  \<open>merge xs ys = xs @ ys\<close>
+    if \<open>\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set ys \<Longrightarrow> compare cmp x y \<noteq> Greater\<close>
   using that by (induction xs ys rule: merge.induct) simp_all
 
 lemma merge_stable_segments:
-  "merge (stable_segment cmp l xs) (stable_segment cmp l ys) =
-     stable_segment cmp l xs @ stable_segment cmp l ys"
+  \<open>merge (stable_segment cmp l xs) (stable_segment cmp l ys) =
+     stable_segment cmp l xs @ stable_segment cmp l ys\<close>
   by (rule merge_eq_appendI) (auto dest: compare.trans_equiv_greater)
 
 lemma sort_by_mergesort_rec:
-  "sort cmp xs =
+  \<open>sort cmp xs =
     merge (sort cmp (take (length xs div 2) xs))
-      (sort cmp (drop (length xs div 2) xs))" (is "_ = ?rhs")
+      (sort cmp (drop (length xs div 2) xs))\<close> (is \<open>_ = ?rhs\<close>)
 proof (rule sort_eqI)
-  have "mset (take (length xs div 2) xs) + mset (drop (length xs div 2) xs) =
-    mset (take (length xs div 2) xs @ drop (length xs div 2) xs)"
+  have \<open>mset (take (length xs div 2) xs) + mset (drop (length xs div 2) xs) =
+    mset (take (length xs div 2) xs @ drop (length xs div 2) xs)\<close>
     by (simp only: mset_append)
-  then show "mset xs = mset ?rhs"
+  then show \<open>mset xs = mset ?rhs\<close>
     by (simp add: mset_merge)
 next
-  show "sorted cmp ?rhs"
+  show \<open>sorted cmp ?rhs\<close>
     by (simp add: sorted_merge)
 next
   fix l
-  have "stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)
-    = stable_segment cmp l xs"
+  have \<open>stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)
+    = stable_segment cmp l xs\<close>
     by (simp only: filter_append [symmetric] append_take_drop_id)
-  have "merge (stable_segment cmp l (take (length xs div 2) xs))
+  have \<open>merge (stable_segment cmp l (take (length xs div 2) xs))
     (stable_segment cmp l (drop (length xs div 2) xs)) =
-    stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)"
+    stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)\<close>
     by (rule merge_eq_appendI) (auto simp add: compare.trans_equiv_greater)
-  also have "\<dots> = stable_segment cmp l xs"
+  also have \<open>\<dots> = stable_segment cmp l xs\<close>
     by (simp only: filter_append [symmetric] append_take_drop_id)
-  finally show "stable_segment cmp l xs = stable_segment cmp l ?rhs"
+  finally show \<open>stable_segment cmp l xs = stable_segment cmp l ?rhs\<close>
     by (simp add: stable_sort filter_merge)
 qed
 
 lemma mergesort_code [code]:
-  "mergesort cmp xs =
+  \<open>mergesort cmp xs =
     (case xs of
       [] \<Rightarrow> []
     | [x] \<Rightarrow> xs
@@ -641,25 +641,25 @@
           half = length xs div 2;
           ys = take half xs;
           zs = drop half xs
-        in merge (mergesort cmp ys) (mergesort cmp zs))"
-proof (cases "length xs \<ge> 3")
+        in merge (mergesort cmp ys) (mergesort cmp zs))\<close>
+proof (cases \<open>length xs \<ge> 3\<close>)
   case False
-  then have "length xs \<in> {0, 1, 2}"
+  then have \<open>length xs \<in> {0, 1, 2}\<close>
     by (auto simp add: not_le le_less less_antisym)
-  then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]"
+  then consider \<open>xs = []\<close> | x where \<open>xs = [x]\<close> | x y where \<open>xs = [x, y]\<close>
     by (auto simp add: length_Suc_conv numeral_2_eq_2)
   then show ?thesis
     by cases simp_all
 next
   case True
-  then obtain x y z zs where "xs = x # y # z # zs"
+  then obtain x y z zs where \<open>xs = x # y # z # zs\<close>
     by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3)
-  moreover have "mergesort cmp xs =
+  moreover have \<open>mergesort cmp xs =
     (let
        half = length xs div 2;
        ys = take half xs;
        zs = drop half xs
-     in merge (mergesort cmp ys) (mergesort cmp zs))"
+     in merge (mergesort cmp ys) (mergesort cmp zs))\<close>
     using sort_by_mergesort_rec [of xs] by (simp add: Let_def)
   ultimately show ?thesis
     by simp