Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
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
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.
I was actually looking at that last night, but with all the dots and
with other information overload, I didn't sort much of it out, so thanks
for the clarification.
I was mainly looking for examples to use as plug 'n play templates,
which can get me some progress sometimes.
Thanks to John Wickerson also for a clarification on the same subject.
This archive was generated by a fusion of
Pipermail (Mailman edition) and