Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Left-open bundle in Leftist_Heap causing problems

Email Gateway (Dec 08 2025 at 17:57):

From: Peter Lammich <lammich@in.tum.de>

Hello List,

the "HOL-Data_Structures.Leftist_Heap" contains an

unbundle pattern_aliases

at top level. This, unfortunately, causes problems with function
definitions later, see below for boiled-down example.

Workaround: use "case ... of (_,_) => _" instead of "let (_,_) = ... in".

Why not restrict opening the bundle to a local context? Anyway, this
might also be a deeper issue with Pattern_Aliases here?

--

Peter

(Note, this is not a regression against 2025-1, it already occurs in
Isabelle2025)

imports Main "HOL-Data_Structures.Leftist_Heap"
begin

fun bfs :: "nat ⇒ unit × unit" where
  "bfs 0 = ((),())"
| "bfs (Suc n) = (let (V,F) = bfs n in ((),()))"

exception THM 1 raised (line 706 of "drule.ML"):
  COMP
  (case h_fd n of (V, F) ⇒ ((), ())) = (case bfs_sumC n of (V, F) ⇒
((), ()))
    [⋀z. bfs_rel z x_fd ⟹ ∃!y. bfs_graph z y, x_fd = Suc n, bfs_graph n
(h_fd n),
      bfs_rel ≡ ??.Week5_Heaps.bfs_rel, bfs_sumC ≡
??.Week5_Heaps.bfs_sumC, bfs_graph ≡ ??.Week5_Heaps.bfs_graph]
  (case bfs_sumC n of (V, F) ⇒ ((), ())) = (case bfs_sumC n of (V, F) ⇒
((), ())) ⟹
  let (V, F) = h_fd n in ((), ()) ≡ let (V, F) = bfs_sumC n in ((), ())
    [⋀z. bfs_rel z x_fd ⟹ ∃!y. bfs_graph z y, x_fd = Suc n, bfs_graph n
(h_fd n),
      bfs_rel ≡ ??.Week5_Heaps.bfs_rel, bfs_sumC ≡
??.Week5_Heaps.bfs_sumC, bfs_graph ≡ ??.Week5_Heaps.bfs_graph]

Email Gateway (Dec 09 2025 at 09:25):

From: Tobias Nipkow <nipkow@in.tum.de>

Thanks, yes, pattern_aliases is too naive here. I'll look into it (later).

Tobias

On 08/12/2025 18:56, Peter Lammich wrote:

Hello List,

the "HOL-Data_Structures.Leftist_Heap" contains an

unbundle pattern_aliases

at top level. This, unfortunately, causes problems with function definitions
later, see below for boiled-down example.

Workaround: use "case ... of (_,_) => _" instead of "let (_,_) = ... in".

Why not restrict opening the bundle to a local context? Anyway, this might also
be a deeper issue with Pattern_Aliases here?

--

Peter

(Note, this is not a regression against 2025-1, it already occurs in Isabelle2025)

imports Main "HOL-Data_Structures.Leftist_Heap"
begin

fun bfs :: "nat ⇒ unit × unit" where
  "bfs 0 = ((),())"
| "bfs (Suc n) = (let (V,F) = bfs n in ((),()))"

---

exception THM 1 raised (line 706 of "drule.ML"):
  COMP
  (case h_fd n of (V, F) ⇒ ((), ())) = (case bfs_sumC n of (V, F) ⇒ ((), ()))
    [⋀z. bfs_rel z x_fd ⟹ ∃!y. bfs_graph z y, x_fd = Suc n, bfs_graph n (h_fd n),
      bfs_rel ≡ ??.Week5_Heaps.bfs_rel, bfs_sumC ≡ ??.Week5_Heaps.bfs_sumC,
bfs_graph ≡ ??.Week5_Heaps.bfs_graph]
  (case bfs_sumC n of (V, F) ⇒ ((), ())) = (case bfs_sumC n of (V, F) ⇒ ((),
())) ⟹
  let (V, F) = h_fd n in ((), ()) ≡ let (V, F) = bfs_sumC n in ((), ())
    [⋀z. bfs_rel z x_fd ⟹ ∃!y. bfs_graph z y, x_fd = Suc n, bfs_graph n (h_fd n),
      bfs_rel ≡ ??.Week5_Heaps.bfs_rel, bfs_sumC ≡ ??.Week5_Heaps.bfs_sumC,
bfs_graph ≡ ??.Week5_Heaps.bfs_graph]

smime.p7s

Last updated: Dec 21 2025 at 20:24 UTC