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