products/Sources/formale Sprachen/Isabelle/HOL/Library/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: multiset_simprocs.ML   Sprache: Isabelle

Untersuchung Isabelle©
(*  Title:      HOL/Library/List_Lenlexorder.thy
*)

section \<open>Lexicographic order on lists\<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

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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot  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