Theory Countable_Complete_Lattices

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

section ‹Countable Complete Lattices›

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) (INFIMUM A f)"
  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) (SUPREMUM A f)"
  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 ‹a ∈ A› have "Inf A ≤ a" by (rule ccInf_lower[rotated]) auto
  with ‹a ≤ b› show "Inf A ≤ 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 ‹b ∈ B› have "b ≤ Sup B" by (rule ccSup_upper[rotated]) auto
  with ‹a ≤ b› show "a ≤ 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 ‹mono f›
  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 ‹mono f› 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 ‹mono f›] 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 ‹mono f›] ccSUP_upper)

end

end

subsubsection ‹Instances of countable complete lattices›

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