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)"
  by (simp add: assms sum_sup)

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
    by (simp add: eq_iff)
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)"
  by (simp add: assms)

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
    by (simp add: eq_iff)
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
    by (simp add: eq_iff)
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.›

lemma sum_fun_add:
  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))"
    by (rule fadd)
  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
    by (simp add: assms sum_flatten1)
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
    by (simp add: assms sum_flatten2)
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}"
    by (simp add: assms sum_distr)
  also have "... = ∑{∑{x ⋅ y |y. y ∈ B} |x. x ∈ A}"
    by (simp add: assms sum_distl)
  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