Theory Comparator

(*  Title:      HOL/Library/Comparator.thy
    Author:     Florian Haftmann, TU Muenchen
*)

theory Comparator
  imports Main
begin

section ‹Comparators on linear quasi-orders›

subsection ‹Basic properties›

datatype comp = Less | Equiv | Greater

locale comparator =
  fixes cmp :: ‹'a ⇒ 'a ⇒ comp›
  assumes refl [simp]: ‹⋀a. cmp a a = Equiv›
    and trans_equiv: ‹⋀a b c. cmp a b = Equiv ⟹ cmp b c = Equiv ⟹ cmp a c = Equiv›
  assumes trans_less: ‹cmp a b = Less ⟹ cmp b c = Less ⟹ cmp a c = Less›
    and greater_iff_sym_less: ‹⋀b a. cmp b a = Greater ⟷ cmp a b = Less›
begin

text ‹Dual properties›

lemma trans_greater:
  ‹cmp a c = Greater› if ‹cmp a b = Greater› ‹cmp b c = Greater›
  using that greater_iff_sym_less trans_less by blast

lemma less_iff_sym_greater:
  ‹cmp b a = Less ⟷ cmp a b = Greater›
  by (simp add: greater_iff_sym_less)

text ‹The equivalence part›

lemma sym:
  ‹cmp b a = Equiv ⟷ cmp a b = Equiv›
  by (metis (full_types) comp.exhaust greater_iff_sym_less)

lemma reflp:
  ‹reflp (λa b. cmp a b = Equiv)›
  by (rule reflpI) simp

lemma symp:
  ‹symp (λa b. cmp a b = Equiv)›
  by (rule sympI) (simp add: sym)

lemma transp:
  ‹transp (λa b. cmp a b = Equiv)›
  by (rule transpI) (fact trans_equiv)

lemma equivp:
  ‹equivp (λa b. cmp a b = Equiv)›
  using reflp symp transp by (rule equivpI)

text ‹The strict part›

lemma irreflp_less:
  ‹irreflp (λa b. cmp a b = Less)›
  by (rule irreflpI) simp

lemma irreflp_greater:
  ‹irreflp (λa b. cmp a b = Greater)›
  by (rule irreflpI) simp

lemma asym_less:
  ‹cmp b a ≠ Less› if ‹cmp a b = Less›
  using that greater_iff_sym_less by force

lemma asym_greater:
  ‹cmp b a ≠ Greater› if ‹cmp a b = Greater›
  using that greater_iff_sym_less by force

lemma asymp_less:
  ‹asymp (λa b. cmp a b = Less)›
  using irreflp_less by (auto dest: asym_less)

lemma asymp_greater:
  ‹asymp (λa b. cmp a b = Greater)›
  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›
  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›
  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›
  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›
  using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less)

lemma transp_less:
  ‹transp (λa b. cmp a b = Less)›
  by (rule transpI) (fact trans_less)

lemma transp_greater:
  ‹transp (λa b. cmp a b = Greater)›
  by (rule transpI) (fact trans_greater)

text ‹The reflexive part›

lemma reflp_not_less:
  ‹reflp (λa b. cmp a b ≠ Less)›
  by (rule reflpI) simp

lemma reflp_not_greater:
  ‹reflp (λa b. cmp a b ≠ Greater)›
  by (rule reflpI) simp

lemma quasisym_not_less:
  ‹cmp a b = Equiv› if ‹cmp a b ≠ Less› and ‹cmp b a ≠ Less›
  using that comp.exhaust greater_iff_sym_less by auto

lemma quasisym_not_greater:
  ‹cmp a b = Equiv› if ‹cmp a b ≠ Greater› and ‹cmp b a ≠ Greater›
  using that comp.exhaust greater_iff_sym_less by auto

lemma trans_not_less:
  ‹cmp a c ≠ Less› if ‹cmp a b ≠ Less› ‹cmp b c ≠ Less›
  using that by (metis comp.exhaust greater_iff_sym_less trans_equiv trans_less)

lemma trans_not_greater:
  ‹cmp a c ≠ Greater› if ‹cmp a b ≠ Greater› ‹cmp b c ≠ Greater›
  using that greater_iff_sym_less trans_not_less by blast

lemma transp_not_less:
  ‹transp (λa b. cmp a b ≠ Less)›
  by (rule transpI) (fact trans_not_less)

lemma transp_not_greater:
  ‹transp (λa b. cmp a b ≠ Greater)›
  by (rule transpI) (fact trans_not_greater)

text ‹Substitution under equivalences›

lemma equiv_subst_left:
  ‹cmp z y = comp ⟷ cmp x y = comp› if ‹cmp z x = Equiv› for comp
proof -
  from that have ‹cmp x z = Equiv›
    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 ⟷ cmp x y = comp› if ‹cmp z y = Equiv› for comp
proof -
  from that have ‹cmp y z = Equiv›
    by (simp add: sym)
  with that show ?thesis
    by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv)
qed

end

typedef 'a comparator = ‹{cmp :: 'a ⇒ 'a ⇒ comp. comparator cmp}›
  morphisms compare Abs_comparator
proof -
  have ‹comparator (λ_ _. Equiv)›
    by standard simp_all
  then show ?thesis
    by auto
qed

setup_lifting type_definition_comparator

global_interpretation compare: comparator ‹compare cmp›
  using compare [of cmp] by simp

lift_definition flat :: ‹'a comparator›
  is ‹λ_ _. Equiv› by standard simp_all

instantiation comparator :: (linorder) default
begin

lift_definition default_comparator :: ‹'a comparator›
  is ‹λx y. if x < y then Less else if x > y then Greater else Equiv›
  by standard (auto split: if_splits)

