author  haftmann 
Fri, 22 Mar 2019 19:18:08 +0000  
changeset 69946  494934c30f38 
parent 69251  d240598e8637 
permissions  rwrr 
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 quasiorders\<close> 

10 

69251  11 
subsection \<open>Basic properties\<close> 
12 

69184  13 
datatype comp = Less  Equiv  Greater 
14 

15 
locale comparator = 

16 
fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp" 

17 
assumes refl [simp]: "\<And>a. cmp a a = Equiv" 

18 
and trans_equiv: "\<And>a b c. cmp a b = Equiv \<Longrightarrow> cmp b c = Equiv \<Longrightarrow> cmp a c = Equiv" 

19 
assumes trans_less: "cmp a b = Less \<Longrightarrow> cmp b c = Less \<Longrightarrow> cmp a c = Less" 

20 
and greater_iff_sym_less: "\<And>b a. cmp b a = Greater \<longleftrightarrow> cmp a b = Less" 

21 
begin 

22 

23 
text \<open>Dual properties\<close> 

24 

25 
lemma trans_greater: 

26 
"cmp a c = Greater" if "cmp a b = Greater" "cmp b c = Greater" 

27 
using that greater_iff_sym_less trans_less by blast 

28 

29 
lemma less_iff_sym_greater: 

30 
"cmp b a = Less \<longleftrightarrow> cmp a b = Greater" 

31 
by (simp add: greater_iff_sym_less) 

32 

33 
text \<open>The equivalence part\<close> 

34 

35 
lemma sym: 

36 
"cmp b a = Equiv \<longleftrightarrow> cmp a b = Equiv" 

37 
by (metis (full_types) comp.exhaust greater_iff_sym_less) 

38 

39 
lemma reflp: 

40 
"reflp (\<lambda>a b. cmp a b = Equiv)" 

41 
by (rule reflpI) simp 

42 

43 
lemma symp: 

44 
"symp (\<lambda>a b. cmp a b = Equiv)" 

45 
by (rule sympI) (simp add: sym) 

46 

47 
lemma transp: 

48 
"transp (\<lambda>a b. cmp a b = Equiv)" 

49 
by (rule transpI) (fact trans_equiv) 

50 

51 
lemma equivp: 

52 
"equivp (\<lambda>a b. cmp a b = Equiv)" 

53 
using reflp symp transp by (rule equivpI) 

54 

55 
text \<open>The strict part\<close> 

56 

57 
lemma irreflp_less: 

58 
"irreflp (\<lambda>a b. cmp a b = Less)" 

59 
by (rule irreflpI) simp 

60 

61 
lemma irreflp_greater: 

62 
"irreflp (\<lambda>a b. cmp a b = Greater)" 

63 
by (rule irreflpI) simp 

64 

65 
lemma asym_less: 

66 
"cmp b a \<noteq> Less" if "cmp a b = Less" 

67 
using that greater_iff_sym_less by force 

68 

69 
lemma asym_greater: 

70 
"cmp b a \<noteq> Greater" if "cmp a b = Greater" 

71 
using that greater_iff_sym_less by force 

72 

73 
lemma asymp_less: 

74 
"asymp (\<lambda>a b. cmp a b = Less)" 

75 
using irreflp_less by (auto intro: asympI dest: asym_less) 

76 

77 
lemma asymp_greater: 

78 
"asymp (\<lambda>a b. cmp a b = Greater)" 

79 
using irreflp_greater by (auto intro!: asympI dest: asym_greater) 

80 

69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

81 
lemma trans_equiv_less: 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

82 
"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

83 
using that 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

84 
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

85 

c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

86 
lemma trans_less_equiv: 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

87 
"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

88 
using that 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

89 
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

90 

c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

91 
lemma trans_equiv_greater: 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

92 
"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

93 
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

94 

c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

95 
lemma trans_greater_equiv: 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

96 
"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

97 
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

98 

69184  99 
lemma transp_less: 
100 
"transp (\<lambda>a b. cmp a b = Less)" 

