Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quelle List_Lenlexorder.thy Sprache: Isabelle

(*  Title:      HOL/Library/List_Lenlexorder.thy
*)

section \<open>Lexicographic order on lists\<close>

text \<open>This version prioritises length and can yield wellorderings\<close>

theory List_Lenlexorder
imports Main
begin

instantiation list :: (ord) ord
begin

definition
  list_less_def: "xs < ys \ (xs, ys) \ lenlex {(u, v). u < v}"

definition
  list_le_def: "(xs :: _ list) \ ys \ xs < ys \ xs = ys"

instance ..

end

instance list :: (order) order
proof
  have tr: "trans {(u, v::'a). u < v}"
    using trans_def by fastforce
  have \<section>: False
    if "(xs,ys) \ lenlex {(u, v). u < v}" "(ys,xs) \ lenlex {(u, v). u < v}" for xs ys :: "'a list"
  proof -
    have "(xs,xs) \ lenlex {(u, v). u < v}"
      using that transD [OF lenlex_transI [OF tr]] by blast
    then show False
      by (meson case_prodD lenlex_irreflexive less_irrefl mem_Collect_eq)
  qed
  show "xs \ xs" for xs :: "'a list" by (simp add: list_le_def)
  show "xs \ zs" if "xs \ ys" and "ys \ zs" for xs ys zs :: "'a list"
    using that transD [OF lenlex_transI [OF tr]] by (auto simp add: list_le_def list_less_def)
  show "xs = ys" if "xs \ ys" "ys \ xs" for xs ys :: "'a list"
    using \<section> that list_le_def list_less_def by blast
  show "xs < ys \ xs \ ys \ \ ys \ xs" for xs ys :: "'a list"
    by (auto simp add: list_less_def list_le_def dest: \<section>)
qed

instance list :: (linorder) linorder
proof
  fix xs ys :: "'a list"
  have "total (lenlex {(u, v::'a). u < v})"
    by (rule total_lenlex) (auto simp: total_on_def)
  then show "xs \ ys \ ys \ xs"
    by (auto simp add: total_on_def list_le_def list_less_def)
qed

instance list :: (wellorder) wellorder
proof
  fix P :: "'a list \ bool" and a
  assume "\x. (\y. y < x \ P y) \ P x"
  then show "P a"
    unfolding list_less_def by (metis wf_lenlex wf_induct wf_lenlex wf)
qed

instantiation list :: (linorder) distrib_lattice
begin

definition "(inf :: 'a list \ _) = min"

definition "(sup :: 'a list \ _) = max"

instance
  by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2)

end

lemma not_less_Nil [simp]: "\ x < []"
  by (simp add: list_less_def)

lemma Nil_less_Cons [simp]: "[] < a # x"
  by (simp add: list_less_def)

lemma Cons_less_Cons: "a # x < b # y \ length x < length y \ length x = length y \ (a < b \ a = b \ x < y)"
  using lenlex_length
  by (fastforce simp: list_less_def Cons_lenlex_iff)

lemma le_Nil [simp]: "x \ [] \ x = []"
  unfolding list_le_def by (cases x) auto

lemma Nil_le_Cons [simp]: "[] \ x"
  unfolding list_le_def by (cases x) auto

lemma Cons_le_Cons: "a # x \ b # y \ length x < length y \ length x = length y \ (a < b \ a = b \ x \ y)"
  by (auto simp: list_le_def Cons_less_Cons)

instantiation list :: (order) order_bot
begin

definition "bot = []"

instance
  by standard (simp add: bot_list_def)

end

end

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

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.