src/HOL/Library/Comparator.thy
author haftmann
Sun Nov 04 15:00:30 2018 +0000 (9 months ago)
changeset 69246 c1fe9dcc274a
parent 69194 6d514e128a85
child 69251 d240598e8637
permissions -rw-r--r--
concrecte sorting algorithms beyond insertion sort
     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 trans_equiv_less:
    80   "cmp a c = Less" if "cmp a b = Equiv" and "cmp b c = Less"
    81   using that
    82   by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
    83 
    84 lemma trans_less_equiv:
    85   "cmp a c = Less" if "cmp a b = Less" and "cmp b c = Equiv"
    86   using that
    87   by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
    88 
    89 lemma trans_equiv_greater:
    90   "cmp a c = Greater" if "cmp a b = Equiv" and "cmp b c = Greater"
    91   using that by (simp add: sym [of a b] greater_iff_sym_less trans_less_equiv)
    92 
    93 lemma trans_greater_equiv:
    94   "cmp a c = Greater" if "cmp a b = Greater" and "cmp b c = Equiv"
    95   using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less)
    96 
    97 lemma transp_less:
    98   "transp (\<lambda>a b. cmp a b = Less)"
    99   by (rule transpI) (fact trans_less)
   100 
   101 lemma transp_greater:
   102   "transp (\<lambda>a b. cmp a b = Greater)"
   103   by (rule transpI) (fact trans_greater)
   104 
   105 text \<open>The reflexive part\<close>
   106 
   107 lemma reflp_not_less:
   108   "reflp (\<lambda>a b. cmp a b \<noteq> Less)"
   109   by (rule reflpI) simp
   110 
   111 lemma reflp_not_greater:
   112   "reflp (\<lambda>a b. cmp a b \<noteq> Greater)"
   113   by (rule reflpI) simp
   114 
   115 lemma quasisym_not_less:
   116   "cmp a b = Equiv" if "cmp a b \<noteq> Less" and "cmp b a \<noteq> Less"
   117   using that comp.exhaust greater_iff_sym_less by auto
   118 
   119 lemma quasisym_not_greater:
   120   "cmp a b = Equiv" if "cmp a b \<noteq> Greater" and "cmp b a \<noteq> Greater"
   121   using that comp.exhaust greater_iff_sym_less by auto
   122 
   123 lemma trans_not_less:
   124   "cmp a c \<noteq> Less" if "cmp a b \<noteq> Less" "cmp b c \<noteq> Less"
   125   using that by (metis comp.exhaust greater_iff_sym_less trans_equiv trans_less)
   126 
   127 lemma trans_not_greater:
   128   "cmp a c \<noteq> Greater" if "cmp a b \<noteq> Greater" "cmp b c \<noteq> Greater"
   129   using that greater_iff_sym_less trans_not_less by blast
   130 
   131 lemma transp_not_less:
   132   "transp (\<lambda>a b. cmp a b \<noteq> Less)"
   133   by (rule transpI) (fact trans_not_less)
   134 
   135 lemma transp_not_greater:
   136   "transp (\<lambda>a b. cmp a b \<noteq> Greater)"
   137   by (rule transpI) (fact trans_not_greater)
   138 
   139 text \<open>Substitution under equivalences\<close>
   140 
   141 lemma equiv_subst_left:
   142   "cmp z y = comp \<longleftrightarrow> cmp x y = comp" if "cmp z x = Equiv" for comp
   143 proof -
   144   from that have "cmp x z = Equiv"
   145     by (simp add: sym)
   146   with that show ?thesis
   147     by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater)
   148 qed
   149 
   150 lemma equiv_subst_right:
   151   "cmp x z = comp \<longleftrightarrow> cmp x y = comp" if "cmp z y = Equiv" for comp
   152 proof -
   153   from that have "cmp y z = Equiv"
   154     by (simp add: sym)
   155   with that show ?thesis
   156     by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv)
   157 qed
   158 
   159 end
   160 
   161 typedef 'a comparator = "{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}"
   162   morphisms compare Abs_comparator
   163 proof -
   164   have "comparator (\<lambda>_ _. Equiv)"
   165     by standard simp_all
   166   then show ?thesis
   167     by auto
   168 qed
   169 
   170 setup_lifting type_definition_comparator
   171 
   172 global_interpretation compare: comparator "compare cmp"
   173   using compare [of cmp] by simp
   174 
   175 lift_definition flat :: "'a comparator"
   176   is "\<lambda>_ _. Equiv" by standard simp_all
   177 
   178 instantiation comparator :: (linorder) default
   179 begin
   180 
   181 lift_definition default_comparator :: "'a comparator"
   182   is "\<lambda>x y. if x < y then Less else if x > y then Greater else Equiv"
   183   by standard (auto split: if_splits)
   184 
   185 instance ..
   186 
   187 end
   188 
   189 text \<open>A rudimentary quickcheck setup\<close>
   190 
   191 instantiation comparator :: (enum) equal
   192 begin
   193 
   194 lift_definition equal_comparator :: "'a comparator \<Rightarrow> 'a comparator \<Rightarrow> bool"
   195   is "\<lambda>f g. \<forall>x \<in> set Enum.enum. f x = g x" .
   196 
   197 instance
   198   by (standard; transfer) (auto simp add: enum_UNIV)
   199 
   200 end
   201 
   202 lemma [code]:
   203   "HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)"
   204   by transfer (simp add: enum_UNIV)
   205 
   206 lemma [code nbe]:
   207   "HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True"
   208   by (fact equal_refl)
   209 
   210 instantiation comparator :: ("{linorder, typerep}") full_exhaustive
   211 begin
   212 
   213 definition full_exhaustive_comparator ::
   214   "('a comparator \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option)
   215     \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   216   where "full_exhaustive_comparator f s =
   217     Quickcheck_Exhaustive.orelse
   218       (f (flat, (\<lambda>u. Code_Evaluation.Const (STR ''Comparator.flat'') TYPEREP('a comparator))))
   219       (f (default, (\<lambda>u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))"
   220 
   221 instance ..
   222 
   223 end
   224 
   225 text \<open>Fundamental comparator combinators\<close>
   226 
   227 lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
   228   is "\<lambda>cmp a b. cmp b a"
   229 proof -
   230   fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
   231   assume "comparator cmp"
   232   then interpret comparator cmp .
   233   show "comparator (\<lambda>a b. cmp b a)"
   234     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
   235 qed
   236 
   237 lift_definition key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator"
   238   is "\<lambda>f cmp a b. cmp (f a) (f b)"
   239 proof -
   240   fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp" and f :: "'b \<Rightarrow> 'a"
   241   assume "comparator cmp"
   242   then interpret comparator cmp .
   243   show "comparator (\<lambda>a b. cmp (f a) (f b))"
   244     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
   245 qed
   246 
   247 end