Email Gateway (Aug 18 2022 at 11:41): Email Gateway (Aug 18 2022 at 11:41):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
Hi:
I want to know how to print the proof procedure of auto-method in Isabelle ,for example the theroy or lemmas used by auto-method ,so I have a good understanding of the proof procedure of some theroy used in verifying security protocol.
Thanks a lot.
Jean
Email Gateway (Aug 18 2022 at 11:41):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
jwang whu.edu.cn (jwang) wrote:
The procedure is found in src/Provers/clasimp.ML, under mk_auto_tac;
it contains the use of the "blast" tactics (see blast.ML) which are very
complex.
But as for the lemmas used, auto_tac uses a "claset" and a "simpset",
the reference manual (chapters 10 and 11) tell you about these. Most
commonly you would use the default ones, possibly adding rules useful
for your particular goal. So if you need to make it work better,
first try adding relevant rules. Second try alternatives - eg force_tac
Jeremy
Last updated: May 03 2024 at 12:27 UTC