101 
by (rule transpI) (fact trans_less) 

102 

103 
lemma transp_greater: 

104 
"transp (\<lambda>a b. cmp a b = Greater)" 

105 
by (rule transpI) (fact trans_greater) 

106 

107 
text \<open>The reflexive part\<close> 

108 

109 
lemma reflp_not_less: 

110 
"reflp (\<lambda>a b. cmp a b \<noteq> Less)" 

111 
by (rule reflpI) simp 

112 

113 
lemma reflp_not_greater: 

114 
"reflp (\<lambda>a b. cmp a b \<noteq> Greater)" 

115 
by (rule reflpI) simp 

116 

117 
lemma quasisym_not_less: 

118 
"cmp a b = Equiv" if "cmp a b \<noteq> Less" and "cmp b a \<noteq> Less" 

119 
using that comp.exhaust greater_iff_sym_less by auto 

120 

121 
lemma quasisym_not_greater: 

122 
"cmp a b = Equiv" if "cmp a b \<noteq> Greater" and "cmp b a \<noteq> Greater" 

123 
using that comp.exhaust greater_iff_sym_less by auto 

124 

125 
lemma trans_not_less: 

126 
"cmp a c \<noteq> Less" if "cmp a b \<noteq> Less" "cmp b c \<noteq> Less" 

127 
using that by (metis comp.exhaust greater_iff_sym_less trans_equiv trans_less) 

128 

129 
lemma trans_not_greater: 

130 
"cmp a c \<noteq> Greater" if "cmp a b \<noteq> Greater" "cmp b c \<noteq> Greater" 

131 
using that greater_iff_sym_less trans_not_less by blast 

132 

133 
lemma transp_not_less: 

134 
"transp (\<lambda>a b. cmp a b \<noteq> Less)" 

135 
by (rule transpI) (fact trans_not_less) 

136 

137 
lemma transp_not_greater: 

138 
"transp (\<lambda>a b. cmp a b \<noteq> Greater)" 

139 
by (rule transpI) (fact trans_not_greater) 

140 

69246
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

141 
text \<open>Substitution under equivalences\<close> 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

142 

c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

143 
lemma equiv_subst_left: 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

144 
"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

145 
proof  
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

146 
from that have "cmp x z = Equiv" 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

147 
by (simp add: sym) 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

148 
with that show ?thesis 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

149 
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

150 
qed 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

151 

c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

152 
lemma equiv_subst_right: 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

153 
"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

154 
proof  
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

155 
from that have "cmp y z = Equiv" 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

156 
by (simp add: sym) 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

157 
with that show ?thesis 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

158 
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

159 
qed 
c1fe9dcc274a
concrecte sorting algorithms beyond insertion sort
haftmann
parents:
69194
diff
changeset

160 

69184  161 
end 
162 

163 
typedef 'a comparator = "{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}" 

164 
morphisms compare Abs_comparator 

165 
proof  

166 
have "comparator (\<lambda>_ _. Equiv)" 

167 
by standard simp_all 

168 
then show ?thesis 

169 
by auto 

170 
qed 

171 

172 
setup_lifting type_definition_comparator 

173 

174 
global_interpretation compare: comparator "compare cmp" 

175 
using compare [of cmp] by simp 

176 

177 
lift_definition flat :: "'a comparator" 

178 
is "\<lambda>_ _. Equiv" by standard simp_all 

179 

180 
instantiation comparator :: (linorder) default 

181 
begin 

182 

183 
lift_definition default_comparator :: "'a comparator" 

184 
is "\<lambda>x y. if x < y then Less else if x > y then Greater else Equiv" 

185 
by standard (auto split: if_splits) 

186 

187 
instance .. 

188 

189 
end 

190 

191 
text \<open>A rudimentary quickcheck setup\<close> 

192 

193 
instantiation comparator :: (enum) equal 

194 
begin 

195 

196 
lift_definition equal_comparator :: "'a comparator \<Rightarrow> 'a comparator \<Rightarrow> bool" 

