--- 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)