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



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.

Best regards,
Tjark






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