Q:

How to prove code correctness lemmas with the "undefined" constant

Given I have a very simple definition for code generation. It is only defined for certain cases and throws a runtime exception otherwise.
definition "blubb a = (if P a then True else undefined)"

Now I want to show blubb correct. The case in which the exception is thrown should be ignored (from my point of view, not the mathematical point of view). However, I end up with a subgoal that assumes that some arbitrary value X is undefined. The following lemma is more or less equivalent to the subgoal. I want to show False as I want to ignore the case in which the exception is thrown (i.e., undefined is returned).
lemma "X = undefined ⟹ False"

This is not provable.
  try

Nitpick found a counterexample for card 'a = 1:
 Free variable:
  X = a1

What is the best way to show correctness of functions that might throw exceptions or deal with undefined?
This relates to this question.

A:

undefined is a constant in Isabelle which you don't know anything about. In particular, you can not in general prove that X ≠ undefined.
If you want to write functions that are only valid for certain inputs, you might consider using the 'a option type, as follows:
definition "blubb a ≡ (if P a then Some True else None)"

and then in your proofs assume that blubb a is defined as follows:
lemma "∃x. blubb a = Some x ⟹ Q (blubb a)"
  ...

or simply:
lemma "a ∈ dom blubb ⟹ Q (blubb a)"
  ...

The value of blubb a can then be extracted using the (blubb a).

