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 *)
5 theory Comparator
6   imports Main
7 begin
9 section \<open>Comparators on linear quasi-orders\<close>
11 datatype comp = Less | Equiv | Greater
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
21 text \<open>Dual properties\<close>
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
27 lemma less_iff_sym_greater:
28   "cmp b a = Less \<longleftrightarrow> cmp a b = Greater"
31 text \<open>The equivalence part\<close>
33 lemma sym:
34   "cmp b a = Equiv \<longleftrightarrow> cmp a b = Equiv"
35   by (metis (full_types) comp.exhaust greater_iff_sym_less)
37 lemma reflp:
38   "reflp (\<lambda>a b. cmp a b = Equiv)"
39   by (rule reflpI) simp
41 lemma symp:
42   "symp (\<lambda>a b. cmp a b = Equiv)"
43   by (rule sympI) (simp add: sym)
45 lemma transp:
46   "transp (\<lambda>a b. cmp a b = Equiv)"
47   by (rule transpI) (fact trans_equiv)
49 lemma equivp:
50   "equivp (\<lambda>a b. cmp a b = Equiv)"
51   using reflp symp transp by (rule equivpI)
53 text \<open>The strict part\<close>
55 lemma irreflp_less:
56   "irreflp (\<lambda>a b. cmp a b = Less)"
57   by (rule irreflpI) simp
59 lemma irreflp_greater:
60   "irreflp (\<lambda>a b. cmp a b = Greater)"
61   by (rule irreflpI) simp
63 lemma asym_less:
64   "cmp b a \<noteq> Less" if "cmp a b = Less"
65   using that greater_iff_sym_less by force
67 lemma asym_greater:
68   "cmp b a \<noteq> Greater" if "cmp a b = Greater"
69   using that greater_iff_sym_less by force
71 lemma asymp_less:
72   "asymp (\<lambda>a b. cmp a b = Less)"
73   using irreflp_less by (auto intro: asympI dest: asym_less)
75 lemma asymp_greater:
76   "asymp (\<lambda>a b. cmp a b = Greater)"
77   using irreflp_greater by (auto intro!: asympI dest: asym_greater)
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)
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)
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)
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)
97 lemma transp_less:
98   "transp (\<lambda>a b. cmp a b = Less)"
99   by (rule transpI) (fact trans_less)
101 lemma transp_greater:
102   "transp (\<lambda>a b. cmp a b = Greater)"
103   by (rule transpI) (fact trans_greater)
105 text \<open>The reflexive part\<close>
107 lemma reflp_not_less:
108   "reflp (\<lambda>a b. cmp a b \<noteq> Less)"
109   by (rule reflpI) simp
111 lemma reflp_not_greater:
112   "reflp (\<lambda>a b. cmp a b \<noteq> Greater)"
113   by (rule reflpI) simp
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
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
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)
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
131 lemma transp_not_less:
132   "transp (\<lambda>a b. cmp a b \<noteq> Less)"
133   by (rule transpI) (fact trans_not_less)
135 lemma transp_not_greater:
136   "transp (\<lambda>a b. cmp a b \<noteq> Greater)"
137   by (rule transpI) (fact trans_not_greater)
139 text \<open>Substitution under equivalences\<close>
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"
146   with that show ?thesis
147     by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater)
148 qed
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"
155   with that show ?thesis
156     by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv)
157 qed
159 end
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
170 setup_lifting type_definition_comparator
172 global_interpretation compare: comparator "compare cmp"
173   using compare [of cmp] by simp
175 lift_definition flat :: "'a comparator"
176   is "\<lambda>_ _. Equiv" by standard simp_all
178 instantiation comparator :: (linorder) default
179 begin
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)
185 instance ..
187 end
189 text \<open>A rudimentary quickcheck setup\<close>
191 instantiation comparator :: (enum) equal
192 begin
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" .
197 instance
198   by (standard; transfer) (auto simp add: enum_UNIV)
200 end
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)
206 lemma [code nbe]:
207   "HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True"
208   by (fact equal_refl)
210 instantiation comparator :: ("{linorder, typerep}") full_exhaustive
211 begin
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))))"
221 instance ..
223 end
225 text \<open>Fundamental comparator combinators\<close>
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
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
247 end