[isabelle] Simplifier and linorder transitivity



Hi,

given the following example

typedecl foo
arities foo :: linorder

lemma
  "[| (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.

Thanks,
Ognjen





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.