(* Title: HOL/Big_Operators.thy
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
with contributions by Jeremy Avigad
*)
header {* Big operators and finite (non-empty) sets *}
theory Big_Operators
imports Finite_Set Option Metis
begin
subsection {* Generic monoid operation over a set *}
no_notation times (infixl "*" 70)
no_notation Groups.one ("1")
locale comm_monoid_set = comm_monoid
begin
definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
where
eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
lemma infinite [simp]:
"\<not> finite A \<Longrightarrow> F g A = 1"
by (simp add: eq_fold)
lemma empty [simp]:
"F g {} = 1"
by (simp add: eq_fold)
lemma insert [simp]:
assumes "finite A" and "x \<notin> A"
shows "F g (insert x A) = g x * F g A"
proof -
interpret comp_fun_commute f
by default (simp add: fun_eq_iff left_commute)
interpret comp_fun_commute "f \<circ> g"
by (rule comp_comp_fun_commute)
from assms show ?thesis by (simp add: eq_fold)
qed
lemma remove:
assumes "finite A" and "x \<in> A"
shows "F g A = g x * F g (A - {x})"
proof -
from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
by (auto dest: mk_disjoint_insert)
moreover from `finite A` this have "finite B" by simp
ultimately show ?thesis by simp
qed
lemma insert_remove:
assumes "finite A"
shows "F g (insert x A) = g x * F g (A - {x})"
using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
lemma neutral:
assumes "\<forall>x\<in>A. g x = 1"
shows "F g A = 1"
proof (cases "finite A")
case True from `finite A` assms show ?thesis by (induct A) simp_all
next
case False then show ?thesis by simp
qed
lemma neutral_const [simp]:
"F (\<lambda>_. 1) A = 1"
by (simp add: neutral)
lemma union_inter:
assumes "finite A" and "finite B"
shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
using assms proof (induct A)
case empty then show ?case by simp
next
case (insert x A) then show ?case
by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
qed
corollary union_inter_neutral:
assumes "finite A" and "finite B"
and I0: "\<forall>x \<in> A \<inter> B. g x = 1"
shows "F g (A \<union> B) = F g A * F g B"
using assms by (simp add: union_inter [symmetric] neutral)
corollary union_disjoint:
assumes "finite A" and "finite B"
assumes "A \<inter> B = {}"
shows "F g (A \<union> B) = F g A * F g B"
using assms by (simp add: union_inter_neutral)
lemma subset_diff:
"B \<subseteq> A \<Longrightarrow> finite A \<Longrightarrow> F g A = F g (A - B) * F g B"
by (metis Diff_partition union_disjoint Diff_disjoint finite_Un inf_commute sup_commute)
lemma reindex:
assumes "inj_on h A"
shows "F g (h ` A) = F (g \<circ> h) A"
proof (cases "finite A")
case True
interpret comp_fun_commute f
by default (simp add: fun_eq_iff left_commute)
interpret comp_fun_commute "f \<circ> g"
by (rule comp_comp_fun_commute)
from assms `finite A` show ?thesis by (simp add: eq_fold fold_image comp_assoc)
next
case False with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD)
with False show ?thesis by simp
qed
lemma cong:
assumes "A = B"
assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
shows "F g A = F h B"
proof (cases "finite A")
case True
then have "\<And>C. C \<subseteq> A \<longrightarrow> (\<forall>x\<in>C. g x = h x) \<longrightarrow> F g C = F h C"
proof induct
case empty then show ?case by simp
next
case (insert x F) then show ?case apply -
apply (simp add: subset_insert_iff, clarify)
apply (subgoal_tac "finite C")
prefer 2 apply (blast dest: finite_subset [rotated])
apply (subgoal_tac "C = insert x (C - {x})")
prefer 2 apply blast
apply (erule ssubst)
apply (simp add: Ball_def del: insert_Diff_single)
done
qed
with `A = B` g_h show ?thesis by simp
next
case False
with `A = B` show ?thesis by simp
qed
lemma strong_cong [cong]:
assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
by (rule cong) (insert assms, simp_all add: simp_implies_def)
lemma UNION_disjoint:
assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I"
apply (insert assms)
apply (induct rule: finite_induct)
apply simp
apply atomize
apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
prefer 2 apply blast
apply (subgoal_tac "A x Int UNION Fa A = {}")
prefer 2 apply blast
apply (simp add: union_disjoint)
done
lemma Union_disjoint:
assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
shows "F g (Union C) = F (F g) C"
proof cases
assume "finite C"
from UNION_disjoint [OF this assms]
show ?thesis
by (simp add: SUP_def)
qed (auto dest: finite_UnionD intro: infinite)
lemma distrib:
"F (\<lambda>x. g x * h x) A = F g A * F h A"
proof (cases "finite A")
case False then show ?thesis by simp
next
case True then show ?thesis by (rule finite_induct) (simp_all add: assoc commute left_commute)
qed
lemma Sigma:
"finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)"
apply (subst Sigma_def)
apply (subst UNION_disjoint, assumption, simp)
apply blast
apply (rule cong)
apply rule
apply (simp add: fun_eq_iff)
apply (subst UNION_disjoint, simp, simp)
apply blast
apply (simp add: comp_def)
done
lemma related:
assumes Re: "R 1 1"
and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)"
and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
shows "R (F h S) (F g S)"
using fS by (rule finite_subset_induct) (insert assms, auto)
lemma eq_general:
assumes h: "\<forall>y\<in>S'. \<exists>!x. x \<in> S \<and> h x = y"
and f12: "\<forall>x\<in>S. h x \<in> S' \<and> f2 (h x) = f1 x"
shows "F f1 S = F f2 S'"
proof-
from h f12 have hS: "h ` S = S'" by blast
{fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
from f12 h H have "x = y" by auto }
hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto
from hS have "F f2 S' = F f2 (h ` S)" by simp
also have "\<dots> = F (f2 o h) S" using reindex [OF hinj, of f2] .
also have "\<dots> = F f1 S " using th cong [of _ _ "f2 o h" f1]
by blast
finally show ?thesis ..
qed
lemma eq_general_reverses:
assumes kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = j x"
shows "F j S = F g T"
(* metis solves it, but not yet available here *)
apply (rule eq_general [of T S h g j])
apply (rule ballI)
apply (frule kh)
apply (rule ex1I[])
apply blast
apply clarsimp
apply (drule hk) apply simp
apply (rule sym)
apply (erule conjunct1[OF conjunct2[OF hk]])
apply (rule ballI)
apply (drule hk)
apply blast
done
lemma mono_neutral_cong_left:
assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
proof-
have eq: "T = S \<union> (T - S)" using `S \<subseteq> T` by blast
have d: "S \<inter> (T - S) = {}" using `S \<subseteq> T` by blast
from `finite T` `S \<subseteq> T` have f: "finite S" "finite (T - S)"
by (auto intro: finite_subset)
show ?thesis using assms(4)
by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
qed
lemma mono_neutral_cong_right:
"\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
\<Longrightarrow> F g T = F h S"
by (auto intro!: mono_neutral_cong_left [symmetric])
lemma mono_neutral_left:
"\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
by (blast intro: mono_neutral_cong_left)
lemma mono_neutral_right:
"\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
by (blast intro!: mono_neutral_left [symmetric])
lemma delta:
assumes fS: "finite S"
shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
proof-
let ?f = "(\<lambda>k. if k=a then b k else 1)"
{ assume a: "a \<notin> S"
hence "\<forall>k\<in>S. ?f k = 1" by simp
hence ?thesis using a by simp }
moreover
{ assume a: "a \<in> S"
let ?A = "S - {a}"
let ?B = "{a}"
have eq: "S = ?A \<union> ?B" using a by blast
have dj: "?A \<inter> ?B = {}" by simp
from fS have fAB: "finite ?A" "finite ?B" by auto
have "F ?f S = F ?f ?A * F ?f ?B"
using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
by simp
then have ?thesis using a by simp }
ultimately show ?thesis by blast
qed
lemma delta':
assumes fS: "finite S"
shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
using delta [OF fS, of a b, symmetric] by (auto intro: cong)
lemma If_cases:
fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
assumes fA: "finite A"
shows "F (\<lambda>x. if P x then h x else g x) A =
F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
proof -
have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}"
"(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
by blast+
from fA
have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
let ?g = "\<lambda>x. if P x then h x else g x"
from union_disjoint [OF f a(2), of ?g] a(1)
show ?thesis
by (subst (1 2) cong) simp_all
qed
lemma cartesian_product:
"F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
apply (rule sym)
apply (cases "finite A")
apply (cases "finite B")
apply (simp add: Sigma)
apply (cases "A={}", simp)
apply simp
apply (auto intro: infinite dest: finite_cartesian_productD2)
apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1)
done
end
notation times (infixl "*" 70)
notation Groups.one ("1")
subsection {* Generalized summation over a set *}
definition (in comm_monoid_add) setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
where
"setsum = comm_monoid_set.F plus 0"
sublocale comm_monoid_add < setsum!: comm_monoid_set plus 0
where
"comm_monoid_set.F plus 0 = setsum"
proof -
show "comm_monoid_set plus 0" ..
then interpret setsum!: comm_monoid_set plus 0 .
from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
qed
abbreviation
Setsum ("\<Sum>_" [1000] 999) where
"\<Sum>A \<equiv> setsum (%x. x) A"
text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
written @{text"\<Sum>x\<in>A. e"}. *}
syntax
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10)
syntax (xsymbols)
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
syntax (HTML output)
"_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
translations -- {* Beware of argument permutation! *}
"SUM i:A. b" == "CONST setsum (%i. b) A"
"\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
@{text"\<Sum>x|P. e"}. *}
syntax
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
syntax (xsymbols)
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
syntax (HTML output)
"_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
translations
"SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
"\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
print_translation {*
let
fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
if x <> y then raise Match
else
let
val x' = Syntax_Trans.mark_bound_body (x, Tx);
val t' = subst_bound (x', t);
val P' = subst_bound (x', P);
in
Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
end
| setsum_tr' _ = raise Match;
in [(@{const_syntax setsum}, setsum_tr')] end
*}
text {* TODO These are candidates for generalization *}
context comm_monoid_add
begin
lemma setsum_reindex_id:
"inj_on f B ==> setsum f B = setsum id (f ` B)"
by (simp add: setsum.reindex)
lemma setsum_reindex_nonzero:
assumes fS: "finite S"
and nz: "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
shows "setsum h (f ` S) = setsum (h \<circ> f) S"
using nz proof (induct rule: finite_induct [OF fS])
case 1 thus ?case by simp
next
case (2 x F)
{ assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
then obtain y where y: "y \<in> F" "f x = f y" by auto
from "2.hyps" y have xy: "x \<noteq> y" by auto
from "2.prems" [of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
also have "\<dots> = setsum (h o f) (insert x F)"
unfolding setsum.insert[OF `finite F` `x\<notin>F`]
using h0
apply (simp cong del: setsum.strong_cong)
apply (rule "2.hyps"(3))
apply (rule_tac y="y" in "2.prems")
apply simp_all
done
finally have ?case . }
moreover
{ assume fxF: "f x \<notin> f ` F"
have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)"
using fxF "2.hyps" by simp
also have "\<dots> = setsum (h o f) (insert x F)"
unfolding setsum.insert[OF `finite F` `x\<notin>F`]
apply (simp cong del: setsum.strong_cong)
apply (rule cong [OF refl [of "op + (h (f x))"]])
apply (rule "2.hyps"(3))
apply (rule_tac y="y" in "2.prems")
apply simp_all
done
finally have ?case . }
ultimately show ?case by blast
qed
lemma setsum_cong2:
"(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
by (auto intro: setsum.cong)
lemma setsum_reindex_cong:
"[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
==> setsum h B = setsum g A"
by (simp add: setsum.reindex)
lemma setsum_restrict_set:
assumes fA: "finite A"
shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
proof-
from fA have fab: "finite (A \<inter> B)" by auto
have aba: "A \<inter> B \<subseteq> A" by blast
let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
from setsum.mono_neutral_left [OF fA aba, of ?g]
show ?thesis by simp
qed
lemma setsum_Union_disjoint:
assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
shows "setsum f (Union C) = setsum (setsum f) C"
using assms by (fact setsum.Union_disjoint)
lemma setsum_cartesian_product:
"(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
by (fact setsum.cartesian_product)
lemma setsum_UNION_zero:
assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
using fSS f0
proof(induct rule: finite_induct[OF fS])
case 1 thus ?case by simp
next
case (2 T F)
then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F"
and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
from fTF have fUF: "finite (\<Union>F)" by auto
from "2.prems" TF fTF
show ?case
by (auto simp add: H [symmetric] intro: setsum.union_inter_neutral [OF fTF(1) fUF, of f])
qed
text {* Commuting outer and inner summation *}
lemma setsum_commute:
"(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
proof (simp add: setsum_cartesian_product)
have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
(\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
(is "?s = _")
apply (simp add: setsum.reindex [where h = "%(i, j). (j, i)"] swap_inj_on)
apply (simp add: split_def)
done
also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
(is "_ = ?t")
apply (simp add: swap_product)
done
finally show "?s = ?t" .
qed
lemma setsum_Plus:
fixes A :: "'a set" and B :: "'b set"
assumes fin: "finite A" "finite B"
shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
proof -
have "A <+> B = Inl ` A \<union> Inr ` B" by auto
moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
by auto
moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
ultimately show ?thesis using fin by(simp add: setsum.union_disjoint setsum.reindex)
qed
end
text {* TODO These are legacy *}
lemma setsum_empty:
"setsum f {} = 0"
by (fact setsum.empty)
lemma setsum_insert:
"finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
by (fact setsum.insert)
lemma setsum_infinite:
"~ finite A ==> setsum f A = 0"
by (fact setsum.infinite)
lemma setsum_reindex:
"inj_on f B \<Longrightarrow> setsum h (f ` B) = setsum (h \<circ> f) B"
by (fact setsum.reindex)
lemma setsum_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
by (fact setsum.cong)
lemma strong_setsum_cong:
"A = B ==> (!!x. x:B =simp=> f x = g x)
==> setsum (%x. f x) A = setsum (%x. g x) B"
by (fact setsum.strong_cong)
lemmas setsum_0 = setsum.neutral_const
lemmas setsum_0' = setsum.neutral
lemma setsum_Un_Int: "finite A ==> finite B ==>
setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
-- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
by (fact setsum.union_inter)
lemma setsum_Un_disjoint: "finite A ==> finite B
==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
by (fact setsum.union_disjoint)
lemma setsum_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
setsum f A = setsum f (A - B) + setsum f B"
by (fact setsum.subset_diff)
lemma setsum_mono_zero_left:
"\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 0 \<rbrakk> \<Longrightarrow> setsum f S = setsum f T"
by (fact setsum.mono_neutral_left)
lemmas setsum_mono_zero_right = setsum.mono_neutral_right
lemma setsum_mono_zero_cong_left:
"\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 0; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
\<Longrightarrow> setsum f S = setsum g T"
by (fact setsum.mono_neutral_cong_left)
lemmas setsum_mono_zero_cong_right = setsum.mono_neutral_cong_right
lemma setsum_delta: "finite S \<Longrightarrow>
setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
by (fact setsum.delta)
lemma setsum_delta': "finite S \<Longrightarrow>
setsum (\<lambda>k. if a = k then b k else 0) S = (if a\<in> S then b a else 0)"
by (fact setsum.delta')
lemma setsum_cases:
assumes "finite A"
shows "setsum (\<lambda>x. if P x then f x else g x) A =
setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
using assms by (fact setsum.If_cases)
(*But we can't get rid of finite I. If infinite, although the rhs is 0,
the lhs need not be, since UNION I A could still be finite.*)
lemma setsum_UN_disjoint:
assumes "finite I" and "ALL i:I. finite (A i)"
and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
using assms by (fact setsum.UNION_disjoint)
(*But we can't get rid of finite A. If infinite, although the lhs is 0,
the rhs need not be, since SIGMA A B could still be finite.*)
lemma setsum_Sigma:
assumes "finite A" and "ALL x:A. finite (B x)"
shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
using assms by (fact setsum.Sigma)
lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
by (fact setsum.distrib)
lemma setsum_Un_zero:
"\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 0 \<rbrakk> \<Longrightarrow>
setsum f (S \<union> T) = setsum f S + setsum f T"
by (fact setsum.union_inter_neutral)
lemma setsum_eq_general_reverses:
assumes fS: "finite S" and fT: "finite T"
and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
shows "setsum f S = setsum g T"
using kh hk by (fact setsum.eq_general_reverses)
subsubsection {* Properties in more restricted classes of structures *}
lemma setsum_Un: "finite A ==> finite B ==>
(setsum f (A Un B) :: 'a :: ab_group_add) =
setsum f A + setsum f B - setsum f (A Int B)"
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
lemma setsum_Un2:
assumes "finite (A \<union> B)"
shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
proof -
have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
by auto
with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+
qed
lemma setsum_diff1: "finite A \<Longrightarrow>
(setsum f (A - {a}) :: ('a::ab_group_add)) =
(if a:A then setsum f A - f a else setsum f A)"
by (erule finite_induct) (auto simp add: insert_Diff_if)
lemma setsum_diff:
assumes le: "finite A" "B \<subseteq> A"
shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
proof -
from le have finiteB: "finite B" using finite_subset by auto
show ?thesis using finiteB le
proof induct
case empty
thus ?case by auto
next
case (insert x F)
thus ?case using le finiteB
by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
qed
qed
lemma setsum_mono:
assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
proof (cases "finite K")
case True
thus ?thesis using le
proof induct
case empty
thus ?case by simp
next
case insert
thus ?case using add_mono by fastforce
qed
next
case False then show ?thesis by simp
qed
lemma setsum_strict_mono:
fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
assumes "finite A" "A \<noteq> {}"
and "!!x. x:A \<Longrightarrow> f x < g x"
shows "setsum f A < setsum g A"
using assms
proof (induct rule: finite_ne_induct)
case singleton thus ?case by simp
next
case insert thus ?case by (auto simp: add_strict_mono)
qed
lemma setsum_strict_mono_ex1:
fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
shows "setsum f A < setsum g A"
proof-
from assms(3) obtain a where a: "a:A" "f a < g a" by blast
have "setsum f A = setsum f ((A-{a}) \<union> {a})"
by(simp add:insert_absorb[OF `a:A`])
also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
using `finite A` by(subst setsum_Un_disjoint) auto
also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
by(rule setsum_mono)(simp add: assms(2))
also have "setsum f {a} < setsum g {a}" using a by simp
also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
finally show ?thesis by (metis add_right_mono add_strict_left_mono)
qed
lemma setsum_negf:
"setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
proof (cases "finite A")
case True thus ?thesis by (induct set: finite) auto
next
case False thus ?thesis by simp
qed
lemma setsum_subtractf:
"setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
setsum f A - setsum g A"
proof (cases "finite A")
case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
next
case False thus ?thesis by simp
qed
lemma setsum_nonneg:
assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
shows "0 \<le> setsum f A"
proof (cases "finite A")
case True thus ?thesis using nn
proof induct
case empty then show ?case by simp
next
case (insert x F)
then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
with insert show ?case by simp
qed
next
case False thus ?thesis by simp
qed
lemma setsum_nonpos:
assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
shows "setsum f A \<le> 0"
proof (cases "finite A")
case True thus ?thesis using np
proof induct
case empty then show ?case by simp
next
case (insert x F)
then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
with insert show ?case by simp
qed
next
case False thus ?thesis by simp
qed
lemma setsum_nonneg_leq_bound:
fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
shows "f i \<le> B"
proof -
have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
using assms by (auto intro!: setsum_nonneg)
moreover
have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
using assms by (simp add: setsum_diff1)
ultimately show ?thesis by auto
qed
lemma setsum_nonneg_0:
fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
shows "f i = 0"
using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
lemma setsum_mono2:
fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
shows "setsum f A \<le> setsum f B"
proof -
have "setsum f A \<le> setsum f A + setsum f (B-A)"
by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
also have "A \<union> (B-A) = B" using sub by blast
finally show ?thesis .
qed
lemma setsum_mono3: "finite B ==> A <= B ==>
ALL x: B - A.
0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
setsum f A <= setsum f B"
apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
apply (erule ssubst)
apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
apply simp
apply (rule add_left_mono)
apply (erule setsum_nonneg)
apply (subst setsum_Un_disjoint [THEN sym])
apply (erule finite_subset, assumption)
apply (rule finite_subset)
prefer 2
apply assumption
apply (auto simp add: sup_absorb2)
done
lemma setsum_right_distrib:
fixes f :: "'a => ('b::semiring_0)"
shows "r * setsum f A = setsum (%n. r * f n) A"
proof (cases "finite A")
case True
thus ?thesis
proof induct
case empty thus ?case by simp
next
case (insert x A) thus ?case by (simp add: distrib_left)
qed
next
case False thus ?thesis by simp
qed
lemma setsum_left_distrib:
"setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
proof (cases "finite A")
case True
then show ?thesis
proof induct
case empty thus ?case by simp
next
case (insert x A) thus ?case by (simp add: distrib_right)
qed
next
case False thus ?thesis by simp
qed
lemma setsum_divide_distrib:
"setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
proof (cases "finite A")
case True
then show ?thesis
proof induct
case empty thus ?case by simp
next
case (insert x A) thus ?case by (simp add: add_divide_distrib)
qed
next
case False thus ?thesis by simp
qed
lemma setsum_abs[iff]:
fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
proof (cases "finite A")
case True
thus ?thesis
proof induct
case empty thus ?case by simp
next
case (insert x A)
thus ?case by (auto intro: abs_triangle_ineq order_trans)
qed
next
case False thus ?thesis by simp
qed
lemma setsum_abs_ge_zero[iff]:
fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
shows "0 \<le> setsum (%i. abs(f i)) A"
proof (cases "finite A")
case True
thus ?thesis
proof induct
case empty thus ?case by simp
next
case (insert x A) thus ?case by auto
qed
next
case False thus ?thesis by simp
qed
lemma abs_setsum_abs[simp]:
fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
proof (cases "finite A")
case True
thus ?thesis
proof induct
case empty thus ?case by simp
next
case (insert a A)
hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" using insert by simp
also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
by (simp del: abs_of_nonneg)
also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
finally show ?case .
qed
next
case False thus ?thesis by simp
qed
lemma setsum_diff1'[rule_format]:
"finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
apply (auto simp add: insert_Diff_if add_ac)
done
lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
unfolding setsum_diff1'[OF assms] by auto
lemma setsum_product:
fixes f :: "'a => ('b::semiring_0)"
shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
lemma setsum_mult_setsum_if_inj:
fixes f :: "'a => ('b::semiring_0)"
shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
by(auto simp: setsum_product setsum_cartesian_product
intro!: setsum_reindex_cong[symmetric])
lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
apply (case_tac "finite A")
prefer 2 apply simp
apply (erule rev_mp)
apply (erule finite_induct, auto)
done
lemma setsum_eq_0_iff [simp]:
"finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
by (induct set: finite) auto
lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
apply(erule finite_induct)
apply (auto simp add:add_is_1)
done
lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
lemma setsum_Un_nat: "finite A ==> finite B ==>
(setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
-- {* For the natural numbers, we have subtraction. *}
by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
(if a:A then setsum f A - f a else setsum f A)"
apply (case_tac "finite A")
prefer 2 apply simp
apply (erule finite_induct)
apply (auto simp add: insert_Diff_if)
apply (drule_tac a = a in mk_disjoint_insert, auto)
done
lemma setsum_diff_nat:
assumes "finite B" and "B \<subseteq> A"
shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
using assms
proof induct
show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
next
fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
and xFinA: "insert x F \<subseteq> A"
and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
by (simp add: setsum_diff1_nat)
from xFinA have "F \<subseteq> A" by simp
with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
by simp
from xnotinF have "A - insert x F = (A - F) - {x}" by auto
with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
by simp
from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
by simp
thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
qed
subsubsection {* Cardinality as special case of @{const setsum} *}
lemma card_eq_setsum:
"card A = setsum (\<lambda>x. 1) A"
proof -
have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
by (simp add: fun_eq_iff)
then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
by (rule arg_cong)
then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
by (blast intro: fun_cong)
then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
qed
lemma setsum_constant [simp]:
"(\<Sum>x \<in> A. y) = of_nat (card A) * y"
apply (cases "finite A")
apply (erule finite_induct)
apply (auto simp add: algebra_simps)
done
lemma setsum_bounded:
assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
shows "setsum f A \<le> of_nat (card A) * K"
proof (cases "finite A")
case True
thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
next
case False thus ?thesis by simp
qed
lemma card_UN_disjoint:
assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
proof -
have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
qed
lemma card_Union_disjoint:
"finite C ==> (ALL A:C. finite A) ==>
(ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
==> card (Union C) = setsum card C"
apply (frule card_UN_disjoint [of C id])
apply (simp_all add: SUP_def id_def)
done
subsubsection {* Cardinality of products *}
lemma card_SigmaI [simp]:
"\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
\<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
(*
lemma SigmaI_insert: "y \<notin> A ==>
(SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
by auto
*)
lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
by (cases "finite A \<and> finite B")
(auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
lemma card_cartesian_product_singleton: "card({x} <*> A) = card(A)"
by (simp add: card_cartesian_product)
subsection {* Generalized product over a set *}
definition (in comm_monoid_mult) setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
where
"setprod = comm_monoid_set.F times 1"
sublocale comm_monoid_mult < setprod!: comm_monoid_set times 1
where
"comm_monoid_set.F times 1 = setprod"
proof -
show "comm_monoid_set times 1" ..
then interpret setprod!: comm_monoid_set times 1 .
from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
qed
abbreviation
Setprod ("\<Prod>_" [1000] 999) where
"\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
syntax
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10)
syntax (xsymbols)
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
syntax (HTML output)
"_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
translations -- {* Beware of argument permutation! *}
"PROD i:A. b" == "CONST setprod (%i. b) A"
"\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A"
text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
@{text"\<Prod>x|P. e"}. *}
syntax
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
syntax (xsymbols)
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
syntax (HTML output)
"_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
translations
"PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
"\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
text {* TODO These are candidates for generalization *}
context comm_monoid_mult
begin
lemma setprod_reindex_id:
"inj_on f B ==> setprod f B = setprod id (f ` B)"
by (auto simp add: setprod.reindex)
lemma setprod_reindex_cong:
"inj_on f A ==> B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
by (frule setprod.reindex, simp)
lemma strong_setprod_reindex_cong:
assumes i: "inj_on f A"
and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
shows "setprod h B = setprod g A"
proof-
have "setprod h B = setprod (h o f) A"
by (simp add: B setprod.reindex [OF i, of h])
then show ?thesis apply simp
apply (rule setprod.cong)
apply simp
by (simp add: eq)
qed
lemma setprod_Union_disjoint:
assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
shows "setprod f (Union C) = setprod (setprod f) C"
using assms by (fact setprod.Union_disjoint)
text{*Here we can eliminate the finiteness assumptions, by cases.*}
lemma setprod_cartesian_product:
"(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
by (fact setprod.cartesian_product)
lemma setprod_Un2:
assumes "finite (A \<union> B)"
shows "setprod f (A \<union> B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \<inter> B)"
proof -
have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
by auto
with assms show ?thesis by simp (subst setprod.union_disjoint, auto)+
qed
end
text {* TODO These are legacy *}
lemma setprod_empty: "setprod f {} = 1"
by (fact setprod.empty)
lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
setprod f (insert a A) = f a * setprod f A"
by (fact setprod.insert)
lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
by (fact setprod.infinite)
lemma setprod_reindex:
"inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
by (fact setprod.reindex)
lemma setprod_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
by (fact setprod.cong)
lemma strong_setprod_cong:
"A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
by (fact setprod.strong_cong)
lemma setprod_Un_one:
"\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 1 \<rbrakk>
\<Longrightarrow> setprod f (S \<union> T) = setprod f S * setprod f T"
by (fact setprod.union_inter_neutral)
lemmas setprod_1 = setprod.neutral_const
lemmas setprod_1' = setprod.neutral
lemma setprod_Un_Int: "finite A ==> finite B
==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
by (fact setprod.union_inter)
lemma setprod_Un_disjoint: "finite A ==> finite B
==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
by (fact setprod.union_disjoint)
lemma setprod_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
setprod f A = setprod f (A - B) * setprod f B"
by (fact setprod.subset_diff)
lemma setprod_mono_one_left:
"\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 1 \<rbrakk> \<Longrightarrow> setprod f S = setprod f T"
by (fact setprod.mono_neutral_left)
lemmas setprod_mono_one_right = setprod.mono_neutral_right
lemma setprod_mono_one_cong_left:
"\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
\<Longrightarrow> setprod f S = setprod g T"
by (fact setprod.mono_neutral_cong_left)
lemmas setprod_mono_one_cong_right = setprod.mono_neutral_cong_right
lemma setprod_delta: "finite S \<Longrightarrow>
setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
by (fact setprod.delta)
lemma setprod_delta': "finite S \<Longrightarrow>
setprod (\<lambda>k. if a = k then b k else 1) S = (if a\<in> S then b a else 1)"
by (fact setprod.delta')
lemma setprod_UN_disjoint:
"finite I ==> (ALL i:I. finite (A i)) ==>
(ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
by (fact setprod.UNION_disjoint)
lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
(\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
(\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
by (fact setprod.Sigma)
lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A = setprod f A * setprod g A"
by (fact setprod.distrib)
subsubsection {* Properties in more restricted classes of structures *}
lemma setprod_zero:
"finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
apply (induct set: finite, force, clarsimp)
apply (erule disjE, auto)
done
lemma setprod_zero_iff[simp]: "finite A ==>
(setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
(EX x: A. f x = 0)"
by (erule finite_induct, auto simp:no_zero_divisors)
lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
(setprod f (A Un B) :: 'a ::{field})
= setprod f A * setprod f B / setprod f (A Int B)"
by (subst setprod_Un_Int [symmetric], auto)
lemma setprod_nonneg [rule_format]:
"(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
--> 0 < setprod f A"
by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
(setprod f (A - {a}) :: 'a :: {field}) =
(if a:A then setprod f A / f a else setprod f A)"
by (erule finite_induct) (auto simp add: insert_Diff_if)
lemma setprod_inversef:
fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
by (erule finite_induct) auto
lemma setprod_dividef:
fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
shows "finite A
==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
apply (subgoal_tac
"setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
apply (erule ssubst)
apply (subst divide_inverse)
apply (subst setprod_timesf)
apply (subst setprod_inversef, assumption+, rule refl)
apply (rule setprod_cong, rule refl)
apply (subst divide_inverse, auto)
done
lemma setprod_dvd_setprod [rule_format]:
"(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
apply (cases "finite A")
apply (induct set: finite)
apply (auto simp add: dvd_def)
apply (rule_tac x = "k * ka" in exI)
apply (simp add: algebra_simps)
done
lemma setprod_dvd_setprod_subset:
"finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
apply (unfold dvd_def, blast)
apply (subst setprod_Un_disjoint [symmetric])
apply (auto elim: finite_subset intro: setprod_cong)
done
lemma setprod_dvd_setprod_subset2:
"finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow>
setprod f A dvd setprod g B"
apply (rule dvd_trans)
apply (rule setprod_dvd_setprod, erule (1) bspec)
apply (erule (1) setprod_dvd_setprod_subset)
done
lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow>
(f i ::'a::comm_semiring_1) dvd setprod f A"
by (induct set: finite) (auto intro: dvd_mult)
lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow>
(d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
apply (cases "finite A")
apply (induct set: finite)
apply auto
done
lemma setprod_mono:
fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
shows "setprod f A \<le> setprod g A"
proof (cases "finite A")
case True
hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
proof (induct A rule: finite_subset_induct)
case (insert a F)
thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
unfolding setprod_insert[OF insert(1,3)]
using assms[rule_format,OF insert(2)] insert
by (auto intro: mult_mono mult_nonneg_nonneg)
qed auto
thus ?thesis by simp
qed auto
lemma abs_setprod:
fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
proof (cases "finite A")
case True thus ?thesis
by induct (auto simp add: field_simps abs_mult)
qed auto
lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)"
apply (erule finite_induct)
apply auto
done
lemma setprod_gen_delta:
assumes fS: "finite S"
shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
proof-
let ?f = "(\<lambda>k. if k=a then b k else c)"
{assume a: "a \<notin> S"
hence "\<forall> k\<in> S. ?f k = c" by simp
hence ?thesis using a setprod_constant[OF fS, of c] by simp }
moreover
{assume a: "a \<in> S"
let ?A = "S - {a}"
let ?B = "{a}"
have eq: "S = ?A \<union> ?B" using a by blast
have dj: "?A \<inter> ?B = {}" by simp
from fS have fAB: "finite ?A" "finite ?B" by auto
have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
apply (rule setprod_cong) by auto
have cA: "card ?A = card S - 1" using fS a by auto
have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto
have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
by simp
then have ?thesis using a cA
by (simp add: fA1 field_simps cong add: setprod_cong cong del: if_weak_cong)}
ultimately show ?thesis by blast
qed
lemma setprod_eq_1_iff [simp]:
"finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
by (induct set: finite) auto
lemma setprod_pos_nat:
"finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
lemma setprod_pos_nat_iff[simp]:
"finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
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
definition F :: "'a set \<Rightarrow> 'a"
where
eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> 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 = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
interpret comp_fun_idem f
by default (simp_all add: fun_eq_iff left_commute)
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 \<notin> A" and "A \<noteq> {}"
shows "F (insert x A) = x * F A"
proof -
interpret comp_fun_idem f
by default (simp_all add: fun_eq_iff left_commute)
from `A \<noteq> {}` obtain b where "b \<in> A" by blast
then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
with `finite A` and `x \<notin> A`
have "finite (insert x B)" and "b \<notin> 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 subsumption:
assumes "finite A" and "x \<in> A"
shows "x * F A = F A"
proof -
from assms have "A \<noteq> {}" by auto
with `finite A` show ?thesis using `x \<in> 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 \<noteq> {}"
shows "F (insert x A) = x * F A"
using assms by (cases "x \<in> A") (simp_all add: insert_absorb subsumption insert_not_elem)
lemma union:
assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
shows "F (A \<union> 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 \<in> 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 \<notin> 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 \<in> A") (simp_all add: insert_absorb remove)
lemma subset:
assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
shows "F B * F A = F A"
proof -
from assms have "A \<noteq> {}" 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 \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
shows "F A \<in> A"
using `finite A` `A \<noteq> {}` 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: "\<And>x y. h (x * y) = h x * h y"
and N: "finite N" "N \<noteq> {}"
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 "\<dots> = h n * h (F N)" by (rule hom)
also have "h (F N) = F (h ` N)" by (rule insert)
also have "h n * \<dots> = 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
end
locale semilattice_order_set = semilattice_order + semilattice_set
begin
lemma bounded_iff:
assumes "finite A" and "A \<noteq> {}"
shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
lemma boundedI:
assumes "finite A"
assumes "A \<noteq> {}"
assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
shows "x \<preceq> F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \<in> A"
shows "F A \<preceq> a"
proof -
from assms have "A \<noteq> {}" by auto
from `finite A` `A \<noteq> {}` `a \<in> 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 \<or> a \<in> B" by simp
then show ?case using insert by (auto intro: coboundedI2)
qed
qed
lemma antimono:
assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
shows "F B \<preceq> F A"
proof (cases "A = B")
case True then show ?thesis by (simp add: refl)
next
case False
have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
then have "F B = F (A \<union> (B - A))" by simp
also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
also have "\<dots> \<preceq> F A" by simp
finally show ?thesis .
qed
end
subsubsection {* With neutral element *}
locale semilattice_neutr_set = semilattice_neutr
begin
definition F :: "'a set \<Rightarrow> 'a"
where
eq_fold: "F A = Finite_Set.fold f 1 A"
lemma infinite [simp]:
"\<not> finite A \<Longrightarrow> 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"
proof -
interpret comp_fun_idem f
by default (simp_all add: fun_eq_iff left_commute)
from assms show ?thesis by (simp add: eq_fold)
qed
lemma subsumption:
assumes "finite A" and "x \<in> A"
shows "x * F A = F A"
proof -
from assms have "A \<noteq> {}" by auto
with `finite A` show ?thesis using `x \<in> 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 \<union> B) = F A * F B"
using assms by (induct A) (simp_all add: ac_simps)
lemma remove:
assumes "finite A" and "x \<in> A"
shows "F A = x * F (A - {x})"
proof -
from assms obtain B where "A = insert x B" and "x \<notin> 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 \<in> A") (simp_all add: insert_absorb remove)
lemma subset:
assumes "finite A" and "B \<subseteq> 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 \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
shows "F A \<in> A"
using `finite A` `A \<noteq> {}` 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 = semilattice_neutr_order + semilattice_neutr_set
begin
lemma bounded_iff:
assumes "finite A"
shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
using assms by (induct A) (simp_all add: bounded_iff)
lemma boundedI:
assumes "finite A"
assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
shows "x \<preceq> F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
assumes "finite A" and "x \<preceq> F A"
obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \<in> A"
shows "F A \<preceq> a"
proof -
from assms have "A \<noteq> {}" by auto
from `finite A` `A \<noteq> {}` `a \<in> 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 \<or> a \<in> B" by simp
then show ?case using insert by (auto intro: coboundedI2)
qed
qed
lemma antimono:
assumes "A \<subseteq> B" and "finite B"
shows "F B \<preceq> F A"
proof (cases "A = B")
case True then show ?thesis by (simp add: refl)
next
case False
have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
then have "F B = F (A \<union> (B - A))" by simp
also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
also have "\<dots> \<preceq> F A" by simp
finally show ?thesis .
qed
end
notation times (infixl "*" 70)
notation Groups.one ("1")
subsection {* Lattice operations on finite sets *}
text {*
For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
to @{class linorder}. This is badly designed: both should depend on a common abstract
distributive lattice rather than having this non-subclass dependecy between two
classes. But for the moment we have to live with it. This forces us to setup
this sublocale dependency simultaneously with the lattice operations on finite
sets, to avoid garbage.
*}
definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
where
"Inf_fin = semilattice_set.F inf"
definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
where
"Sup_fin = semilattice_set.F sup"
definition (in linorder) Min :: "'a set \<Rightarrow> 'a"
where
"Min = semilattice_set.F min"
definition (in linorder) Max :: "'a set \<Rightarrow> 'a"
where
"Max = semilattice_set.F max"
sublocale linorder < 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
text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
sublocale linorder < min_max!: distrib_lattice min less_eq less max
where
"semilattice_inf.Inf_fin min = Min"
and "semilattice_sup.Sup_fin max = Max"
proof -
show "class.distrib_lattice min less_eq less max"
proof
fix x y z
show "max x (min y z) = min (max x y) (max x z)"
by (auto simp add: min_def max_def)
qed (auto simp add: min_def max_def not_le less_imp_le)
then interpret min_max!: distrib_lattice min less_eq less max .
show "semilattice_inf.Inf_fin min = Min"
by (simp only: min_max.Inf_fin_def Min_def)
show "semilattice_sup.Sup_fin max = Max"
by (simp only: min_max.Sup_fin_def Max_def)
qed
lemmas le_maxI1 = min_max.sup_ge1
lemmas le_maxI2 = min_max.sup_ge2
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
min.left_commute
lemmas max_ac = min_max.sup_assoc min_max.sup_commute
max.left_commute
text {* Lattice operations proper *}
sublocale semilattice_inf < 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
sublocale semilattice_sup < 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
text {* An aside again: @{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 \<Rightarrow> 'a)"
by (simp add: Inf_fin_def Min_def inf_min)
lemma Sup_fin_Max:
"Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
by (simp add: Sup_fin_def Max_def sup_max)
subsection {* Infimum and Supremum over non-empty sets *}
text {*
After this non-regular bootstrap, things continue canonically.
*}
context lattice
begin
lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A"
apply(subgoal_tac "EX a. a:A")
prefer 2 apply blast
apply(erule exE)
apply(rule order_trans)
apply(erule (1) Inf_fin.coboundedI)
apply(erule (1) Sup_fin.coboundedI)
done
lemma sup_Inf_absorb [simp]:
"finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a"
apply(subst sup_commute)
apply(simp add: sup_absorb2 Inf_fin.coboundedI)
done
lemma inf_Sup_absorb [simp]:
"finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a"
by (simp add: inf_absorb1 Sup_fin.coboundedI)
end
context distrib_lattice
begin
lemma sup_Inf1_distrib:
assumes "finite A"
and "A \<noteq> {}"
shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> 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 \<noteq> {}" and B: "finite B" "B \<noteq> {}"
shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> 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 \<in> B}"
by (rule finite_surj [where f = "sup x", OF B(1)], auto)
have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
proof -
have "{sup a b |a b. a \<in> A \<and> b \<in> 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 \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
using insert by simp
also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
using insert by(simp add:sup_Inf1_distrib[OF B])
also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
(is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
using B insert
by (simp add: Inf_fin.union [OF finB _ finAB ne])
also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
by blast
finally show ?case .
qed
lemma inf_Sup1_distrib:
assumes "finite A" and "A \<noteq> {}"
shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> 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 \<noteq> {}" and B: "finite B" "B \<noteq> {}"
shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> 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 \<in> B}"
by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
proof -
have "{inf a b |a b. a \<in> A \<and> b \<in> 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 \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
using insert by simp
also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
using insert by(simp add:inf_Sup1_distrib[OF B])
also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
(is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
using B insert
by (simp add: Sup_fin.union [OF finB _ finAB ne])
also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
by blast
finally show ?case .
qed
end
context complete_lattice
begin
lemma Inf_fin_Inf:
assumes "finite A" and "A \<noteq> {}"
shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf 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 \<noteq> {}"
shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup 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
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 \<noteq> {}"
shows "Min A \<in> A"
using assms by (auto simp add: min_def Min.closed)
lemma Max_in [simp]:
assumes "finite A" and "A \<noteq> {}"
shows "Max A \<in> A"
using assms by (auto simp add: max_def Max.closed)
lemma Min_le [simp]:
assumes "finite A" and "x \<in> A"
shows "Min A \<le> x"
using assms by (fact Min.coboundedI)
lemma Max_ge [simp]:
assumes "finite A" and "x \<in> A"
shows "x \<le> Max A"
using assms by (fact Max.coboundedI)
lemma Min_eqI:
assumes "finite A"
assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
and "x \<in> A"
shows "Min A = x"
proof (rule antisym)
from `x \<in> A` have "A \<noteq> {}" by auto
with assms show "Min A \<ge> x" by simp
next
from assms show "x \<ge> Min A" by simp
qed
lemma Max_eqI:
assumes "finite A"
assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
and "x \<in> A"
shows "Max A = x"
proof (rule antisym)
from `x \<in> A` have "A \<noteq> {}" by auto
with assms show "Max A \<le> x" by simp
next
from assms show "x \<le> Max A" by simp
qed
lemma Min_ge_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
using assms by (fact Min.bounded_iff)
lemma Max_le_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
using assms by (fact Max.bounded_iff)
lemma Min_gr_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
using assms by (induct rule: finite_ne_induct) simp_all
lemma Max_less_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
using assms by (induct rule: finite_ne_induct) simp_all
lemma Min_le_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
using assms by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
lemma Max_ge_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
using assms by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
lemma Min_less_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
using assms by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
lemma Max_gr_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
using assms by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
lemma Min_antimono:
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Min N \<le> Min M"
using assms by (fact Min.antimono)
lemma Max_mono:
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Max M \<le> Max N"
using assms by (fact Max.antimono)
lemma mono_Min_commute:
assumes "mono f"
assumes "finite A" and "A \<noteq> {}"
shows "f (Min A) = Min (f ` A)"
proof (rule linorder_class.Min_eqI [symmetric])
from `finite A` show "finite (f ` A)" by simp
from assms show "f (Min A) \<in> f ` A" by simp
fix x
assume "x \<in> f ` A"
then obtain y where "y \<in> A" and "x = f y" ..
with assms have "Min A \<le> y" by auto
with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
with `x = f y` show "f (Min A) \<le> x" by simp
qed
lemma mono_Max_commute:
assumes "mono f"
assumes "finite A" and "A \<noteq> {}"
shows "f (Max A) = Max (f ` A)"
proof (rule linorder_class.Max_eqI [symmetric])
from `finite A` show "finite (f ` A)" by simp
from assms show "f (Max A) \<in> f ` A" by simp
fix x
assume "x \<in> f ` A"
then obtain y where "y \<in> A" and "x = f y" ..
with assms have "y \<le> Max A" by auto
with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
with `x = f y` show "x \<le> f (Max A)" by simp
qed
lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
assumes fin: "finite A"
and empty: "P {}"
and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
shows "P A"
using fin empty insert
proof (induct rule: finite_psubset_induct)
case (psubset A)
have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact
have fin: "finite A" by fact
have empty: "P {}" by fact
have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
show "P A"
proof (cases "A = {}")
assume "A = {}"
then show "P A" using `P {}` by simp
next
let ?B = "A - {Max A}"
let ?A = "insert (Max A) ?B"
have "finite ?B" using `finite A` by simp
assume "A \<noteq> {}"
with `finite A` have "Max A : A" by auto
then have A: "?A = A" using insert_Diff_single insert_absorb by auto
then have "P ?B" using `P {}` step IH [of ?B] by blast
moreover
have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
qed
qed
lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
"\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
end
context linordered_ab_semigroup_add
begin
lemma add_Min_commute:
fixes k
assumes "finite N" and "N \<noteq> {}"
shows "k + Min N = Min {k + m | m. m \<in> N}"
proof -
have "\<And>x y. k + min x y = min (k + x) (k + y)"
by (simp add: min_def not_le)
(blast intro: antisym less_imp_le add_left_mono)
with assms show ?thesis
using hom_Min_commute [of "plus k" N]
by simp (blast intro: arg_cong [where f = Min])
qed
lemma add_Max_commute:
fixes k
assumes "finite N" and "N \<noteq> {}"
shows "k + Max N = Max {k + m | m. m \<in> N}"
proof -
have "\<And>x y. k + max x y = max (k + x) (k + y)"
by (simp add: max_def not_le)
(blast intro: antisym less_imp_le add_left_mono)
with assms show ?thesis
using hom_Max_commute [of "plus k" N]
by simp (blast intro: arg_cong [where f = Max])
qed
end
context linordered_ab_group_add
begin
lemma minus_Max_eq_Min [simp]:
"finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
lemma minus_Min_eq_Max [simp]:
"finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
end
context complete_linorder
begin
lemma Min_Inf:
assumes "finite A" and "A \<noteq> {}"
shows "Min A = Inf A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
qed
lemma Max_Sup:
assumes "finite A" and "A \<noteq> {}"
shows "Max A = Sup A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
qed
end
end