Email Gateway (Aug 18 2022 at 13:46): Email Gateway (Aug 18 2022 at 13:46):From: Stephan Merz <Stephan.Merz@loria.fr>
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 ...)
Thanks,
Stephan
Email Gateway (Aug 18 2022 at 13:46):From: Lawrence Paulson <lp15@cam.ac.uk>
I don't think there is an easy way to do this any more. But as you
say, sometimes it would be useful.
Larry
Email Gateway (Aug 18 2022 at 13:47):From: John Matthews <matthews@galois.com>
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.
-john
Email Gateway (Aug 18 2022 at 13:47):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 13:47):From: Christian Urban <urbanc@in.tum.de>
Makarius writes:
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.
People who cannot participate in this workshop might find
the Programming Tutorial helpful [1]. It explains in slow
motion attributes on page 30pp and named theorem lists
on page 35.
Christian
[1] http://isabelle.in.tum.de/nominal/activities/idp/
Last updated: Nov 21 2024 at 12:39 UTC