theory McCarthy imports Main begin
function M :: \int \ _\ where \M n = (if n > 100 then n - 10 else M (M (n + 11)))\
by simp_all
termination
proof
let ?R = \measure (\n. nat (101 - n))\
show \wf ?R\ ..
fix n :: int
assume \\ n > 100\
moreover from this show \(n + 11, n) \ ?R\
by simp
assume \M_dom (n + 11)\
moreover have \n - 10 \ M n\ if \M_dom n\ for n
using that by induct (force simp: M.psimps)
ultimately show \(M (n + 11), n) \ ?R\
by force
qed
theorem \M n = (if n > 100 then n - 10 else 91)\
by (induct n rule: M.induct) simp
end