197 
is "\<lambda>f g. \<forall>x \<in> set Enum.enum. f x = g x" . 

198 

199 
instance 

200 
by (standard; transfer) (auto simp add: enum_UNIV) 

201 

202 
end 

203 

204 
lemma [code]: 

205 
"HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)" 

206 
by transfer (simp add: enum_UNIV) 

207 

208 
lemma [code nbe]: 

209 
"HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True" 

210 
by (fact equal_refl) 

211 

212 
instantiation comparator :: ("{linorder, typerep}") full_exhaustive 

213 
begin 

214 

215 
definition full_exhaustive_comparator :: 

216 
"('a comparator \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) 

217 
\<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" 

218 
where "full_exhaustive_comparator f s = 

219 
Quickcheck_Exhaustive.orelse 

220 
(f (flat, (\<lambda>u. Code_Evaluation.Const (STR ''Comparator.flat'') TYPEREP('a comparator)))) 

221 
(f (default, (\<lambda>u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))" 

222 

223 
instance .. 

224 

225 
end 

226 

69251  227 

228 
subsection \<open>Fundamental comparator combinators\<close> 

69194  229 

69184  230 
lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator" 
231 
is "\<lambda>cmp a b. cmp b a" 

232 
proof  

233 
fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp" 

234 
assume "comparator cmp" 

235 
then interpret comparator cmp . 

236 
show "comparator (\<lambda>a b. cmp b a)" 

237 
by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less) 

238 
qed 

239 

240 
lift_definition key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator" 

241 
is "\<lambda>f cmp a b. cmp (f a) (f b)" 

242 
proof  

243 
fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp" and f :: "'b \<Rightarrow> 'a" 

244 
assume "comparator cmp" 

245 
then interpret comparator cmp . 

246 
show "comparator (\<lambda>a b. cmp (f a) (f b))" 

247 
by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less) 

248 
qed 

249 

69251  250 

251 
subsection \<open>Direct implementations for linear orders on selected types\<close> 

252 

253 
definition comparator_bool :: "bool comparator" 

254 
where [simp, code_abbrev]: "comparator_bool = default" 

255 

256 
lemma compare_comparator_bool [code abstract]: 

257 
"compare comparator_bool = (\<lambda>p q. 

258 
if p then if q then Equiv else Greater 

259 
else if q then Less else Equiv)" 

260 
by (auto simp add: fun_eq_iff) (transfer; simp)+ 

261 

262 
definition raw_comparator_nat :: "nat \<Rightarrow> nat \<Rightarrow> comp" 

263 
where [simp]: "raw_comparator_nat = compare default" 

264 

265 
lemma default_comparator_nat [simp, code]: 

266 
"raw_comparator_nat (0::nat) 0 = Equiv" 

267 
"raw_comparator_nat (Suc m) 0 = Greater" 

268 
"raw_comparator_nat 0 (Suc n) = Less" 

269 
"raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n" 

270 
by (transfer; simp)+ 

271 

272 
definition comparator_nat :: "nat comparator" 

273 
where [simp, code_abbrev]: "comparator_nat = default" 

274 

275 
lemma compare_comparator_nat [code abstract]: 

276 
"compare comparator_nat = raw_comparator_nat" 

277 
by simp 

278 

279 
definition comparator_linordered_group :: "'a::linordered_ab_group_add comparator" 

280 
where [simp, code_abbrev]: "comparator_linordered_group = default" 

281 

282 
lemma comparator_linordered_group [code abstract]: 

283 
"compare comparator_linordered_group = (\<lambda>a b. 

284 
let c = a  b in if c < 0 then Less 

285 
else if c = 0 then Equiv else Greater)" 

286 
proof (rule ext)+ 

287 
fix a b :: 'a 

288 
show "compare comparator_linordered_group a b = 

289 
(let c = a  b in if c < 0 then Less 

290 
else if c = 0 then Equiv else Greater)" 

291 
by (simp add: Let_def not_less) (transfer; auto) 

292 
qed 

293 

69184  294 
end 