# 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.*