From: Sarah Tilscher <sarah.tilscher@tum.de>
Dear isabelle developers,
When defining a fixpoint algorithm using the function package and its
domintros option, I get an Interrupt_Breakdown exception already after
proving the pattern completeness. I extracted the following small (but
not anymore meaningful) example:
theory Scratch
imports Main
begin
definition lookup_default :: "('x, nat) map ⇒ 'x ⇒ nat" where
"lookup_default σ x ≡ case σ x of Some v ⇒ v | None ⇒ 0"
function (domintros)
iterate :: "'x ⇒ ('x, nat) map ⇒ nat"
where
"iterate x σ = (
let d_new = lookup_default σ x in
if lookup_default σ x = d_new then
iterate x (σ(x ↦ lookup_default σ x))
else 0)"
apply auto
done (* Interrupt_Breakdown exception thrown *)
end
Does someone know why/where this exception is thrown? Any idea how to
fix or circumvent this?
Thanks,
Sarah
From: Kevin Kappelmann <kevin.kappelmann@tum.de>
I have no idea, but here is a shorter example:
function (domintros) f :: "'a ⇒ 'a" where
"f x = (let x' = x in if x = x' then f x else x)"
apply auto
done
On 21.11.24 14:50, Sarah Tilscher wrote:
Dear isabelle developers,
When defining a fixpoint algorithm using the function package and its
domintros option, I get an Interrupt_Breakdown exception already after
proving the pattern completeness. I extracted the following small (but
not anymore meaningful) example:theory Scratch
imports Main
begindefinition lookup_default :: "('x, nat) map ⇒ 'x ⇒ nat" where
"lookup_default σ x ≡ case σ x of Some v ⇒ v | None ⇒ 0"function (domintros)
iterate :: "'x ⇒ ('x, nat) map ⇒ nat"
where
"iterate x σ = (
let d_new = lookup_default σ x in
if lookup_default σ x = d_new then
iterate x (σ(x ↦ lookup_default σ x))
else 0)"
apply auto
done (* Interrupt_Breakdown exception thrown *)end
Does someone know why/where this exception is thrown? Any idea how to
fix or circumvent this?Thanks,
Sarah
From: Tobias Nipkow <nipkow@in.tum.de>
Hi Sarah,
It it looks like something in the function definition command does not terminate
(and is forcefully terminated by the system, I suspect). Of course that
shouldn't happen. This particular example can be fixed by expanding the "let".
(you can always recover the original version later on as a lemma).
Tobias
On 21/11/2024 14:50, Sarah Tilscher wrote:
Dear isabelle developers,
When defining a fixpoint algorithm using the function package and its domintros
option, I get an Interrupt_Breakdown exception already after proving the pattern
completeness. I extracted the following small (but not anymore meaningful) example:theory Scratch
imports Main
begindefinition lookup_default :: "('x, nat) map ⇒ 'x ⇒ nat" where
"lookup_default σ x ≡ case σ x of Some v ⇒ v | None ⇒ 0"function (domintros)
iterate :: "'x ⇒ ('x, nat) map ⇒ nat"
where
"iterate x σ = (
let d_new = lookup_default σ x in
if lookup_default σ x = d_new then
iterate x (σ(x ↦ lookup_default σ x))
else 0)"
apply auto
done (* Interrupt_Breakdown exception thrown *)end
Does someone know why/where this exception is thrown? Any idea how to fix or
circumvent this?Thanks,
Sarah
From: mohammad.abdulaziz8@gmail.com
Having an equation and its flipped version causes the simplifier to not
terminate. The following works:
function (domintros) f :: "'a ⇒ 'a" where
"f x = (let x' = x in if x' = x then f x else x)"
by (pat_completeness) auto
Mohammad
On 21/11/2024 14:27, Kevin Kappelmann wrote:
I have no idea, but here is a shorter example:
function (domintros) f :: "'a ⇒ 'a" where "f x = (let x' = x in if x = x' then f x else x)" apply auto done
On 21.11.24 14:50, Sarah Tilscher wrote:
Dear isabelle developers,
When defining a fixpoint algorithm using the function package and its
domintros option, I get an Interrupt_Breakdown exception already after
proving the pattern completeness. I extracted the following small (but
not anymore meaningful) example:theory Scratch
imports Main
begindefinition lookup_default :: "('x, nat) map ⇒ 'x ⇒ nat" where
"lookup_default σ x ≡ case σ x of Some v ⇒ v | None ⇒ 0"function (domintros)
iterate :: "'x ⇒ ('x, nat) map ⇒ nat"
where
"iterate x σ = (
let d_new = lookup_default σ x in
if lookup_default σ x = d_new then
iterate x (σ(x ↦ lookup_default σ x))
else 0)"
apply auto
done (* Interrupt_Breakdown exception thrown *)end
Does someone know why/where this exception is thrown? Any idea how to
fix or circumvent this?Thanks,
Sarah
From: Sarah Tilscher <sarah.tilscher@tum.de>
Thank you for looking into this! I also just found out, that flipping
the condition in the if-statement avoids the problem. This also works
for my original definition. Inlining the let-definition is a bit more
cumbersome, because it is used in several places.
Sarah
On 21.11.24 15:45, mohammad.abdulaziz8@gmail.com wrote:
Having an equation and its flipped version causes the simplifier to not
terminate. The following works:
function (domintros) f :: "'a ⇒ 'a" where "f x = (let x' = x in if x' = x then f x else x)" by (pat_completeness) auto
Mohammad
On 21/11/2024 14:27, Kevin Kappelmann wrote:
I have no idea, but here is a shorter example:
function (domintros) f :: "'a ⇒ 'a" where "f x = (let x' = x in if x = x' then f x else x)" apply auto done
On 21.11.24 14:50, Sarah Tilscher wrote:
Dear isabelle developers,
When defining a fixpoint algorithm using the function package and its
domintros option, I get an Interrupt_Breakdown exception already
after proving the pattern completeness. I extracted the following
small (but not anymore meaningful) example:theory Scratch
imports Main
begindefinition lookup_default :: "('x, nat) map ⇒ 'x ⇒ nat" where
"lookup_default σ x ≡ case σ x of Some v ⇒ v | None ⇒ 0"function (domintros)
iterate :: "'x ⇒ ('x, nat) map ⇒ nat"
where
"iterate x σ = (
let d_new = lookup_default σ x in
if lookup_default σ x = d_new then
iterate x (σ(x ↦ lookup_default σ x))
else 0)"
apply auto
done (* Interrupt_Breakdown exception thrown *)end
Does someone know why/where this exception is thrown? Any idea how to
fix or circumvent this?Thanks,
Sarah
Last updated: Jan 04 2025 at 20:18 UTC