Re: [isabelle] proving finite universe



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