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:

@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:

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

Answer 2

My first attempt to the problem would be a comprehension set that is defined recursively (for simplicity, I just look at the infinite sequence of prime numbers, but it would be easy to add an additional condition like i<size to get a finite sequence):

axm1:  primeSeq1 ∈ ℕ1 --> ℕ1
axm2:  primeSeq1 = { i↦p ∣ i∈ℕ1 ∧ p∈ℕ ∧
                           ( (i=1 ⇒ p=2)
                           ∧ (i>1 ⇒ ( p>primeSeq1(i−1) ∧
                                      ∀x·(x∈primeSeq1(i−1)‥p−1 ⇒
                                          ∃a,b·(a∈2‥x−1 ∧ a∗b=x)) ∧
                           ¬(∃a,b·(a∈2‥p−1 ∧ a∗b=p))     )))}

In words: We have a hard-coded base case that 2 is the first prime number. Then for i>1: p is the ith prime number if it is larger than the (i-1)th prime number (recursion!), all numbers between the last prime and p are not primes and p itself is a prime number.

This version still needs two axioms, one just for type checking, the other with the definition. Rodin does not accept it without axm1. And it is not a lambda expression.

Now we use an ugly hack: We use a comprehension set variable ps as a local variable to define the recursive set to eliminate the need for axm1:

axm3:  primeSeq2 = { j,ps · j∈ℕ1 ∧ ps∈ℕ1→ℕ ∧
                            ps = { i↦p ∣ i∈ℕ1 ∧ p∈ℕ ∧
                                        ( (i=1 ⇒ p=2)
                                        ∧ (i>1 ⇒ ( p>ps(i−1) ∧
                                                   ∀x·(x∈ps(i−1)‥p−1 ⇒
                                                       ∃a,b·(a∈2‥x−1 ∧ a∗b=x)) ∧
                                                   ¬(∃a,b·(a∈2‥p−1 ∧ a∗b=p))     )))}
                          ∣ j↦ps(j) }

Please note, that we used another syntactical form of a comprehension set where we added an expression (j↦ps(j)) for each element of the set.

So primeSeq2 is defined by using just one expression. But it is not a lambda expression.

Again we use a trick. We surround the comprehension set by a lamda expression:

axm4:  primeSeq3 = (λk·k∈ℕ1 ∣ primeSeq2(k))

So we have a lambda expression. To have it in one definition, we just copy primeSeq2 into the expression:

axm5:  primeSeq4 = (λk·k∈ℕ1 ∣ { j,ps · j∈ℕ1 ∧ ps∈ℕ1→ℕ ∧
                                       ps = { i↦p ∣ i∈ℕ1 ∧ p∈ℕ ∧
                                                   ( (i=1 ⇒ p=2)
                                                     ∧ (i>1 ⇒ ( p>ps(i−1) ∧
                                                                ∀x·(x∈ps(i−1)‥p−1 ⇒
                                                                    ∃a,b·(a∈2‥x−1 ∧ a∗b=x)) ∧
                                                                ¬(∃a,b·(a∈2‥p−1 ∧ a∗b=p))     )))}
                                     ∣ j↦ps(j) }(k))

So, to answer your question: Yes it is possible to define such a sequence with just one lambda expression. But the result is extremely messy :)

I didn't prove (and don't plan to do it!) any properties about the expressions above. So there might be some errors in it. I just type checked the formulas.

Update: After writing down the solution above, I realized that you don't need the recursion at all. You can use your original definitions of primeSet, primeSeq, etc. and put it into a comprehension set of the form

primeSeq1 =  (%i . i:NAT1 | ({ primeSet, primeSeq, ... . Definitions | 0|->primeSeq }(0))i)

But still, even the WD conditions would be very hard to prove.