Search code examples
isabelle

Conditional definition in Isabelle

Assume you want to formalize the following definition in Isabelle:

add a b = 
 if f(a,b) ≠ 0 then add_1 a b
 if g(a,b) ≠ 0 then add_2 a b

where I do not want to give any preference to any option. In fact, the next properties I need to prove are:

  1. add assigns at least one value for any input
  2. add is well-defined

what should I use to model this definition in Isabelle? Perhaps a partial function?

You can see equation (17) and lemmas 4.3.4, 4.3.4 on this paper to see what lemmas I am talking about.

Solution

  • You can use the function command with overlapping equations and preconditions:

    function add :: "..." where
  "add a b = add_1 a b" if "f a b ≠ 0"
| "add a b = add_2 a b" if "g a b ≠ 0"
apply(atomize_elim) (* makes the exhaustiveness goal more readable *)

    This gives you a proof obligations that the cases are really exhaustive and that the right hand sides denode the same when they overlap. Once you have shown this, you then must show termination (if your function is not recursive, then this is done trivially by

    termination by lexicographic_order

    If your equations are actually not exhaustive, then you first have to add more cases. In this example, you could add

    | "add a b = undefined a b" if "f a b = 0 & g a b = 0"

    which says that if both f and g are 0, then add a b shall denote some unspecified value and this value may be different for every such choice of a and b.