event-b: is it possible generate sequence from ... to ... of prime numbers via lambda in one expression?

Question

I wonder if it's possible to generate a sequence of prime numbers with just one lambda expression in event-b. This is what I have so far:

Click to copy

@axm1 primeSet = {x∣ x ∈ 1‥100 ∧ ¬(∃y·y < x ∧ y > 1 ∧ x mod y = 0)} ∧ finite(primeSet)
@axm2 primeSeq ∈ 1‥card(primeSet) >->> primeSet
@axm3 ∀a,b,c,d·a↦b ∈ primeSeq ∧ c↦d ∈ primeSeq ∧ a↦b ≠ c↦d ⇒ (a < c ⇒ b < d)

@axm1 generates a set of primes, @axm2 defines the type of the sequence and @axm3 constrains this set further to a deterministic solution. I have no idea how to do this with one lambda expression and i don't think it's even possible but I want to know what others think.

Answer 1

I believe this lambda function satisfies your request:

Click to copy

@axm1 primeSeq = {size↦X| size∈ℕ ∧ X⊆ℕ ∧ ∀x·x∈X ⇒ (x∈1‥size ∧ (∀y·y∈1‥x ∧ y≠1 ∧ y≠x ⇒ x mod y ≠ 0))}