Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: GenClassPoolJar.java Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/List_Lexorder.thy
    Author:     Norbert Voelker
*)

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

theory List_Lexorder
imports Main
begin

instantiation list :: (ord) ord
begin

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

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

instance ..

end

instance list :: (order) order
proof
  let ?r = "{(u, v::'a). u < v}"
  have tr: "trans ?r"
    using trans_def by fastforce
  have \<section>: False
    if "(xs,ys) \ lexord ?r" "(ys,xs) \ lexord ?r" for xs ys :: "'a list"
  proof -
    have "(xs,xs) \ lexord ?r"
      using that transD [OF lexord_transI [OF tr]] by blast
    then show False
      by (meson case_prodD lexord_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 lexord_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 (lexord {(u, v::'a). u < v})"
    by (rule total_lexord) (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

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 [simp]: "a # x < b # y \ a < b \ a = b \ x < y"
  by (simp add: list_less_def)

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 [simp]: "a # x \ b # y \ a < b \ a = b \ x \ y"
  unfolding list_le_def by auto

instantiation list :: (order) order_bot
begin

definition "bot = []"

instance
  by standard (simp add: bot_list_def)

end

lemma less_list_code [code]:
  "xs < ([]::'a::{equal, order} list) \ False"
  "[] < (x::'a::{equal, order}) # xs \ True"
  "(x::'a::{equal, order}) # xs < y # ys \ x < y \ x = y \ xs < ys"
  by simp_all

lemma less_eq_list_code [code]:
  "x # xs \ ([]::'a::{equal, order} list) \ False"
  "[] \ (xs::'a::{equal, order} list) \ True"
  "(x::'a::{equal, order}) # xs \ y # ys \ x < y \ x = y \ xs \ ys"
  by simp_all

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.