Quellcode-Bibliothek Finite_Lattice.thy Sprache: Isabelle

(*  Title:      HOL/Library/Finite_Lattice.thy
    Author:     Alessandro Coglio
*)

section \<open>Finite Lattices\<close>

theory Finite_Lattice
imports Product_Order
begin

subsection \<open>Finite Complete Lattices\<close>

text \<open>A non-empty finite lattice is a complete lattice.
Since types are never empty in Isabelle/HOL,
a type of classes \<^class>\<open>finite\<close> and \<^class>\<open>lattice\<close>
should also have class \<^class>\<open>complete_lattice\<close>.
A type class is defined
that extends classes \<^class>\<open>finite\<close> and \<^class>\<open>lattice\<close>
with the operators \<^const>\<open>bot\<close>, \<^const>\<open>top\<close>, \<^const>\<open>Inf\<close>, and \<^const>\<open>Sup\<close>,
along with assumptions that define these operators
in terms of the ones of classes \<^class>\<open>finite\<close> and \<^class>\<open>lattice\<close>.
The resulting class is a subclass of \<^class>\<open>complete_lattice\<close>.\<close>

class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
  assumes bot_def: "bot = Inf_fin UNIV"
  assumes top_def: "top = Sup_fin UNIV"
  assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
  assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"

text \<open>The definitional assumptions
on the operators \<^const>\<open>bot\<close> and \<^const>\<open>top\<close>
of class \<^class>\<open>finite_lattice_complete\<close>
ensure that they yield bottom and top.\<close>

lemma finite_lattice_complete_bot_least: "(bot::'a::finite_lattice_complete) \ x"
  by (auto simp: bot_def intro: Inf_fin.coboundedI)

instance finite_lattice_complete \<subseteq> order_bot
  by standard (auto simp: finite_lattice_complete_bot_least)

lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \ x"
  by (auto simp: top_def Sup_fin.coboundedI)

instance finite_lattice_complete \<subseteq> order_top
  by standard (auto simp: finite_lattice_complete_top_greatest)

instance finite_lattice_complete \<subseteq> bounded_lattice ..

text \<open>The definitional assumptions
on the operators \<^const>\<open>Inf\<close> and \<^const>\<open>Sup\<close>
of class \<^class>\<open>finite_lattice_complete\<close>
ensure that they yield infimum and supremum.\<close>

lemma finite_lattice_complete_Inf_empty: "Inf {} = (top :: 'a::finite_lattice_complete)"
  by (simp add: Inf_def)

lemma finite_lattice_complete_Sup_empty: "Sup {} = (bot :: 'a::finite_lattice_complete)"
  by (simp add: Sup_def)

lemma finite_lattice_complete_Inf_insert:
  fixes A :: "'a::finite_lattice_complete set"
  shows "Inf (insert x A) = inf x (Inf A)"
proof -
  interpret comp_fun_idem "inf :: 'a \ _"
    by (fact comp_fun_idem_inf)
  show ?thesis by (simp add: Inf_def)
qed

lemma finite_lattice_complete_Sup_insert:
  fixes A :: "'a::finite_lattice_complete set"
  shows "Sup (insert x A) = sup x (Sup A)"
proof -
  interpret comp_fun_idem "sup :: 'a \ _"
    by (fact comp_fun_idem_sup)
  show ?thesis by (simp add: Sup_def)
qed

lemma finite_lattice_complete_Inf_lower:
  "(x::'a::finite_lattice_complete) \ A \ Inf A \ x"
  using finite [of A]
  by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)

lemma finite_lattice_complete_Inf_greatest:
  "\x::'a::finite_lattice_complete \ A. z \ x \ z \ Inf A"
  using finite [of A]
  by (induct A) (auto simp add: finite_lattice_complete_Inf_empty finite_lattice_complete_Inf_insert)

