Re: [isabelle] Pitfall with type-classes in Isar-Lemma format



On Wed, 15 Feb 2012, Peter Lammich wrote:

Is this just an exercise in driving the system into an unspecified /
uninhabitable state, or does it have some practical significance?

I have distilled that from a practical example, that went like this:

schematic_lemma
 notes [refine_transfer] = <Some lemmas that only makes sense for this
particular refinement proof>
 shows "?concrete_program <= abstract_program"
 by (tactic that uses lemmas declared with attribute
	"refine_transfer" (which is a NamedThms structure)

BTW, the thing given as arguments to the command 'by' is called "proof method" or just "method" in Isar terminology. There are further explanations and some examples in section 6.2 of the Isabelle/Implementation manual. (The same manual also explains the traditional concept of "tactic" in Isabelle/ML, see section 4.1.)


An alternative would be to pass the lemmas as parameters to my tactic, which I have already (partially) implemented

This would indeed follow the standard convention: a method that accepts implicit arguments via the context also allows the same as explicit arguments on the spot. The my_simp' example from the quoted section 6.2 above does exactly that.


	Makarius





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