Email Gateway (Aug 18 2022 at 15:48): Email Gateway (Aug 18 2022 at 15:48):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hi,
I want to understand the hoare_tac.ML (to customize it). the vcg
method is setup at the end of the linked file
http://isabelle.in.tum.de/library/HOL/Hoare/Hoare_Logic.html
and it uses the Scan struct (somehow a parser). is there a
documentation/reference for this Scan? i only found several theories
using it for 'method_setup', and in none of the manuals.
i found something called scan.ML in src/HOL/Import, and there is a
function called succeed (as in the call in the file above) in line
117, but it takes two arguments, whereas in the call there is only one
argument.
my next question is, if there is a reference (or someone can explain
me) the SIMPLE_METHOD' construct.
Best Regards
Nils
Email Gateway (Aug 18 2022 at 15:48):From: Stefan Berghofer <berghofe@in.tum.de>
Nils Jähnig wrote:
Hi Nils,
I would recommend reading chapter 5 of the "Isabelle Cookbook"
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf
There is also an example theory explaining how to use parsers in connection
with methods available at
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/cambridge%20tutorial/raw-file/tip/T05_Methods.thy
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 15:48):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Nils,
there is the Isabelle Cookbook, a tutorial for programming Isabelle at
the ML level, from the Isabelle documentation project at:
http://isabelle.in.tum.de/nominal/activities/idp/
It explains what Scan and SIMPLE_METHOD are good for and how they are
typically used.
Hope this helps,
Andreas
Nils Jähnig schrieb:
Email Gateway (Aug 18 2022 at 15:52):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hi Stefan, hi Andreas,
thank you for this link. the cook book seems really helpful, if not
even exactly what I needed.
i think there should be a link on the Isabelle website, even if it is
only a draft.
Greetings
Nils
Last updated: Apr 25 2024 at 08:20 UTC