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