author | haftmann |
Sun, 04 Nov 2018 15:00:30 +0000 | |
changeset 69246 | c1fe9dcc274a |
parent 69194 | 6d514e128a85 |
child 69251 | d240598e8637 |
permissions | -rw-r--r-- |
69184 | 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 |
||
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
79 |
lemma trans_equiv_less: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
80 |
"cmp a c = Less" if "cmp a b = Equiv" and "cmp b c = Less" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
81 |
using that |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
82 |
by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
83 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
84 |
lemma trans_less_equiv: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
85 |
"cmp a c = Less" if "cmp a b = Less" and "cmp b c = Equiv" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
86 |
using that |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
87 |
by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
88 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
89 |
lemma trans_equiv_greater: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
90 |
"cmp a c = Greater" if "cmp a b = Equiv" and "cmp b c = Greater" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
91 |
using that by (simp add: sym [of a b] greater_iff_sym_less trans_less_equiv) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
92 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
93 |
lemma trans_greater_equiv: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
94 |
"cmp a c = Greater" if "cmp a b = Greater" and "cmp b c = Equiv" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
95 |
using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
96 |
|
69184 | 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 |
||
69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
139 |
text \<open>Substitution under equivalences\<close> |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
140 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
141 |
lemma equiv_subst_left: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
142 |
"cmp z y = comp \<longleftrightarrow> cmp x y = comp" if "cmp z x = Equiv" for comp |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
143 |
proof - |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
144 |
from that have "cmp x z = Equiv" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
145 |
by (simp add: sym) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
146 |
with that show ?thesis |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
147 |
by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
148 |
qed |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
149 |
|
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
150 |
lemma equiv_subst_right: |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
151 |
"cmp x z = comp \<longleftrightarrow> cmp x y = comp" if "cmp z y = Equiv" for comp |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
152 |
proof - |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
153 |
from that have "cmp y z = Equiv" |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
154 |
by (simp add: sym) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
155 |
with that show ?thesis |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
156 |
by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv) |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
157 |
qed |
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset
|
158 |
|
69184 | 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 |
||
69194 | 225 |
text \<open>Fundamental comparator combinators\<close> |
226 |
||
69184 | 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 |