Re: [isabelle] Automated proofs for lattices

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)

The names of some of the theorems have changed in the meantime. Some of the steps could be simplified.


P.S. Tobias: On my machine "isar_proof" works perfectly well. I'll try to reproduce your problems on a Linux machine.

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