Email Gateway (Aug 18 2022 at 18:41): Email Gateway (Aug 18 2022 at 18:41):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
I have the following definitions:
datatype Tree =
leaf1 | leaf2 | "tree" "Tree" "Tree" (infixr ".." 65)
primrec Special :: "Tree => bool" where
"Special leaf1 = True" |
"Special leaf2 = True" |
"Special (x .. y) = (case x of leaf1 => Special y | leaf2 => Special y
| (u .. v) ⇒ u = leaf1 /\ Special y /\ (Special v))"
On the definition of Special I get the error:
Extra variables on rhs: "Special"
The error(s) above occurred in definition "Special_def"
How could Special be an extra variable? Is it possible
to fix this definition?
Using fun instead of primrec seem to solve the problem,
but fun seems more general.
Best regards,
Viorel Preoteasa
Email Gateway (Aug 18 2022 at 18:41):From: Lawrence Paulson <lp15@cam.ac.uk>
That's precisely the point. There are very few reasons to prefer primrec to fun. The latter will also give you an induction rule exactly tailored to your function, and other benefits.
Larry Paulson
Email Gateway (Aug 18 2022 at 18:41):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Viorel,
your specification of Special is not primitively recursive, because the last
line calls special on the right child v of the left child x, but primitive
recursion only allows to call Special on the immediate children x and y.
Admittedly, the error message could be better.
There are two ways to solve this:
a) Since your function is not primitvely recursive, use the more general
function package. This way, you can also transform the ugly case expression into
multiple pattern matches. Moreover, fun generates custom rules for induction and
case analysis.
b) Transform your definition into primitive recursion. I think the following is
equivalent to your definition:
primrec Special :: "Tree => bool" where
"Special leaf1 = True" |
"Special leaf2 = True" |
"Special (x .. y) = (Special x /\ Special y /\
(case x of (u .. v) => u = leaf1 | _ => True))"
Andreas
Email Gateway (Aug 18 2022 at 18:41):From: Lukas Bulwahn <bulwahn@in.tum.de>
The error message might be misleading, but this function is not
primitive recursive,
in the third equation, you would only be allowed to use recursive calls
Special x and Special y, but not Special v.
One can probably reformulate it to fit the syntactic criteria of
primrec, but it certainly easier just to use fun, as Larry suggested.
Lukas
Email Gateway (Aug 18 2022 at 18:41):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Thank you all for the quick answers.
I will use "fun". I was afraid that using fun
would require providing the well founded
relation which ensures termination.
However it seems that in this case Isabelle
figures it out automatically.
Viorel
Email Gateway (Aug 18 2022 at 18:41):From: Tjark Weber <webertj@in.tum.de>
Viorel,
The Tutorial on Function Definitions
(http://isabelle.in.tum.de/dist/Isabelle2011-1/doc/functions.pdf)
contains useful descriptions of the "fun" and "function" commands.
Kind regards,
Tjark
Email Gateway (Aug 18 2022 at 18:44):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
That's precisely the point. There are very few reasons to prefer primrec to fun.
well, it's a matter of taste, but there are:
a) didactic: markup primitive recursive functions as such
b) efficiency: primrec is faster than fun
c) automation: the primrec construction always works, whereas for
function you rely on a huge stack of layers, where borderline cases you
have not foreseen could break down the whole matter (important when you
write packages with themselves define recursive functions)
d) generality: in datatypes involving higher-order arguments for
constructors, primrec may succeed, whereas function is stumbling over
those function arguments.
What I see most critical nowadays is
The latter will also give you an induction rule exactly tailored to your function, and other benefits.
e) simplicity: if you have a primitive recursive function specification
and define it by means of primrec, the reader of your theory sees that
the corresponding proof principle is structural induction on the
corresponding datatype, whereas function would suggest that a special
induction rule should apply.
None of these is a reason to artificially bend a straightforward
non-primrec specification to a primrec one.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 20:47):From: "Vromen, H.J. (Huub)" <H.Vromen@ftr.ru.nl>
I am trying to formalize David Lewis' account of common knowledge. My theory starts with:
[cid:656F2C7C9E19423CB5CB0AC3827EF818]
In line 9, I get the error message "Ill-formed equation (expected "lhs = rhs") at
⋀p. shared_reason_to_believe 0 p ≡ λw. ∀i. R i p w".
Could someone tell me what I am doing wrong?
Huub Vromen
Radboud University-Nijmegen, Department of Philosophy
Room E 16.11
Erasmusplein 1, 6525 HT Nijmegen, Netherlands
Attachment.tiff
Email Gateway (Aug 22 2022 at 20:47):From: Dominic Mulligan <Dominic.Mulligan@arm.com>
Hi Huub,
Email Gateway (Aug 22 2022 at 20:48):From: Makarius <makarius@sketis.net>
I find it difficult to see anything on this low-resolution screen shot.
Why not make a proper copy-paste of the source text?
You probably merely need to use HOL equality "=" in the proper way. In
applications you rarely see the Pure equality "==" or "≡", although some
users like to confuse other users and (ab)use the latter for its
sometimes more convenient syntax precedence.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC