I have Isabelle definition:
definition two_integer_max_case_def :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case_def a b = (case a > b of True ⇒ a | False ⇒ b)"
with output
consts
two_integer_max_case_def :: "nat ⇒ nat ⇒ nat
And I can get value from this definition:
value "two_integer_max_case_def 3 4"
with output:
"4"
:: "nat"
So, this is recognizable and correct expression/term. But I tried to declare lemma using this definition:
lemma spec_1:
assumes "a: nat" "b: nat" "a > b"
shows "two_integer_max_case_def a b = a"
Unfortunately, this lemma is not accepted (no goals/subgoals are generated) and instead the error message is given:
Type unification failed: Clash of types "_ ⇒ _" and "_ set"
Type error in application: incompatible operand type
Operator: (∈) a :: ??'a set ⇒ bool
Operand: nat :: int ⇒ nat
What is wrong with my lemma? Am I just using incorrectly equality operation (maybe there are some subtleties - confusion of nat instances with sets of nat) or is it more general problem? Maybe I am not allowed to state theorems/lemmas for (possibly interminating) definitions and I can state lemmas only for functions for which the termination proof has been already done (at the time of statement of function)?
Is it possible to correct (in case if lemma can be stated for definition) my lemma so it gets accepted and generates goals for proof?
There is nothing inherently wrong with the lemma you propose, the only issue here is how the types of a and b are declared.
The expression a: nat is interpreted as a ∈ nat which produces a type error. The error message you're seeing says that the second argument to the ∈ operator, nat, should be of type 'a set but is int => nat.
In order to declare the types of variables in a lemma you can use the fixes keyword as below.
lemma spec_1:
fixes a :: nat and b :: nat
assumes "a > b"
shows "two_integer_max_case_def a b = a"