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