*To*: Johannes Hölzl <hoelzl at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Recursion through Types*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 21 Oct 2013 14:22:27 +0200*In-reply-to*: <1382356599.2666.25.camel@macbroy12.informatik.tu-muenchen.de>*References*: <1382117356.10613.2.camel@weber> <CAL0S8BeHRWZHVdqfMEY=Ys5SV=p=DSNcKumEHVqWm=GuuUybAw@mail.gmail.com> <1382356599.2666.25.camel@macbroy12.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hi Tjark and Johannes,

typedef 'a succ = "{0..<CARD('a)+1}" ... consts f :: "'a :: len word => 'b :: len word" defs (overloaded) f_base: "f (x :: num1 word) = ..." -- "base case n = 1" f_rec: "f (x :: 'a :: len succ word) = ... f (... :: 'a :: len word)" Best, Andreas On 21/10/13 13:56, Johannes Hölzl wrote:

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

**References**:**[isabelle] Recursion through Types***From:*Tjark Weber

**Re: [isabelle] Recursion through Types***From:*Jesus Aransay

**Re: [isabelle] Recursion through Types***From:*Johannes Hölzl

- Previous by Date: [isabelle] Isabelle2013-1-RC3: setup_lifting raises TYPE
- Next by Date: [isabelle] Calling sublocale A < B in A’s context?
- Previous by Thread: Re: [isabelle] Recursion through Types
- Next by Thread: [isabelle] Computing divisors
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list