Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Countable_Complete_Lattices.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Countable_Complete_Lattices.thy
    Author:     Johannes Hölzl
*)

section \<open>Countable Complete Lattices\<close>

theory Countable_Complete_Lattices
  imports Main Countable_Set
begin

lemma UNIV_nat_eq: "UNIV = insert 0 (range Suc)"
  by (metis UNIV_eq_I nat.nchotomy insertCI rangeI)

class countable_complete_lattice = lattice + Inf + Sup + bot + top +
  assumes ccInf_lower: "countable A \ x \ A \ Inf A \ x"
  assumes ccInf_greatest: "countable A \ (\x. x \ A \ z \ x) \ z \ Inf A"
  assumes ccSup_upper: "countable A \ x \ A \ x \ Sup A"
  assumes ccSup_least: "countable A \ (\x. x \ A \ x \ z) \ Sup A \ z"
  assumes ccInf_empty [simp]: "Inf {} = top"
  assumes ccSup_empty [simp]: "Sup {} = bot"
begin

subclass bounded_lattice
proof
  fix a
  show "bot \ a" by (auto intro: ccSup_least simp only: ccSup_empty [symmetric])
  show "a \ top" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric])
qed

lemma ccINF_lower: "countable A \ i \ A \ (INF i \ A. f i) \ f i"
  using ccInf_lower [of "f ` A"] by simp

lemma ccINF_greatest: "countable A \ (\i. i \ A \ u \ f i) \ u \ (INF i \ A. f i)"
  using ccInf_greatest [of "f ` A"] by auto

lemma ccSUP_upper: "countable A \ i \ A \ f i \ (SUP i \ A. f i)"
  using ccSup_upper [of "f ` A"] by simp

lemma ccSUP_least: "countable A \ (\i. i \ A \ f i \ u) \ (SUP i \ A. f i) \ u"
  using ccSup_least [of "f ` A"] by auto

lemma ccInf_lower2: "countable A \ u \ A \ u \ v \ Inf A \ v"
  using ccInf_lower [of A u] by auto

lemma ccINF_lower2: "countable A \ i \ A \ f i \ u \ (INF i \ A. f i) \ u"
  using ccINF_lower [of A i f] by auto

lemma ccSup_upper2: "countable A \ u \ A \ v \ u \ v \ Sup A"
  using ccSup_upper [of A u] by auto

lemma ccSUP_upper2: "countable A \ i \ A \ u \ f i \ u \ (SUP i \ A. f i)"
  using ccSUP_upper [of A i f] by auto

lemma le_ccInf_iff: "countable A \ b \ Inf A \ (\a\A. b \ a)"
  by (auto intro: ccInf_greatest dest: ccInf_lower)

lemma le_ccINF_iff: "countable A \ u \ (INF i \ A. f i) \ (\i\A. u \ f i)"
  using le_ccInf_iff [of "f ` A"] by simp

lemma ccSup_le_iff: "countable A \ Sup A \ b \ (\a\A. a \ b)"
  by (auto intro: ccSup_least dest: ccSup_upper)

lemma ccSUP_le_iff: "countable A \ (SUP i \ A. f i) \ u \ (\i\A. f i \ u)"
  using ccSup_le_iff [of "f ` A"] by simp

lemma ccInf_insert [simp]: "countable A \ Inf (insert a A) = inf a (Inf A)"
  by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower)

lemma ccINF_insert [simp]: "countable A \ (INF x\insert a A. f x) = inf (f a) (Inf (f ` A))"
  unfolding image_insert by simp

lemma ccSup_insert [simp]: "countable A \ Sup (insert a A) = sup a (Sup A)"
  by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper)

lemma ccSUP_insert [simp]: "countable A \ (SUP x\insert a A. f x) = sup (f a) (Sup (f ` A))"
  unfolding image_insert by simp

lemma ccINF_empty [simp]: "(INF x\{}. f x) = top"
  unfolding image_empty by simp

lemma ccSUP_empty [simp]: "(SUP x\{}. f x) = bot"
  unfolding image_empty by simp

lemma ccInf_superset_mono: "countable A \ B \ A \ Inf A \ Inf B"
  by (auto intro: ccInf_greatest ccInf_lower countable_subset)

lemma ccSup_subset_mono: "countable B \ A \ B \ Sup A \ Sup B"
  by (auto intro: ccSup_least ccSup_upper countable_subset)

