# HG changeset patch
# User nipkow
# Date 1525607497 -7200
# Node ID d730a8cfc6e0466deced2cd085e521b882e628cf
# Parent  b25ccd85b1fd2f696ab487cbb18085172b711d92
removed asm "finite"

diff -r b25ccd85b1fd -r d730a8cfc6e0 src/HOL/List.thy
--- 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)"