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