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 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

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,
> Chris
>





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