Quelle Sorted_Less.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

section \<open>Lists Sorted wrt $<$\<close>

theory Sorted_Less
imports Less_False
begin

hide_const sorted

text \<open>Is a list sorted without duplicates, i.e., wrt \<open><\<close>?.\<close>

abbreviation sorted :: "'a::linorder list \ bool" where
"sorted \ sorted_wrt (<)"

lemmas sorted_wrt_Cons = sorted_wrt.simps(2)

text \<open>The definition of \<^const>\<open>sorted_wrt\<close> relates each element to all the elements after it.
This causes a blowup of the formulas. Thus we simplify matters by only comparing adjacent elements.\<close>

declare
  sorted_wrt.simps(2)[simp del]
  sorted_wrt1[simp] sorted_wrt2[OF transp_on_less, simp]

lemma sorted_cons: "sorted (x#xs) \ sorted xs"
by(simp add: sorted_wrt_Cons)

lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \ sorted xs"
by(rule ASSUMPTION_D [THEN sorted_cons])

lemma sorted_snoc: "sorted (xs @ [y]) \ sorted xs"
by(simp add: sorted_wrt_append)

lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \ sorted xs"
by(rule ASSUMPTION_D [THEN sorted_snoc])

lemma sorted_mid_iff:
  "sorted(xs @ y # ys) = (sorted(xs @ [y]) \ sorted(y # ys))"
by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)

lemma sorted_mid_iff2:
  "sorted(x # xs @ y # ys) =
  (sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))"
by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)

lemma sorted_mid_iff': "NO_MATCH [] ys \
  sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))"
by(rule sorted_mid_iff)

lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'

text\<open>Splay trees need two additional \<^const>\<open>sorted\<close> lemmas:\<close>

lemma sorted_snoc_le:
  "ASSUMPTION(sorted(xs @ [x])) \ x \ y \ sorted (xs @ [y])"
by (auto simp add: sorted_wrt_append ASSUMPTION_def)

lemma sorted_Cons_le:
  "ASSUMPTION(sorted(x # xs)) \ y \ x \ sorted (y # xs)"
by (auto simp add: sorted_wrt_Cons ASSUMPTION_def)

end

quality98%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.