lemma ccInf_mono:
  assumes [intro]: "countable B" "countable A"
  assumes "\b. b \ B \ \a\A. a \ b"
  shows "Inf A \ Inf B"
proof (rule ccInf_greatest)
  fix b assume "b \ B"
  with assms obtain a where "a \ A" and "a \ b" by blast
  from \<open>a \<in> A\<close> have "Inf A \<le> a" by (rule ccInf_lower[rotated]) auto
  with \<open>a \<le> b\<close> show "Inf A \<le> b" by auto
qed auto

lemma ccINF_mono:
  "countable A \ countable B \ (\m. m \ B \ \n\A. f n \ g m) \ (INF n\A. f n) \ (INF n\B. g n)"
  using ccInf_mono [of "g ` B" "f ` A"] by auto

lemma ccSup_mono:
  assumes [intro]: "countable B" "countable A"
  assumes "\a. a \ A \ \b\B. a \ b"
  shows "Sup A \ Sup B"
proof (rule ccSup_least)
  fix a assume "a \ A"
  with assms obtain b where "b \ B" and "a \ b" by blast
  from \<open>b \<in> B\<close> have "b \<le> Sup B" by (rule ccSup_upper[rotated]) auto
  with \<open>a \<le> b\<close> show "a \<le> Sup B" by auto
qed auto

lemma ccSUP_mono:
  "countable A \ countable B \ (\n. n \ A \ \m\B. f n \ g m) \ (SUP n\A. f n) \ (SUP n\B. g n)"
  using ccSup_mono [of "g ` B" "f ` A"] by auto

lemma ccINF_superset_mono:
  "countable A \ B \ A \ (\x. x \ B \ f x \ g x) \ (INF x\A. f x) \ (INF x\B. g x)"
  by (blast intro: ccINF_mono countable_subset dest: subsetD)

lemma ccSUP_subset_mono:
  "countable B \ A \ B \ (\x. x \ A \ f x \ g x) \ (SUP x\A. f x) \ (SUP x\B. g x)"
  by (blast intro: ccSUP_mono countable_subset dest: subsetD)

lemma less_eq_ccInf_inter: "countable A \ countable B \ sup (Inf A) (Inf B) \ Inf (A \ B)"
  by (auto intro: ccInf_greatest ccInf_lower)

lemma ccSup_inter_less_eq: "countable A \ countable B \ Sup (A \ B) \ inf (Sup A) (Sup B)"
  by (auto intro: ccSup_least ccSup_upper)

lemma ccInf_union_distrib: "countable A \ countable B \ Inf (A \ B) = inf (Inf A) (Inf B)"
  by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2)

lemma ccINF_union:
  "countable A \ countable B \ (INF i\A \ B. M i) = inf (INF i\A. M i) (INF i\B. M i)"
  by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower)

lemma ccSup_union_distrib: "countable A \ countable B \ Sup (A \ B) = sup (Sup A) (Sup B)"
  by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2)

lemma ccSUP_union:
  "countable A \ countable B \ (SUP i\A \ B. M i) = sup (SUP i\A. M i) (SUP i\B. M i)"
  by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper)

lemma ccINF_inf_distrib: "countable A \ inf (INF a\A. f a) (INF a\A. g a) = (INF a\A. inf (f a) (g a))"
  by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono)

lemma ccSUP_sup_distrib: "countable A \ sup (SUP a\A. f a) (SUP a\A. g a) = (SUP a\A. sup (f a) (g a))"
  by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono)

lemma ccINF_const [simp]: "A \ {} \ (INF i \ A. f) = f"
  unfolding image_constant_conv by auto

lemma ccSUP_const [simp]: "A \ {} \ (SUP i \ A. f) = f"
  unfolding image_constant_conv by auto

lemma ccINF_top [simp]: "(INF x\A. top) = top"
  by (cases "A = {}") simp_all

lemma ccSUP_bot [simp]: "(SUP x\A. bot) = bot"
  by (cases "A = {}") simp_all

lemma ccINF_commute: "countable A \ countable B \ (INF i\A. INF j\B. f i j) = (INF j\B. INF i\A. f i j)"
  by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym)

