Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide



On Wed, May 22, 2013 at 10:16 AM, Christoph LANGE
<math.semantic.web at gmail.com> wrote:
> Dear Isabelle community,
>
> I am currently working with lists constructed from finite sets, and I'm
> missing the following two lemmas that would really help me to get my
> work done.  At the moment my Isabelle experience is not sufficient for
> proving them myself, plus I think it would make sense if they were part
> of the library (List.thy).
>
> lemma sorted_list_of_set_not_empty [simp] :
>   assumes "finite S" and "S ≠ {}"
>   shows "sorted_list_of_set S ≠ []"
using assms by (metis sorted_list_of_set set.simps(1))

A different formulation might make a more useful simp rule:

lemma sorted_list_of_set_empty_iff:
  assumes "finite S"
  shows "sorted_list_of_set S = [] ⟷ S = {}"

> lemma sorted_list_of_set_distinct [simp] :
>   shows "distinct (sorted_list_of_set S)"
apply (cases "finite S")
apply (induct set: finite)
apply (simp_all add: distinct_insort)
done

- Brian




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