Search code examples
isabelle

Function termination/completeness on Isabelle

I have a locale field and the function pow_F defined as follows

function (in field)
  pow_F :: "'a ⇒ nat ⇒ 'a" where
  "pow_F x 0 = ONE_F" |
  "pow_F x (Suc n) = x ⋆ (pow_F x n)"

where ONE_F and ⋆ are the neutral one element and multiplication function defined on the field locale.

This function behaves strangely, since I can't even prove the following

lemma (in field) "pow_F x 0 = ONE_F"

despite the fact that it follows directly from the definition of pow_F. And when I run sledgehammer, the provers either give up or the timer runs out.

What is going on?

Solution

  • When you use function, you have to prove termination before you can use the pow_F.simps rules. You probably want to use fun instead (which proves termination automatically).