Measure functions

The idea of a measure function, is to take every possible tuple of arguments, and map each of them to a natural number, such that each subsequent call maps to a smaller number. For example, consider Euler's GCD function:

$$\text{gcd}(a, b) = \begin{cases} \text{gcd}(a\mathop{\text{mod}}b, a) & \text{if }b \ne 0 \\ a & \text{otherwise} \end{cases}$$

This function cannot be show to terminate by a lexicographic ordering argument, so we need to find a measure function. Call the \(\text{gcd}\) arguments \((a, b),\) and the new arguments \((a', b').\) Notice that neither \(a'\) nor \(b'\) can be larger than \(a\) or \(b.\) Also, notice that either \(a'\) or \(b'\) is less \(a\) or \(b.\) Thus, a simple measure function, to prove \(\text{gcd}\) terminates, is \(m(a, b) = a + b.\)

---

theory Scratch imports Main begin

function gcd :: "nat ⇒ nat ⇒ nat" where
"gcd a b = (if b ≠ 0 then gcd (a mod b) a else a)"
apply auto
done

termination gcd
apply lexicographic_order
oops

termination gcd
apply (relation "measure (λ(a, b). a + b)")
apply simp
apply (subst in_measure)
apply clarify
apply (simp only: add_ac(2) nat_add_left_cancel_less)
apply (rule mod_less_divisor)
apply assumption
done

end