added lemma
authornipkow
Tue Sep 12 12:14:38 2017 +0200 (21 months ago)
changeset 666544a812abde314
parent 66653 52bf9f67a3c9
child 66655 e9be3d6995f9
added lemma
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Mon Sep 11 18:36:13 2017 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Sep 12 12:14:38 2017 +0200
     1.3 @@ -5123,7 +5123,7 @@
     1.4  
     1.5  text\<open>Currently it is not shown that @{const sort} returns a
     1.6  permutation of its input because the nicest proof is via multisets,
     1.7 -which are not yet available. Alternatively one could define a function
     1.8 +which are not part of Main. Alternatively one could define a function
     1.9  that counts the number of occurrences of an element in a list and use
    1.10  that instead of multisets to state the correctness property.\<close>
    1.11  
    1.12 @@ -5336,6 +5336,59 @@
    1.13    "sorted (map fst (enumerate n xs))"
    1.14    by (simp add: enumerate_eq_zip)
    1.15  
    1.16 +text \<open>Stability of function @{const sort_key}:\<close>
    1.17 +
    1.18 +lemma sort_key_stable:
    1.19 +  "x \<in> set xs \<Longrightarrow> [y <- sort_key f xs. f y = f x] = [y <- xs. f y = f x]"
    1.20 +proof (induction xs arbitrary: x)
    1.21 +  case Nil thus ?case by simp
    1.22 +next  
    1.23 +  case (Cons a xs)
    1.24 +  thus ?case 
    1.25 +  proof (cases "x \<in> set xs")
    1.26 +    case True 
    1.27 +    thus ?thesis
    1.28 +    proof (cases "f a = f x")
    1.29 +      case False thus ?thesis 
    1.30 +        using Cons.IH by (metis (mono_tags) True filter.simps(2) filter_sort)
    1.31 +    next
    1.32 +      case True
    1.33 +      hence ler: "[y <- (a # xs). f y = f x] = a # [y <- xs. f y = f a]" by simp
    1.34 +      have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
    1.35 +      hence "insort_key f a (sort_key f [y <- xs. f y = f a]) 
    1.36 +              = a # (sort_key f [y <- xs. f y = f a])"
    1.37 +        by (simp add: insort_is_Cons)
    1.38 +      hence lel: "[y <- sort_key f (a # xs). f y = f x] = a # [y <- sort_key f xs. f y = f a]"
    1.39 +        by (metis True filter_sort ler sort_key_simps(2))
    1.40 +      from lel ler show ?thesis using Cons.IH \<open>x \<in> set xs\<close> by (metis True filter_sort)
    1.41 +    qed
    1.42 +  next
    1.43 +    case False
    1.44 +    from Cons.prems have "x = a" by (metis False set_ConsD)
    1.45 +    have ler: "[y <- (a # xs). f y = f a] = a # [y <- xs. f y = f a]" by simp
    1.46 +    have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
    1.47 +    hence "insort_key f a (sort_key f [y <- xs. f y = f a]) 
    1.48 +           = a # (sort_key f [y <- xs. f y = f a])"
    1.49 +      by (simp add: insort_is_Cons)
    1.50 +    hence lel: "[y <- sort_key f (a # xs). f y = f a] = a # [y <- sort_key f xs. f y = f a]"
    1.51 +      by (metis (mono_tags) filter.simps(2) filter_sort sort_key_simps(2))
    1.52 +    show ?thesis (is "?l = ?r")
    1.53 +    proof (cases "f a \<in> set (map f xs)")
    1.54 +      case False
    1.55 +      hence "\<forall>y \<in> set xs. f y \<noteq> f a" by (metis image_eqI set_map)
    1.56 +      hence R: "?r = [a]" using ler \<open>x=a\<close> by simp
    1.57 +      have L: "?l = [a]" using lel \<open>x=a\<close> by (metis R filter_sort insort_key.simps(1) sort_key_simps)
    1.58 +      from L R show ?thesis ..
    1.59 +    next
    1.60 +      case True
    1.61 +      then obtain z where Z: "z \<in> set xs \<and> f z = f a" by auto
    1.62 +      hence L: "[y <- sort_key f xs. f y = f z] = [y <- sort_key f xs. f y = f a]" by simp
    1.63 +      from Z have R: "[y <- xs. f y = f z] = [y <- xs. f y = f a]" by simp 
    1.64 +      from L R Z show ?thesis using Cons.IH ler lel \<open>x=a\<close> by metis
    1.65 +    qed
    1.66 +  qed
    1.67 +qed
    1.68 +
    1.69  
    1.70  subsubsection \<open>@{const transpose} on sorted lists\<close>
    1.71