Re: [isabelle] proving finite universe



Thank you all for your replies; they have been helpful.

Chris

On Mon, Oct 20, 2008 at 7:16 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 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.