Theory Compare_Order_Instances

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
*)
subsection ‹Defining Compare-Order-Instances for Common Types›

theory Compare_Order_Instances
imports
  Compare_Instances
  "HOL-Library.List_Lexorder"
  "HOL-Library.Product_Lexorder"
  "HOL-Library.Option_ord"
begin

text ‹We now also instantiate class @{class compare_order} and not only @{class compare}.
  Here, we also prove that our definitions do not clash with existing orders on
  @{type list}, @{type option}, and @{type prod}.
  
  For @{type sum} we just define the linear orders via their comparator.›

derive compare_order sum

instance list :: (compare_order)compare_order
proof
  note [simp] = le_of_comp_def lt_of_comp_def comparator_of_def
  show "le_of_comp (compare :: 'a list comparator) = (≤)" 
    unfolding compare_list_def compare_is_comparator_of 
  proof (intro ext)
    fix xs ys :: "'a list"
    show "le_of_comp (comparator_list comparator_of) xs ys = (xs ≤ ys)"
    proof (induct xs arbitrary: ys)
      case (Nil ys)
      show ?case
        by (cases ys, simp_all)
    next
      case (Cons x xs yys) note IH = this
      thus ?case
      proof (cases yys)
        case Nil
        thus ?thesis by auto
      next
        case (Cons y ys)
        show ?thesis unfolding Cons
          using IH[of ys]
          by (cases x y rule: linorder_cases, auto)
      qed
    qed
  qed
  show "lt_of_comp (compare :: 'a list comparator) = (<)" 
    unfolding compare_list_def compare_is_comparator_of 
  proof (intro ext)
    fix xs ys :: "'a list"
    show "lt_of_comp (comparator_list comparator_of) xs ys = (xs < ys)"
    proof (induct xs arbitrary: ys)
      case (Nil ys)
      show ?case
        by (cases ys, simp_all)
    next
      case (Cons x xs yys) note IH = this
      thus ?case
      proof (cases yys)
        case Nil
        thus ?thesis by auto
      next
        case (Cons y ys)
        show ?thesis unfolding Cons
          using IH[of ys]
          by (cases x y rule: linorder_cases, auto)
      qed
    qed
  qed
qed

instance prod :: (compare_order, compare_order)compare_order
proof
  note [simp] = le_of_comp_def lt_of_comp_def comparator_of_def
  show "le_of_comp (compare :: ('a,'b)prod comparator) = (≤)" 
    unfolding compare_prod_def compare_is_comparator_of 
  proof (intro ext)
    fix xy1 xy2 :: "('a,'b)prod"
    show "le_of_comp (comparator_prod comparator_of comparator_of) xy1 xy2 = (xy1 ≤ xy2)"
      by (cases xy1, cases xy2, auto)
  qed
  show "lt_of_comp (compare :: ('a,'b)prod comparator) = (<)" 
    unfolding compare_prod_def compare_is_comparator_of 
  proof (intro ext)
    fix xy1 xy2 :: "('a,'b)prod"
    show "lt_of_comp (comparator_prod comparator_of comparator_of) xy1 xy2 = (xy1 < xy2)"
      by (cases xy1, cases xy2, auto)
  qed
qed

instance option :: (compare_order)compare_order
proof
  note [simp] = le_of_comp_def lt_of_comp_def comparator_of_def
  show "le_of_comp (compare :: 'a option comparator) = (≤)" 
    unfolding compare_option_def compare_is_comparator_of 
  proof (intro ext)
    fix xy1 xy2 :: "'a option"
    show "le_of_comp (comparator_option comparator_of) xy1 xy2 = (xy1 ≤ xy2)"
      by (cases xy1, (cases xy2, auto split: if_splits)+)
  qed
  show "lt_of_comp (compare :: 'a option comparator) = (<)" 
    unfolding compare_option_def compare_is_comparator_of 
  proof (intro ext)
    fix xy1 xy2 :: "'a option"
    show "lt_of_comp (comparator_option comparator_of) xy1 xy2 = (xy1 < xy2)"
      by (cases xy1, (cases xy2, auto split: if_splits)+)
  qed
qed

end