Theory Type_Classes

section ‹Type Classes›

theory Type_Classes
  imports HOLCF_Main
begin


subsection ‹Eq class›

class Eq =
  fixes eq :: "'a → 'a → tr"

text ‹
  The Haskell type class does allow /= to be specified separately. For now, we assume
  that all modeled type classes use the default implementation, or an equivalent.
›
fixrec neq :: "'a::Eq → 'a → tr" where
  "neq⋅x⋅y = neg⋅(eq⋅x⋅y)"

class Eq_strict = Eq +
  assumes eq_strict [simp]:
    "eq⋅x⋅⊥ = ⊥"
    "eq⋅⊥⋅y = ⊥"

class Eq_sym = Eq_strict +
  assumes eq_sym: "eq⋅x⋅y = eq⋅y⋅x"

class Eq_equiv = Eq_sym +
  assumes eq_self_neq_FF [simp]: "eq⋅x⋅x ≠ FF"
    and eq_trans: "eq⋅x⋅y = TT ⟹ eq⋅y⋅z = TT ⟹ eq⋅x⋅z = TT"
begin

lemma eq_refl: "eq⋅x⋅x ≠ ⊥ ⟹ eq⋅x⋅x = TT"
  by (cases "eq⋅x⋅x") simp+

end

class Eq_eq = Eq_sym +
  assumes eq_self_neq_FF': "eq⋅x⋅x ≠ FF"
    and eq_TT_dest: "eq⋅x⋅y = TT ⟹ x = y"
begin