lemma finite_lattice_complete_Sup_upper:
  "(x::'a::finite_lattice_complete) \ A \ Sup A \ x"
  using finite [of A]
  by (induct A) (auto simp add: finite_lattice_complete_Sup_insert intro: le_supI2)

lemma finite_lattice_complete_Sup_least:
  "\x::'a::finite_lattice_complete \ A. z \ x \ z \ Sup A"
  using finite [of A]
  by (induct A) (auto simp add: finite_lattice_complete_Sup_empty finite_lattice_complete_Sup_insert)

instance finite_lattice_complete \<subseteq> complete_lattice
proof
qed (auto simp:
  finite_lattice_complete_Inf_lower
  finite_lattice_complete_Inf_greatest
  finite_lattice_complete_Sup_upper
  finite_lattice_complete_Sup_least
  finite_lattice_complete_Inf_empty
  finite_lattice_complete_Sup_empty)

text \<open>The product of two finite lattices is already a finite lattice.\<close>

lemma finite_bot_prod:
  "(bot :: ('a::finite_lattice_complete \ 'b::finite_lattice_complete)) =
    Inf_fin UNIV"
  by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)

lemma finite_top_prod:
  "(top :: ('a::finite_lattice_complete \ 'b::finite_lattice_complete)) =
    Sup_fin UNIV"
  by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)

lemma finite_Inf_prod:
  "Inf(A :: ('a::finite_lattice_complete \ 'b::finite_lattice_complete) set) =
    Finite_Set.fold inf top A"
  by (metis Inf_fold_inf finite)

lemma finite_Sup_prod:
  "Sup (A :: ('a::finite_lattice_complete \ 'b::finite_lattice_complete) set) =
    Finite_Set.fold sup bot A"
  by (metis Sup_fold_sup finite)

instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
  by standard (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)

text \<open>Functions with a finite domain and with a finite lattice as codomain
already form a finite lattice.\<close>

lemma finite_bot_fun: "(bot :: ('a::finite \ 'b::finite_lattice_complete)) = Inf_fin UNIV"
  by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite)

lemma finite_top_fun: "(top :: ('a::finite \ 'b::finite_lattice_complete)) = Sup_fin UNIV"
  by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite)

lemma finite_Inf_fun:
  "Inf (A::('a::finite \ 'b::finite_lattice_complete) set) =
    Finite_Set.fold inf top A"
  by (metis Inf_fold_inf finite)

lemma finite_Sup_fun:
  "Sup (A::('a::finite \ 'b::finite_lattice_complete) set) =
    Finite_Set.fold sup bot A"
  by (metis Sup_fold_sup finite)

instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
  by standard (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)

subsection \<open>Finite Distributive Lattices\<close>

text \<open>A finite distributive lattice is a complete lattice
whose \<^const>\<open>inf\<close> and \<^const>\<open>sup\<close> operators
distribute over \<^const>\<open>Sup\<close> and \<^const>\<open>Inf\<close>.\<close>

class finite_distrib_lattice_complete =
  distrib_lattice + finite_lattice_complete

lemma finite_distrib_lattice_complete_sup_Inf:
  "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y\A. sup x y)"
  using finite
  by (induct A rule: finite_induct) (simp_all add: sup_inf_distrib1)

lemma finite_distrib_lattice_complete_inf_Sup:
  "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y\A. inf x y)"
  using finite [of A] by induct (simp_all add: inf_sup_distrib1)

