Re: [isabelle] Recursion through Types



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
>
>
>



-- 
Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España




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