Re: [isabelle] Simplifier and linorder transitivity



Dear Tobias,

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.

Best,
Ognjen

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:
> 
> 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.