Stream: Beginner Questions

Topic: Construction a set

John Hughes (Feb 04 2025 at 23:47):

I've got a datatype

datatype a2ln = A2Ordinary "real" "real"
  | A2Vertical "real"

for representing lines in the Cartesian plane. A2Ordinary m b is supposed to represent the line we usually describe as $y = mx + b$. Naturally, that only works when m is nonzero, so I'd like to form a set called Lines consisting of all items of this datatype...except for the Ordinary ones with m = 0. I tried writing

definition A2Lines::"a2ln set"
  where "A2Lines ≡ (UNIV::a2ln set) - {k . λ k . ∃ b . k = (Ordinary 0 b)}"

but Isabelle doesn't like that. (I've only used sets in Isabelle a little bit, so I'm still pretty shaky on them).

Can someone suggest how I might define that set?

I'm sure that there's a way to define it positively rather than with a set-difference, but if the set-difference way is possible, I'd like to see how to do it for later use.

irvin (Feb 05 2025 at 03:22):

This is currently what your second term is with the syntax sugar removed

(*   Set syntax    |  Set body    *)
term "Collect (λk . (λ k . ∃ b . k = (Ordinary 0 b)))"

irvin (Feb 05 2025 at 03:25):

More generally

(*Notice how both terms are printed the same in isabelle*)
lemma "Collect (λx . P x) = {x. P x}"
  by (fact refl)

Mathias Fleury (Feb 05 2025 at 04:50):

This is the syntax you are looking for I think:

term ‹{k | b . k = (Ordinary 0 b)}›

Mathias Fleury (Feb 05 2025 at 04:51):

(the λ is implicit and the ∃ is in the | basically)

Christian Pardillo Laursen (Feb 05 2025 at 12:36):

Just to answer the question, a non-set difference way to define this is

{k. ∃b c. k = A2Ordinary b c ∧ c ≠ 0}

And a set difference way is

- {k. ∃b. k = A2Ordinary 0 b}

John Hughes (Feb 05 2025 at 17:10):

Thanks. I was (perhaps mistakenly) trying to use the first 'set comprehension' notation from the theory Set:

```
"{x. P}" ⇌ "CONST Collect (λx. P)"

but this second version, with the vertical bar, looks more workable. I had earlier tried something that looked like
`{A2Ordinary m b .  ... }` but couldn't make it work, and thought the problem might be the use of a constructor at the start rather than just a variable-name.

Thanks, everyone!

Last updated: Mar 09 2025 at 12:28 UTC