Re: [isabelle] resolve current subgoal with matching premise



Am 05.12.2014 um 15:24 schrieb Christian Sternagel <c.sternagel at gmail.com>:

> For a manual proof in Isar I completely agree. However, this is just a single example of many that are automatically generated inside a package. And the tactic should work for all generated goals (whose shape depends on the underlying datatype). For making the tactic structured - also I might be wrong since I never tried very hard - it seemed that I would have to do a lot of awkward code about how many premises and IHs are there and at what positions do they fit together etc. I had at least the feeling that such things should be left to some automatic search. But of course I would be delighted to be convinced otherwise.

This might be one of those cases where "Subgoal.FOCUS" and friends can be used. I often avoid it due to its treatment of schematics, but it sounds like what you are looking for. Perhaps someone who has experience with calling it from tactics could comment more on this?

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.