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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and