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