subclass Eq_equiv
  by standard (auto simp: eq_self_neq_FF' dest: eq_TT_dest)

lemma eqD [dest]:
  "eq⋅x⋅y = TT ⟹ x = y"
  "eq⋅x⋅y = FF ⟹ x ≠ y"
  by (auto elim: eq_TT_dest)

end

subsubsection ‹Class instances›

instantiation lift :: (countable) Eq_eq
begin

definition "eq ≡ (Λ(Def x) (Def y). Def (x = y))"

instance
  by standard (auto simp: eq_lift_def flift1_def split: lift.splits)

end

lemma eq_ONE_ONE [simp]: "eq⋅ONE⋅ONE = TT"
  unfolding ONE_def eq_lift_def by simp


subsection ‹Ord class›

domain Ordering = LT | EQ | GT

definition oppOrdering :: "Ordering → Ordering" where
  "oppOrdering = (Λ x. case x of LT ⇒ GT | EQ ⇒ EQ | GT ⇒ LT)"

lemma oppOrdering_simps [simp]:
  "oppOrdering⋅LT = GT"
  "oppOrdering⋅EQ = EQ"
  "oppOrdering⋅GT = LT"
  "oppOrdering⋅⊥ = ⊥"
  unfolding oppOrdering_def by simp_all

class Ord = Eq +
  fixes compare :: "'a → 'a → Ordering"
begin

definition lt :: "'a → 'a → tr" where
  "lt = (Λ x y. case compare⋅x⋅y of LT ⇒ TT | EQ ⇒ FF | GT ⇒ FF)"

definition le :: "'a → 'a → tr" where
  "le = (Λ x y. case compare⋅x⋅y of LT ⇒ TT | EQ ⇒ TT | GT ⇒ FF)"

lemma lt_eq_TT_iff: "lt⋅x⋅y = TT ⟷ compare⋅x⋅y = LT"
  by (cases "compare⋅x⋅y") (simp add: lt_def)+

end

class Ord_strict = Ord +
  assumes compare_strict [simp]:
    "compare⋅⊥⋅y = ⊥"
    "compare⋅x⋅⊥ = ⊥"
begin

lemma lt_strict [simp]:
  shows "lt⋅⊥⋅x = ⊥"
    and "lt⋅x⋅⊥ = ⊥"
  by (simp add: lt_def)+

lemma le_strict [simp]:
  shows "le⋅⊥⋅x = ⊥"
    and "le⋅x⋅⊥ = ⊥"
  by (simp add: le_def)+

end

text ‹TODO: It might make sense to have a class for preorders too,
analogous to class ‹eq_equiv›.›

class Ord_linear = Ord_strict +
  assumes eq_conv_compare: "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    and oppOrdering_compare [simp]:
    "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    and compare_EQ_dest: "compare⋅x⋅y = EQ ⟹ x = y"
    and compare_self_below_EQ: "compare⋅x⋅x ⊑ EQ"
    and compare_LT_trans:
    "compare⋅x⋅y = LT ⟹ compare⋅y⋅z = LT ⟹ compare⋅x⋅z = LT"
  (*BH: Is this set of axioms complete?*)
  (*CS: How about totality of the order?*)
begin

lemma eq_TT_dest: "eq⋅x⋅y = TT ⟹ x = y"
  by (cases "compare⋅x⋅y") (auto dest: compare_EQ_dest simp: eq_conv_compare)+

lemma le_iff_lt_or_eq:
  "le⋅x⋅y = TT ⟷ lt⋅x⋅y = TT ∨ eq⋅x⋅y = TT"
  by (cases "compare⋅x⋅y") (simp add: le_def lt_def eq_conv_compare)+

lemma compare_sym:
  "compare⋅x⋅y = (case compare⋅y⋅x of LT ⇒ GT | EQ ⇒ EQ | GT ⇒ LT)"
  by (subst oppOrdering_compare [symmetric]) (simp add: oppOrdering_def)

lemma compare_self_neq_LT [simp]: "compare⋅x⋅x ≠ LT"
  using compare_self_below_EQ [of x] by clarsimp

lemma compare_self_neq_GT [simp]: "compare⋅x⋅x ≠ GT"
  using compare_self_below_EQ [of x] by clarsimp

declare compare_self_below_EQ [simp]

lemma lt_trans: "lt⋅x⋅y = TT ⟹ lt⋅y⋅z = TT ⟹ lt⋅x⋅z = TT"
  unfolding lt_eq_TT_iff by (rule compare_LT_trans)

lemma compare_GT_iff_LT: "compare⋅x⋅y = GT ⟷ compare⋅y⋅x = LT"
  by (cases "compare⋅x⋅y", simp_all add: compare_sym [of y x])

lemma compare_GT_trans:
  "compare⋅x⋅y = GT ⟹ compare⋅y⋅z = GT ⟹ compare⋅x⋅z = GT"
  unfolding compare_GT_iff_LT by (rule compare_LT_trans)

lemma compare_EQ_iff_eq_TT:
  "compare⋅x⋅y = EQ ⟷ eq⋅x⋅y = TT"
  by (cases "compare⋅x⋅y") (simp add: is_EQ_def eq_conv_compare)+

lemma compare_EQ_trans:
  "compare⋅x⋅y = EQ ⟹ compare⋅y⋅z = EQ ⟹ compare⋅x⋅z = EQ"
  by (blast dest: compare_EQ_dest)

lemma le_trans:
  "le⋅x⋅y = TT ⟹ le⋅y⋅z = TT ⟹ le⋅x⋅z = TT"
  by (auto dest: eq_TT_dest lt_trans simp: le_iff_lt_or_eq)

lemma neg_lt: "neg⋅(lt⋅x⋅y) = le⋅y⋅x"
  by (cases "compare⋅x⋅y", simp_all add: le_def lt_def compare_sym [of y x])

lemma neg_le: "neg⋅(le⋅x⋅y) = lt⋅y⋅x"
  by (cases "compare⋅x⋅y", simp_all add: le_def lt_def compare_sym [of y x])

subclass Eq_eq
proof
  fix x y
  show "eq⋅x⋅y = eq⋅y⋅x"
    unfolding eq_conv_compare
    by (cases "compare⋅x⋅y", simp_all add: compare_sym [of y x])
  show "eq⋅x⋅⊥ = ⊥"
    unfolding eq_conv_compare by simp
  show "eq⋅⊥⋅y = ⊥"
    unfolding eq_conv_compare by simp
  show "eq⋅x⋅x ≠ FF"
    unfolding eq_conv_compare
    by (cases "compare⋅x⋅x", simp_all)
  show "x = y" if "eq⋅x⋅y = TT"
    using that
    unfolding eq_conv_compare
    by (cases "compare⋅x⋅y", auto dest: compare_EQ_dest)
qed

end

text ‹A combinator for defining Ord instances for datatypes.›

definition thenOrdering :: "Ordering → Ordering → Ordering" where
  "thenOrdering = (Λ x y. case x of LT ⇒ LT | EQ ⇒ y | GT ⇒ GT)"

lemma thenOrdering_simps [simp]:
  "thenOrdering⋅LT⋅y = LT"
  "thenOrdering⋅EQ⋅y = y"
  "thenOrdering⋅GT⋅y = GT"
  "thenOrdering⋅⊥⋅y = ⊥"
  unfolding thenOrdering_def by simp_all

lemma thenOrdering_LT_iff [simp]:
  "thenOrdering⋅x⋅y = LT ⟷ x = LT ∨ x = EQ ∧ y = LT"
  by (cases x, simp_all)

lemma thenOrdering_EQ_iff [simp]:
  "thenOrdering⋅x⋅y = EQ ⟷ x = EQ ∧ y = EQ"
  by (cases x, simp_all)

lemma thenOrdering_GT_iff [simp]:
  "thenOrdering⋅x⋅y = GT ⟷ x = GT ∨ x = EQ ∧ y = GT"
  by (cases x, simp_all)

lemma thenOrdering_below_EQ_iff [simp]:
  "thenOrdering⋅x⋅y ⊑ EQ ⟷ x ⊑ EQ ∧ (x = ⊥ ∨ y ⊑ EQ)"
  by (cases x) simp_all

lemma is_EQ_thenOrdering [simp]:
  "is_EQ⋅(thenOrdering⋅x⋅y) = (is_EQ⋅x andalso is_EQ⋅y)"
  by (cases x) simp_all

lemma oppOrdering_thenOrdering:
  "oppOrdering⋅(thenOrdering⋅x⋅y) =
    thenOrdering⋅(oppOrdering⋅x)⋅(oppOrdering⋅y)"
  by (cases x) simp_all

instantiation lift :: ("{linorder,countable}") Ord_linear
begin

definition
  "compare ≡ (Λ (Def x) (Def y).
    if x < y then LT else if x > y then GT else EQ)"

