Re: [isabelle] Automated proofs for lattices
Unfortunately you are right. I thought I had tried the metis call, but
had not. :-(
Peter Lammich wrote:
> 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
> 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 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)
>>> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and