[isabelle] Simplifier and linorder transitivity
given the following example
arities foo :: linorder
"[| (a :: foo) <= b; b <= c |] ==> P & a <= c & Q"
I would like to simplify the conclusion to "P & Q". For int and nat,
certain arith simprocs produce the desired result, but I can't come up
with a simple way to do it for the (non-arithmetic) type foo. Any
suggestions are of course welcome.
This archive was generated by a fusion of
Pipermail (Mailman edition) and