Re: [isabelle] Recursion through Types



Hi Tjark,

I also think the general answer is no.

But maybe there is a trick (also called ugly hack) using type classes:

For a function "f" you want to define with primitive recursion on a type
"'a" you introduce a new type class:

  class f_def =
    fixes f :: "'a ⇒ nat"

Now you instantiate the option type (as the successor type):

  instantiation option :: (f_def) f_def
  begin

  definition 
    "f_option (x::'a option) = f (undefined :: 'a) + 1"

  instance ..
  end

and one for the unit type (as termination)

  instantiation unit :: f_def
  begin

  definition f_unit :: "unit ⇒ nat" where
    "f_unit (x::unit) = 0"

  instance ..
  end

But a problem is that numeral types used by the word library and by
Multivariate Analysis use a binary representation instead of a unary
representation.

 - Johannes


Am Sonntag, den 20.10.2013, 11:44 +0200 schrieb Jesus Aransay:
> Dear Tjark,
> 
> I don't know how far the following solution is applicable to your
> setting, but a somehow similar problem (and two different solutions)
> were proposed in the mailing list by J. Harrison a while ago, for the
> definition of determinants of matrices of dimension n, in terms of
> determinants of matrices of size "n - 1":
> 
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-January/msg00015.html
> 
> Hope it helps,
> 
> best,
> 
> Jesus
> 
> 
> On Fri, Oct 18, 2013 at 7:29 PM, Tjark Weber <webertj at in.tum.de> wrote:
> > Hi,
> >
> > There is a trick (due to John Harrison) to encode the dimension N of,
> > e.g., N-bit words with a type argument.  The word libraries in
> > Isabelle/HOL and HOL4 are based on this approach.
> >
> > In this setting, what is the recommended way to define a function that
> > performs recursion over N, i.e., whose result for an (N+1)-bit word is
> > naturally expressed in terms of its result for an N-bit word?
> >
> > Best,
> > Tjark
> >
> >
> >
> 
> 
> 







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