CODEWITHSUNDEEP
isabelle
TomR
TomR

Reputation: 3056

How to include statement about type of the variable in the Isabelle/HOL term

I have following simple Isabelle/HOL theory:

theory Max_Of_Two_Integers_Real
  imports Main
    "HOL-Library.Multiset"
    "HOL-Library.Code_Target_Numeral"
    "HOL-Library.Code_Target_Nat"
    "HOL-Library.Code_Abstract_Nat"
begin

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)"

lemma spec_final:
  fixes a :: nat and b :: nat
  assumes "a > b" (* and "b < a" *)
  shows "two_integer_max_case_def a b = a"
  using assms by (simp add: two_integer_max_case_def_def) 

lemma spec_1:
  fixes a :: nat and b :: nat
  shows "a > b ⟹ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def) 

lemma spec_2:
  shows " (a ∈ nat set) ∧ (b ∈ nat set) ∧  (a > b) ⟹ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

end

Three lemmas try to express and prove that same statement, but progressively I am trying to move information from assumes and fixes towards the term. First 2 lemmas are correct, but the third (last) lemma is failing syntactically with the error message:

Type unification failed: Clash of types "_ ⇒ _" and "int"

Type error in application: incompatible operand type

Operator:  nat :: int ⇒ nat
Operand:   set :: ??'a list ⇒ ??'a set

My aim in this lemma is to move type information from the fixes towards the term/statement? How I make statements about the type of variable in the term (of inner syntax)?

Maybe I should use, if I am trying to avoid fixes clause (in which the variables may be declared), the full ForAll expression like:

lemma spec_final_3:
  shows "∀ a :: nat . ∀ b :: nat . ( (a > b) ⟹ two_integer_max_case_def a b = a)"
  by (simp add: two_integer_max_case_def_def)

But it is failing syntactically as well with the error message:

Inner syntax error: unexpected end of input⌂
Failed to parse prop

So - is it possible to include type statements in the term directly (without fixes clause) and is there any difference between fixes clause and type statement in the term? Maybe such differences start to appear during (semi)automatic proofs, e.g., when simplification tactics are applied or some other tactics?

Upvotes: 0

Views: 269

Answers (1)

Alexander Kogtenkov
Alexander Kogtenkov

Reputation: 5810

nat set is interpreted as a function (that does not type correctly). The set of natural numbers can be expressed as UNIV :: nat set. Then, spec_2 reads

lemma spec_2:
  shows "a ∈ (UNIV :: nat set) ∧ b ∈ (UNIV :: nat set) ∧ a > b ⟹
         two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

However, more natural way would be to include the type information in spec_1 without fixes clause:

lemma spec_1':
  shows "(a :: nat) > (b :: nat) ⟹ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

∀ belongs to HOL, so the HOL implication should be used in spec_final_3:

lemma spec_final_3:
  shows "∀ a :: nat. ∀ b :: nat. a > b ⟶ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

spec_1 can also be rewritten using an explicit meta-logic qualification (and implication) to look similar to spec_final_3:

lemma spec_1'':
  shows "⋀ a :: nat. ⋀ b :: nat. a > b ⟹ two_integer_max_case_def a b = a"
  by (simp add: two_integer_max_case_def_def)

Upvotes: 3

Related Questions