Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Show termination of function with recursive ca...

Email Gateway (Aug 22 2022 at 20:38):

From: "Max W. Haslbeck" <max.haslbeck@gmx.de>
Hi,

I want to write a function definition where I "hide" the recursive call in a let definition. I have the following minimal working example:

function test :: "nat ⇒ nat" where
"test n = (let f = test in (if n > 0 then f (n - 1) else 0))"
by pat_completeness auto
termination
apply(rule)

In the proof context all useful information to show termination is apparently lost. The output panel shows

proof (prove)
goal (2 subgoals):

1. wf ?R
2. /\n x. (x, n) ∈ ?R

Can I show termination of this function or do I have to do without the let definition?

Thanks and Gruß
Max

Email Gateway (Aug 22 2022 at 20:38):

From: Alexander Krauss <krauss@in.tum.de>
Hi Max,

Here, the static analysis in the function package fails to recognize the
arguments of the recursive calls here, since they are obscured by the
let construct.

In this case, you can guide the analysis by adding a congruence rule:

context
begin

lemma let_unfold_cong[fundef_cong]: "f x = g y ⟹ Let x f = Let y g"
by simp

fun test :: "nat ⇒ nat" where
"test n = (let f = test in (if n > 0 then f (n - 1) else 0))"

end

Disclaimer: This works nicely in this simple case, but may produce
unexpected effects in other situations.

Alex

Last updated: Apr 26 2024 at 08:19 UTC