src/HOL/Library/Comparator.thy
author haftmann
Fri Oct 26 08:20:45 2018 +0000 (10 months ago)
changeset 69194 6d514e128a85
parent 69184 91fd09f2b86e
child 69246 c1fe9dcc274a
permissions -rw-r--r--
dedicated theory for sorting algorithms
     1 (*  Title:      HOL/Library/Comparator.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 theory Comparator
     6   imports Main
     7 begin
     8 
     9 section \<open>Comparators on linear quasi-orders\<close>
    10 
    11 datatype comp = Less | Equiv | Greater
    12 
    13 locale comparator =
    14   fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
    15   assumes refl [simp]: "\<And>a. cmp a a = Equiv"
    16     and trans_equiv: "\<And>a b c. cmp a b = Equiv \<Longrightarrow> cmp b c = Equiv \<Longrightarrow> cmp a c = Equiv"
    17   assumes trans_less: "cmp a b = Less \<Longrightarrow> cmp b c = Less \<Longrightarrow> cmp a c = Less"
    18     and greater_iff_sym_less: "\<And>b a. cmp b a = Greater \<longleftrightarrow> cmp a b = Less"
    19 begin
    20 
    21 text \<open>Dual properties\<close>
    22 
    23 lemma trans_greater:
    24   "cmp a c = Greater" if "cmp a b = Greater" "cmp b c = Greater"
    25   using that greater_iff_sym_less trans_less by blast
    26 
    27 lemma less_iff_sym_greater:
    28   "cmp b a = Less \<longleftrightarrow> cmp a b = Greater"
    29   by (simp add: greater_iff_sym_less)
    30 
    31 text \<open>The equivalence part\<close>
    32 
    33 lemma sym:
    34   "cmp b a = Equiv \<longleftrightarrow> cmp a b = Equiv"
    35   by (metis (full_types) comp.exhaust greater_iff_sym_less)
    36 
    37 lemma reflp:
    38   "reflp (\<lambda>a b. cmp a b = Equiv)"
    39   by (rule reflpI) simp
    40 
    41 lemma symp:
    42   "symp (\<lambda>a b. cmp a b = Equiv)"
    43   by (rule sympI) (simp add: sym)
    44 
    45 lemma transp:
    46   "transp (\<lambda>a b. cmp a b = Equiv)"
    47   by (rule transpI) (fact trans_equiv)
    48 
    49 lemma equivp:
    50   "equivp (\<lambda>a b. cmp a b = Equiv)"
    51   using reflp symp transp by (rule equivpI)
    52 
    53 text \<open>The strict part\<close>
    54 
    55 lemma irreflp_less:
    56   "irreflp (\<lambda>a b. cmp a b = Less)"
    57   by (rule irreflpI) simp
    58 
    59 lemma irreflp_greater:
    60   "irreflp (\<lambda>a b. cmp a b = Greater)"
    61   by (rule irreflpI) simp
    62 
    63 lemma asym_less:
    64   "cmp b a \<noteq> Less" if "cmp a b = Less"
    65   using that greater_iff_sym_less by force
    66 
    67 lemma asym_greater:
    68   "cmp b a \<noteq> Greater" if "cmp a b = Greater"
    69   using that greater_iff_sym_less by force
    70 
    71 lemma asymp_less:
    72   "asymp (\<lambda>a b. cmp a b = Less)"
    73   using irreflp_less by (auto intro: asympI dest: asym_less)
    74 
    75 lemma asymp_greater:
    76   "asymp (\<lambda>a b. cmp a b = Greater)"
    77   using irreflp_greater by (auto intro!: asympI dest: asym_greater)
    78 
    79 lemma transp_less:
    80   "transp (\<lambda>a b. cmp a b = Less)"
    81   by (rule transpI) (fact trans_less)
    82 
    83 lemma transp_greater:
    84   "transp (\<lambda>a b. cmp a b = Greater)"
    85   by (rule transpI) (fact trans_greater)
    86 
    87 text \<open>The reflexive part\<close>
    88 
    89 lemma reflp_not_less:
    90   "reflp (\<lambda>a b. cmp a b \<noteq> Less)"
    91   by (rule reflpI) simp
    92 
    93 lemma reflp_not_greater:
    94   "reflp (\<lambda>a b. cmp a b \<noteq> Greater)"
    95   by (rule reflpI) simp
    96 
    97 lemma quasisym_not_less:
    98   "cmp a b = Equiv" if "cmp a b \<noteq> Less" and "cmp b a \<noteq> Less"
    99   using that comp.exhaust greater_iff_sym_less by auto
   100 
   101 lemma quasisym_not_greater:
   102   "cmp a b = Equiv" if "cmp a b \<noteq> Greater" and "cmp b a \<noteq> Greater"
   103   using that comp.exhaust greater_iff_sym_less by auto
   104 
   105 lemma trans_not_less:
   106   "cmp a c \<noteq> Less" if "cmp a b \<noteq> Less" "cmp b c \<noteq> Less"
   107   using that by (metis comp.exhaust greater_iff_sym_less trans_equiv trans_less)
   108 
   109 lemma trans_not_greater:
   110   "cmp a c \<noteq> Greater" if "cmp a b \<noteq> Greater" "cmp b c \<noteq> Greater"
   111   using that greater_iff_sym_less trans_not_less by blast
   112 
   113 lemma transp_not_less:
   114   "transp (\<lambda>a b. cmp a b \<noteq> Less)"
   115   by (rule transpI) (fact trans_not_less)
   116 
   117 lemma transp_not_greater:
   118   "transp (\<lambda>a b. cmp a b \<noteq> Greater)"
   119   by (rule transpI) (fact trans_not_greater)
   120 
   121 end
   122 
   123 typedef 'a comparator = "{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}"
   124   morphisms compare Abs_comparator
   125 proof -
   126   have "comparator (\<lambda>_ _. Equiv)"
   127     by standard simp_all
   128   then show ?thesis
   129     by auto
   130 qed
   131 
   132 setup_lifting type_definition_comparator
   133 
   134 global_interpretation compare: comparator "compare cmp"
   135   using compare [of cmp] by simp
   136 
   137 lift_definition flat :: "'a comparator"
   138   is "\<lambda>_ _. Equiv" by standard simp_all
   139 
   140 instantiation comparator :: (linorder) default
   141 begin
   142 
   143 lift_definition default_comparator :: "'a comparator"
   144   is "\<lambda>x y. if x < y then Less else if x > y then Greater else Equiv"
   145   by standard (auto split: if_splits)
   146 
   147 instance ..
   148 
   149 end
   150 
   151 text \<open>A rudimentary quickcheck setup\<close>
   152 
   153 instantiation comparator :: (enum) equal
   154 begin
   155 
   156 lift_definition equal_comparator :: "'a comparator \<Rightarrow> 'a comparator \<Rightarrow> bool"
   157   is "\<lambda>f g. \<forall>x \<in> set Enum.enum. f x = g x" .
   158 
   159 instance
   160   by (standard; transfer) (auto simp add: enum_UNIV)
   161 
   162 end
   163 
   164 lemma [code]:
   165   "HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)"
   166   by transfer (simp add: enum_UNIV)
   167 
   168 lemma [code nbe]:
   169   "HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True"
   170   by (fact equal_refl)
   171 
   172 instantiation comparator :: ("{linorder, typerep}") full_exhaustive
   173 begin
   174 
   175 definition full_exhaustive_comparator ::
   176   "('a comparator \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option)
   177     \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   178   where "full_exhaustive_comparator f s =
   179     Quickcheck_Exhaustive.orelse
   180       (f (flat, (\<lambda>u. Code_Evaluation.Const (STR ''Comparator.flat'') TYPEREP('a comparator))))
   181       (f (default, (\<lambda>u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))"
   182 
   183 instance ..
   184 
   185 end
   186 
   187 text \<open>Fundamental comparator combinators\<close>
   188 
   189 lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
   190   is "\<lambda>cmp a b. cmp b a"
   191 proof -
   192   fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
   193   assume "comparator cmp"
   194   then interpret comparator cmp .
   195   show "comparator (\<lambda>a b. cmp b a)"
   196     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
   197 qed
   198 
   199 lift_definition key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator"
   200   is "\<lambda>f cmp a b. cmp (f a) (f b)"
   201 proof -
   202   fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp" and f :: "'b \<Rightarrow> 'a"
   203   assume "comparator cmp"
   204   then interpret comparator cmp .
   205   show "comparator (\<lambda>a b. cmp (f a) (f b))"
   206     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
   207 qed
   208 
   209 end