src/HOL/Library/Comparator.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69251 d240598e8637
permissions -rw-r--r--
improved code equations taken over from AFP
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 \<open>Comparators on linear quasi-orders\<close>
haftmann@69184
    10
haftmann@69251
    11
subsection \<open>Basic properties\<close>
haftmann@69251
    12
haftmann@69184
    13
datatype comp = Less | Equiv | Greater
haftmann@69184
    14
haftmann@69184
    15
locale comparator =
haftmann@69184
    16
  fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
haftmann@69184
    17
  assumes refl [simp]: "\<And>a. cmp a a = Equiv"
haftmann@69184
    18
    and trans_equiv: "\<And>a b c. cmp a b = Equiv \<Longrightarrow> cmp b c = Equiv \<Longrightarrow> cmp a c = Equiv"
haftmann@69184
    19
  assumes trans_less: "cmp a b = Less \<Longrightarrow> cmp b c = Less \<Longrightarrow> cmp a c = Less"
haftmann@69184
    20
    and greater_iff_sym_less: "\<And>b a. cmp b a = Greater \<longleftrightarrow> cmp a b = Less"
haftmann@69184
    21
begin
haftmann@69184
    22
haftmann@69184
    23
text \<open>Dual properties\<close>
haftmann@69184
    24
haftmann@69184
    25
lemma trans_greater:
haftmann@69184
    26
  "cmp a c = Greater" if "cmp a b = Greater" "cmp b c = Greater"
haftmann@69184
    27
  using that greater_iff_sym_less trans_less by blast
haftmann@69184
    28
haftmann@69184
    29
lemma less_iff_sym_greater:
haftmann@69184
    30
  "cmp b a = Less \<longleftrightarrow> cmp a b = Greater"
haftmann@69184
    31
  by (simp add: greater_iff_sym_less)
haftmann@69184
    32
haftmann@69184
    33
text \<open>The equivalence part\<close>
haftmann@69184
    34
haftmann@69184
    35
lemma sym:
haftmann@69184
    36
  "cmp b a = Equiv \<longleftrightarrow> cmp a b = Equiv"
haftmann@69184
    37
  by (metis (full_types) comp.exhaust greater_iff_sym_less)
haftmann@69184
    38
haftmann@69184
    39
lemma reflp:
haftmann@69184
    40
  "reflp (\<lambda>a b. cmp a b = Equiv)"
haftmann@69184
    41
  by (rule reflpI) simp
haftmann@69184
    42
haftmann@69184
    43
lemma symp:
haftmann@69184
    44
  "symp (\<lambda>a b. cmp a b = Equiv)"
haftmann@69184
    45
  by (rule sympI) (simp add: sym)
haftmann@69184
    46
haftmann@69184
    47
lemma transp:
haftmann@69184
    48
  "transp (\<lambda>a b. cmp a b = Equiv)"
haftmann@69184
    49
  by (rule transpI) (fact trans_equiv)
haftmann@69184
    50
haftmann@69184
    51
lemma equivp:
haftmann@69184
    52
  "equivp (\<lambda>a b. cmp a b = Equiv)"
haftmann@69184
    53
  using reflp symp transp by (rule equivpI)
haftmann@69184
    54
haftmann@69184
    55
text \<open>The strict part\<close>
haftmann@69184
    56
haftmann@69184
    57
lemma irreflp_less:
haftmann@69184
    58
  "irreflp (\<lambda>a b. cmp a b = Less)"
haftmann@69184
    59
  by (rule irreflpI) simp
haftmann@69184
    60
haftmann@69184
    61
lemma irreflp_greater:
haftmann@69184
    62
  "irreflp (\<lambda>a b. cmp a b = Greater)"
haftmann@69184
    63
  by (rule irreflpI) simp
haftmann@69184
    64
haftmann@69184
    65
lemma asym_less:
haftmann@69184
    66
  "cmp b a \<noteq> Less" if "cmp a b = Less"
haftmann@69184
    67
  using that greater_iff_sym_less by force
haftmann@69184
    68
haftmann@69184
    69
lemma asym_greater:
haftmann@69184
    70
  "cmp b a \<noteq> Greater" if "cmp a b = Greater"
haftmann@69184
    71
  using that greater_iff_sym_less by force
haftmann@69184
    72
haftmann@69184
    73
lemma asymp_less:
haftmann@69184
    74
  "asymp (\<lambda>a b. cmp a b = Less)"
