Email Gateway (Aug 16 2020 at 10:09): Email Gateway (Aug 16 2020 at 10:09):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
Email Gateway (Aug 17 2020 at 12:56):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
Email Gateway (Aug 17 2020 at 13:11):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: Jul 15 2022 at 23:21 UTC