src/HOL/List.thy
changeset 68083 d730a8cfc6e0
parent 68028 1f9f973eed2a
child 68085 7fe53815cce9
--- 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)"