From: Niels Mündler <n.muendler@tum.de>

Hello everyone,

Working with the latest Isabelle distribution, I have encountered an

internal exception when using `pattern_aliases`

in combination with

`let`

statements. As a minimal breaking example, the function

"weird_swin" can be found in the code appended. Thanks to Manuel Eberl,

a non-breaking version could be formulated which can also be found,

named "not_so_weird_swin".

I am just curious whether this issue is known and suggest that the issue

should be fixed, myself having no clue what caused it.

Best regards,

Niels Mündler

Breaking.thy

From: Manuel Eberl <eberlm@in.tum.de>

I tried to track it down but failed so far. Even with ML exception trace

and ML exception debugger enabled (and Pure + HOL rebuilt), I see no

trace for the exception. Rebuilding HOL with the full ML debugger is not

feasible (doesn't terminate).

I did find out, however, that it is /not/ a problem with the function

package but rather a problem with pattern aliases. The function

definition does not use pattern aliases at all, and if you just disable

pattern aliases, the exception goes away.

Manuel

From: Manuel Eberl <eberlm@in.tum.de>

Okay, I managed to get somewhere. First of all, the problem doesn't seem

to be pattern aliases as such but a fundef_cong rule it declares:

lemma let_cong_unfolding [fundef_cong]:

"M = N ⟹ f N = g N ⟹ Let M f = Let N g"

by simp

The problem is probably due to the combination of "Let" and "case", but

I cannot see what exactly the problem is.

Minimal breaking example and exception trace below.

Manuel

theory Foo

imports "~~/src/HOL/Fun_Def"

begin

lemma let_cong_unfolding [fundef_cong]:

"M = N ⟹ f N = g N ⟹ Let M f = Let N g"

by simp

fun foo :: "nat ⇒ unit × unit" where

"foo 0 = undefined" |

"foo (Suc n) = (let (a', l') = foo n in undefined)"

end

Exception trace - exception THM 1 raised (line 700 of "drule.ML"): COMP

Function_Context_Tree.rewrite_by_tree(5)rewrite_help (line 244 of

"~~/src/HOL/Tools/Function/function_context_tree.ML")

Function_Context_Tree.rewrite_by_tree (line 242 of

"~~/src/HOL/Tools/Function/function_context_tree.ML")

Function_Core.mk_replacement_lemma (line 256 of

"~~/src/HOL/Tools/Function/function_core.ML")

Function_Core.prove_stuff (line 390 of

"~~/src/HOL/Tools/Function/function_core.ML")

Function_Core.prepare_function (line 825 of

"~~/src/HOL/Tools/Function/function_core.ML")

Function_Mutual.prepare_function_mutual (line 303 of

"~~/src/HOL/Tools/Function/mutual.ML")

Function.prepare_function (line 72 of

"~~/src/HOL/Tools/Function/function.ML")

Function.gen_add_function (line 139 of

"~~/src/HOL/Tools/Function/function.ML")

Function_Fun.gen_add_fun (line 155 of "~~/src/HOL/Tools/Function/fun.ML")

exception THM 1 raised (line 700 of "drule.ML"):

COMP

(case h_fd n of (a', l') ⇒ undefined) = (case foo_sumC n of (a', l') ⇒

undefined)

[⋀z. foo_rel z x_fd ⟹ ∃!y. foo_graph z y, x_fd = Suc n, foo_graph n

(h_fd n),

foo_rel ≡ ??.Foo.foo_rel, foo_sumC ≡ ??.Foo.foo_sumC, foo_graph ≡

??.Foo.foo_graph]

(case foo_sumC n of (a', l') ⇒ undefined) = (case foo_sumC n of (a',

l') ⇒ undefined) ⟹

let (a', l') = h_fd n in undefined ≡ let (a', l') = foo_sumC n in

undefined

[⋀z. foo_rel z x_fd ⟹ ∃!y. foo_graph z y, x_fd = Suc n, foo_graph n

(h_fd n),

foo_rel ≡ ??.Foo.foo_rel, foo_sumC ≡ ??.Foo.foo_sumC, foo_graph ≡

??.Foo.foo_graph]

Last updated: Jan 25 2022 at 02:35 UTC