Existing constants (e.g. constructors) in type class instantiations

Question

Consider this Isabelle code

theory Scratch imports Main begin

datatype Expr = Const nat | Plus Expr Expr

it is quite reasonable to instantiate the plus type class to get nice syntax for the Plus constructor:

instantiation Expr :: plus
begin
  definition "plus_Exp = Plus"
instance..
end

But now, + and Plus are still separate constants. In particular, I cannot (easily) use + in a function definition, e.g.

fun swap where
   "swap (Const n) = Const n"
 | "swap (e1 + e2) = e2 + e1"

will print

Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀e1 e2. swap (e1 + e2) = e2 + e1

How can I instantiate a type class with an existing constant instead of defining a new one?

Answer 1

Type class instantiations in Isabelle always introduce new constants for the parameters of the type class. Thus, you cannot say that plus (written infix as +) shall be the same as Plus. However, you can go the other way around, namely instantiate the type class first and only later declare the operations on the type class as the constructors of the datatype.

One such case can be found in the theory Extended_Nat where the type enat is constructed manually via a typedef, then the infinity type class is instantiated, and finally enat is declared as a datatype with two constructors using old_rep_datatype. However, this is a very simple case of a non-recursive datatype without type variables. In case of your expression example, I recommend that you do the following:

1. Define a type expr_aux with datatype expr_aux = Const_aux nat | Plus_aux expr_aux expr_aux.

2. Define a expr as a type copy of expr_aux with typedef expr = "UNIV :: expr_aux set" and setup_lifting type_definition_expr.

3. Lift the constructor Const_aux to expr with the lifting package: lift_definition Const :: "nat => expr" is Const_aux .

4. Instantiate the type class plus:

 

instantiation expr :: plus begin
lift_definition plus_expr :: "expr => expr => expr" is Plus_aux .
instance ..
end

5. Register expr as a datatype with old_rep_datatype expr Const "plus :: expr => _" and an appropriate proof (use transfer).

6. Define an abbreviation Plus :: "expr => expr => expr" where "Plus == plus"

Obviously, this is very tedious. If you just want to use pattern matching in functions, you can use the free_constructor command to register the constructors Const and plus :: expr => expr => expr as new constructors of expr after the instantiation. If you then add "Plus = plus" as a simp rule, this should be almost as good as the tedious way. Yet, I do not know how well the various packages (in particular case syntax) cope with this re-registration of the constructors.