lambda - event-b: 1 つの式でラムダを介して素数の ... から ... までのシーケンスを生成することは可能ですか?

Question

event-b のラムダ式を1 つだけ使用して素数のシーケンスを生成できるかどうか疑問に思います。これは私がこれまでに持っているものです:

@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このセットをさらに決定論的な解に制約します。1つのラムダ式でこれを行う方法がわかりません。それが可能だとは思いませんが、他の人の考えを知りたいです。

Answer 1

このラムダ関数はあなたの要求を満たすと思います:

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