src/HOL/Library/Comparator.thy
 author haftmann Fri Oct 26 08:20:45 2018 +0000 (10 months ago) changeset 69194 6d514e128a85 parent 69184 91fd09f2b86e child 69246 c1fe9dcc274a permissions -rw-r--r--
dedicated theory for sorting algorithms
```     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
```
```    79 lemma transp_less:
```
```    80   "transp (\<lambda>a b. cmp a b = Less)"
```
```    81   by (rule transpI) (fact trans_less)
```
```    82
```
```    83 lemma transp_greater:
```
```    84   "transp (\<lambda>a b. cmp a b = Greater)"
```
```    85   by (rule transpI) (fact trans_greater)
```
```    86
```
```    87 text \<open>The reflexive part\<close>
```
```    88
```
```    89 lemma reflp_not_less:
```
```    90   "reflp (\<lambda>a b. cmp a b \<noteq> Less)"
```
```    91   by (rule reflpI) simp
```
```    92
```
```    93 lemma reflp_not_greater:
```
```    94   "reflp (\<lambda>a b. cmp a b \<noteq> Greater)"
```
```    95   by (rule reflpI) simp
```
```    96
```
```    97 lemma quasisym_not_less:
```
```    98   "cmp a b = Equiv" if "cmp a b \<noteq> Less" and "cmp b a \<noteq> Less"
```
```    99   using that comp.exhaust greater_iff_sym_less by auto
```
```   100
```
```   101 lemma quasisym_not_greater:
```
```   102   "cmp a b = Equiv" if "cmp a b \<noteq> Greater" and "cmp b a \<noteq> Greater"
```
```   103   using that comp.exhaust greater_iff_sym_less by auto
```
```   104
```
```   105 lemma trans_not_less:
```
```   106   "cmp a c \<noteq> Less" if "cmp a b \<noteq> Less" "cmp b c \<noteq> Less"
```
```   107   using that by (metis comp.exhaust greater_iff_sym_less trans_equiv trans_less)
```
```   108
```
```   109 lemma trans_not_greater:
```
```   110   "cmp a c \<noteq> Greater" if "cmp a b \<noteq> Greater" "cmp b c \<noteq> Greater"
```
```   111   using that greater_iff_sym_less trans_not_less by blast
```
```   112
```
```   113 lemma transp_not_less:
```
```   114   "transp (\<lambda>a b. cmp a b \<noteq> Less)"
```
```   115   by (rule transpI) (fact trans_not_less)
```
```   116
```
```   117 lemma transp_not_greater:
```
```   118   "transp (\<lambda>a b. cmp a b \<noteq> Greater)"
```
```   119   by (rule transpI) (fact trans_not_greater)
```
```   120
```
```   121 end
```
```   122
```
```   123 typedef 'a comparator = "{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}"
```
```   124   morphisms compare Abs_comparator
```
```   125 proof -
```
```   126   have "comparator (\<lambda>_ _. Equiv)"
```
```   127     by standard simp_all
```
```   128   then show ?thesis
```
```   129     by auto
```
```   130 qed
```
```   131
```
```   132 setup_lifting type_definition_comparator
```
```   133
```
```   134 global_interpretation compare: comparator "compare cmp"
```
```   135   using compare [of cmp] by simp
```
```   136
```
```   137 lift_definition flat :: "'a comparator"
```
```   138   is "\<lambda>_ _. Equiv" by standard simp_all
```
```   139
```
```   140 instantiation comparator :: (linorder) default
```
```   141 begin
```
```   142
```
```   143 lift_definition default_comparator :: "'a comparator"
```
```   144   is "\<lambda>x y. if x < y then Less else if x > y then Greater else Equiv"
```
```   145   by standard (auto split: if_splits)
```
```   146
```
```   147 instance ..
```
```   148
```
```   149 end
```
```   150
```
```   151 text \<open>A rudimentary quickcheck setup\<close>
```
```   152
```
```   153 instantiation comparator :: (enum) equal
```
```   154 begin
```
```   155
```
```   156 lift_definition equal_comparator :: "'a comparator \<Rightarrow> 'a comparator \<Rightarrow> bool"
```
```   157   is "\<lambda>f g. \<forall>x \<in> set Enum.enum. f x = g x" .
```
```   158
```
```   159 instance
```
```   160   by (standard; transfer) (auto simp add: enum_UNIV)
```
```   161
```
```   162 end
```
```   163
```
```   164 lemma [code]:
```
```   165   "HOL.equal cmp1 cmp2 \<longleftrightarrow> Enum.enum_all (\<lambda>x. compare cmp1 x = compare cmp2 x)"
```
```   166   by transfer (simp add: enum_UNIV)
```
```   167
```
```   168 lemma [code nbe]:
```
```   169   "HOL.equal (cmp :: 'a::enum comparator) cmp \<longleftrightarrow> True"
```
```   170   by (fact equal_refl)
```
```   171
```
```   172 instantiation comparator :: ("{linorder, typerep}") full_exhaustive
```
```   173 begin
```
```   174
```
```   175 definition full_exhaustive_comparator ::
```
```   176   "('a comparator \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option)
```
```   177     \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
```
```   178   where "full_exhaustive_comparator f s =
```
```   179     Quickcheck_Exhaustive.orelse
```
```   180       (f (flat, (\<lambda>u. Code_Evaluation.Const (STR ''Comparator.flat'') TYPEREP('a comparator))))
```
```   181       (f (default, (\<lambda>u. Code_Evaluation.Const (STR ''HOL.default_class.default'') TYPEREP('a comparator))))"
```
```   182
```
```   183 instance ..
```
```   184
```
```   185 end
```
```   186
```
```   187 text \<open>Fundamental comparator combinators\<close>
```
```   188
```
```   189 lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
```
```   190   is "\<lambda>cmp a b. cmp b a"
```
```   191 proof -
```
```   192   fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp"
```
```   193   assume "comparator cmp"
```
```   194   then interpret comparator cmp .
```
```   195   show "comparator (\<lambda>a b. cmp b a)"
```
```   196     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
```
```   197 qed
```
```   198
```
```   199 lift_definition key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a comparator \<Rightarrow> 'b comparator"
```
```   200   is "\<lambda>f cmp a b. cmp (f a) (f b)"
```
```   201 proof -
```
```   202   fix cmp :: "'a \<Rightarrow> 'a \<Rightarrow> comp" and f :: "'b \<Rightarrow> 'a"
```
```   203   assume "comparator cmp"
```
```   204   then interpret comparator cmp .
```
```   205   show "comparator (\<lambda>a b. cmp (f a) (f b))"
```
```   206     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
```
```   207 qed
```
```   208
```
```   209 end
```