Re: [isabelle] Simprocs in type class locales
Indeed, it looks like the simproc you mention wasn't setup to support
local reasoning, while the transitivity reasoner for linear orders
(which is a solver and is provided at the same place) is.
Basically, what you need is the following:
- A generic data slot that receives theorems needed by the simproc.
- An attribute that is declared for these theorems in the target
context linorder, and that stores the theorems in the data slot.
- A simproc, that inspects its generic data slot and acts based on its
If you now enter a context that is, imports or interprets linorder,
the theorems are declared and the attribute pushes them into into the
data slot, from where the simproc will pick them up.
To get an idea how to do this, look at Ordering.thy, structure Orders.
This is a bit more complicated than what you need. There's also a
paper by Chaieb and Wenzel, where they elaborate this idea in the
context of algebraic simplification. You might actually want to
extend the existing structure Orders a bit instead of providing your
Quoting Andreas Lochbihler <andreas.lochbihler at kit.edu>:
I am currently moving a formalisation which resides in the theory
context, but uses the linorder type class, to the local context of
the linorder type class. My goal is to use the (transferred)
formalisation in other contexts where type class instantiation is
not possible, but locale interpretation is.
My problem now is that some proofs break when I move them from the
type class to the local context. Here is a simple example:
(* original *)
lemma "¬ (a :: 'a :: linorder) < x ==> ¬ x < a ==> f x = f a" by simp
(* moved *)
lemma (in linorder) "¬ (a :: 'a) < x ==> ¬ x < a ==> f x = f a"
simp cannot prove the second lemma. By tracing the simplifier, I
found that for the original lemma, the "antisym less" simproc in
Orderings.thy produces the rewrite rule "¬ a < x == a = x" for the
original lemma, but it does not for the new version because 'a lacks
the sort constraint linorder.
What do I have to do to make the simproc work in the local context, too?
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 023
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales
Forschungszentrum in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and