src/HOL/Library/Comparator.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (3 months ago) changeset 69946 494934c30f38 parent 69251 d240598e8637 permissions -rw-r--r--
improved code equations taken over from AFP
```     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 subsection \<open>Basic properties\<close>
```
```    12
```
```    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
```
```    81 lemma trans_equiv_less:
```
```    82   "cmp a c = Less" if "cmp a b = Equiv" and "cmp b c = Less"
```
```    83   using that
```
```    84   by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
```
```    85
```
```    86 lemma trans_less_equiv:
```
```    87   "cmp a c = Less" if "cmp a b = Less" and "cmp b c = Equiv"
```
```    88   using that
```
```    89   by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
```
```    90
```
```    91 lemma trans_equiv_greater:
```
```    92   "cmp a c = Greater" if "cmp a b = Equiv" and "cmp b c = Greater"
```
```    93   using that by (simp add: sym [of a b] greater_iff_sym_less trans_less_equiv)
```
```    94
```
```    95 lemma trans_greater_equiv:
```
```    96   "cmp a c = Greater" if "cmp a b = Greater" and "cmp b c = Equiv"
```
```    97   using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less)
```
```    98
```
```    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
```
```   141 text \<open>Substitution under equivalences\<close>
```
```   142
```
```   143 lemma equiv_subst_left:
```
```   144   "cmp z y = comp \<longleftrightarrow> cmp x y = comp" if "cmp z x = Equiv" for comp
```
```   145 proof -
```
```   146   from that have "cmp x z = Equiv"
```
```   147     by (simp add: sym)
```
```   148   with that show ?thesis
```
```   149     by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater)
```
```   150 qed
```
```   151
```
```   152 lemma equiv_subst_right:
```
```   153   "cmp x z = comp \<longleftrightarrow> cmp x y = comp" if "cmp z y = Equiv" for comp
```
```   154 proof -
```
```   155   from that have "cmp y z = Equiv"
```
```   156     by (simp add: sym)
```
```   157   with that show ?thesis
```
```   158     by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv)
```
```   159 qed
```
```   160
```
```   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
```
```   227
```
```   228 subsection \<open>Fundamental comparator combinators\<close>
```
```   229
```
```   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
```
```   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
```
```   294 end
```