Existing constants (e.g. constructors) in class class instances
Consider this Isabella code
theory Scratch imports Main begin
datatype Expr = Const nat | Plus Expr Expr
It's perfectly reasonable to instantiate the class plus
to get good syntax for the constructor plus
:
instantiation Expr :: plus
begin
definition "plus_Exp = Plus"
instance..
end
But now +
and plus
still are separate constants. In particular, I cannot (easily) use +
in a function definition like
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?
source to share
An instance of the Type class in Isabelle always introduces new constants for the parameters of the type class. So you cannot say that plus
(written infix how +
) should 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 data type constructors.
One such case can be found in the Extended_Nat theory , where a type enat
is manually typedef
instantiated through , then an instance of the infinity class is instantiated, and finally enat
declared as a data type with two constructors using old_rep_datatype
. However, this is a very simple case of a non-recursive data type with no type variables. In the case of your example expression, I recommend that you do the following:
-
Determine the type
expr_aux
withdatatype expr_aux = Const_aux nat | Plus_aux expr_aux expr_aux
. -
Define
expr
as a copy of the typeexpr_aux
usingtypedef expr = "UNIV :: expr_aux set"
andsetup_lifting type_definition_expr
. -
Lift the constructor
Const_aux
upexpr
with a lift bag:lift_definition Const :: "nat => expr" is Const_aux .
-
Create an instance of the class
plus
:
instantiation expr :: plus begin
lift_definition plus_expr :: "expr => expr => expr" is Plus_aux .
instance ..
end
-
Register
expr
as datatype withold_rep_datatype expr Const "plus :: expr => _"
and the corresponding proof (usetransfer
). -
Define
abbreviation Plus :: "expr => expr => expr" where "Plus == plus"
Obviously, this is very tiring. If you just want to use pattern matching in functions, you can use the command free_constructor
to register constructors Const
and plus :: expr => expr => expr
as new constructors expr
after instantiation. If you then add "Plus = plus" as the simp rule, it is almost as good as the tedious way. However, I don't know how well the various packages (specifically the case syntax) handle this constructor re-registration.
source to share