src/HOL/Library/Comparator.thy
 author haftmann Thu Oct 25 12:42:17 2018 +0000 (9 months ago) changeset 69184 91fd09f2b86e child 69194 6d514e128a85 permissions -rw-r--r--
executable comparators apt for sorting
 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@69184 ` 187` ```lift_definition reversed :: "'a comparator \ 'a comparator" ``` haftmann@69184 ` 188` ``` is "\cmp a b. cmp b a" ``` haftmann@69184 ` 189` ```proof - ``` haftmann@69184 ` 190` ``` fix cmp :: "'a \ 'a \ comp" ``` haftmann@69184 ` 191` ``` assume "comparator cmp" ``` haftmann@69184 ` 192` ``` then interpret comparator cmp . ``` haftmann@69184 ` 193` ``` show "comparator (\a b. cmp b a)" ``` haftmann@69184 ` 194` ``` by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less) ``` haftmann@69184 ` 195` ```qed ``` haftmann@69184 ` 196` haftmann@69184 ` 197` ```lift_definition key :: "('b \ 'a) \ 'a comparator \ 'b comparator" ``` haftmann@69184 ` 198` ``` is "\f cmp a b. cmp (f a) (f b)" ``` haftmann@69184 ` 199` ```proof - ``` haftmann@69184 ` 200` ``` fix cmp :: "'a \ 'a \ comp" and f :: "'b \ 'a" ``` haftmann@69184 ` 201` ``` assume "comparator cmp" ``` haftmann@69184 ` 202` ``` then interpret comparator cmp . ``` haftmann@69184 ` 203` ``` show "comparator (\a b. cmp (f a) (f b))" ``` haftmann@69184 ` 204` ``` by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less) ``` haftmann@69184 ` 205` ```qed ``` haftmann@69184 ` 206` haftmann@69184 ` 207` ```end ```