# Theory Finite_Suprema

```(* Title:      Finite Suprema
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Finite Suprema›

theory Finite_Suprema
imports Dioid
begin

text ‹This file contains an adaptation of Isabelle's library for
finite sums to the case of (join) semilattices and dioids. In this
setting, addition is idempotent; finite sums are finite suprema.

We add some basic properties of finite suprema for (join) semilattices
and dioids.›

subsection ‹Auxiliary Lemmas›

lemma fun_im: "{f a |a. a ∈ A} = {b. b ∈ f ` A}"
by auto

lemma fset_to_im: "{f x |x. x ∈ X} = f ` X"
by auto

lemma cart_flip_aux: "{f (snd p) (fst p) |p. p ∈ (B × A)} = {f (fst p) (snd p) |p. p ∈ (A × B)}"
by auto

lemma cart_flip: "(λp. f (snd p) (fst p)) ` (B × A) = (λp. f (fst p) (snd p)) ` (A × B)"
by (metis cart_flip_aux fset_to_im)

lemma fprod_aux: "{x ⋅ y |x y. x ∈ (f ` A) ∧ y ∈ (g ` B)} = {f x ⋅ g y |x y. x ∈ A ∧ y ∈ B}"
by auto

subsection ‹Finite Suprema in Semilattices›

text ‹The first lemma shows that, in the context of semilattices,
finite sums satisfy the defining property of finite suprema.›

lemma sum_sup:
assumes "finite (A :: 'a::join_semilattice_zero set)"
shows "∑A ≤ z ⟷ (∀a ∈ A. a ≤ z)"
proof (induct rule: finite_induct[OF assms])
fix z ::'a
show "(∑{} ≤ z) = (∀a ∈ {}. a ≤ z)"
by simp
next
fix x z :: 'a and F :: "'a set"
assume finF: "finite F"
and xnF: "x ∉ F"
and indhyp: "(∑F ≤ z) = (∀a ∈ F. a ≤ z)"
show "(∑(insert x F) ≤ z) = (∀a ∈ insert x F. a ≤ z)"
proof -
have "∑(insert x F) ≤ z ⟷ (x + ∑F) ≤ z"
by (metis finF sum.insert xnF)
also have "... ⟷ x ≤ z ∧ ∑F ≤ z"
by simp
also have "... ⟷ x ≤ z ∧ (∀a ∈ F. a ≤ z)"
by (metis (lifting) indhyp)
also have "... ⟷ (∀a ∈ insert x F. a ≤ z)"
by (metis insert_iff)
ultimately show "(∑(insert x F) ≤ z) = (∀a ∈ insert x F. a ≤ z)"
by blast
qed
qed

text ‹This immediately implies some variants.›

lemma sum_less_eqI:
"(⋀x. x ∈ A ⟹ f x ≤ y) ⟹ sum f A ≤ (y::'a::join_semilattice_zero)"
apply (atomize (full))
apply (case_tac "finite A")
apply (erule finite_induct)
apply simp_all
done

lemma sum_less_eqE:
"⟦ sum f A ≤ y; x ∈ A; finite A ⟧ ⟹ f x ≤ (y::'a::join_semilattice_zero)"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule finite_induct)
apply auto
done

lemma sum_fun_image_sup:
fixes f :: "'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A :: 'a set)"
shows "∑(f ` A) ≤ z ⟷ (∀a ∈ A. f a ≤ z)"

lemma sum_fun_sup:
fixes f :: "'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A ::'a set)"
shows "∑{f a | a. a ∈ A} ≤ z ⟷ (∀a ∈ A. f a ≤ z)"
by (simp only: fset_to_im assms sum_fun_image_sup)

lemma sum_intro:
assumes "finite (A :: 'a::join_semilattice_zero set)" and "finite B"
shows "(∀a ∈ A. ∃b ∈ B. a ≤ b) ⟶ (∑A ≤ ∑B)"
by (metis assms order_refl order_trans sum_sup)

text ‹Next we prove an additivity property for suprema.›

lemma sum_union:
assumes "finite (A :: 'a::join_semilattice_zero set)"
and "finite (B :: 'a::join_semilattice_zero set)"
shows "∑(A ∪ B) = ∑A + ∑B"
proof -
have "∀z. ∑(A ∪ B) ≤ z ⟷ (∑A + ∑B ≤ z)"
by (auto simp add: assms sum_sup)
thus ?thesis
qed

