tuned proof
authornipkow
Fri May 31 12:29:02 2019 +0200 (7 weeks ago)
changeset 702968dd987397e31
parent 70295 39f5db308fe0
child 70300 22c7eee0dd56
tuned proof
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri May 31 10:39:35 2019 +0200
     1.2 +++ b/src/HOL/List.thy	Fri May 31 12:29:02 2019 +0200
     1.3 @@ -5486,26 +5486,7 @@
     1.4  text \<open>Stability of \<^const>\<open>sort_key\<close>:\<close>
     1.5  
     1.6  lemma sort_key_stable: "filter (\<lambda>y. f y = k) (sort_key f xs) = filter (\<lambda>y. f y = k) xs"
     1.7 -proof (induction xs)
     1.8 -  case Nil thus ?case by simp
     1.9 -next
    1.10 -  case (Cons a xs)
    1.11 -  thus ?case
    1.12 -  proof (cases "f a = k")
    1.13 -    case False thus ?thesis
    1.14 -      using Cons.IH by (metis (mono_tags) filter.simps(2) filter_sort)
    1.15 -  next
    1.16 -    case True
    1.17 -    hence ler: "filter (\<lambda>y. f y = k) (a # xs) = a # filter (\<lambda>y. f y = f a) xs" by simp
    1.18 -    have "\<forall>y \<in> set (sort_key f (filter (\<lambda>y. f y = f a) xs)). f y = f a" by simp
    1.19 -    hence "insort_key f a (sort_key f (filter (\<lambda>y. f y = f a) xs))
    1.20 -            = a # (sort_key f (filter (\<lambda>y. f y = f a) xs))"
    1.21 -      by (simp add: insort_is_Cons)
    1.22 -    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)"
    1.23 -      by (metis True filter_sort ler sort_key_simps(2))
    1.24 -    from lel ler show ?thesis using Cons.IH True by (auto)
    1.25 -  qed
    1.26 -qed
    1.27 +by (induction xs) (auto simp: filter_insort insort_is_Cons filter_insort_triv)
    1.28  
    1.29  corollary stable_sort_key_sort_key: "stable_sort_key sort_key"
    1.30  by(simp add: stable_sort_key_def sort_key_stable)