Email Gateway (Aug 19 2022 at 08:00): Email Gateway (Aug 19 2022 at 08:00):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi people out there,
New beginner here, and so beginner's questions :-P
My first one: what's the difference between “fun” and “primrec” please ?
Both looks similar or synonymous, but surprisingly, when Main is not
imported (yes, I know it should, but that's for testing), “fun” seems not
available.
Email Gateway (Aug 19 2022 at 08:00):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Yannick,
this is not the first time this question is asked. Maybe it is best to
read through the previous discussions and come back if still questions
remain:
Search for "fun primrec" here:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/
cheers
chris
Email Gateway (Aug 19 2022 at 08:00):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
OK, thanks Christian, found something via your link.
P.S. I am using this list via a Usenet reader, and I have not imported all
of the old messages when I suscribed to
gmane.science.mathematics.logic.isabelle.user. That's the reason why I
could not know.
Email Gateway (Aug 19 2022 at 08:01):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Additionally, “isabelle2012/doc/prog-prove.pdf” also says on page 18
The attribute simp declares theorems to be simplification rules, which
the
simplifier will use automatically. In addition, datatype and fun
commands im-
plicitly declare some simplification rules: datatype the distinctness
and injec-
tivity rules, fun the defining equations.
But this does not implies primrec don't too. Will check a later day.
Email Gateway (Aug 19 2022 at 08:01):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Yannick,
a very useful command to find out what theorems are newly added as part
of some previous command (e.g., datatype, primrec, fun) is
print_theorems
(Just type it in your *.thy file directly after the command you are
interested in).
It will give a list of all the new theorems. So you will see that when
defining a function f via primrec or via fun, both times you will get
g.simps (of course it is a different matter whether those new theorems
are already included in automatic tools like 'simp', which is the case
for g.simps from "fun" and "primrec").
cheers
chris
Email Gateway (Aug 19 2022 at 08:01):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Sorry, typo: function g
Email Gateway (Aug 19 2022 at 08:29):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Answer is at “isar-ref.pdf”/10.3 (page 204 and 205)
“
primrec defines primitive recursive functions over datatypes
(see also datatype and rep datatype). The given equations
specify reduction rules […] At most one reduction rule for
each constructor can be given. […] The reduction rules are
declared as simp by default […]
function defines functions by general well‑founded recursion.
[…] The function is specified by a set of (possibly conditional)
recursive equations with arbitrary pattern matching. The command
generates proof obligations for the completeness and the compatibility
of patterns. […] The termination command can then be used to establish
that the function is total.
fun is a shorthand notation for “function (sequential ), followed
by automated proof attempts regarding pattern matching and
termination.
”
That's nearly all the basics one needs to know :-) After that, I feel it's
better to use Function only when Primrec is not enough and to use Fun only
when Function is not enough (especially if one wish to avoid to rely on
implicit automated proofs).
Last updated: Apr 30 2024 at 16:19 UTC