Re: [isabelle] Simplifier and linorder transitivity



Dear Ognjen,

There are a number of so called solvers that know about ordering type classes.
For example, this works:

lemma
  "[| (a :: foo) <= b; b <= c; c <= d |] ==> ~ d < a"
apply simp

However, subformulas that are true are not simplified away, only whole
propositions are proved.

Best
Tobias


Am 01/03/2013 17:25, schrieb Ognjen Maric:
> 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.