How can I derive other type classes in Isabelle/HOL?

Question

The AFP entry Deriving provides a way to derive the following classes:

class	description
comparator	generate comparators for given types
compare	register types in class compare
compare_order	register types in class compare_order
countable	register datatypes is class countable
equality	generate an equality function
hash_code	generate a hash function
hashable	register types in class hashable
linorder	register types in class linorder

I saw that there is an exposed function register_derive, and would like to add another class. How does this work?

Answer 1

To register a new type class with the Deriving_Manager, I found Derive_Aux.define_overloaded useful. Here is an example usage :

theory Derive_enum
  imports Datatype_Order_Generator.Derive_Aux Deriving.Derive
begin

ML ‹

The Derive_Manager.register_derive function expects us to implement a function string -> string -> (theory -> theory):

let
  fun derive_enum tyco params thy = undefined (* ... *)
in
  Derive_Manager.register_derive "enum" "derives enum for a datatype" derive_enum
    |> Theory.setup
end›

Now a call derive (p) enum mytype will end up calling derive_enum "mytype" "p"" and apply the theory morphism to the current theory.

---

Recall that we want to define the following terms for enum:

instantiation
  mytype :: enum
  enum_mytype == enum_class.enum :: mytype list
  enum_all_mytype == enum_class.enum_all :: (mytype ⇒ bool) ⇒ bool
  enum_ex_mytype == enum_class.enum_ex :: (mytype ⇒ bool) ⇒ bool

Implementing derive_enum is fairly straight-forward, as those definitions are quite simple too:

fun derive_enum tyco params thy =
  let
    (* extract the relevant information from the theory: *)
    val base_name = Long_Name.base_name tyco
    val sort = @{sort enum}
    val info = BNF_LFP_Compat.the_info thy [] tyco

    (* only derive for types with nullary constructors *)
    val ctors_opt = (case #descr info of
        [(_,(_,_,ctor_strs))] =>
          if List.all (snd #> null) ctor_strs then SOME (map fst ctor_strs) else NONE
      | _ => NONE)

    (* if all the constructors are nullary: *)
    fun go ctor_strs =
    let
      open Ctr_Sugar_Util

      val _ = writeln ("creating enum for datatype " ^ base_name)

      (* these are our constructors in HOL *)
      val T = Type (tyco, [])
      val ctors = map (fn x => Const (x, T)) ctor_strs

      (* enum = [ctor0, ctor1...] *)
      val enum_lhs = Const (@{const_name enum_class.enum}, HOLogic.listT T)
      val enum_rhs = HOLogic.mk_list T ctors
      val enum_def = Derive_Aux.mk_def (HOLogic.listT T) @{const_name enum_class.enum} enum_rhs

      val p = Free ("p", T --> @{typ bool})
      val pT = (T --> @{typ bool}) --> @{typ bool}
      val psT = (T --> @{typ bool}) --> HOLogic.listT T --> @{typ bool}

      (* enum_all = λp. list_all p enum *)
      val enum_all_rhs = lambda p
        (Const (@{const_name List.list_all}, psT) $ p $ enum_lhs)
      val enum_all_def = Derive_Aux.mk_def pT @{const_name enum_class.enum_all} enum_all_rhs

      (* enum_ex = λp. list_ex p enum *)
      val enum_ex_rhs = lambda p
        (Const (@{const_name List.list_ex}, psT) $ p $ enum_lhs)
      val enum_ex_def = Derive_Aux.mk_def pT @{const_name enum_class.enum_ex} enum_ex_rhs

      (* define the constants *)
      val (((enum_thm, enum_all_thm), enum_ex_thm), lthy) =
        Class.instantiation ([tyco],[],sort) thy
          |> Derive_Aux.define_overloaded ("enum_" ^ base_name ^ "_def", enum_def)
          ||>> Derive_Aux.define_overloaded ("enum_all_" ^ base_name ^ "_def", enum_all_def)
          ||>> Derive_Aux.define_overloaded ("enum_ex_" ^ base_name ^ "_def", enum_ex_def)

      (* build the tactics required: *)
      val enum_thms = [enum_thm RS @{thm meta_eq_to_obj_eq}, enum_all_thm, enum_ex_thm]

      (* UNIV = {ctor0...} *)
      fun UNIV_eq_tac ctxt =
        EVERY' [rtac ctxt @{thm UNIV_eq_I}, rtac ctxt (#exhaust info)] THEN_ALL_NEW
        EVERY' [K (unfold_tac ctxt (enum_thms @ @{thms list.set insert_iff})), blast_tac ctxt]

      (* _ {ctor0...} _ = _ UNIV _ *)
      fun pred_aux_tac ctxt = EVERY'
        [rtac ctxt @{thm arg_cong[where f="λx. _ x _"]},
         rtac ctxt @{thm sym},
         UNIV_eq_tac ctxt]

      fun enum_tac ctxt = EVERY
        [unfold_tac ctxt (@{thms list_all_iff list_ex_iff list.set} @ enum_thms),
         HEADGOAL (UNIV_eq_tac ctxt),
         HEADGOAL (simp_tac ctxt),
         HEADGOAL (pred_aux_tac ctxt),
         HEADGOAL (pred_aux_tac ctxt)]

      val thy' = Class.prove_instantiation_exit
        (fn ctxt => Class.intro_classes_tac ctxt [] THEN enum_tac ctxt) lthy
      val _ = writeln ("registered " ^ base_name ^ " in class enum")
    in
      thy'
    end

  in case ctors_opt of
      SOME ctors => go ctors
    | _ => warning ("cannot create enum for datatype " ^ base_name) |> K thy
  end

---

And to show how it all fits together:

datatype day = Sat | Sun | Mon | Tue | Wed | Thu | Fri
derive enum day
print_derives
(*
The following sorts can be derived
...
enum: derives enum for a datatype 
...
*)
value "Enum.enum :: day list" (* [Sat, Sun, Mon, Tue, Wed, Thu, Fri] *)