# HG changeset patch
# User nipkow
# Date 1559298542 -7200
# Node ID 8dd987397e314a5c688132b1fc599b3c18fb0c7a
# Parent  39f5db308fe0525ac47ff927f3dfbe90a39c22a1
tuned proof

diff -r 39f5db308fe0 -r 8dd987397e31 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 31 10:39:35 2019 +0200
+++ b/src/HOL/List.thy	Fri May 31 12:29:02 2019 +0200
@@ -5486,26 +5486,7 @@
 text \<open>Stability of \<^const>\<open>sort_key\<close>:\<close>
 
 lemma sort_key_stable: "filter (\<lambda>y. f y = k) (sort_key f xs) = filter (\<lambda>y. f y = k) xs"
-proof (induction xs)
-  case Nil thus ?case by simp
-next
-  case (Cons a xs)
-  thus ?case
-  proof (cases "f a = k")
-    case False thus ?thesis
-      using Cons.IH by (metis (mono_tags) filter.simps(2) filter_sort)
-  next
-    case True
-    hence ler: "filter (\<lambda>y. f y = k) (a # xs) = a # filter (\<lambda>y. f y = f a) xs" by simp
-    have "\<forall>y \<in> set (sort_key f (filter (\<lambda>y. f y = f a) xs)). f y = f a" by simp
-    hence "insort_key f a (sort_key f (filter (\<lambda>y. f y = f a) xs))
-            = a # (sort_key f (filter (\<lambda>y. f y = f a) xs))"
-      by (simp add: insort_is_Cons)
-    hence lel: "filter (\<lambda>y. f y = k) (sort_key f (a # xs)) = a # filter (\<lambda>y. f y = f a) (sort_key f xs)"
-      by (metis True filter_sort ler sort_key_simps(2))
-    from lel ler show ?thesis using Cons.IH True by (auto)
-  qed
-qed
+by (induction xs) (auto simp: filter_insort insort_is_Cons filter_insort_triv)
 
 corollary stable_sort_key_sort_key: "stable_sort_key sort_key"
 by(simp add: stable_sort_key_def sort_key_stable)