Re: [isabelle] Simplifier and linorder transitivity
There are a number of so called solvers that know about ordering type classes.
For example, this works:
"[| (a :: foo) <= b; b <= c; c <= d |] ==> ~ d < a"
However, subformulas that are true are not simplified away, only whole
propositions are proved.
Am 01/03/2013 17:25, schrieb Ognjen Maric:
> given the following example
> typedecl foo
> 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