5121 |
5121 |
5122 subsubsection \<open>Sorting functions\<close> |
5122 subsubsection \<open>Sorting functions\<close> |
5123 |
5123 |
5124 text\<open>Currently it is not shown that @{const sort} returns a |
5124 text\<open>Currently it is not shown that @{const sort} returns a |
5125 permutation of its input because the nicest proof is via multisets, |
5125 permutation of its input because the nicest proof is via multisets, |
5126 which are not yet available. Alternatively one could define a function |
5126 which are not part of Main. Alternatively one could define a function |
5127 that counts the number of occurrences of an element in a list and use |
5127 that counts the number of occurrences of an element in a list and use |
5128 that instead of multisets to state the correctness property.\<close> |
5128 that instead of multisets to state the correctness property.\<close> |
5129 |
5129 |
5130 context linorder |
5130 context linorder |
5131 begin |
5131 begin |
5333 qed |
5333 qed |
5334 |
5334 |
5335 lemma sorted_enumerate [simp]: |
5335 lemma sorted_enumerate [simp]: |
5336 "sorted (map fst (enumerate n xs))" |
5336 "sorted (map fst (enumerate n xs))" |
5337 by (simp add: enumerate_eq_zip) |
5337 by (simp add: enumerate_eq_zip) |
|
5338 |
|
5339 text \<open>Stability of function @{const sort_key}:\<close> |
|
5340 |
|
5341 lemma sort_key_stable: |
|
5342 "x \<in> set xs \<Longrightarrow> [y <- sort_key f xs. f y = f x] = [y <- xs. f y = f x]" |
|
5343 proof (induction xs arbitrary: x) |
|
5344 case Nil thus ?case by simp |
|
5345 next |
|
5346 case (Cons a xs) |
|
5347 thus ?case |
|
5348 proof (cases "x \<in> set xs") |
|
5349 case True |
|
5350 thus ?thesis |
|
5351 proof (cases "f a = f x") |
|
5352 case False thus ?thesis |
|
5353 using Cons.IH by (metis (mono_tags) True filter.simps(2) filter_sort) |
|
5354 next |
|
5355 case True |
|
5356 hence ler: "[y <- (a # xs). f y = f x] = a # [y <- xs. f y = f a]" by simp |
|
5357 have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp |
|
5358 hence "insort_key f a (sort_key f [y <- xs. f y = f a]) |
|
5359 = a # (sort_key f [y <- xs. f y = f a])" |
|
5360 by (simp add: insort_is_Cons) |
|
5361 hence lel: "[y <- sort_key f (a # xs). f y = f x] = a # [y <- sort_key f xs. f y = f a]" |
|
5362 by (metis True filter_sort ler sort_key_simps(2)) |
|
5363 from lel ler show ?thesis using Cons.IH \<open>x \<in> set xs\<close> by (metis True filter_sort) |
|
5364 qed |
|
5365 next |
|
5366 case False |
|
5367 from Cons.prems have "x = a" by (metis False set_ConsD) |
|
5368 have ler: "[y <- (a # xs). f y = f a] = a # [y <- xs. f y = f a]" by simp |
|
5369 have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp |
|
5370 hence "insort_key f a (sort_key f [y <- xs. f y = f a]) |
|
5371 = a # (sort_key f [y <- xs. f y = f a])" |
|
5372 by (simp add: insort_is_Cons) |
|
5373 hence lel: "[y <- sort_key f (a # xs). f y = f a] = a # [y <- sort_key f xs. f y = f a]" |
|
5374 by (metis (mono_tags) filter.simps(2) filter_sort sort_key_simps(2)) |
|
5375 show ?thesis (is "?l = ?r") |
|
5376 proof (cases "f a \<in> set (map f xs)") |
|
5377 case False |
|
5378 hence "\<forall>y \<in> set xs. f y \<noteq> f a" by (metis image_eqI set_map) |
|
5379 hence R: "?r = [a]" using ler \<open>x=a\<close> by simp |
|
5380 have L: "?l = [a]" using lel \<open>x=a\<close> by (metis R filter_sort insort_key.simps(1) sort_key_simps) |
|
5381 from L R show ?thesis .. |
|
5382 next |
|
5383 case True |
|
5384 then obtain z where Z: "z \<in> set xs \<and> f z = f a" by auto |
|
5385 hence L: "[y <- sort_key f xs. f y = f z] = [y <- sort_key f xs. f y = f a]" by simp |
|
5386 from Z have R: "[y <- xs. f y = f z] = [y <- xs. f y = f a]" by simp |
|
5387 from L R Z show ?thesis using Cons.IH ler lel \<open>x=a\<close> by metis |
|
5388 qed |
|
5389 qed |
|
5390 qed |
5338 |
5391 |
5339 |
5392 |
5340 subsubsection \<open>@{const transpose} on sorted lists\<close> |
5393 subsubsection \<open>@{const transpose} on sorted lists\<close> |
5341 |
5394 |
5342 lemma sorted_transpose[simp]: |
5395 lemma sorted_transpose[simp]: |