Re: [isabelle] Structured induction with custom tactics
On Sat, 13 Feb 2010, Christian Urban wrote:
To give more help, maybe it would be helpful if you describe exactly
what you like to do. In your last email you described your problem in
abstract terms. Judging from the absence of replies, it seems nobody was
able to give an appropriate answer. Maybe a concrete example or even a
small theory file would be more helpful....
According to Stefan Berghofer, this is how to implement sophisticated
(1) Make some typical examples (in plain Isar source language).
(2) You see the general idea.
(3) Implement the general idea in ML.
Steps 2 and 3 are not so trivial. I recommend to take the concrete Isar
proofs and inspect intermediate situations with Isar.goal(), Isar.state()
etc. in ML. Don't try to reconstruct situtions in ML by hand, let Isar
produce them and merely look at the results.
For the actual goal manipulation part, combinators like SUBPROOF or
Subgoal.FOCUS can be helpful, beause they represent Isar structure quite
closely at the ML level.
This archive was generated by a fusion of
Pipermail (Mailman edition) and