| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Data_Structures/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 2 kB |
|
Quelle Sorted_Less.thySprache: Isabelle |
|||||||||||||||
|
(* Author: Tobias Nipkow *) section ‹Lists Sorted wrt $<$\› theory Sorted_Less imports Less_False begin hide_const sorted text ‹Is a list sorted without duplicates, i.e., wrt ‹<\<close>?.› sorted :: "'a::linorder list → bool" where sorted ≡ sorted_wrt (<)" sorted_wrt_Cons = sorted_wrt.simps(2) ‹The definition of const‹sorted_wrt› relates each element to all the elements a causes a blowup of the formulas. Thus we simplify matters by only comparing adj sorted_wrt.simps(2)[simp del] sorted_wrt1[simp] sorted_wrt2[OF transp_on_less, simp] sorted_cons: "sorted (x#xs) ==> sorted xs" (simp add: sorted_wrt_Cons) sorted_cons': "ASSUMPTION (sorted (x#xs)) ==> sorted xs" (rule ASSUMPTION_D [THEN sorted_cons]) sorted_snoc: "sorted (xs @ [y]) ==> sorted xs" (simp add: sorted_wrt_append) sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) ==> sorted xs" (rule ASSUMPTION_D [THEN sorted_snoc]) sorted_mid_iff: "sorted(xs @ y # ys) = (sorted(xs @ [y]) ∧ sorted(y # ys))" (fastforce simp add: sorted_wrt_Cons sorted_wrt_append) sorted_mid_iff2: "sorted(x # xs @ y # ys) = (sorted(x # xs) ∧ x < y ∧ sorted(xs @ [y]) ∧ sorted(y # ys))" (fastforce simp add: sorted_wrt_Cons sorted_wrt_append) sorted_mid_iff': "NO_MATCH [] ys ==> sorted(xs @ y # ys) = (sorted(xs @ [y]) ∧ sorted(y # ys))" (rule sorted_mid_iff) sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc' ‹Splay trees need two additional const‹sorted› lemmas:› sorted_snoc_le: "ASSUMPTION(sorted(xs @ [x])) ==> x ≤ y ==> sorted (xs @ [y])" (auto simp add: sorted_wrt_append ASSUMPTION_def) sorted_Cons_le: "ASSUMPTION(sorted(x # xs)) ==> y ≤ x ==> sorted (y # xs)" (auto simp add: sorted_wrt_Cons ASSUMPTION_def)
¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09