(* Title: HOL/Lattices_Big.thy
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
with contributions by Jeremy Avigad
*)
section \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\
subsubsection \Without neutral element\
locale semilattice_set = semilattice
begin
interpretation comp_fun_idem f
by standard (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 standard (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 \<^bold>* 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 \<^bold>* 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 \<^bold>* 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 \<^bold>* 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 \<^bold>* 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 \<^bold>* 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 \<^bold>* 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 \<^bold>* 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 \<^bold>* 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 \<^bold>* y) = h x \<^bold>* 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 \<^bold>* F N)" by simp
also have "\ = h n \<^bold>* h (F N)" by (rule hom)
also have "h (F N) = F (h ` N)" by (rule insert)
also have "h n \<^bold>* \ = 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 \<^bold>\ F A \ (\a\A. x \<^bold>\ 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 \<^bold>\ a"
shows "x \<^bold>\ F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
assumes "finite A" and "A \ {}" and "x \<^bold>\ F A"
obtains "\a. a \ A \ x \<^bold>\ a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \ A"
shows "F A \<^bold>\ 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 \<^bold>\ 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 \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
also have "\ \<^bold>\ 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 standard (simp_all add: fun_eq_iff left_commute)
definition F :: "'a set \ 'a"
where
eq_fold: "F A = Finite_Set.fold f \<^bold>1 A"
lemma infinite [simp]:
"\ finite A \ F A = \<^bold>1"
by (simp add: eq_fold)
lemma empty [simp]:
"F {} = \<^bold>1"
by (simp add: eq_fold)
lemma insert [simp]:
assumes "finite A"
shows "F (insert x A) = x \<^bold>* F A"
using assms by (simp add: eq_fold)
lemma in_idem:
assumes "finite A" and "x \ A"
shows "x \<^bold>* 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 \<^bold>* F B"
using assms by (induct A) (simp_all add: ac_simps)
lemma remove:
assumes "finite A" and "x \ A"
shows "F A = x \<^bold>* 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 \<^bold>* 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 \<^bold>* 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 \<^bold>* 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 \<^bold>\ F A \ (\a\A. x \<^bold>\ a)"
using assms by (induct A) (simp_all add: bounded_iff)
lemma boundedI:
assumes "finite A"
assumes "\a. a \ A \ x \<^bold>\ a"
shows "x \<^bold>\ F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
assumes "finite A" and "x \<^bold>\ F A"
obtains "\a. a \ A \ x \<^bold>\ a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \ A"
shows "F A \<^bold>\ 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 \<^bold>\ 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 \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
also have "\ \<^bold>\ F A" by simp
finally show ?thesis .
qed
end
subsection \Lattice operations on finite sets\
context semilattice_inf
begin
sublocale Inf_fin: semilattice_order_set inf less_eq less
defines
Inf_fin ("\\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Inf_fin.F ..
end
context semilattice_sup
begin
sublocale Sup_fin: semilattice_order_set sup greater_eq greater
defines
Sup_fin ("\\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Sup_fin.F ..
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 (\