context finite_distrib_lattice_complete
begin
subclass finite_distrib_lattice
proof -
  show "class.finite_distrib_lattice Inf Sup inf (\) (<) sup bot top"
  proof
    show "bot = Inf UNIV"
      unfolding bot_def top_def Inf_def
      using Inf_fin.eq_fold Inf_fin.insert inf.absorb2 by force
  next
    show "top = Sup UNIV"
      unfolding bot_def top_def Sup_def
      using Sup_fin.eq_fold Sup_fin.insert by force
  next
    show "Inf {} = Sup UNIV"
      unfolding Inf_def Sup_def bot_def top_def
      using Sup_fin.eq_fold Sup_fin.insert by force
  next
    show "Sup {} = Inf UNIV"
      unfolding Inf_def Sup_def bot_def top_def
      using Inf_fin.eq_fold Inf_fin.insert inf.absorb2 by force
  next
    interpret comp_fun_idem_inf: comp_fun_idem inf
      by (fact comp_fun_idem_inf)
    show "Inf (insert a A) = inf a (Inf A)" for a A
      using comp_fun_idem_inf.fold_insert_idem Inf_def finite by simp
  next
    interpret comp_fun_idem_sup: comp_fun_idem sup
      by (fact comp_fun_idem_sup)
    show "Sup (insert a A) = sup a (Sup A)" for a A
      using comp_fun_idem_sup.fold_insert_idem Sup_def finite by simp
  qed
qed
end

instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice ..

text \<open>The product of two finite distributive lattices
is already a finite distributive lattice.\<close>

instance prod ::
  (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
  finite_distrib_lattice_complete
  ..

text \<open>Functions with a finite domain
and with a finite distributive lattice as codomain
already form a finite distributive lattice.\<close>

instance "fun" ::
  (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
  ..

subsection \<open>Linear Orders\<close>

text \<open>A linear order is a distributive lattice.
A type class is defined
that extends class \<^class>\<open>linorder\<close>
with the operators \<^const>\<open>inf\<close> and \<^const>\<open>sup\<close>,
along with assumptions that define these operators
in terms of the ones of class \<^class>\<open>linorder\<close>.
The resulting class is a subclass of \<^class>\<open>distrib_lattice\<close>.\<close>

class linorder_lattice = linorder + inf + sup +
  assumes inf_def: "inf x y = (if x \ y then x else y)"
  assumes sup_def: "sup x y = (if x \ y then x else y)"

text \<open>The definitional assumptions
on the operators \<^const>\<open>inf\<close> and \<^const>\<open>sup\<close>
of class \<^class>\<open>linorder_lattice\<close>
ensure that they yield infimum and supremum
and that they distribute over each other.\<close>

lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \ x"
  unfolding inf_def by (metis (full_types) linorder_linear)

lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \ y"
  unfolding inf_def by (metis (full_types) linorder_linear)

lemma linorder_lattice_inf_greatest:
  "(x::'a::linorder_lattice) \ y \ x \ z \ x \ inf y z"
  unfolding inf_def by (metis (full_types))

lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \ x"
  unfolding sup_def by (metis (full_types) linorder_linear)

lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \ y"
  unfolding sup_def by (metis (full_types) linorder_linear)

lemma linorder_lattice_sup_least:
  "(x::'a::linorder_lattice) \ y \ x \ z \ x \ sup y z"
  by (auto simp: sup_def)

lemma linorder_lattice_sup_inf_distrib1:
  "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
  by (auto simp: inf_def sup_def)

instance linorder_lattice \<subseteq> distrib_lattice
proof
qed (auto simp:
  linorder_lattice_inf_le1
  linorder_lattice_inf_le2
  linorder_lattice_inf_greatest
  linorder_lattice_sup_ge1
  linorder_lattice_sup_ge2
  linorder_lattice_sup_least
  linorder_lattice_sup_inf_distrib1)

subsection \<open>Finite Linear Orders\<close>

text \<open>A (non-empty) finite linear order is a complete linear order.\<close>

class finite_linorder_complete = linorder_lattice + finite_lattice_complete

instance finite_linorder_complete \<subseteq> complete_linorder ..

text \<open>A (non-empty) finite linear order is a complete lattice
whose \<^const>\<open>inf\<close> and \<^const>\<open>sup\<close> operators
distribute over \<^const>\<open>Sup\<close> and \<^const>\<open>Inf\<close>.\<close>

instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..

end

quality99%

¤ 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.0.16Bemerkung: (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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.