haftmann@69184
    75
  using irreflp_less by (auto intro: asympI dest: asym_less)
haftmann@69184
    76
haftmann@69184
    77
lemma asymp_greater:
haftmann@69184
    78
  "asymp (\<lambda>a b. cmp a b = Greater)"
haftmann@69184
    79
  using irreflp_greater by (auto intro!: asympI dest: asym_greater)
haftmann@69184
    80
haftmann@69246
    81
lemma trans_equiv_less:
haftmann@69246
    82
  "cmp a c = Less" if "cmp a b = Equiv" and "cmp b c = Less"
haftmann@69246
    83
  using that
haftmann@69246
    84
  by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
haftmann@69246
    85
haftmann@69246
    86
lemma trans_less_equiv:
haftmann@69246
    87
  "cmp a c = Less" if "cmp a b = Less" and "cmp b c = Equiv"
haftmann@69246
    88
  using that
haftmann@69246
    89
  by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
haftmann@69246
    90
haftmann@69246
    91
lemma trans_equiv_greater:
haftmann@69246
    92
  "cmp a c = Greater" if "cmp a b = Equiv" and "cmp b c = Greater"
haftmann@69246
    93
  using that by (simp add: sym [of a b] greater_iff_sym_less trans_less_equiv)
haftmann@69246
    94
haftmann@69246
    95
lemma trans_greater_equiv:
haftmann@69246
    96
  "cmp a c = Greater" if "cmp a b = Greater" and "cmp b c = Equiv"
haftmann@69246
    97
  using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less)
haftmann@69246
    98
haftmann@69184
    99
lemma transp_less:
haftmann@69184
   100
  "transp (\<lambda>a b. cmp a b = Less)"
haftmann@69184
   101
  by (rule transpI) (fact trans_less)
haftmann@69184
   102
haftmann@69184
   103
lemma transp_greater:
haftmann@69184
   104
  "transp (\<lambda>a b. cmp a b = Greater)"
haftmann@69184
   105
  by (rule transpI) (fact trans_greater)
haftmann@69184
   106
haftmann@69184
   107
text \<open>The reflexive part\<close>
haftmann@69184
   108
haftmann@69184
   109
lemma reflp_not_less:
haftmann@69184
   110
  "reflp (\<lambda>a b. cmp a b \<noteq> Less)"
haftmann@69184
   111
  by (rule reflpI) simp
haftmann@69184
   112
haftmann@69184
   113
lemma reflp_not_greater:
haftmann@69184
   114
  "reflp (\<lambda>a b. cmp a b \<noteq> Greater)"
haftmann@69184
   115
  by (rule reflpI) simp
haftmann@69184
   116
haftmann@69184
   117
lemma quasisym_not_less:
haftmann@69184
   118
  "cmp a b = Equiv" if "cmp a b \<noteq> Less" and "cmp b a \<noteq> Less"
haftmann@69184
   119
  using that comp.exhaust greater_iff_sym_less by auto
haftmann@69184
   120
haftmann@69184
   121
lemma quasisym_not_greater:
haftmann@69184
   122
  "cmp a b = Equiv" if "cmp a b \<noteq> Greater" and "cmp b a \<noteq> Greater"
haftmann@69184
   123
  using that comp.exhaust greater_iff_sym_less by auto
haftmann@69184
   124
haftmann@69184
   125
lemma trans_not_less:
haftmann@69184
   126
  "cmp a c \<noteq> Less" if "cmp a b \<noteq> Less" "cmp b c \<noteq> Less"
haftmann@69184
   127
  using that by (metis comp.exhaust greater_iff_sym_less trans_equiv trans_less)
haftmann@69184
   128
haftmann@69184
   129
lemma trans_not_greater:
haftmann@69184
   130
  "cmp a c \<noteq> Greater" if "cmp a b \<noteq> Greater" "cmp b c \<noteq> Greater"
haftmann@69184
   131
  using that greater_iff_sym_less trans_not_less by blast
haftmann@69184
   132
haftmann@69184
   133
lemma transp_not_less:
haftmann@69184
   134
  "transp (\<lambda>a b. cmp a b \<noteq> Less)"
haftmann@69184
   135
  by (rule transpI) (fact trans_not_less)
haftmann@69184
   136
haftmann@69184
   137
lemma transp_not_greater:
haftmann@69184
   138
  "transp (\<lambda>a b. cmp a b \<noteq> Greater)"
haftmann@69184
   139
  by (rule transpI) (fact trans_not_greater)
haftmann@69184
   140