instance ..

end

lemma compare_default_eq_Less_iff [simp]:
  ‹compare default x y = Less ⟷ x < y›
  by transfer simp

lemma compare_default_eq_Equiv_iff [simp]:
  ‹compare default x y = Equiv ⟷ x = y›
  by transfer auto

lemma compare_default_eq_Greater_iff [simp]:
  ‹compare default x y = Greater ⟷ x > y›
  by transfer auto

text ‹A rudimentary quickcheck setup›

instantiation comparator :: (enum) equal
begin

lift_definition equal_comparator :: ‹'a comparator ⇒ 'a comparator ⇒ bool›
  is ‹λf g. ∀x ∈ set Enum.enum. f x = g x› .

instance
  by (standard; transfer) (auto simp add: enum_UNIV)

end

lemma [code nbe]:
  ‹HOL.equal (cmp :: 'a::enum comparator) cmp ⟷ True›
  by (fact equal_refl)

lemma [code]:
  ‹HOL.equal cmp1 cmp2 ⟷ Enum.enum_all (λx. compare cmp1 x = compare cmp2 x)›
  by transfer (simp add: enum_UNIV)

instantiation comparator :: ("{linorder, typerep}") full_exhaustive
begin

definition full_exhaustive_comparator ::
  ‹('a comparator × (unit ⇒ term) ⇒ (bool × term list) option)
    ⇒ natural ⇒ (bool × term list) option›
  where ‹full_exhaustive_comparator f s =
    Quickcheck_Exhaustive.orelse
      (f (flat, (λu. Code_Evaluation.Const (STR ''Comparator.flat'') TYPEREP('a comparator))))
      (f (default, (λu. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))›

instance ..

end


subsection ‹Fundamental comparator combinators›

lift_definition reversed :: ‹'a comparator ⇒ 'a comparator›
  is ‹λcmp a b. cmp b a›
proof -
  fix cmp :: ‹'a ⇒ 'a ⇒ comp›
  assume ‹comparator cmp›
  then interpret comparator cmp .
  show ‹comparator (λa b. cmp b a)›
    by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
qed

lemma compare_reversed_apply [simp]:
  ‹compare (reversed cmp) x y = compare cmp y x›
  by transfer simp

lift_definition key :: ‹('b ⇒ 'a) ⇒ 'a comparator ⇒ 'b comparator›
  is ‹λf cmp a b. cmp (f a) (f b)›
proof -
  fix cmp :: ‹'a ⇒ 'a ⇒ comp› and f :: ‹'b ⇒ 'a›
  assume ‹comparator cmp›
  then interpret comparator cmp .
  show ‹comparator (λa b. cmp (f a) (f b))›
    by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
qed

lemma compare_key_apply [simp]:
  ‹compare (key f cmp) x y = compare cmp (f x) (f y)›
  by transfer simp

lift_definition prod_lex :: ‹'a comparator ⇒ 'b comparator ⇒ ('a × 'b) comparator›
  is ‹λf g (a, c) (b, d). case f a b of Less ⇒ Less | Equiv ⇒ g c d | Greater ⇒ Greater›
proof -
  fix f :: ‹'a ⇒ 'a ⇒ comp› and g :: ‹'b ⇒ 'b ⇒ comp›
  assume ‹comparator f›
  then interpret f: comparator f .
  assume ‹comparator g›
  then interpret g: comparator g .
  define h where ‹h = (λ(a, c) (b, d). case f a b of Less ⇒ Less | Equiv ⇒ g c d | Greater ⇒ Greater)›
  then have h_apply [simp]: ‹h (a, c) (b, d) = (case f a b of Less ⇒ Less | Equiv ⇒ g c d | Greater ⇒ Greater)› for a b c d
    by simp
  have h_equiv: ‹h p q = Equiv ⟷ f (fst p) (fst q) = Equiv ∧ g (snd p) (snd q) = Equiv› for p q
    by (cases p; cases q) (simp split: comp.split)
  have h_less: ‹h p q = Less ⟷ f (fst p) (fst q) = Less ∨ f (fst p) (fst q) = Equiv ∧ g (snd p) (snd q) = Less› for p q
    by (cases p; cases q) (simp split: comp.split)
  have h_greater: ‹h p q = Greater ⟷ f (fst p) (fst q) = Greater ∨ f (fst p) (fst q) = Equiv ∧ g (snd p) (snd q) = Greater› for p q
    by (cases p; cases q) (simp split: comp.split)
  have ‹comparator h›
    apply standard
       apply (simp_all add: h_equiv h_less h_greater f.greater_iff_sym_less g.greater_iff_sym_less f.sym g.sym)
      apply (auto intro: f.trans_equiv g.trans_equiv f.trans_less g.trans_less f.trans_less_equiv f.trans_equiv_less)
    done
  then show ‹comparator (λ(a, c) (b, d). case f a b of Less ⇒ Less
    | Equiv ⇒ g c d
    | Greater ⇒ Greater)›
    by (simp add: h_def)
qed

lemma compare_prod_lex_apply:
  ‹compare (prod_lex cmp1 cmp2) p q =
    (case compare (key fst cmp1) p q of Less ⇒ Less | Equiv ⇒ compare (key snd cmp2) p q | Greater ⇒ Greater)›
  by transfer (simp add: split_def)


subsection ‹Direct implementations for linear orders on selected types›

definition comparator_bool :: ‹bool comparator›
  where [simp, code_abbrev]: ‹comparator_bool = default›

lemma compare_comparator_bool [code abstract]:
  ‹compare comparator_bool = (λ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)

definition raw_comparator_nat :: ‹nat ⇒ nat ⇒ 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 = (λ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