Re: [isabelle] Automated proofs for lattices



apply (metis ge_sup_conv le_iff_sup sup_absorb1 sup_assoc sup_commute sup_ge1)

Larry

On 28 May 2010, at 14:56, 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.