Theory Num_Class

section ‹The Num Class›

theory Num_Class
  imports
    Type_Classes
    Data_Integer
    Data_Tuple
begin


subsection ‹Num class›

(* TODO: Show class (jb) *)

class Num_syn =
  Eq +
  plus +
  minus +
  times +
  zero +
  one +
  fixes  negate :: "'a → 'a"
  and   abs :: "'a → 'a"
  and   signum :: "'a → 'a"
  and   fromInteger :: "Integer → 'a"

(* If I create this class in one step I get problems with Num_faithful... (jb) *)
class Num = Num_syn + plus_cpo + minus_cpo + times_cpo

class Num_strict = Num +
  assumes plus_strict[simp]:
    "x + ⊥ = (⊥::'a::Num)"
    "⊥ + x = ⊥"
  assumes minus_strict[simp]:
    "x - ⊥ = ⊥"
    "⊥ - x = ⊥"
  assumes mult_strict[simp]:
    "x * ⊥ = ⊥"
    "⊥ * x = ⊥"
  assumes negate_strict[simp]:
    "negate⋅⊥ = ⊥"
  assumes abs_strict[simp]:
    "abs⋅⊥ = ⊥"
  assumes signum_strict[simp]:
    "signum⋅⊥ = ⊥"
  assumes fromInteger_strict[simp]:
    "fromInteger⋅⊥ = ⊥"

(* TODO: How to name the type class that adds the reqiured relations? For Eq, we have Eq_equiv
resp. Eq_eq, but for Num I don't see a nice name. Also, a generic name might be nicer. (jb) *)

class Num_faithful =
  (* TODO: Why is it not possible to use Num here? I get
     Type unification failed: No type arity lift :: minus
     (jb)
  *)
  Num_syn +
  (* This is the only relation about Num required by the Haskell report. By using eq we leave it
  to the users choice of Eq_eq or Eq_equiv whether the relations should hold up to equivalence or
  syntactic equality. (jb) *)
  assumes abs_signum_eq: "(eq⋅((abs⋅x) * (signum⋅x))⋅(x::'a::{Num_syn})) ⊑ TT"
  (* TODO: Should we add sensible relations on our own? (jb) *)

  (* The zero and one type class are "artificial", so we ensure they do what expected. *)
  (* Unfortunately, this is not working. Is isabelle trying to give all occurrences of 0
      the same type?
  assumes "0 = fromInteger⋅0"
  assumes "1 = fromInteger⋅1"
  *)

class Integral =
  Num +
  (* fixes quot rem  *)
  fixes div mod :: "'a → 'a → ('a::Num)"
  fixes toInteger :: "'a → Integer"
begin
  (* fixrec quotRem :: "'a → 'a → ⟨'a, 'a⟩"  where "quotRem⋅x⋅y = ⟨quot⋅x⋅y, (rem⋅x⋅y)⟩" *)
  fixrec divMod :: "'a → 'a → ⟨'a, 'a⟩"  where "divMod⋅x⋅y = ⟨div⋅x⋅y, mod⋅x⋅y⟩"

  fixrec even :: "'a → tr" where "even⋅x = eq⋅(div⋅x⋅(fromInteger⋅2))⋅0"
  fixrec odd :: "'a → tr" where "odd⋅x = neg⋅(even⋅x)"
end

class Integral_strict = Integral +
  assumes div_strict[simp]:
    "div⋅x⋅⊥ = (⊥::'a::Integral)"
    "div⋅⊥⋅x = ⊥"
  assumes mod_strict[simp]:
    "mod⋅x⋅⊥ = ⊥"
    "mod⋅⊥⋅x = ⊥"
  assumes toInteger_strict[simp]:
    "toInteger⋅⊥ = ⊥"

class Integral_faithful =
  Integral +
  Num_faithful +
  (* assumes "¬(eq⋅y⋅0 = TT) ⟹ quot⋅x⋅y * y + rem⋅x⋅y = (x::'a::{Integral})" *)
  assumes "eq⋅y⋅0 = FF ⟹ div⋅x⋅y * y + mod⋅x⋅y = (x::'a::{Integral})"


subsection ‹Instances for Integer›

instantiation Integer :: Num_syn
begin
  definition "negate = (Λ (MkI⋅x). MkI⋅(uminus x))"
  definition "abs = (Λ (MkI⋅x) . MkI⋅(¦x¦))"
  definition "signum = (Λ (MkI⋅x) . MkI⋅(sgn x))"
  definition "fromInteger = (Λ x. x)"
  instance..
end

instance Integer :: Num
  by standard

instance Integer :: Num_faithful
  apply standard
  apply (rename_tac x, case_tac x)
   apply simp
  apply (simp add: signum_Integer_def abs_Integer_def)
  apply (metis mult.commute mult_sgn_abs)
  done

instance Integer :: Num_strict
  apply standard
  unfolding signum_Integer_def abs_Integer_def negate_Integer_def fromInteger_Integer_def
  by simp_all

instantiation Integer :: Integral
begin
  definition "div = (Λ (MkI⋅x) (MkI⋅y). MkI⋅(Rings.divide x y))"
  definition "mod = (Λ (MkI⋅x) (MkI⋅y). MkI⋅(Rings.modulo x y))"
  definition "toInteger = (Λ x. x)"
  instance ..
end

instance Integer :: Integral_strict
  apply standard
  unfolding div_Integer_def mod_Integer_def toInteger_Integer_def
      apply simp_all
   apply (rename_tac x, case_tac x, simp, simp)+
  done

instance Integer :: Integral_faithful
  apply standard
  unfolding div_Integer_def mod_Integer_def
  apply (rename_tac y x)
  apply (case_tac y, simp)
  apply (case_tac x, simp)
  apply simp
  done

lemma Integer_Integral_simps[simp]:
  "div⋅(MkI⋅x)⋅(MkI⋅y) = MkI⋅(Rings.divide x y)"
  "mod⋅(MkI⋅x)⋅(MkI⋅y) = MkI⋅(Rings.modulo x y)"
  "fromInteger⋅i = i"
  unfolding mod_Integer_def div_Integer_def fromInteger_Integer_def by simp_all

end