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



On Fri, 10 Jul 2009, 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 ...)

The prehistoric "foobarset" types have been replaced by the universal Proof.context many years ago. The simpset, claset, and clasimpset are still left in the internally for historical reasons. While simpset is practically able to emulute a proper context (cf. Simplifier.the_context etc.) the low-level entry points for claset/clasimpset based tools still prevent tool plugins (e.g. those based on the Simplifier) to refer to their proper context, causing some strange behaviour occasionally.


Anyway, the question of collecting "declarations" for rules according to different tool contexts first came up around 1999, when the original version of locales was implemented (cf. Kammüller, Paulson, Wenzel). The basic idea is as follows:

  * the context contains all the tool data
  * tools provide data declaration functions (usually as attributes)
  * the locale mechanism manages arbitrary declarations, to be activated
    in specific situations (after applying what is now called "morphism")

The following example illustrates this old idea in Isabelle2009. In particular, NamedThmsFun is used to maintain named collections of theorems, which are easier to track in the example than actual tool context data.


theory Scratch
imports Main
begin

ML {* structure Foo =
  NamedThmsFun(val name = "foo" val description = "foo rule") *}
setup Foo.setup

ML {* structure Bar =
  NamedThmsFun(val name = "bar" val description = "bar rule") *}
setup Bar.setup

locale my_decls
begin

declare sym [foo]
declare refl [bar]
declare trans [bar]

end

lemma True
proof
  thm foo
  thm bar
  interpret my_decls .
  thm foo
  thm bar
qed

end


In more recent years, we have introduced further mechanisms to maintain and activate such generic context declarations. There are plenty of possibilities, but it all depends on the specific applications how to wrap them up conveniently.

BTW, just before TPHOLs we will have a small semi-formal workshop in Munich that tries to recover the ability of Isabelle users to use ML for their applications -- among other things.


	Makarius


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