CODEWITHSUNDEEP
isabelle
thor
thor

Reputation: 22460

What is the main symbol in Isabelle's set operator (‘) :: ('a => 'b) => 'a set => 'b set?

I was wondering what is the symbol ‘ in the Isabelle tutorial main.pdf below (under the section "Set")?

(‘)  :: ('a => 'b) => 'a set => 'b set

By looking into the symbols tab, the closest in shape I could find is \<acute> under the "Unsorted" category. I tried to evaluate the following expression, but it doesn't parse:

value "´ (λ(n::nat). n+1) {1,2}"

value "(λ(n::nat). n+1) ´ {1,2}"

Can anyone help to explain the usage here and what it does?

Upvotes: 0

Views: 89

Answers (1)

user9716869 - supports Ukraine
user9716869 - supports Ukraine

Reputation: 1941

I believe that the symbol that you are looking for is `, not ‘ or ´. The symbol ` is an infix notation for the constant image that is defined in theory Set.thy in the main library of Isabelle/HOL. Hopefully, the name of the constant is self-explanatory. For completeness, I restate the definition in this answer:

definition image :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set"    (infixr "`" 90)
  where "f ` A = {y. ∃x∈A. y = f x}"

Thence,

value "(λ(n::nat). n+1) ` {1,2}"

evaluates to "{2, 3}" :: "nat set", as expected.

Upvotes: 3

Related Questions