Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Separating local facts from rules in sledgeham...

Email Gateway (May 28 2025 at 18:35):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi all,

in an example like

notepad
begin
fix xs :: ‹'a list›
assume ‹distinct xs›
have ‹card (Pow (set xs)) = 2 ^ length xs›
…
end

sledgehammer will generate a proof similar to:

by (metis List.finite_set ‹distinct xs› card_Pow distinct_card)

Would it be possible to separate local facts (from the current proof)
from generic rules (from the surrounding context)?

using ‹distinct xs› by (metis List.finite_set card_Pow distinct_card)

The reason why I ask is that this would make such proofs easier to read
and also easier to maintain.

Cheers,
Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Email Gateway (May 28 2025 at 20:14):

From: Tobias Nipkow <nipkow@in.tum.de>
I support Florian's suggestion because I reorganize my proofs like that
manually. But I know there are only 25 hours in the day...

Tobias

On 28/05/2025 20:34, Florian Haftmann wrote:

Hi all,

in an example like

notepad
begin
  fix xs :: ‹'a list›
  assume ‹distinct xs›
  have ‹card (Pow (set xs)) = 2 ^ length xs›
    …
end

sledgehammer will generate a proof similar to:

by (metis List.finite_set ‹distinct xs› card_Pow distinct_card)

Would it be possible to separate local facts (from the current proof) from
generic rules (from the surrounding context)?

using ‹distinct xs› by (metis List.finite_set card_Pow distinct_card)

The reason why I ask is that this would make such proofs easier to read and also
easier to maintain.

Cheers,
    Florian

smime.p7s

Email Gateway (May 28 2025 at 20:42):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
We have a macro (and a keyboard shortcut) which transforms
by (metis  A B C D)
to
using A B C D metis
No distinction between local and global facts.
I find this macro close to necessary since I usually try to optimize the
proof.

Stepan

On 28-May-25 10:14 PM, Tobias Nipkow wrote:

I support Florian's suggestion because I reorganize my proofs like
that manually. But I know there are only 25 hours in the day...

Tobias

On 28/05/2025 20:34, Florian Haftmann wrote:

Hi all,

in an example like

notepad
begin
   fix xs :: ‹'a list›
   assume ‹distinct xs›
   have ‹card (Pow (set xs)) = 2 ^ length xs›
     …
end

sledgehammer will generate a proof similar to:

by (metis List.finite_set ‹distinct xs› card_Pow distinct_card)

Would it be possible to separate local facts (from the current proof)
from generic rules (from the surrounding context)?

using ‹distinct xs› by (metis List.finite_set card_Pow
distinct_card)

The reason why I ask is that this would make such proofs easier to
read and also easier to maintain.

Cheers,
     Florian

Email Gateway (Jun 04 2025 at 07:52):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Florian,

It's a good idea. I tend to do the same in my own proofs, and I'm glad to see I'm not alone. The change shouldn't be very difficult to implement, although there are some tricky aspects related to preplaying. (We don't want Sledgehammer to say "Try this:" and then the metis call fails.) I'll discuss this with Martin, who is Sledgehammer's de facto main maintainer these days.

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

On 28. May 2025, at 20:34, Florian Haftmann <florian.haftmann@cit.tum.de> wrote:

Hi all,

in an example like

notepad
begin
fix xs :: ‹'a list›
assume ‹distinct xs›
have ‹card (Pow (set xs)) = 2 ^ length xs›
…
end

sledgehammer will generate a proof similar to:

by (metis List.finite_set ‹distinct xs› card_Pow distinct_card)

Would it be possible to separate local facts (from the current proof) from generic rules (from the surrounding context)?

using ‹distinct xs› by (metis List.finite_set card_Pow distinct_card)

The reason why I ask is that this would make such proofs easier to read and also easier to maintain.

Cheers,
Florian


OpenPGP_0xA707172232CFA4E9.asc
smime.p7s

Last updated: Jun 20 2025 at 16:26 UTC