haftmann@69246
   141
text \<open>Substitution under equivalences\<close>
haftmann@69246
   142
haftmann@69246
   143
lemma equiv_subst_left:
haftmann@69246
   144
  "cmp z y = comp \<longleftrightarrow> cmp x y = comp" if "cmp z x = Equiv" for comp
haftmann@69246
   145
proof -
haftmann@69246
   146
  from that have "cmp x z = Equiv"
haftmann@69246
   147
    by (simp add: sym)
haftmann@69246
   148
  with that show ?thesis
haftmann@69246
   149
    by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater)
haftmann@69246
   150
qed
haftmann@69246
   151
haftmann@69246
   152
lemma equiv_subst_right:
haftmann@69246
   153
  "cmp x z = comp \<longleftrightarrow> cmp x y = comp" if "cmp z y = Equiv" for comp
haftmann@69246
   154
proof -
haftmann@69246
   155
  from that have "cmp y z = Equiv"
haftmann@69246
   156
    by (simp add: sym)
haftmann@69246
   157
  with that show ?thesis
haftmann@69246
   158
    by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv)
haftmann@69246
   159
qed
haftmann@69246
   160
haftmann@69184
   161
end
haftmann@69184
   162
haftmann@69184
   163
typedef 'a comparator = "{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}"
haftmann@69184
   164
  morphisms compare Abs_comparator
haftmann@69184
   165
proof -
haftmann@69184
   166
  have "comparator (\<lambda>_ _. Equiv)"
haftmann@69184
   167
    by standard simp_all
haftmann@69184
   168
  then show ?thesis
haftmann@69184
   169
    by auto
haftmann@69184
   170
qed
haftmann@69184
   171
haftmann@69184
   172
setup_lifting type_definition_comparator
haftmann@69184
   173
haftmann@69184
   174
global_interpretation compare: comparator "compare cmp"
haftmann@69184
   175
  using compare [of cmp] by simp
haftmann@69184
   176
haftmann@69184
   177
lift_definition flat :: "'a comparator"
haftmann@69184
   178
  is "\<lambda>_ _. Equiv" by standard simp_all
haftmann@69184
   179
haftmann@69184
   180
instantiation comparator :: (linorder) default
haftmann@69184
   181
begin
haftmann@69184
   182
haftmann@69184
   183
lift_definition default_comparator :: "'a comparator"
haftmann@69184
   184
  is "\<lambda>x y. if x < y then Less else if x > y then Greater else Equiv"
haftmann@69184
   185
  by standard (auto split: if_splits)
haftmann@69184
   186
haftmann@69184
   187
instance ..
haftmann@69184
   188
haftmann@69184
   189
end
haftmann@69184
   190
haftmann@69184
   191
text \<open>A rudimentary quickcheck setup\<close>
haftmann@69184
   192
haftmann@69184
   193
instantiation comparator :: (enum) equal
haftmann@69184
   194
begin
haftmann@69184
   195
haftmann@69184
   196
lift_definition equal_comparator :: "'a comparator \<Rightarrow> 'a comparator \<Rightarrow> bool"
haftmann@69184
   197
  is "\<lambda>f g. \<forall>x \<in> set Enum.enum. f x = g x" .
haftmann@69184
   198
haftmann@69184
   199
instance
haftmann@69184
   200
  by (standard; transfer) (auto simp add: enum_UNIV)
haftmann@69184
   201
haftmann@69184
   202
end
haftmann@69184
   203
haftmann@69184
   204
lemma [code]:
haftmann@69184
   205
  "HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)"
haftmann@69184
   206
  by transfer (simp add: enum_UNIV)
haftmann@69184
   207
haftmann@69184
   208
lemma [code nbe]:
haftmann@69184
   209
  "HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True"
haftmann@69184
   210
  by (fact equal_refl)
haftmann@69184
   211
haftmann@69184
   212
instantiation comparator :: ("{linorder, typerep}") full_exhaustive
haftmann@69184
   213
begin
haftmann@69184
   214
haftmann@69184
   215
definition full_exhaustive_comparator ::
haftmann@69184
   216
  "('a comparator \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option)
haftmann@69184
   217
    \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
haftmann@69184
   218
  where "full_exhaustive_comparator f s =
haftmann@69184
   219
    Quickcheck_Exhaustive.orelse
