proving function definition correctness in Isabelle

Question

I want to prove function definition correctness using the function keyword definition. Here is the definition of an addition function on the usual inductive definition of natural numbers:

theory FunctionDefinition
imports Main

begin

datatype natural = Zero | Succ natural

function add :: "natural => natural => natural"
where 
  "add Zero     m = m"
| "add (Succ n) m = Succ (add n m)"

Isabelle/JEdit shows me the following subgoals:

goal (4 subgoals):
 1. ⋀P x. (⋀m. x = (Zero, m) ⟹ P) ⟹ (⋀n m. x = (Succ n, m) ⟹ P) ⟹ P
 2. ⋀m ma. (Zero, m) = (Zero, ma) ⟹ m = ma
 3. ⋀m n ma. (Zero, m) = (Succ n, ma) ⟹ m = Succ (add_sumC (n, ma))
 4. ⋀n m na ma. (Succ n, m) = (Succ na, ma) ⟹ Succ (add_sumC (n, m)) = Succ (add_sumC (na, ma)) 
Auto solve_direct: ⋀m ma. (Zero, m) = (Zero, ma) ⟹ m = ma can be solved directly with
  Product_Type.Pair_inject: (?a, ?b) = (?a', ?b') ⟹ (?a = ?a' ⟹ ?b = ?b' ⟹ ?R) ⟹ ?R

using

apply (auto simp add: Product_Type.Pair_inject)

I get

goal (1 subgoal):
 1. ⋀P a b. (⋀m. a = Zero ∧ b = m ⟹ P) ⟹ (⋀n m. a = Succ n ∧ b = m ⟹ P) ⟹ P

It is not clear how to proceed. At all, is this the right way to tackle this problem?

I know that Isabelle would do this automatically if I used a fun definition -- I want to learn how to do this manually .

Answer 1

The tutorial on the function package mentions in section 3 that fun f where ... abbreviates

function (sequential) f where ...
by pat_completeness auto
termination by lexicographic_order

Here pat_completeness is a proof method from the function package that automates proof of completeness for patterns of datatype constructors. This is the first subgoal that you have to prove. It is recommended to apply pat_completeness before auto, because auto changes the syntactic structure of the goal and pat_completeness might not work after auto.

If you want to prove pattern completeness without pat_completeness, you should try to do case analysis of all function parameters, i.e., case_tac a in your example.

Answer 2

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 measures, 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