# HG changeset patch
# User noschinl
# Date 1369311769 -7200
# Node ID 510709f8881deadb39d0fae1215007dffe9109aa
# Parent  5b889b1b465b4ea0472740569ef8c9d8eabefffc
more lemmas for sorted_list_of_set

diff -r 5b889b1b465b -r 510709f8881d src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 23 13:51:21 2013 +1000
+++ b/src/HOL/List.thy	Thu May 23 14:22:49 2013 +0200
@@ -4881,11 +4881,19 @@
   shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
   using assms by (fact sorted_list_of_set.insert_remove)
 
+lemma sorted_list_of_set_eq_Nil_iff [simp]:
+  "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
+  using assms by (auto simp: sorted_list_of_set.remove)
+
 lemma sorted_list_of_set [simp]:
   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
     \<and> distinct (sorted_list_of_set A)"
   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
 
+lemma distinct_sorted_list_of_set:
+  "distinct (sorted_list_of_set A)"
+  using sorted_list_of_set by (cases "finite A") auto
+
 lemma sorted_list_of_set_sort_remdups [code]:
   "sorted_list_of_set (set xs) = sort (remdups xs)"
 proof -