Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Comparator.thy Sprache: Isabelle

Original von: Isabelle^©

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

theory Comparator
  imports Main
begin

section \<open>Comparators on linear quasi-orders\<close>

subsection \<open>Basic properties\<close>

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 \<open>Dual properties\<close>

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 \<open>The equivalence part\<close>

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 \<open>The strict part\<close>

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 intro: asympI dest: asym_less)

lemma asymp_greater:
  "asymp (\a b. cmp a b = Greater)"
  using irreflp_greater by (auto intro!: asympI 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 \<open>The reflexive part\<close>

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 \<open>Substitution under equivalences\<close>

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 \<Rightarrow> 'a \<Rightarrow> 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

text \<open>A rudimentary quickcheck setup\<close>

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]:
  "HOL.equal cmp1 cmp2 \ Enum.enum_all (\x. compare cmp1 x = compare cmp2 x)"
  by transfer (simp add: enum_UNIV)

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

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

definition full_exhaustive_comparator ::
  "('a comparator \ (unit \ term) \ (bool \ term list) option)
    \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
  where "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))))"

instance ..

end

subsection \<open>Fundamental comparator combinators\<close>

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

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

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 = (\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 \ 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

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.