Re: [isabelle] proving finite universe



Hi Chris,

With the theory Infinite_Set from the HOL library, yor lemma becomes very easy:

lemma "infinite (UNIV :: string set)"
  unfolding infinite_iff_countable_subset
proof
  show "inj (%n. replicate n arbitrary) &
        range (%n. replicate n arbitrary) <= UNIV"
    by(metis injI length_replicate subset_UNIV)
qed

Best,
Andreas


Chris Osborn schrieb:
Does anyone know how I can prove the following:

"not (finite (UNIV::string set))"

I have been unable to find applicable lemmas.

Thanks in advance,
Chris







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.