Re: [isabelle] Simprocs in type class locales

Hi Andreas,

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 content.

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 own.


Quoting Andreas Lochbihler <andreas.lochbihler at>:

Hi all,

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
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
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 MHonArc.