lambda - event-b:是否可以在一个表达式中通过 lambda 生成从 ... 到 ... 的素数序列？

Question

我想知道是否可以仅用一个 lambda 生成素数序列表达式 event-b 。这是我到目前为止所拥有的:

@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 生成一组素数，@axm2 定义序列的类型，@axm3 进一步将此集合限制为确定性的解决方案。我不知道如何用一个 lambda 表达式来做到这一点，我认为这甚至不可能，但我想知道其他人的想法。

Answer 1

我相信这个 lambda 函数满足您的要求:

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