Re: [isabelle] collections of rules for automatic proof methods

I would definitely find this useful. It might be hard to support fully general attribute lists, but even just having Isar syntax to support simpsets and clasets as first-class values would be helpful.


On Jul 10, 2009, at 3:24 AM, Stephan Merz wrote:

I would sometimes like to define collections of rules that could be given to automatic proof methods in one fell swoop, say

lemmas myRules = intro1 [intro] elim1 elim2 [elim] simp1 simp2 simp3 [simp]

in preparation for

by (auto add: myRules)

While I can give a name to a list of lemmas, I haven't found a way to tag them with attributes that would later be exploited by the automatic methods, i.e. the best I can do is something like

lemmas myRulesI = intro1
lemmas myRulesE = elim1 elim2
lemmas myRulesS = simp1 simp2 simp3

by (auto intro: myRulesI elim: myRulesE simp add: myRulesS)

Did I miss something? Would such a facility be useful? (In prehistory, one could define "clasimpsets", bind them to ML identifiers, and merge them later. Maybe this is still somehow available, but it's clumsy and it goes against the spirit of the current proof language ...)

Stephan Merz, INRIA Nancy & LORIA
Stephan.Merz at

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