Re: [isabelle] Automated proofs for lattices



Unfortunately you are right. I thought I had tried the metis call, but
had not. :-(

Tobias

Peter Lammich wrote:
> Hi
> Tobias Nipkow schrieb:
>> This is what sledgehammer (with the help of Spass and minimization)
>> gives me quite quickly:
>>
>>  by (metis le_sup_iff order_trans_rules(23) sup_ge1 sup_ge2).
>>   
> I also got something similar by sledge-hammering and minimization using
> Spass.
> However, I interrupted the metis-prover after approx 3 minutes, b/c it
> did not terminate. (I'm using Isabelle2009-1)
> For your proposal, metis also did not yet terminate within 5 minutes ...
> 
> Best and thanks,
>  Peter
> 
>> Tobias
>>
>> Peter Lammich wrote:
>>  
>>> Hi all,
>>>
>>> I have to prove the following lemma:
>>>  lemma "[| a <= sup b c; e <= sup d a |] ==> e <= sup (sup d b)
>>> (c::'a::upper_semilattice)"
>>>
>>> auto, force,blast,fast, etc cannot prove this automatically.
>>> Is there any way to prove this automatically, or to feed the right
>>> lemmas to auto?
>>>
>>>
>>> Best,
>>>  Peter
>>>     
>>
>>   






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