How to prove that a function is total on its domain?

Question

I have the following theory:

theory Color 
imports Main 

begin 

datatype color = RED | GREEN 

function invert :: "color => color" 
where 
  "invert RED   = GREEN" 
| "invert GREEN = RED  " 
apply (pat_completeness) 
apply auto 
done 
termination by lexicographic_order 

lemma invert_univ: "invert_dom = (λx. True)"

I would like to prove that invert is total on its whole domain, so invert_dom defines the universal set on datatype color. How can proceed with this proof? Or, should I formulate this by other means?

Manuel Eberl Manuel Eberl · Accepted Answer · 2014-06-19T18:04:34

First of all, you really do not need to use function here. The termination proof for this function is trivial and can be found automatically, so you can just write

fun invert :: "color ⇒ color" 
where 
  "invert RED   = GREEN" 
| "invert GREEN = RED"

or, since it is primitively recursive on the datatype color:

primrec invert :: "color ⇒ color" 
where 
  "invert RED   = GREEN" 
| "invert GREEN = RED"

or even just

definition invert :: "color ⇒ color" where
  "invert c = (case c of RED ⇒ GREEN | GREEN ⇒ RED)"

In the last case, you have to unfold the definition of invert manually using the lemma invert_def.

Now to your actual question: technically, in HOL, every function is total. This is necessarily the case because logics in which expressions can have no value at all tend to get very messy. You can “simulate” nontotality by returning undefined on some inputs, which is some arbitrary value that you know nothing about. undefined :: int is some integer value – it could be 0, or it could be 42 or any other integer. For functions defined with the function package, this is only relevant if you let cases unspecified (e.g. by not giving an equation for one case) or if the function does not terminate on some inputs (then things get messy; if you want to do any reasoning about the function then, you have to prove it terminates on the input you give it first)

If you have given a termination proof – which you have, in this case, since the function trivially terminates – the invert_dom predicate is basically useless. You don't need it.

Otherwise, you can prove that invert_dom holds on a given input using the invert.domintros rules. Since they are rarely needed in practice, you have to switch their generation on manually, by using function (domintros) instead of function. Then you can prove the lemma you suggested like this:

lemma "invert_dom = (λ_. True)"
proof
  fix x show "invert_dom x = True"
    by (cases x) (auto intro: invert.domintros)
qed

But, again, the *_dom predicates are very rarely used in practice.

How to prove that a function is total on its domain?

1 Answers