Re: [isabelle] proving finite universe
With the theory Infinite_Set from the HOL library, yor lemma becomes
lemma "infinite (UNIV :: string set)"
show "inj (%n. replicate n arbitrary) &
range (%n. replicate n arbitrary) <= UNIV"
by(metis injI length_replicate subset_UNIV)
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and