Re: [isabelle] lift_definition + constructor



On Tue, Nov 19, 2013 at 9:57 AM, Walther Neuper <wneuper at ist.tugraz.at> wrote:
> In Isabelle2013-1 in HOL/Library/Polynomial there is
>
> lift_definition pCons :: "'a::zero => 'a poly => 'a poly"
> is "λa p. nat_case a (coeff p)"
...
> Is there a way to have a constructor "pCons" instead of function "pCons"?
> I.e. a constructor like
>
> datatype 'a pcons = Zero | pCons 'a "'a pcons"
>
> could be somehow associated with lift_definition ? Or is this possible with
> datatype_new ?

What exactly do you mean by "constructor"? HOL doesn't have any
built-in logical distinction between constructors and other functions.

The datatype package maintains its own internal database of
"constructor" functions, which is used for various kinds of proof
automation. Independently defined constructors can be registered after
the fact with "rep_datatype". However, Zero and pCons do not meet the
datatype package's requirement for distinctness, as pCons 0 Zero =
Zero.

Perhaps you hope to gain access to some form of automation for pCons
that would normally be provided by the datatype package? (E.g.
cases/induct proofs, case expressions, code generation, function
definitions by pattern matching, etc.) If so, then it is likely that
there is another way to get what you want with a little more work.

- Brian




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