products/Sources/formale Sprachen/Isabelle/HOL/ex image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Radix_Sort.thy   Sprache: Isabelle

Original von: Isabelle©

(* Author: Tobias Nipkow *)

theory Radix_Sort
imports
  "HOL-Library.List_Lexorder" 
  "HOL-Library.Sublist" 
  "HOL-Library.Multiset" 
begin

text \<open>The \<open>Radix_Sort\<close> locale provides a sorting function \<open>radix_sort\<close> that sorts
lists of lists. It is parameterized by a sorting function \<open>sort1 f\<close> that also sorts
lists of lists, but only w.r.t. the column selected by \<open>f\<close>.
Working with lists, \<open>f\<close> is instantiated with \<^term>\<open>\<lambda>xs. xs ! n\<close> to select the \<open>n\<close>-th element.
A more efficient implementation would sort lists of arrays because arrays support
constant time access to every element.\<close>

locale Radix_Sort =
fixes sort1 :: "('a list \ 'a::linorder) \ 'a list list \ 'a list list"
assumes sorted: "sorted (map f (sort1 f xss))"
assumes mset: "mset (sort1 f xss) = mset xss"
assumes stable: "stable_sort_key sort1"
begin

lemma set_sort1[simp]: "set(sort1 f xss) = set xss"
by (metis mset set_mset_mset)

abbreviation "sort_col i xss \ sort1 (\xs. xs ! i) xss"
abbreviation "sorted_col i xss \ sorted (map (\xs. xs ! i) xss)"

fun radix_sort :: "nat \ 'a list list \ 'a list list" where
"radix_sort 0 xss = xss" |
"radix_sort (Suc i) xss = radix_sort i (sort_col i xss)"

lemma mset_radix_sort: "mset (radix_sort i xss) = mset xss"
by(induction i arbitrary: xss) (auto simp: mset)

abbreviation "sorted_from i xss \ sorted (map (drop i) xss)"

definition "cols xss n = (\xs \ set xss. length xs = n)"

lemma cols_sort1: "cols xss n \ cols (sort1 f xss) n"
by(simp add: cols_def)

lemma sorted_from_Suc2:
  "\ cols xss n; i < n;
    sorted_col i xss;
    \<And>x. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = x] \<rbrakk>
  \<Longrightarrow> sorted_from i xss"
proof(induction xss rule: induct_list012)
  case 1 show ?case by simp
next
  case 2 show ?case by simp
next
  case (3 xs1 xs2 xss)
  have lxs1: "length xs1 = n" and lxs2: "length xs2 = n"
    using "3.prems"(1) by(auto simp: cols_def)
  have *: "drop i xs1 \ drop i xs2"
  proof -
    have "drop i xs1 = xs1!i # drop (i+1) xs1"
      using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs1)
    also have "\ \ xs2!i # drop (i+1) xs2"
      using "3.prems"(3) "3.prems"(4)[of "xs2!i"by(auto)
    also have "\ = drop i xs2"
      using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs2)
    finally show ?thesis .
  qed
  have "sorted_from i (xs2 # xss)"
  proof(rule "3.IH"[OF _ "3.prems"(2)])
    show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def)
    show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
    show "\x. sorted_from (i+1) [ys\xs2 # xss . ys ! i = x]"
      using "3.prems"(4)
        sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
      by fastforce
  qed
  with * show ?case by (auto)
qed

lemma sorted_from_radix_sort_step:
assumes "cols xss n" and "i < n" and "sorted_from (i+1) xss"
shows "sorted_from i (sort_col i xss)"
proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)])
  show "sorted_col i (sort_col i xss)" by(simp add: sorted)
  fix x show "sorted_from (i+1) [ys \ sort_col i xss . ys ! i = x]"
  proof -
    from assms(3)
    have "sorted_from (i+1) (filter (\ys. ys!i = x) xss)"
      by(rule sorted_filter)
    thus "sorted (map (drop (i+1)) (filter (\ys. ys!i = x) (sort_col i xss)))"
      by (metis stable stable_sort_key_def)
  qed
qed

lemma sorted_from_radix_sort:
  "\ cols xss n; i \ n; sorted_from i xss \ \ sorted_from 0 (radix_sort i xss)"
proof(induction i arbitrary: xss)
  case 0 thus ?case by simp
next
  case (Suc i)
  thus ?case by(simp add: sorted_from_radix_sort_step cols_sort1)
qed

corollary sorted_radix_sort: "cols xss n \ sorted (radix_sort n xss)"
apply(frule sorted_from_radix_sort[OF _ le_refl])
 apply(auto simp add: cols_def sorted_iff_nth_mono)
done

end

end

¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff