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

consider isabelle code

theory scratch imports main begin  datatype expr = const nat | plus expr expr 

it quite reasonable instantiate plus type class nice syntax plus constructor:

instantiation expr :: plus begin   definition "plus_exp = plus" instance.. end 

but now, + , plus still separate constants. in particular, cannot (easily) use + in function definition, e.g.

fun swap    "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 instantiate type class existing constant instead of defining new one?

type class instantiations in isabelle introduce new constants parameters of type class. thus, cannot plus (written infix +) shall same plus. however, can go other way around, namely instantiate type class first , later declare operations on type class constructors of datatype.

one such case can found in theory extended_nat type enat constructed manually via typedef, infinity type class instantiated, , enat declared datatype 2 constructors using old_rep_datatype. however, simple case of non-recursive datatype without type variables. in case of expression example, recommend following:

1. define type expr_aux datatype expr_aux = const_aux nat | plus_aux expr_aux expr_aux.

2. define expr type copy of expr_aux typedef expr = "univ :: expr_aux set" , setup_lifting type_definition_expr.

3. lift constructor const_aux expr lifting package: lift_definition const :: "nat => expr" const_aux .

4. instantiate type class plus:

 

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

5. register expr datatype old_rep_datatype expr const "plus :: expr => _" , appropriate proof (use transfer).

6. define abbreviation plus :: "expr => expr => expr" "plus == plus"

obviously, tedious. if want use pattern matching in functions, can use free_constructor command register constructors const , plus :: expr => expr => expr new constructors of expr after instantiation. if add "plus = plus" simp rule, should tedious way. yet, not know how various packages (in particular case syntax) cope re-registration of constructors.