Can Isabelle lemma be used for stating fact about definition?

Question

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?

braewebb braewebb · Accepted Answer · 2021-04-10T01:38:05

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"

Can Isabelle lemma be used for stating fact about definition?

1 Answers