Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?



On Wed, 25 Jan 2012, Nils Jähnig wrote:

I try to rewrite an apply-style proof into a tactic, for future
automization.

Appendix C of the "isar-ref" manual explains the correspondence of ML tactic expressions and Isar proof methods a little. It was originally written to help converting old ML proof scripts, which are now obsolete and hardly ever encountered in recent years, but it also helps in the other direction.

The "implementation" manual explains further things about rules and tactics from the bottom up. The important FOCUS combinator has already been mentioned -- it is based on Isar structuring principles in ML, and is able to get rid of most res_inst_tac applications in practice. For plain thm instantiation you mainly use Thm.instantiate, despite various later attempts (mostly outdated now) to produce more convenient alternatives.


	Makarius


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