Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Tactic Emulation

Email Gateway (Aug 18 2022 at 10:18):

From: Peter Chapman <pc@cs.st-and.ac.uk>
Thanks Christian

This sounds like the kind of thing I want to do, but I've hit a snag
in implementing your suggestion of writing the tactics in ML and then
using this directly in Isar.

Say I have a lemma " |- A --> A --> A --> A", then using the Isar
method of doing things, I use

apply ((rule impr)+)?

which returns

Subgoal:

A, A, A |- A

as expected. However, if I use the direct tactic from Isabelle

apply (tactic {* REPEAT (rtac impr 1) *} )

I simply get back the original goal; the rule fails to be applied
even once. This was confirmed when I tried

apply (tactic {* rtac impr 1 *} )

which fails. After scouring the manuals for both Isar (Appendix B:
Converting between Isabelle and Isar) and Isabelle (Chapters 3 and
4), I cannot figure out why the two representations do not have the
same behaviour. If it is important, the theorems are declared in a
file called G3cp.thy, which is included in the file where I am
actually performing the calculations, G3cpExamples.thy.

Thanks

Peter

Email Gateway (Aug 18 2022 at 10:19):

From: Christian Urban <urbanc@in.tum.de>
An offline discussion revealed that the problem was due to
non-existing ML-bindings for theorems one proves in ones own
theories. While theorems, like conjI from HOL, have an ML-binding
with the same name, ones own theorems must be fetched from
the theorem-database. This can be done with the functions
"thm" and "get_thm".

Christian

Peter Chapman writes:

Thanks Christian

This sounds like the kind of thing I want to do, but I've hit a snag
in implementing your suggestion of writing the tactics in ML and then
using this directly in Isar.

Say I have a lemma " |- A --> A --> A --> A", then using the Isar
method of doing things, I use

apply ((rule impr)+)?

which returns

Subgoal:

A, A, A |- A

as expected. However, if I use the direct tactic from Isabelle

apply (tactic {* REPEAT (rtac impr 1) *} )

I simply get back the original goal; the rule fails to be applied
even once. This was confirmed when I tried

apply (tactic {* rtac impr 1 *} )

which fails. After scouring the manuals for both Isar (Appendix B:
Converting between Isabelle and Isar) and Isabelle (Chapters 3 and
4), I cannot figure out why the two representations do not have the
same behaviour. If it is important, the theorems are declared in a
file called G3cp.thy, which is included in the file where I am
actually performing the calculations, G3cpExamples.thy.

Thanks

Peter

Last updated: May 03 2024 at 04:19 UTC