src/HOL/Library/Comparator.thy
 changeset 69251 d240598e8637 parent 69246 c1fe9dcc274a
```     1.1 --- a/src/HOL/Library/Comparator.thy	Wed Nov 07 11:08:10 2018 +0000
1.2 +++ b/src/HOL/Library/Comparator.thy	Wed Nov 07 11:08:11 2018 +0000
1.3 @@ -8,6 +8,8 @@
1.4
1.5  section \<open>Comparators on linear quasi-orders\<close>
1.6
1.7 +subsection \<open>Basic properties\<close>
1.8 +
1.9  datatype comp = Less | Equiv | Greater
1.10
1.11  locale comparator =
1.12 @@ -222,7 +224,8 @@
1.13
1.14  end
1.15
1.16 -text \<open>Fundamental comparator combinators\<close>
1.17 +
1.18 +subsection \<open>Fundamental comparator combinators\<close>
1.19
1.20  lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
1.21    is "\<lambda>cmp a b. cmp b a"
1.22 @@ -244,4 +247,48 @@
1.23      by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
1.24  qed
1.25
1.26 +
1.27 +subsection \<open>Direct implementations for linear orders on selected types\<close>
1.28 +
1.29 +definition comparator_bool :: "bool comparator"
1.30 +  where [simp, code_abbrev]: "comparator_bool = default"
1.31 +
1.32 +lemma compare_comparator_bool [code abstract]:
1.33 +  "compare comparator_bool = (\<lambda>p q.
1.34 +    if p then if q then Equiv else Greater
1.35 +    else if q then Less else Equiv)"
1.36 +  by (auto simp add: fun_eq_iff) (transfer; simp)+
1.37 +
1.38 +definition raw_comparator_nat :: "nat \<Rightarrow> nat \<Rightarrow> comp"
1.39 +  where [simp]: "raw_comparator_nat = compare default"
1.40 +
1.41 +lemma default_comparator_nat [simp, code]:
1.42 +  "raw_comparator_nat (0::nat) 0 = Equiv"
1.43 +  "raw_comparator_nat (Suc m) 0 = Greater"
1.44 +  "raw_comparator_nat 0 (Suc n) = Less"
1.45 +  "raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n"
1.46 +  by (transfer; simp)+
1.47 +
1.48 +definition comparator_nat :: "nat comparator"
1.49 +  where [simp, code_abbrev]: "comparator_nat = default"
1.50 +
1.51 +lemma compare_comparator_nat [code abstract]:
1.52 +  "compare comparator_nat = raw_comparator_nat"
1.53 +  by simp
1.54 +
1.55 +definition comparator_linordered_group :: "'a::linordered_ab_group_add comparator"
1.56 +  where [simp, code_abbrev]: "comparator_linordered_group = default"
1.57 +
1.58 +lemma comparator_linordered_group [code abstract]:
1.59 +  "compare comparator_linordered_group = (\<lambda>a b.
1.60 +    let c = a - b in if c < 0 then Less
1.61 +    else if c = 0 then Equiv else Greater)"
1.62 +proof (rule ext)+
1.63 +  fix a b :: 'a
1.64 +  show "compare comparator_linordered_group a b =
1.65 +    (let c = a - b in if c < 0 then Less
1.66 +       else if c = 0 then Equiv else Greater)"
1.67 +    by (simp add: Let_def not_less) (transfer; auto)
1.68 +qed
1.69 +
1.70  end
```