Re: [isabelle] Simplifier and linorder transitivity
thanks for the reply. Unfortunately, in my case splitting the goal would
yield too many new ones. I was hoping I wasn't the first one to run into
this and that somebody would have a ready-made solution.
Do you know which solvers exactly are capable of dealing with this?
Also, is there a general way to get such information from the
simplifier? simp_trace didn't seem to be useful here.
On 03/01/2013 09:06 PM, Tobias Nipkow wrote:
> Dear Ognjen,
> 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"
> apply simp
> 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