lemma ccSUP_commute: "countable A \ countable B \ (SUP i\A. SUP j\B. f i j) = (SUP j\B. SUP i\A. f i j)"
  by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym)

end

context
  fixes a :: "'a::{countable_complete_lattice, linorder}"
begin

lemma less_ccSup_iff: "countable S \ a < Sup S \ (\x\S. a < x)"
  unfolding not_le [symmetric] by (subst ccSup_le_iff) auto

lemma less_ccSUP_iff: "countable A \ a < (SUP i\A. f i) \ (\x\A. a < f x)"
  using less_ccSup_iff [of "f ` A"] by simp

lemma ccInf_less_iff: "countable S \ Inf S < a \ (\x\S. x < a)"
  unfolding not_le [symmetric] by (subst le_ccInf_iff) auto

lemma ccINF_less_iff: "countable A \ (INF i\A. f i) < a \ (\x\A. f x < a)"
  using ccInf_less_iff [of "f ` A"] by simp

end

class countable_complete_distrib_lattice = countable_complete_lattice +
  assumes sup_ccInf: "countable B \ sup a (Inf B) = (INF b\B. sup a b)"
  assumes inf_ccSup: "countable B \ inf a (Sup B) = (SUP b\B. inf a b)"
begin

lemma sup_ccINF:
  "countable B \ sup a (INF b\B. f b) = (INF b\B. sup a (f b))"
  by (simp only: sup_ccInf image_image countable_image)

lemma inf_ccSUP:
  "countable B \ inf a (SUP b\B. f b) = (SUP b\B. inf a (f b))"
  by (simp only: inf_ccSup image_image countable_image)

subclass distrib_lattice
proof
  fix a b c
  from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d\{b, c}. sup a d)"
    by simp
  then show "sup a (inf b c) = inf (sup a b) (sup a c)"
    by simp
qed

lemma ccInf_sup:
  "countable B \ sup (Inf B) a = (INF b\B. sup b a)"
  by (simp add: sup_ccInf sup_commute)

lemma ccSup_inf:
  "countable B \ inf (Sup B) a = (SUP b\B. inf b a)"
  by (simp add: inf_ccSup inf_commute)

lemma ccINF_sup:
  "countable B \ sup (INF b\B. f b) a = (INF b\B. sup (f b) a)"
  by (simp add: sup_ccINF sup_commute)

lemma ccSUP_inf:
  "countable B \ inf (SUP b\B. f b) a = (SUP b\B. inf (f b) a)"
  by (simp add: inf_ccSUP inf_commute)

lemma ccINF_sup_distrib2:
  "countable A \ countable B \ sup (INF a\A. f a) (INF b\B. g b) = (INF a\A. INF b\B. sup (f a) (g b))"
  by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup)

lemma ccSUP_inf_distrib2:
  "countable A \ countable B \ inf (SUP a\A. f a) (SUP b\B. g b) = (SUP a\A. SUP b\B. inf (f a) (g b))"
  by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf)

context
  fixes f :: "'a \ 'b::countable_complete_lattice"
  assumes "mono f"
begin

lemma mono_ccInf:
  "countable A \ f (Inf A) \ (INF x\A. f x)"
  using \<open>mono f\<close>
  by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD)

lemma mono_ccSup:
  "countable A \ (SUP x\A. f x) \ f (Sup A)"
  using \<open>mono f\<close> by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD)

lemma mono_ccINF:
  "countable I \ f (INF i \ I. A i) \ (INF x \ I. f (A x))"
  by (intro countable_complete_lattice_class.ccINF_greatest monoD[OF \<open>mono f\<close>] ccINF_lower)

lemma mono_ccSUP:
  "countable I \ (SUP x \ I. f (A x)) \ f (SUP i \ I. A i)"
  by (intro countable_complete_lattice_class.ccSUP_least monoD[OF \<open>mono f\<close>] ccSUP_upper)

end

end

subsubsection \<open>Instances of countable complete lattices\<close>

instance "fun" :: (type, countable_complete_lattice) countable_complete_lattice
  by standard
     (auto simp: le_fun_def intro!: ccSUP_upper ccSUP_least ccINF_lower ccINF_greatest)

subclass (in complete_lattice) countable_complete_lattice
  by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)

subclass (in complete_distrib_lattice) countable_complete_distrib_lattice
  by standard (auto intro: sup_Inf inf_Sup)

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.