Email Gateway (Aug 18 2022 at 18:09): Email Gateway (Aug 18 2022 at 18:09):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
Usually, after a function f has been defined via fun or primrec, its
defining equations are available under the name
f.simps as theorems, e.g., thm "f.simps".
However, how could I access specifically each one of these equations
(simplification rules)?
I tried something as f.simps_1 (after seeing the trace example in the
tutorial), f.simps_2, etc., but
it did not work.
Thanks!
Email Gateway (Aug 18 2022 at 18:09):From: Randy Pollack <rpollack@inf.ed.ac.uk>
f.simps(2)
Email Gateway (Aug 18 2022 at 18:09):From: Alfio Martini <alfio.martini@acm.org>
Great!! Thanks for the quick reply!
Email Gateway (Aug 18 2022 at 18:09):From: Alexander Krauss <krauss@in.tum.de>
You can also name the rules at definition time:
fun/primrec f :: "..."
where
name1: "..."
| name2: "..."
Alex
Email Gateway (Aug 18 2022 at 18:09):From: Alfio Martini <alfio.martini@acm.org>
Hi Alexander,
This is also very nice, because one now can refer to the specific rule
as f.name1 and so on. Very helpful.
Many thanks again!
Email Gateway (Aug 18 2022 at 18:10):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
In order to keep it in the same thread, I am pasting an answer Alexander
gave me about a remaining doubt I had concerning the main topic of all
these messages.
Best!
----------------------------------------------xxxxxxxx--------------------------------------------------
Hi Alfio,
I have small problem. Using 'primrec" I can access the individual rules
Last updated: Apr 19 2024 at 20:15 UTC