Stream: General

Topic: Isabelle's fun package raises an exception

irvin (Jan 29 2026 at 10:33):

I've noticed that isabelle raises an exception given this function

function test :: "nat ⇒ nat" where
"test n = (if n = 0 then 0 else
          let x = (λn. test n) in
          test (x (n - 1)))"

I'm not sure whether it's worth reporting since the condition generated is going to be impossible to prove anyway see this which succeeds but can't be proved.

function test :: "nat ⇒ nat" where
"test n = (if n = 0 then 0 else
          let x = (λn. test n) in
          (x (n - 1)))"

irvin (Jan 29 2026 at 10:50):

The package also raises exceptions when you give bad fundef_cong rules but that's also kinda to be expected

Fabian Huch (Jan 29 2026 at 11:37):

This is surely worth reporting, especially because it can be broken to relatively simple functions, e.g.

fun f :: "nat ⇒ nat" where
  "f 0 = 0" |
  "f _ = (let x = f in f 0)"

irvin (Jan 29 2026 at 11:40):

Isn't f still unprovable due to how the let cong rule works

Fabian Huch (Jan 29 2026 at 11:44):

Not sure what you mean by that

Fabian Huch (Jan 29 2026 at 11:44):

Surely one can always remove the let e.g. via Let_const rule?

Fabian Huch (Jan 29 2026 at 11:46):

In any case, throwing a raw exception is not good

irvin (Jan 29 2026 at 11:46):

function test :: "nat ⇒ nat" where
"test n = (if n = 0 then 0 else
          let x = test in
          (x (0)))"
   apply pat_completeness
  by auto
termination test
  apply(relation "measure id ")
  apply auto (*the goal here is unprovable *)

irvin (Jan 29 2026 at 11:48):

lemma let_cong [fundef_cong]: "M = N ⟹ (⋀x. x = N ⟹ f x = g x) ⟹ Let M f = Let N g"

The issue here is that M = N is not restricted

irvin (Jan 29 2026 at 11:48):

And you can't restrict a cong rule this way

irvin (Jan 29 2026 at 11:52):

Maybe @Alexander Krauss knows how to make the fun package support this?

irvin (Jan 29 2026 at 11:54):

Fabian Huch said:

Surely one can always remove the let e.g. via Let_const rule?

If you inline by removing the let it's provable i think

irvin (Jan 29 2026 at 11:55):

But you can't inline unconditionally without having to fix back the induction rule

Kevin Kappelmann (Jan 29 2026 at 12:01):

You can use an alternative congruence rule for let:

lemma let_cong_alt [fundef_cong]: "f x = g y ⟹ Let x f = Let y g" by auto

function test :: "nat ⇒ nat" where
"test n = (if n = 0 then 0 else
          let x = test in x 0)"
by auto
termination by (relation "measure id ") auto

irvin (Jan 29 2026 at 12:03):

Do you know how to phrase the MAP cong rule for this?

function test :: "nat ⇒ nat" where
"test n = (if n = 0 then 0 else
          hd (map (λf. f (n - 1)) [test]))"

Kevin Kappelmann (Jan 29 2026 at 12:11):

lemma map_cong_single [fundef_cong]: "f x = g y ⟹ map f [x] = map g [y]"
by auto

Fabian Huch (Jan 29 2026 at 14:29):

irvin said:

And you can't restrict a cong rule this way

You can just ignore the variable, e.g. with "f = g ⟹ Let x (λ_. f) = Let y (λ_. g)". With that, the function package works of course, but raising a THM 0 instead of reporting that it could not find termination is not great IMO.

Last updated: Feb 06 2026 at 20:37 UTC