Email Gateway (Aug 18 2022 at 12:32): Email Gateway (Aug 18 2022 at 12:32):From: Chris Osborn <chrisosb@gmail.com>
Update: I was able to solve this problem as follows:
lemma fin_maxlen: "finite (X::string set) ==> (EX n. ALL s:X. size s < n)"
apply (induct rule: finite.induct)
apply simp
apply clarify
apply (rule_tac x="max n (size a) + 1" in exI)
apply auto
done
lemma string_any_size: "EX (s::string). size s = n"
apply (induct n)
apply auto
apply (rule_tac x="''a''@s" in exI)
apply simp
done
lemma univ_infinite: "not (finite (UNIV::string set))"
apply clarify
apply (drule fin_maxlen)
apply clarsimp
apply (cut_tac n="n" in string_any_size)
apply auto
done
Is there a cleaner way?
Thanks,
Chris
Email Gateway (Aug 18 2022 at 12:32):From: Chris Osborn <cosborn3@uiuc.edu>
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
Email Gateway (Aug 18 2022 at 12:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Chris,
Update: I was able to solve this problem as follows:
Is there a cleaner way?
Taking into account that strings are just lists of characters and lists
under size are similar to natural numbers, the infiniteness of strings
follows from the infiniteness of natural numbers. The proof of
infinite_UNIV_nat in theory Finite_Set is already not trivial, so I
don't think you have to worry about your proof being to complicated.
Hope this helps
Florian
florian_haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 12:32):From: Stephan Merz <Stephan.Merz@loria.fr>
Chris,
the theory HOL/Library/Infinite_Set contains several lemmas that can be
useful here. In particular, it proves that a set if infinite iff it
contains a countable subset (lemma infinite_iff_countable_subset), which
should help you to prove your goal.
Best,
Stephan
Chris Osborn wrote:
Stephan_Merz.vcf
Email Gateway (Aug 18 2022 at 12:32):From: Tobias Nipkow <nipkow@in.tum.de>
I have simplified your proof a little bit. It works for arbitrary lists now:
lemma finite_maxlen: "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
apply (induct rule: finite.induct)
apply auto
apply (rule_tac x="max n (size a) + 1" in exI)
apply auto
done
lemma infinite_list_UNIVI: "~ finite(UNIV::'a list set)"
apply(rule notI)
apply(drule finite_maxlen)
apply (metis UNIV_I length_replicate less_not_refl)
done
That will go in the library, thanks.
Tobias
Chris Osborn wrote:
Email Gateway (Aug 18 2022 at 12:33):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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:
Email Gateway (Aug 18 2022 at 12:33):From: Chris Osborn <chrisosb@gmail.com>
Thank you all for your replies; they have been helpful.
Chris
Last updated: May 03 2024 at 12:27 UTC