Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Interrupt_Breakdown exception for function (do...


view this post on Zulip Email Gateway (Nov 21 2024 at 13:58):

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

view this post on Zulip Email Gateway (Nov 21 2024 at 14:32):

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
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

view this post on Zulip Email Gateway (Nov 21 2024 at 14:33):

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
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

smime.p7s

view this post on Zulip Email Gateway (Nov 21 2024 at 14:45):

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
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

view this post on Zulip Email Gateway (Nov 21 2024 at 14:52):

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
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


Last updated: Jan 04 2025 at 20:18 UTC