CODEWITHSUNDEEP
isabelletheorem-proving
user779130
user779130

Reputation: 11

Why Isabelle prover can't recognize a defined class?

class semigroup=
  fixes mult::"'a⇒'a⇒'a" (infixl "⊗" 70)
  assumes assoc: "(x⊗y)⊗z=x⊗(y⊗z)"

theorem main_theorem:
  fixes K::"semigroup"
  shows "∀x,y,z∈K. (x⊗y)⊗z=x⊗(y⊗z)"

The code fixes K::"semigroup" prompted an error with "Undefined type name: semigroup".

Upvotes: 0

Views: 65

Answers (1)

Mathias Fleury
Mathias Fleury

Reputation: 2261

Classes are sorts, i.e., properties on types, not type. This has two major advantages when using them. First a type can be in multiple classes. Second, two types can be in a single class. However, Isabelle does not allow you to have one type in the same class multiple times.

What does this mean for you:

class semigroup=
  fixes mult::"'a⇒'a⇒'a" (infixl "⊗" 70)
  assumes assoc: "(x⊗y)⊗z=x⊗(y⊗z)"

theorem main_theorem:
  fixes x y z ::"'a :: semigroup"
  shows "(x⊗y)⊗z=x⊗(y⊗z)"

Here is an example where you need two classes:

  fixes x y z ::"'a :: {semigroup, plus}"
  shows "(x⊗y)⊗z=x⊗(y+z)"

If you omit the sort plus, you will get the error message Variable 'a::semigroup not of sort plus.

It is more common in Isabelle to no write ∀ and instead rely on the generalization done automatically by lemma. The pure forall is also nicer to manipulate.

Upvotes: 1

Related Questions