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