--- a/src/HOL/List.thy Fri May 04 22:26:25 2018 +0200
+++ b/src/HOL/List.thy Sun May 06 13:51:37 2018 +0200
@@ -5607,15 +5607,23 @@
"finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
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_key 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 set_sorted_list_of_set [simp]:
+ "finite A \<Longrightarrow> set (sorted_list_of_set A) = A"
+by(induct A rule: finite_induct) (simp_all add: set_insort_key)
+
+lemma sorted_sorted_list_of_set [simp]: "sorted (sorted_list_of_set A)"
+proof (cases "finite A")
+ case True thus ?thesis by(induction A) (simp_all add: sorted_insort)
+next
+ case False thus ?thesis by simp
+qed
+
+lemma distinct_sorted_list_of_set [simp]: "distinct (sorted_list_of_set A)"
+proof (cases "finite A")
+ case True thus ?thesis by(induction A) (simp_all add: distinct_insort)
+next
+ case False thus ?thesis by simp
+qed
lemma sorted_list_of_set_sort_remdups [code]:
"sorted_list_of_set (set xs) = sort (remdups xs)"