Re: [isabelle] Generalized elimination rule?



Stephan Merz wrote:
I second this request. More precisely, I'd like to be able to annotate a rule such that it is applied by the automatic proof methods only if the first n hypotheses are present in the current proof state. As a simple example, consider bspec, which would make a perfect elimination rule when its two assumptions can be proved by assumption. As others have pointed out, it is not hard to write a tactic that applies a rule only if the first n hypotheses can be proved by assumption, however, I don't know how to make such a tactic work inside auto and friends.

Thanks,
Stephan
Stephan,

This is described in Section 10.4 of the Reference Manual. (NOT the Isar reference manual, the Isabelle Reference Manual). For bspec, addSD2 is exactly what you want. (or maybe addD2). Modifying the current claset (or creating a new one) is used by all the tactics involving the classical reasoning set, eg safe_tac, clarify_tac, auto_tac, force_tac

Jeremy






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