[Proof] M and Σ (are / should be) infinite sets

[nrryuya]

I guess M and ∑ in the paper should be infinite. The current definitions of them of ours are infinite?

(* Definition 2.7 *)
fun 
  Σ_i :: "params ⇒ nat ⇒ state set" and
  M_i :: "params ⇒ nat ⇒ message set"
  where 
    "Σ_i params 0 = {∅}"
  | "Σ_i params n = {σ ∈ Pow (M_i params (n - 1)). ∀ m. m ∈ σ ⟶ justification m ⊆ σ}"
  | "M_i params n = {m. est m ∈ C params ∧ sender m ∈ V params ∧ justification m ∈ (Σ_i params n) ∧ est m ∈ ε params (justification m)}" 

fun M :: "params ⇒ message set"
  where
    "M params =  ⋃ (M_i params `ℕ)"

fun Σ :: "params ⇒ state set"
  where
    "Σ params = ⋃ (Σ_i params `ℕ)"

NOTE: Isabelle says {n ∈ ℕ} and {σ ∈ (Σ params)} are finite.

value "finite {n ∈ ℕ}"
(* True  *)

lemma "∀ params. finite {σ ∈ (Σ params)}"
  by auto

[myuon]

value "finite {n ∈ ℕ}" is True because {n ∈ ℕ} will be evaluated to {True} or {False}. (You can check term "{n ∈ ℕ}" and this must say a set of boolean) I think your sets can be infinite correctly. No problem.

[myuon]

See below for the complete definitions of set comprehension syntax. I guess this case is parsed using _Finset syntax. https://isabelle.in.tum.de/dist/library/HOL/HOL/Set.html

[nrryuya]

value "finite {n ∈ ℕ}" is True because {n ∈ ℕ} will be evaluated to {True} or {False}. (You can check term "{n ∈ ℕ}" and this must say a set of boolean)

Yeah, I found this mistake in another place a while ago... ;) Thank you for your clarification.

I think your sets can be infinite correctly. No problem.

Oh, nice! I'll try to prove they are infinite. It seems that it's not so straightforward, though.