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

Last updated: May 30 2025 at 04:27 UTC