src/HOL/Library/Comparator.thy

--- a/src/HOL/Library/Comparator.thy	Wed Nov 07 11:08:10 2018 +0000
+++ b/src/HOL/Library/Comparator.thy	Wed Nov 07 11:08:11 2018 +0000
@@ -8,6 +8,8 @@
 
 section \<open>Comparators on linear quasi-orders\<close>
 
+subsection \<open>Basic properties\<close>
+
 datatype comp = Less | Equiv | Greater
 
 locale comparator =
@@ -222,7 +224,8 @@
 
 end
 
-text \<open>Fundamental comparator combinators\<close>
+
+subsection \<open>Fundamental comparator combinators\<close>
 
 lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
   is "\<lambda>cmp a b. cmp b a"
@@ -244,4 +247,48 @@
     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"
+
+lemma compare_comparator_bool [code abstract]:
+  "compare comparator_bool = (\<lambda>p q.
+    if p then if q then Equiv else Greater
+    else if q then Less else Equiv)"
+  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"
+
+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"
+  by (transfer; simp)+
+
+definition comparator_nat :: "nat comparator"
+  where [simp, code_abbrev]: "comparator_nat = default"
+
+lemma compare_comparator_nat [code abstract]:
+  "compare comparator_nat = raw_comparator_nat"
+  by simp
+
+definition comparator_linordered_group :: "'a::linordered_ab_group_add comparator"
+  where [simp, code_abbrev]: "comparator_linordered_group = default"
+
+lemma comparator_linordered_group [code abstract]:
+  "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)"
+proof (rule ext)+
+  fix a b :: 'a
+  show "compare comparator_linordered_group a b =
+    (let c = a - b in if c < 0 then Less
+       else if c = 0 then Equiv else Greater)"
+    by (simp add: Let_def not_less) (transfer; auto)
+qed
+
 end