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: series.prf   Sprache: Isabelle

Untersuchung Isabelle©
(*  Author:     Tobias Nipkow
    Copyright   1994 TU Muenchen
*)

section \<open>Quicksort with function package\<close>

theory Quicksort
imports "HOL-Library.Multiset"
begin

context linorder
begin

fun quicksort :: "'a list \ 'a list" where
  "quicksort [] = []"
| "quicksort (x#xs) = quicksort [y\xs. \ x\y] @ [x] @ quicksort [y\xs. x\y]"

lemma [code]:
  "quicksort [] = []"
  "quicksort (x#xs) = quicksort [y\xs. yxs. x\y]"
  by (simp_all add: not_le)

lemma quicksort_permutes [simp]:
  "mset (quicksort xs) = mset xs"
by (induction xs rule: quicksort.induct) (simp_all)

lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
proof -
  have "set_mset (mset (quicksort xs)) = set_mset (mset xs)"
    by simp
  then show ?thesis by (simp only: set_mset_mset)
qed

lemma sorted_quicksort: "sorted (quicksort xs)"
  by (induct xs rule: quicksort.induct) (auto simp add: sorted_append not_le less_imp_le)

theorem sort_quicksort:
  "sort = quicksort"
  by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+

end

end

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.22Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff