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