*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Fri, 18 Jan 2013 09:07:46 -0600*In-reply-to*: <50F8FAE2.8010205@in.tum.de>*References*: <50F85B11.4080205@gmx.com> <50F85E20.2060301@gmx.com> <50F8D10E.9000502@gmx.com> <50F8FAE2.8010205@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 1/18/2013 1:33 AM, Lars Noschinski wrote:

On 18.01.2013 05:35, Gottfried Barrow wrote:primrec sFOLf :: "sFOLdt => bool" where "sFOLf (In u1 u2) = (u1 inS u2)" | "sFOLf (And f1 f2) = ((sFOLf (Rec f1)) & (sFOLf (Rec f2)))" | "sFOLf (Rec f) = True"This definition is not primitive recursive and hence rejected byprimrec (recursive calls my only make the arguments structurallysmaller, so "sFOLf (Rec f1)" is not valid on the rhs.

Lars,

Thanks, GB

**Follow-Ups**:

**References**:**[isabelle] Trying to use "datatype" to restrict types of formulas used, getting error***From:*Gottfried Barrow

**Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error***From:*Gottfried Barrow

**Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error***From:*Gottfried Barrow

**Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Two questions of a beginner
- Next by Date: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Previous by Thread: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Next by Thread: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Cl-isabelle-users January 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