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

On 22.05.2013 19:16, Christoph LANGE wrote:
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).

I first wondered why you had problems with these proofs; then I discovered that Florians rework of Big_Operators in the development version added some crucial lemmas ;)

lemma sorted_list_of_set_not_empty [simp] :
   assumes "finite S" and "S ≠ {}"
   shows "sorted_list_of_set S ≠ []"

Sledeghammer is able to find a proof after unfolding sorted_list_of_set_def. A nicer proof however is to prove the following first:

lemma sorted_list_of_set_remove':
  assumes "finite A" "x ∈ A"
    "sorted_list_of_set A = insort x (sorted_list_of_set (A - {x}))"
proof -
  from assms have "insert x (A - {x}) = A" by blast
then have "sorted_list_of_set A = sorted_list_of_set (insert x (A - {x}))"
    by simp
  also have "... = insort x (sorted_list_of_set (A - {x}))"
    using assms by simp
  finally show ?thesis .

then your proof goes through with

  using assms by (auto simp: sorted_list_of_set_remove')

BTW, a nicer lemma would be:

lemma sorted_list_of_set_eq_Nil_iff:
  assumes "finite S"
  shows "sorted_list_of_set S = [] <-> S = []"
  using assms by (auto simp: sorted_list_of_set_remove')

lemma sorted_list_of_set_distinct [simp] :
   shows "distinct (sorted_list_of_set S)"

This property does not hold in Isabelle 2013, as Finite_Set.fold is only defined for finite sets (i.e., we cannot prove anything about infinite sets). So you need to district your lemma to finite sets. Then the proof is easy:

lemma sorted_list_of_set_distinct [simp] :
  assumes "finite S" shows "distinct (sorted_list_of_set S)"
  using assms sorted_list_of_set by auto

(In the next version of Isabelle, Finite_Set.fold will probably return the initial argument for infinite sets).

Finally, lists-from-sets are probably not even what I need to get my
actual work done.  I.e. if you think that there is no good reason for me
using them, I'm willing to abandon them.  Originally I'm working with
finite sets, but I defined a custom Max-like operation on them, which
recursively folds the comparison of two elements over the whole
set/list.  As I'm not yet capable of understanding the internals behind

definition (in linorder) Max :: "'a set ⇒ 'a" where
   "Max = fold1 max"

in Big_Operators.thy (which seem to depend on certain idempotence laws
that max satisfies), but wanted to prove some properties of my Max-like
operation and got stuck in my initial attempt to use finite_ne_induct, I
resorted to converting my finite sets to lists and using
list_nonempty_induct – which did the job, except for the two missing
lemmas mentioned above.

As sets have no order, fold is only well-defined if the operation you define is commutative.

  -- Lars

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