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?
Andreas
--
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
http://pp.info.uni-karlsruhe.de

`KIT - Universität des Landes Baden-Württemberg und nationales
``Forschungszentrum in der Helmholtz-Gemeinschaft
`