Re: [isabelle] proving finite universe
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 (rule_tac x="max n (size a) + 1" in exI)
lemma string_any_size: "EX (s::string). size s = n"
apply (induct n)
apply (rule_tac x="''a''@s" in exI)
lemma univ_infinite: "not (finite (UNIV::string set))"
apply (drule fin_maxlen)
apply (cut_tac n="n" in string_any_size)
Is there a cleaner way?
On Sun, Oct 19, 2008 at 1:36 PM, Chris Osborn <cosborn3 at uiuc.edu> wrote:
> 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