# HG changeset patch
# User nipkow
# Date 1590130343 -7200
# Node ID 3e343c0c2138156813352e5874264f318d6f03c2
# Parent  6a51e64ba13df930acc4aae03bd01ade34931b9f
added simp lemma

diff -r 6a51e64ba13d -r 3e343c0c2138 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 21 20:00:09 2020 +0000
+++ b/src/HOL/List.thy	Fri May 22 08:52:23 2020 +0200
@@ -414,6 +414,9 @@
 
 end
 
+lemma strict_sorted_iff: "strict_sorted l \<longleftrightarrow> sorted l \<and> distinct l"
+by (induction l) (use less_le in auto)
+
 
 subsubsection \<open>List comprehension\<close>
 
@@ -6049,6 +6052,10 @@
   case False thus ?thesis by simp
 qed
 
+lemma length_sorted_list_of_set[simp]:
+  "finite A \<Longrightarrow> length(sorted_list_of_set A) = card A"
+by(simp flip: distinct_card)
+
 lemmas sorted_list_of_set = set_sorted_list_of_set sorted_sorted_list_of_set distinct_sorted_list_of_set
 
 lemma sorted_list_of_set_sort_remdups [code]:
@@ -6075,9 +6082,6 @@
   "sorted_list_of_set {m..<n} = [m..<n]"
 by (rule sorted_distinct_set_unique) simp_all
 
-lemma strict_sorted_iff: "strict_sorted l \<longleftrightarrow> sorted l \<and> distinct l"
-  by (induction l) (use less_le in auto)
-
 lemma strict_sorted_list_of_set [simp]: "strict_sorted (sorted_list_of_set A)"
   by (simp add: strict_sorted_iff)