Email Gateway (Aug 18 2022 at 17:06): Email Gateway (Aug 18 2022 at 17:06):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Email Gateway (Aug 18 2022 at 17:08):From: Clemens Ballarin <ballarin@in.tum.de>
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:
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.
Clemens
Quoting Andreas Lochbihler <andreas.lochbihler@kit.edu>:
Last updated: Nov 21 2024 at 12:39 UTC