Manuel already mentioned it in his comment, but I thought a more detailed example might be helpful anyway. Here is what you can do manually:
First you specify your function as usual
function add :: "natural => natural => natural"
where
"add Zero m = m" |
"add (Succ n) m = Succ (add n m)"
and then you prove that the given patterns cover all cases by
by (pat_completeness) auto
Afterwards you take care of termination. E.g., every datatype
comes with a size
function and you might note that the first argument of add
strictly decreases in size for every recursive call. By default function
will bundle all arguments of a function into a tuple for a termination proof, i.e., instead of two arguments n
and m
, in the termination proof you work with the single pair (n, m)
. Thus if you want to tell the system that it should use the size of the first argument you can do this as follows:
termination add
apply (relation "measure (size o fst)")
This will yield the remaining goals:
goal (2 subgoals):
1. wf (measure (size o fst))
2. !!n m. ((n, m), Succ n, m) : measure (size o fst)
That is, you have to show that the given relation is well-founded (which is trivial for measure
s, which are always well-founded, since they are constructed by mapping arguments to natural numbers and then using less-than on the naturals as relation) and that for every recursive call the arguments are actually in the given relation. Both goals are easily dispatched by simp
.
apply simp
apply simp
done