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