summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 12 Sep 2017 12:14:38 +0200 | |

changeset 66654 | 4a812abde314 |

parent 66653 | 52bf9f67a3c9 |

child 66655 | e9be3d6995f9 |

added lemma

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Mon Sep 11 18:36:13 2017 +0200 +++ b/src/HOL/List.thy Tue Sep 12 12:14:38 2017 +0200 @@ -5123,7 +5123,7 @@ text\<open>Currently it is not shown that @{const sort} returns a permutation of its input because the nicest proof is via multisets, -which are not yet available. Alternatively one could define a function +which are not part of Main. Alternatively one could define a function that counts the number of occurrences of an element in a list and use that instead of multisets to state the correctness property.\<close> @@ -5336,6 +5336,59 @@ "sorted (map fst (enumerate n xs))" by (simp add: enumerate_eq_zip) +text \<open>Stability of function @{const sort_key}:\<close> + +lemma sort_key_stable: + "x \<in> set xs \<Longrightarrow> [y <- sort_key f xs. f y = f x] = [y <- xs. f y = f x]" +proof (induction xs arbitrary: x) + case Nil thus ?case by simp +next + case (Cons a xs) + thus ?case + proof (cases "x \<in> set xs") + case True + thus ?thesis + proof (cases "f a = f x") + case False thus ?thesis + using Cons.IH by (metis (mono_tags) True filter.simps(2) filter_sort) + next + case True + hence ler: "[y <- (a # xs). f y = f x] = a # [y <- xs. f y = f a]" by simp + have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp + hence "insort_key f a (sort_key f [y <- xs. f y = f a]) + = a # (sort_key f [y <- xs. f y = f a])" + by (simp add: insort_is_Cons) + hence lel: "[y <- sort_key f (a # xs). f y = f x] = a # [y <- sort_key f xs. f y = f a]" + by (metis True filter_sort ler sort_key_simps(2)) + from lel ler show ?thesis using Cons.IH \<open>x \<in> set xs\<close> by (metis True filter_sort) + qed + next + case False + from Cons.prems have "x = a" by (metis False set_ConsD) + have ler: "[y <- (a # xs). f y = f a] = a # [y <- xs. f y = f a]" by simp + have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp + hence "insort_key f a (sort_key f [y <- xs. f y = f a]) + = a # (sort_key f [y <- xs. f y = f a])" + by (simp add: insort_is_Cons) + hence lel: "[y <- sort_key f (a # xs). f y = f a] = a # [y <- sort_key f xs. f y = f a]" + by (metis (mono_tags) filter.simps(2) filter_sort sort_key_simps(2)) + show ?thesis (is "?l = ?r") + proof (cases "f a \<in> set (map f xs)") + case False + hence "\<forall>y \<in> set xs. f y \<noteq> f a" by (metis image_eqI set_map) + hence R: "?r = [a]" using ler \<open>x=a\<close> by simp + have L: "?l = [a]" using lel \<open>x=a\<close> by (metis R filter_sort insort_key.simps(1) sort_key_simps) + from L R show ?thesis .. + next + case True + then obtain z where Z: "z \<in> set xs \<and> f z = f a" by auto + hence L: "[y <- sort_key f xs. f y = f z] = [y <- sort_key f xs. f y = f a]" by simp + from Z have R: "[y <- xs. f y = f z] = [y <- xs. f y = f a]" by simp + from L R Z show ?thesis using Cons.IH ler lel \<open>x=a\<close> by metis + qed + qed +qed + subsubsection \<open>@{const transpose} on sorted lists\<close>