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 proof tools:

  (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 MHonArc.