*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 12:08:59 -0600*In-reply-to*: <1358527720.7289.4.camel@weber>*References*: <50F85B11.4080205@gmx.com> <50F85E20.2060301@gmx.com> <50F8D10E.9000502@gmx.com> <50F8FAE2.8010205@in.tum.de> <50F96542.3020505@gmx.com> <1358527720.7289.4.camel@weber>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 1/18/2013 10:48 AM, Tjark Weber wrote:

On Fri, 2013-01-18 at 09:07 -0600, Gottfried Barrow wrote:However, it's not obvious to me why "sFOLf (Rec f1)" is not smaller. No matter what "f1" is, it looks like I should get ""sFOLf (Rec f1) = True" on the second call of sFOLf.You know that, but the primrec command doesn't. Quoting from Section 10.3 of the Isabelle/Isar reference manual (http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2012/doc/isar-ref.pdf): Each equation needs to be of the form: f x1 ... xm (C y1 ... yk) z1 ... zn = rhs such that C is a datatype constructor, rhs contains only the free variables on the left-hand side (or from the context), and all recursive occurrences of f in rhs are of the form f ... yi ... for some i.

Thanks to John Wickerson also for a clarification on the same subject. Regards, GB

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

**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:*Tjark Weber

- Previous by Date: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Next by Date: [isabelle] ADG Post-Proceedings
- 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