(* Title: HOL/Lattices_Big.thy
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
with contributions by Jeremy Avigad
*)
header {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}
theory Lattices_Big
imports Finite_Set Option
begin
subsection {* Generic lattice operations over a set *}
no_notation times (infixl "*" 70)
no_notation Groups.one ("1")
subsubsection {* Without neutral element *}
locale semilattice_set = semilattice
begin
interpretation comp_fun_idem f
by default (simp_all add: fun_eq_iff left_commute)
definition F :: "'a set \ 'a"
where
eq_fold': "F A = the (Finite_Set.fold (\x y. Some (case y of None \ x | Some z \ f x z)) None A)"
lemma eq_fold:
assumes "finite A"
shows "F (insert x A) = Finite_Set.fold f x A"
proof (rule sym)
let ?f = "\x y. Some (case y of None \ x | Some z \ f x z)"
interpret comp_fun_idem "?f"
by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
from assms show "Finite_Set.fold f x A = F (insert x A)"
proof induct
case empty then show ?case by (simp add: eq_fold')
next
case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
qed
qed
lemma singleton [simp]:
"F {x} = x"
by (simp add: eq_fold)
lemma insert_not_elem:
assumes "finite A" and "x \ A" and "A \ {}"
shows "F (insert x A) = x * F A"
proof -
from `A \ {}` obtain b where "b \ A" by blast
then obtain B where *: "A = insert b B" "b \ B" by (blast dest: mk_disjoint_insert)
with `finite A` and `x \ A`
have "finite (insert x B)" and "b \ insert x B" by auto
then have "F (insert b (insert x B)) = x * F (insert b B)"
by (simp add: eq_fold)
then show ?thesis by (simp add: * insert_commute)
qed
lemma in_idem:
assumes "finite A" and "x \ A"
shows "x * F A = F A"
proof -
from assms have "A \ {}" by auto
with `finite A` show ?thesis using `x \ A`
by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
qed
lemma insert [simp]:
assumes "finite A" and "A \ {}"
shows "F (insert x A) = x * F A"
using assms by (cases "x \ A") (simp_all add: insert_absorb in_idem insert_not_elem)
lemma union:
assumes "finite A" "A \ {}" and "finite B" "B \ {}"
shows "F (A \ B) = F A * F B"
using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
lemma remove:
assumes "finite A" and "x \ A"
shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
proof -
from assms obtain B where "A = insert x B" and "x \ B" by (blast dest: mk_disjoint_insert)
with assms show ?thesis by simp
qed
lemma insert_remove:
assumes "finite A"
shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
using assms by (cases "x \ A") (simp_all add: insert_absorb remove)
lemma subset:
assumes "finite A" "B \ {}" and "B \ A"
shows "F B * F A = F A"
proof -
from assms have "A \ {}" and "finite B" by (auto dest: finite_subset)
with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
qed
lemma closed:
assumes "finite A" "A \ {}" and elem: "\x y. x * y \ {x, y}"
shows "F A \ A"
using `finite A` `A \ {}` proof (induct rule: finite_ne_induct)
case singleton then show ?case by simp
next
case insert with elem show ?case by force
qed
lemma hom_commute:
assumes hom: "\x y. h (x * y) = h x * h y"
and N: "finite N" "N \ {}"
shows "h (F N) = F (h ` N)"
using N proof (induct rule: finite_ne_induct)
case singleton thus ?case by simp
next
case (insert n N)
then have "h (F (insert n N)) = h (n * F N)" by simp
also have "\ = h n * h (F N)" by (rule hom)
also have "h (F N) = F (h ` N)" by (rule insert)
also have "h n * \ = F (insert (h n) (h ` N))"
using insert by simp
also have "insert (h n) (h ` N) = h ` insert n N" by simp
finally show ?case .
qed
lemma infinite: "\ finite A \ F A = the None"
unfolding eq_fold' by (cases "finite (UNIV::'a set)") (auto intro: finite_subset fold_infinite)
end
locale semilattice_order_set = binary?: semilattice_order + semilattice_set
begin
lemma bounded_iff:
assumes "finite A" and "A \ {}"
shows "x \ F A \ (\a\A. x \ a)"
using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
lemma boundedI:
assumes "finite A"
assumes "A \ {}"
assumes "\a. a \ A \ x \ a"
shows "x \ F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
assumes "finite A" and "A \ {}" and "x \ F A"
obtains "\a. a \ A \ x \ a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \ A"
shows "F A \ a"
proof -
from assms have "A \ {}" by auto
from `finite A` `A \ {}` `a \ A` show ?thesis
proof (induct rule: finite_ne_induct)
case singleton thus ?case by (simp add: refl)
next
case (insert x B)
from insert have "a = x \ a \ B" by simp
then show ?case using insert by (auto intro: coboundedI2)
qed
qed
lemma antimono:
assumes "A \ B" and "A \ {}" and "finite B"
shows "F B \ F A"
proof (cases "A = B")
case True then show ?thesis by (simp add: refl)
next
case False
have B: "B = A \ (B - A)" using `A \ B` by blast
then have "F B = F (A \ (B - A))" by simp
also have "\ = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
also have "\ \ F A" by simp
finally show ?thesis .
qed
end
subsubsection {* With neutral element *}
locale semilattice_neutr_set = semilattice_neutr
begin
interpretation comp_fun_idem f
by default (simp_all add: fun_eq_iff left_commute)
definition F :: "'a set \ 'a"
where
eq_fold: "F A = Finite_Set.fold f 1 A"
lemma infinite [simp]:
"\ finite A \ F A = 1"
by (simp add: eq_fold)
lemma empty [simp]:
"F {} = 1"
by (simp add: eq_fold)
lemma insert [simp]:
assumes "finite A"
shows "F (insert x A) = x * F A"
using assms by (simp add: eq_fold)
lemma in_idem:
assumes "finite A" and "x \ A"
shows "x * F A = F A"
proof -
from assms have "A \ {}" by auto
with `finite A` show ?thesis using `x \ A`
by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
qed
lemma union:
assumes "finite A" and "finite B"
shows "F (A \ B) = F A * F B"
using assms by (induct A) (simp_all add: ac_simps)
lemma remove:
assumes "finite A" and "x \ A"
shows "F A = x * F (A - {x})"
proof -
from assms obtain B where "A = insert x B" and "x \ B" by (blast dest: mk_disjoint_insert)
with assms show ?thesis by simp
qed
lemma insert_remove:
assumes "finite A"
shows "F (insert x A) = x * F (A - {x})"
using assms by (cases "x \ A") (simp_all add: insert_absorb remove)
lemma subset:
assumes "finite A" and "B \ A"
shows "F B * F A = F A"
proof -
from assms have "finite B" by (auto dest: finite_subset)
with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
qed
lemma closed:
assumes "finite A" "A \ {}" and elem: "\x y. x * y \ {x, y}"
shows "F A \ A"
using `finite A` `A \ {}` proof (induct rule: finite_ne_induct)
case singleton then show ?case by simp
next
case insert with elem show ?case by force
qed
end
locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
begin
lemma bounded_iff:
assumes "finite A"
shows "x \ F A \ (\a\A. x \ a)"
using assms by (induct A) (simp_all add: bounded_iff)
lemma boundedI:
assumes "finite A"
assumes "\a. a \ A \ x \ a"
shows "x \ F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
assumes "finite A" and "x \ F A"
obtains "\a. a \ A \ x \ a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \ A"
shows "F A \ a"
proof -
from assms have "A \ {}" by auto
from `finite A` `A \ {}` `a \ A` show ?thesis
proof (induct rule: finite_ne_induct)
case singleton thus ?case by (simp add: refl)
next
case (insert x B)
from insert have "a = x \ a \ B" by simp
then show ?case using insert by (auto intro: coboundedI2)
qed
qed
lemma antimono:
assumes "A \ B" and "finite B"
shows "F B \ F A"
proof (cases "A = B")
case True then show ?thesis by (simp add: refl)
next
case False
have B: "B = A \ (B - A)" using `A \ B` by blast
then have "F B = F (A \ (B - A))" by simp
also have "\ = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
also have "\ \ F A" by simp
finally show ?thesis .
qed
end
notation times (infixl "*" 70)
notation Groups.one ("1")
subsection {* Lattice operations on finite sets *}
context semilattice_inf
begin
definition Inf_fin :: "'a set \ 'a" ("\\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
where
"Inf_fin = semilattice_set.F inf"
sublocale Inf_fin!: semilattice_order_set inf less_eq less
where
"semilattice_set.F inf = Inf_fin"
proof -
show "semilattice_order_set inf less_eq less" ..
then interpret Inf_fin!: semilattice_order_set inf less_eq less .
from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
qed
end
context semilattice_sup
begin
definition Sup_fin :: "'a set \ 'a" ("\\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
where
"Sup_fin = semilattice_set.F sup"
sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
where
"semilattice_set.F sup = Sup_fin"
proof -
show "semilattice_order_set sup greater_eq greater" ..
then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
qed
end
subsection {* Infimum and Supremum over non-empty sets *}
context lattice
begin
lemma Inf_fin_le_Sup_fin [simp]:
assumes "finite A" and "A \ {}"
shows "\\<^sub>f\<^sub>i\<^sub>nA \ \\<^sub>f\<^sub>i\<^sub>nA"
proof -
from `A \ {}` obtain a where "a \ A" by blast
with `finite A` have "\\<^sub>f\<^sub>i\<^sub>nA \ a" by (rule Inf_fin.coboundedI)
moreover from `finite A` `a \ A` have "a \ \\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
ultimately show ?thesis by (rule order_trans)
qed
lemma sup_Inf_absorb [simp]:
"finite A \ a \ A \ \\<^sub>f\<^sub>i\<^sub>nA \ a = a"
by (rule sup_absorb2) (rule Inf_fin.coboundedI)
lemma inf_Sup_absorb [simp]:
"finite A \ a \ A \ a \ \\<^sub>f\<^sub>i\<^sub>nA = a"
by (rule inf_absorb1) (rule Sup_fin.coboundedI)
end
context distrib_lattice
begin
lemma sup_Inf1_distrib:
assumes "finite A"
and "A \ {}"
shows "sup x (\\<^sub>f\<^sub>i\<^sub>nA) = \\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \ A}"
using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
(rule arg_cong [where f="Inf_fin"], blast)
lemma sup_Inf2_distrib:
assumes A: "finite A" "A \ {}" and B: "finite B" "B \ {}"
shows "sup (\\<^sub>f\<^sub>i\<^sub>nA) (\\<^sub>f\<^sub>i\<^sub>nB) = \\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \ A \ b \ B}"
using A proof (induct rule: finite_ne_induct)
case singleton then show ?case
by (simp add: sup_Inf1_distrib [OF B])
next
case (insert x A)
have finB: "finite {sup x b |b. b \ B}"
by (rule finite_surj [where f = "sup x", OF B(1)], auto)
have finAB: "finite {sup a b |a b. a \ A \ b \ B}"
proof -
have "{sup a b |a b. a \ A \ b \ B} = (UN a:A. UN b:B. {sup a b})"
by blast
thus ?thesis by(simp add: insert(1) B(1))
qed
have ne: "{sup a b |a b. a \ A \ b \ B} \ {}" using insert B by blast
have "sup (\\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\\<^sub>f\<^sub>i\<^sub>nA)) (\\<^sub>f\<^sub>i\<^sub>nB)"
using insert by simp
also have "\ = inf (sup x (\\<^sub>f\<^sub>i\<^sub>nB)) (sup (\\<^sub>f\<^sub>i\<^sub>nA) (\\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2)
also have "\ = inf (\\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \ B}) (\\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \ A \ b \ B})"
using insert by(simp add:sup_Inf1_distrib[OF B])
also have "\ = \\<^sub>f\<^sub>i\<^sub>n({sup x b |b. b \ B} \ {sup a b |a b. a \ A \ b \ B})"
(is "_ = \\<^sub>f\<^sub>i\<^sub>n?M")
using B insert
by (simp add: Inf_fin.union [OF finB _ finAB ne])
also have "?M = {sup a b |a b. a \ insert x A \ b \ B}"
by blast
finally show ?case .
qed
lemma inf_Sup1_distrib:
assumes "finite A" and "A \ {}"
shows "inf x (\\<^sub>f\<^sub>i\<^sub>nA) = \\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \ A}"
using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
(rule arg_cong [where f="Sup_fin"], blast)
lemma inf_Sup2_distrib:
assumes A: "finite A" "A \ {}" and B: "finite B" "B \ {}"
shows "inf (\\<^sub>f\<^sub>i\<^sub>nA) (\\<^sub>f\<^sub>i\<^sub>nB) = \\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \ A \ b \ B}"
using A proof (induct rule: finite_ne_induct)
case singleton thus ?case
by(simp add: inf_Sup1_distrib [OF B])
next
case (insert x A)
have finB: "finite {inf x b |b. b \ B}"
by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
have finAB: "finite {inf a b |a b. a \ A \ b \ B}"
proof -
have "{inf a b |a b. a \ A \ b \ B} = (UN a:A. UN b:B. {inf a b})"
by blast
thus ?thesis by(simp add: insert(1) B(1))
qed
have ne: "{inf a b |a b. a \ A \ b \ B} \ {}" using insert B by blast
have "inf (\\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\\<^sub>f\<^sub>i\<^sub>nA)) (\\<^sub>f\<^sub>i\<^sub>nB)"
using insert by simp
also have "\ = sup (inf x (\\<^sub>f\<^sub>i\<^sub>nB)) (inf (\\<^sub>f\<^sub>i\<^sub>nA) (\\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2)
also have "\ = sup (\\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \ B}) (\\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \ A \ b \ B})"
using insert by(simp add:inf_Sup1_distrib[OF B])
also have "\ = \\<^sub>f\<^sub>i\<^sub>n({inf x b |b. b \ B} \ {inf a b |a b. a \ A \ b \ B})"
(is "_ = \\<^sub>f\<^sub>i\<^sub>n?M")
using B insert
by (simp add: Sup_fin.union [OF finB _ finAB ne])
also have "?M = {inf a b |a b. a \ insert x A \ b \ B}"
by blast
finally show ?case .
qed
end
context complete_lattice
begin
lemma Inf_fin_Inf:
assumes "finite A" and "A \ {}"
shows "\\<^sub>f\<^sub>i\<^sub>nA = \A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
qed
lemma Sup_fin_Sup:
assumes "finite A" and "A \ {}"
shows "\\<^sub>f\<^sub>i\<^sub>nA = \A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
qed
end
subsection {* Minimum and Maximum over non-empty sets *}
context linorder
begin
definition Min :: "'a set \ 'a"
where
"Min = semilattice_set.F min"
definition Max :: "'a set \ 'a"
where
"Max = semilattice_set.F max"
sublocale Min!: semilattice_order_set min less_eq less
+ Max!: semilattice_order_set max greater_eq greater
where
"semilattice_set.F min = Min"
and "semilattice_set.F max = Max"
proof -
show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
then interpret Min!: semilattice_order_set min less_eq less .
show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
then interpret Max!: semilattice_order_set max greater_eq greater .
from Min_def show "semilattice_set.F min = Min" by rule
from Max_def show "semilattice_set.F max = Max" by rule
qed
end
text {* An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
lemma Inf_fin_Min:
"Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \ 'a)"
by (simp add: Inf_fin_def Min_def inf_min)
lemma Sup_fin_Max:
"Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \ 'a)"
by (simp add: Sup_fin_def Max_def sup_max)
context linorder
begin
lemma dual_min:
"ord.min greater_eq = max"
by (auto simp add: ord.min_def max_def fun_eq_iff)
lemma dual_max:
"ord.max greater_eq = min"
by (auto simp add: ord.max_def min_def fun_eq_iff)
lemma dual_Min:
"linorder.Min greater_eq = Max"
proof -
interpret dual!: linorder greater_eq greater by (fact dual_linorder)
show ?thesis by (simp add: dual.Min_def dual_min Max_def)
qed
lemma dual_Max:
"linorder.Max greater_eq = Min"
proof -
interpret dual!: linorder greater_eq greater by (fact dual_linorder)
show ?thesis by (simp add: dual.Max_def dual_max Min_def)
qed
lemmas Min_singleton = Min.singleton
lemmas Max_singleton = Max.singleton
lemmas Min_insert = Min.insert
lemmas Max_insert = Max.insert
lemmas Min_Un = Min.union
lemmas Max_Un = Max.union
lemmas hom_Min_commute = Min.hom_commute
lemmas hom_Max_commute = Max.hom_commute
lemma Min_in [simp]:
assumes "finite A" and "A \ {}"
shows "Min A \ A"
using assms by (auto simp add: min_def Min.closed)
lemma Max_in [simp]:
assumes "finite A" and "A \ {}"
shows "Max A \