*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Automated proofs for lattices*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Fri, 28 May 2010 16:26:45 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Tobias Nipkow <nipkow at in.tum.de>*In-reply-to*: <4BFFCB7E.1050701@uni-muenster.de>*References*: <4BFFC725.3020600@uni-muenster.de> <4BFFCA42.4030409@in.tum.de> <4BFFCB7E.1050701@uni-muenster.de>

Hi Peter, > 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 Using the lattest repository version of Isabelle, I invoked Sledgehammer with the "[isar_proof, isar_shrink_factor = 2]" options and got the following structured proof, which is quite fast to process: proof - assume A1: "a \<le> sup b c" assume "e \<le> sup d a" hence F1: "\<forall>u\<ge>sup d a. e \<le> u" by (metis xtrans(6)) have F2: "\<forall>u. a \<le> sup (sup b c) u" by (metis A1 sup_ge1 xtrans(6)) have "\<forall>u. a \<le> u \<and> d \<le> u \<longrightarrow> e \<le> u" by (metis F1 le_supI semilattice_sup_class.sup.commute) hence "e \<le> sup b (sup c d)" by (metis F2 le_supE semilattice_sup_class.sup.assoc sup_ge2) hence "e \<le> sup c (sup b d)" by (metis semilattice_sup_class.sup.left_commute) thus "e \<le> sup (sup d b) c" by (metis semilattice_sup_class.sup.commute) qed The names of some of the theorems have changed in the meantime. Some of the steps could be simplified. Jasmin P.S. Tobias: On my machine "isar_proof" works perfectly well. I'll try to reproduce your problems on a Linux machine.

**References**:**[isabelle] Automated proofs for lattices***From:*Peter Lammich

**Re: [isabelle] Automated proofs for lattices***From:*Tobias Nipkow

**Re: [isabelle] Automated proofs for lattices***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Automated proofs for lattices
- Next by Date: [isabelle] New AFP entries: Data Refinement and Graph Marking
- Previous by Thread: Re: [isabelle] Automated proofs for lattices
- Next by Thread: Re: [isabelle] Automated proofs for lattices
- Cl-isabelle-users May 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list