(* 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