text ‹It follows that the sum (supremum) of a two-element set is the
join of its elements.›

lemma sum_bin[simp]: "∑{(x :: 'a::join_semilattice_zero),y} = x + y"
by (subst insert_is_Un, subst sum_union, auto)

text ‹Next we show that finite suprema are order preserving.›

lemma sum_iso:
assumes "finite (B :: 'a::join_semilattice_zero set)"
shows "A ⊆ B ⟶ ∑ A ≤ ∑ B"
by (metis assms finite_subset order_refl rev_subsetD sum_sup)

text ‹The following lemmas state unfold properties for suprema and
finite sets. They are subtly different from the non-idempotent case,
where additional side conditions are required.›

lemma sum_insert [simp]:
assumes "finite (A :: 'a::join_semilattice_zero set)"
shows "∑(insert x A) = x + ∑A"
proof -
have "∑(insert x A) = ∑{x} + ∑A"
by (metis insert_is_Un assms finite.emptyI finite.insertI sum_union)
thus ?thesis
by auto
qed

lemma sum_fun_insert:
fixes f :: "'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A :: 'a set)"
shows "∑(f ` (insert x A)) = f x + ∑(f ` A)"

text ‹Now we show that set comprehensions with nested suprema can
be flattened.›

lemma flatten1_im:
fixes f :: "'a ⇒ 'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A :: 'a set)"
and "finite (B :: 'a set)"
shows "∑((λx. ∑(f x ` B)) ` A) = ∑((λp. f (fst p) (snd p)) ` (A × B))"
proof -
have "∀z. ∑((λx. ∑(f x ` B)) ` A) ≤ z ⟷ ∑((λp. f (fst p) (snd p)) ` (A × B)) ≤ z"
by (simp add: assms finite_cartesian_product sum_fun_image_sup)
thus ?thesis
qed

lemma flatten2_im:
fixes f :: "'a ⇒ 'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A ::'a set)"
and "finite (B ::'a set)"
shows "∑((λy. ∑ ((λx. f x y) ` A)) ` B) = ∑((λp. f (fst p) (snd p)) ` (A × B))"
by (simp only: flatten1_im assms cart_flip)

lemma sum_flatten1:
fixes f :: "'a ⇒ 'a ⇒ 'b::join_semilattice_zero"
assumes "finite (A :: 'a set)"
and "finite (B :: 'a set)"
shows "∑{∑{f x y |y. y ∈ B} |x. x ∈ A} = ∑{f x y |x y. x ∈ A ∧ y ∈ B}"
apply (simp add: fset_to_im assms flatten1_im)
apply (subst fset_to_im[symmetric])
apply simp
done

lemma sum_flatten2:
fixes f :: "'a ⇒ 'a ⇒ 'b::join_semilattice_zero"
assumes "finite A"
and "finite B"
shows "∑{∑ {f x y |x. x ∈ A} |y. y ∈ B} = ∑{f x y |x y. x ∈ A ∧ y ∈ B}"
apply (simp add: fset_to_im assms flatten2_im)
apply (subst fset_to_im[symmetric])
apply simp
done

text ‹Next we show another additivity property for suprema.›

lemma sum_fun_sum:
fixes f g :: "'a ⇒ 'b::join_semilattice_zero"
assumes  "finite (A :: 'a set)"
shows "∑((λx. f x + g x) ` A) = ∑(f ` A) + ∑(g ` A)"
proof -
{
fix z:: 'b
have "∑((λx. f x + g x) ` A) ≤ z ⟷ ∑(f ` A) + ∑(g ` A) ≤ z"
by (auto simp add: assms sum_fun_image_sup)
}
thus ?thesis
qed

text ‹The last lemma of this section prepares the distributivity
laws that hold for dioids. It states that a strict additive function
distributes over finite suprema, which is a continuity property in
the finite.›

