[isabelle] default implementations for type classes



Hi!

Is there any way to provide default implementations for type class functions that may be overwritten by the user?

I'm thinking of something like the Haskell Show class, i.e.,

types "shows" = "string => string"

  class "show" =
    fixes "show" :: "'a => string"
      and shows_prec :: "nat => 'a => shows"
      and shows_list :: "'a list => shows"

together with the functions

  definition "shows" :: "'a::show => shows"
  where "shows = shows_prec (0::nat)"

  fun showl :: "('a ⇒ shows) ⇒ string ⇒ 'a list ⇒ string"
  where "showl showx s [] = CHR '']'' # s"
      | "showl showx s (x#xs) = CHR '','' # showx x (showl showx s xs)"

  fun shows_list_aux :: "('a ⇒ shows) ⇒ 'a list ⇒ shows"
  where "shows_list_aux _ [] s = ''[]'' @ s"
      | "shows_list_aux showx (x#xs) s =
        (CHR ''['') # showx x (showl showx s xs)"

  hide const showl

where the default implementations could be

  show x = shows_prec 0 x ''''
  shows_prec d x s = show x @ s
  shows_list xs s = show_list_aux shows xs s

Any ideas?

cheers

christian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.