haftmann@69184
   220
      (f (flat, (\<lambda>u. Code_Evaluation.Const (STR ''Comparator.flat'') TYPEREP('a comparator))))
haftmann@69184
   221
      (f (default, (\<lambda>u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))"
haftmann@69184
   222
haftmann@69184
   223
instance ..
haftmann@69184
   224
haftmann@69184
   225
end
haftmann@69184
   226
haftmann@69251
   227
haftmann@69251
   228
subsection \<open>Fundamental comparator combinators\<close>
haftmann@69194
   229
haftmann@69184
   230
lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
haftmann@69184
   231
  is "\<lambda>cmp a b. cmp b a"
haftmann@69184
   232
proof -
haftmann@69184
   233
  fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
haftmann@69184
   234
  assume "comparator cmp"
haftmann@69184
   235
  then interpret comparator cmp .
haftmann@69184
   236
  show "comparator (\<lambda>a b. cmp b a)"
haftmann@69184
   237
    by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
haftmann@69184
   238
qed
haftmann@69184
   239
haftmann@69184
   240
lift_definition key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator"
haftmann@69184
   241
  is "\<lambda>f cmp a b. cmp (f a) (f b)"
haftmann@69184
   242
proof -
haftmann@69184
   243
  fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp" and f :: "'b \<Rightarrow> 'a"
haftmann@69184
   244
  assume "comparator cmp"
haftmann@69184
   245
  then interpret comparator cmp .
haftmann@69184
   246
  show "comparator (\<lambda>a b. cmp (f a) (f b))"
haftmann@69184
   247
    by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
haftmann@69184
   248
qed
haftmann@69184
   249
haftmann@69251
   250
haftmann@69251
   251
subsection \<open>Direct implementations for linear orders on selected types\<close>
haftmann@69251
   252
haftmann@69251
   253
definition comparator_bool :: "bool comparator"
haftmann@69251
   254
  where [simp, code_abbrev]: "comparator_bool = default"
haftmann@69251
   255
haftmann@69251
   256
lemma compare_comparator_bool [code abstract]:
haftmann@69251
   257
  "compare comparator_bool = (\<lambda>p q.
haftmann@69251
   258
    if p then if q then Equiv else Greater
haftmann@69251
   259
    else if q then Less else Equiv)"
haftmann@69251
   260
  by (auto simp add: fun_eq_iff) (transfer; simp)+
haftmann@69251
   261
haftmann@69251
   262
definition raw_comparator_nat :: "nat \<Rightarrow> nat \<Rightarrow> comp"
haftmann@69251
   263
  where [simp]: "raw_comparator_nat = compare default"
haftmann@69251
   264
haftmann@69251
   265
lemma default_comparator_nat [simp, code]:
haftmann@69251
   266
  "raw_comparator_nat (0::nat) 0 = Equiv"
haftmann@69251
   267
  "raw_comparator_nat (Suc m) 0 = Greater"
haftmann@69251
   268
  "raw_comparator_nat 0 (Suc n) = Less"
haftmann@69251
   269
  "raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n"
haftmann@69251
   270
  by (transfer; simp)+
haftmann@69251
   271
haftmann@69251
   272
definition comparator_nat :: "nat comparator"
haftmann@69251
   273
  where [simp, code_abbrev]: "comparator_nat = default"
haftmann@69251
   274
haftmann@69251
   275
lemma compare_comparator_nat [code abstract]:
haftmann@69251
   276
  "compare comparator_nat = raw_comparator_nat"
haftmann@69251
   277
  by simp
haftmann@69251
   278
haftmann@69251
   279
definition comparator_linordered_group :: "'a::linordered_ab_group_add comparator"
haftmann@69251
   280
  where [simp, code_abbrev]: "comparator_linordered_group = default"
haftmann@69251
   281
haftmann@69251
   282
lemma comparator_linordered_group [code abstract]:
haftmann@69251
   283
  "compare comparator_linordered_group = (\<lambda>a b.
haftmann@69251
   284
    let c = a - b in if c < 0 then Less
haftmann@69251
   285
    else if c = 0 then Equiv else Greater)"
haftmann@69251
   286
proof (rule ext)+
haftmann@69251
   287
  fix a b :: 'a
haftmann@69251
   288
  show "compare comparator_linordered_group a b =
haftmann@69251
   289
    (let c = a - b in if c < 0 then Less
haftmann@69251
   290
       else if c = 0 then Equiv else Greater)"
haftmann@69251
   291
    by (simp add: Let_def not_less) (transfer; auto)
haftmann@69251
   292
qed
haftmann@69251
   293
haftmann@69184
   294
end