fixes f :: "'a::join_semilattice_zero ⇒ 'b::join_semilattice_zero"
assumes "finite (X :: 'a set)"
and fstrict: "f 0 = 0"
and fadd: "⋀x y. f (x + y) = f x + f y"
shows "f (∑ X) = ∑(f ` X)"
proof (induct rule: finite_induct[OF assms(1)])
show "f (∑{}) = ∑(f ` {})"
by (metis fstrict image_empty sum.empty)
fix x :: 'a and  F ::" 'a set"
assume finF: "finite F"
and indhyp: "f (∑F) = ∑(f ` F)"
have "f (∑(insert x F)) = f (x + ∑F)"
by (metis sum_insert finF)
also have "... = f x + (f (∑F))"
also have "... = f x + ∑(f ` F)"
by (metis indhyp)
also have "... = ∑(f ` (insert x F))"
by (metis finF sum_fun_insert)
finally show "f (∑(insert x F)) = ∑(f ` insert x F)" .
qed

subsection ‹Finite Suprema in Dioids›

text ‹In this section we mainly prove variants of distributivity laws.›

lemma sum_distl:
assumes "finite Y"
shows "(x :: 'a::dioid_one_zero) ⋅ (∑Y) = ∑{x ⋅ y|y. y ∈ Y}"
by (simp only: sum_fun_add assms annir distrib_left Collect_mem_eq fun_im)

lemma sum_distr:
assumes "finite X"
shows "(∑X) ⋅ (y :: 'a::dioid_one_zero) = ∑{x ⋅ y|x. x ∈ X}"
proof -
have "(∑ X) ⋅ y = ∑ ((λx. x ⋅ y) ` X)"
by (rule sum_fun_add, metis assms, rule annil, rule distrib_right)
thus ?thesis
by (metis Collect_mem_eq fun_im)
qed

lemma sum_fun_distl:
fixes f :: "'a ⇒ 'b::dioid_one_zero"
assumes "finite (Y :: 'a set)"
shows "x ⋅ ∑(f ` Y) = ∑{x ⋅ f y |y. y ∈ Y}"
by (simp add: assms fun_im image_image sum_distl)

lemma sum_fun_distr:
fixes f :: "'a ⇒ 'b::dioid_one_zero"
assumes "finite (X :: 'a set)"
shows "∑(f ` X) ⋅ y = ∑{f x ⋅ y |x. x ∈ X}"
by (simp add: assms fun_im image_image sum_distr)

lemma sum_distl_flat:
assumes "finite (X ::'a::dioid_one_zero set)"
and "finite Y"
shows "∑{x ⋅ ∑Y |x. x ∈ X} = ∑{x ⋅ y|x y. x ∈ X ∧ y ∈ Y}"
by (simp only: assms sum_distl sum_flatten1)

lemma sum_distr_flat:
assumes "finite X"
and "finite (Y :: 'a::dioid_one_zero set)"
shows "∑{(∑X) ⋅ y |y. y ∈ Y} = ∑{x ⋅ y|x y. x ∈ X ∧ y ∈ Y}"
by (simp only: assms sum_distr sum_flatten2)

lemma sum_sum_distl:
assumes "finite (X :: 'a::dioid_one_zero set)"
and "finite Y"
shows "∑((λx. x ⋅ (∑Y)) ` X) = ∑{x ⋅ y |x y. x ∈ X ∧ y ∈ Y}"
proof -
have "∑((λx. x ⋅ (∑Y)) ` X) = ∑{∑{x ⋅ y |y. y ∈ Y} |x. x ∈ X}"
by (auto simp add: sum_distl assms fset_to_im)
thus ?thesis
qed

lemma sum_sum_distr:
assumes "finite X"
and "finite Y"
shows "∑((λy. (∑X) ⋅ (y :: 'a::dioid_one_zero)) ` Y) = ∑{x ⋅ y|x y. x ∈ X ∧ y ∈ Y}"
proof -
have "∑((λy. (∑X) ⋅ y) ` Y) = ∑{∑{x ⋅ y |x. x ∈ X} |y. y ∈ Y}"
by (auto simp add: sum_distr assms fset_to_im)
thus ?thesis
qed

lemma sum_sum_distl_fun:
fixes f g :: "'a ⇒ 'b::dioid_one_zero"
fixes h :: "'a ⇒ 'a set"
assumes "⋀x. finite (h x)"
and "finite X"
shows "∑((λx. f x ⋅ ∑(g ` h x)) ` X) = ∑{∑ {f x ⋅ g y |y. y ∈ h x} |x. x ∈ X}"
by (auto simp add: sum_fun_distl assms fset_to_im)