instance proof
  fix x y z :: "'a lift"
  show "compare⋅⊥⋅y = ⊥"
    unfolding compare_lift_def by simp
  show "compare⋅x⋅⊥ = ⊥"
    unfolding compare_lift_def by (cases x, simp_all)
  show "oppOrdering⋅(compare⋅x⋅y) = compare⋅y⋅x"
    unfolding compare_lift_def
    by (cases x, cases y, simp, simp,
      cases y, simp, simp add: not_less less_imp_le)
  show "x = y" if "compare⋅x⋅y = EQ"
    using that
    unfolding compare_lift_def
    by (cases x, cases y, simp, simp,
        cases y, simp, simp split: if_splits)
  show "compare⋅x⋅z = LT" if "compare⋅x⋅y = LT" and "compare⋅y⋅z = LT"
    using that
    unfolding compare_lift_def
    by (cases x, simp, cases y, simp, cases z, simp,
        auto split: if_splits)
  show "eq⋅x⋅y = is_EQ⋅(compare⋅x⋅y)"
    unfolding eq_lift_def compare_lift_def
    by (cases x, simp, cases y, simp, auto)
  show "compare⋅x⋅x ⊑ EQ"
    unfolding compare_lift_def
    by (cases x, simp_all)
qed

end

lemma lt_le:
  "lt⋅(x::'a::Ord_linear)⋅y = (le⋅x⋅y andalso neq⋅x⋅y)"
  by (cases "compare⋅x⋅y")
     (auto simp: lt_def le_def eq_conv_compare)

end