CODEWITHSUNDEEP
setisabellemlhol
Jonas
Jonas

Reputation: 75

Function that constructs a Set of all elements that statisfy a given condition in Isabelle

I am trying to learn set construction in Isabelle but I am failing. Consider you want a function that gives you all natural numbers that are smaller than a given number. I thought this should work:

fun set_of_nats ::"'nat ⇒'nat set" where
  "set_of_nats b = {a |(a::nat). a < b}"

But it doesnt. Error:

Type unification failed: Variable 'nat::type not of sort ord

Type error in application: incompatible operand type

Operator:  (<) a :: ??'a ⇒ bool
Operand:   b :: 'nat

The same error also occurs when I do not construct the set dynamically but rather give it a fixed condition, e.g replace b with any nat, like 5. Error remains the same.

what am I doing wrong here? And how can Isabelle handle potentially infinite sets in such a case (imagine the comparison is not less than but rather greather then)

Upvotes: 0

Views: 65

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8278

You should write nat instead of 'nat. The ' indicates that this is a type variable, i.e. an arbitrary type.

By the way, a few remarks:

  1. For non-recursive definitions, it is more common to use the definition command instead of the fun command, but you can of course use fun as well.
  2. There is already a pre-defined constant (with corresponding notation) for the thing that you want to define. It is called lessThan and you can write it as {..<b}.
  3. You don't need the |a in your definition. You can just write {a. a < b}. You only need the a if you have a more complicated expression to the left of the ., e.g. {a+1. |a. a < b}.

Upvotes: 0

Related Questions