[isabelle] Simprocs in type class locales

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