lemma sum_sum_distr_fun:
fixes f g :: "'a ⇒ 'b::dioid_one_zero"
fixes h :: "'a ⇒ 'a set"
assumes "finite Y"
and "⋀y. finite (h y)"
shows "∑((λy. ∑(f ` h y) ⋅ g y) ` Y) = ∑{∑{f x ⋅ g y |x. x ∈ (h y)} |y. y ∈ Y}"
by (auto simp add: sum_fun_distr assms fset_to_im)

lemma sum_dist:
assumes "finite (A :: 'a::dioid_one_zero set)"
and "finite B"
shows "(∑A) ⋅ (∑B) = ∑{x ⋅ y |x y. x ∈ A ∧ y ∈ B}"
proof -
have "(∑A) ⋅ (∑B) = ∑{x ⋅ ∑B |x. x ∈ A}"
also have "... = ∑{∑{x ⋅ y |y. y ∈ B} |x. x ∈ A}"
finally show ?thesis
by  (simp only: sum_flatten1 assms finite_cartesian_product)
qed

lemma dioid_sum_prod_var:
fixes f g :: "'a ⇒ 'b::dioid_one_zero"
assumes "finite (A ::'a set)"
shows "(∑(f ` A)) ⋅ (∑ (g ` A)) = ∑{f x ⋅ g y |x y. x ∈ A ∧ y ∈ A}"
by (simp add: assms sum_dist fprod_aux)

lemma dioid_sum_prod:
fixes f g :: "'a ⇒ 'b::dioid_one_zero"
assumes "finite (A :: 'a set)"
shows "(∑{f x |x. x ∈ A}) ⋅ (∑{g x |x. x ∈ A}) = ∑{f x ⋅ g y |x y. x ∈ A ∧ y ∈ A}"
by (simp add: assms dioid_sum_prod_var fset_to_im)

lemma sum_image:
fixes f :: "'a ⇒ 'b::join_semilattice_zero"
assumes "finite X"
shows "sum f X = ∑(f ` X)"
using assms
proof (induct rule: finite_induct)
case empty thus ?case by simp
next
case insert thus ?case
by (metis sum.insert sum_fun_insert)
qed

lemma sum_interval_cong:
"⟦ ⋀ i. ⟦ m ≤ i; i ≤ n ⟧ ⟹ P(i) = Q(i) ⟧ ⟹ (∑i=m..n. P(i)) = (∑i=m..n. Q(i))"
by (auto intro: sum.cong)

lemma sum_interval_distl:
fixes f :: "nat ⇒ 'a::dioid_one_zero"
assumes "m ≤ n"
shows "x ⋅ (∑i=m..n. f(i)) = (∑i=m..n. (x ⋅ f(i)))"
proof -
have "x ⋅ (∑i=m..n. f(i)) = x ⋅ ∑(f ` {m..n})"
by (metis finite_atLeastAtMost sum_image)
also have "... = ∑{x ⋅ y |y. y ∈ f ` {m..n}}"
by (metis finite_atLeastAtMost fset_to_im image_image sum_fun_distl)
also have "... = ∑((λi. x ⋅ f i) ` {m..n})"
by (metis fset_to_im image_image)
also have "... = (∑i=m..n. (x ⋅ f(i)))"
by (metis finite_atLeastAtMost sum_image)
finally show ?thesis .
qed

lemma sum_interval_distr:
fixes f :: "nat ⇒ 'a::dioid_one_zero"
assumes "m ≤ n"
shows "(∑i=m..n. f(i)) ⋅ y = (∑i=m..n. (f(i) ⋅ y))"
proof -
have "(∑i=m..n. f(i)) ⋅ y = ∑(f ` {m..n}) ⋅ y"
by (metis finite_atLeastAtMost sum_image)
also have "... = ∑{x ⋅ y |x. x ∈ f ` {m..n}}"
by (metis calculation finite_atLeastAtMost finite_imageI fset_to_im sum_distr)
also have "... = ∑((λi. f(i) ⋅ y) ` {m..n})"
by (auto intro: sum.cong)
also have "... = (∑i=m..n. (f(i) ⋅ y))"
by (metis finite_atLeastAtMost sum_image)
finally show ?thesis .
qed

text ‹There are interesting theorems for finite sums in Kleene
algebras; we leave them for future consideration.›

end
```