Theory Matrix_Aggregation_Algebras
section ‹Matrix Algebras for Aggregation and Minimisation›
text ‹
This theory formalises aggregation orders and lattices as introduced in \<^cite>‹"Guttmann2018a"›.
Aggregation in these algebras is an associative and commutative operation satisfying additional properties related to the partial order and its least element.
We apply the aggregation operation to finite matrices over the aggregation algebras, which shows that they form an s-algebra.
By requiring the aggregation algebras to be linearly ordered, we also obtain that the matrices form an m-algebra.
This is an intermediate step in demonstrating that weighted graphs form an s-algebra and an m-algebra.
The present theory specifies abstract properties for the edge weights and shows that matrices over such weights form an instance of s-algebras and m-algebras.
A second step taken in a separate theory gives concrete instances of edge weights satisfying the abstract properties introduced here.
Lifting the aggregation to matrices requires finite sums over elements taken from commutative semigroups with an element that is a unit on the image of the semigroup operation.
Because standard sums assume a commutative monoid we have to derive a number of properties of these generalised sums as their statements or proofs are different.
›
theory Matrix_Aggregation_Algebras
imports Stone_Kleene_Relation_Algebras.Matrix_Kleene_Algebras Aggregation_Algebras Semigroups_Big
begin
no_notation
inf (infixl "⊓" 70)
and uminus ("- _" [81] 80)
subsection ‹Aggregation Orders and Finite Sums›
text ‹
An aggregation order is a partial order with a least element and an associative commutative operation satisfying certain properties.
Axiom ‹add_add_bot› introduces almost a commutative monoid; we require that ‹bot› is a unit only on the image of the aggregation operation.
This is necessary since it is not a unit of a number of aggregation operations we are interested in.
Axiom ‹add_right_isotone› states that aggregation is $\leq$-isotone on the image of the aggregation operation.
Its assumption $x \neq bot$ is necessary because the introduction of new edges can decrease the aggregated value.
Axiom ‹add_bot› expresses that aggregation is zero-sum-free.
›
class aggregation_order = order_bot + ab_semigroup_add +
assumes add_right_isotone: "x ≠ bot ∧ x + bot ≤ y + bot ⟶ x + z ≤ y + z"
assumes add_add_bot [simp]: "x + y + bot = x + y"
assumes add_bot: "x + y = bot ⟶ x = bot"
begin
abbreviation "zero ≡ bot + bot"
sublocale aggregation: ab_semigroup_add_0 where plus = plus and zero = zero
apply unfold_locales
using add_assoc add_add_bot by auto
lemma add_bot_bot_bot:
"x + bot + bot + bot = x + bot"
by simp
end
text ‹
We introduce notation for finite sums over aggregation orders.
The index variable of the summation ranges over the finite universe of its type.
Finite sums are defined recursively using the binary aggregation and $\bot + \bot$ for the empty sum.
›
syntax (xsymbols)
"_sum_ab_semigroup_add_0" :: "idt ⇒ 'a::bounded_semilattice_sup_bot ⇒ 'a" ("(∑⇩_ _)" [0,10] 10)
translations
"∑⇩x t" => "XCONST ab_semigroup_add_0.sum_0 XCONST plus (XCONST plus XCONST bot XCONST bot) (λx . t) { x . CONST True }"
text ‹
The following are basic properties of such sums.
›
lemma agg_sum_bot:
"(∑⇩k bot::'a::aggregation_order) = bot + bot"
proof (induct rule: infinite_finite_induct)
case (infinite A)
thus ?case
by simp
next
case empty
thus ?case
by simp
next
case (insert x F)
thus ?case
by (metis add.commute add_add_bot aggregation.sum_0.insert)
qed
lemma agg_sum_bot_bot:
"(∑⇩k bot + bot::'a::aggregation_order) = bot + bot"
by (rule aggregation.sum_0.neutral_const)
lemma agg_sum_not_bot_1:
fixes f :: "'a::finite ⇒ 'b::aggregation_order"
assumes "f i ≠ bot"
shows "(∑⇩k f k) ≠ bot"
by (metis assms add_bot aggregation.sum_0.remove finite_code mem_Collect_eq)
lemma agg_sum_not_bot:
fixes f :: "('a::finite,'b::aggregation_order) square"
assumes "f (i,j) ≠ bot"
shows "(∑⇩k ∑⇩l f (k,l)) ≠ bot"
by (metis assms agg_sum_not_bot_1)
lemma agg_sum_distrib:
fixes f g :: "'a ⇒ 'b::aggregation_order"
shows "(∑⇩k f k + g k) = (∑⇩k f k) + (∑⇩k g k)"
by (rule aggregation.sum_0.distrib)
lemma agg_sum_distrib_2:
fixes f g :: "('a,'b::aggregation_order) square"
shows "(∑⇩k ∑⇩l f (k,l) + g (k,l)) = (∑⇩k ∑⇩l f (k,l)) + (∑⇩k ∑⇩l g (k,l))"
proof -
have "(∑⇩k ∑⇩l f (k,l) + g (k,l)) = (∑⇩k (∑⇩l f (k,l)) + (∑⇩l g (k,l)))"
by (metis (no_types) aggregation.sum_0.distrib)
also have "... = (∑⇩k ∑⇩l f (k,l)) + (∑⇩k ∑⇩l g (k,l))"
by (metis (no_types) aggregation.sum_0.distrib)
finally show ?thesis
.
qed
lemma agg_sum_add_bot:
fixes f :: "'a ⇒ 'b::aggregation_order"
shows "(∑⇩k f k) = (∑⇩k f k) + bot"
by (metis (no_types) add_add_bot aggregation.sum_0.F_one)
lemma agg_sum_add_bot_2:
fixes f :: "'a ⇒ 'b::aggregation_order"
shows "(∑⇩k f k + bot) = (∑⇩k f k)"
proof -
have "(∑⇩k f k + bot) = (∑⇩k f k) + (∑⇩k::'a bot::'b)"
using agg_sum_distrib by simp
also have "... = (∑⇩k f k) + (bot + bot)"
by (metis agg_sum_bot)
also have "... = (∑⇩k f k)"
by simp
finally show ?thesis
by simp
qed
lemma agg_sum_commute:
fixes f :: "('a,'b::aggregation_order) square"
shows "(∑⇩k ∑⇩l f (k,l)) = (∑⇩l ∑⇩k f (k,l))"
by (rule aggregation.sum_0.swap)
lemma agg_delta:
fixes f :: "'a::finite ⇒ 'b::aggregation_order"
shows "(∑⇩l if l = j then f l else zero) = f j + bot"
apply (subst aggregation.sum_0.delta)
apply simp
by (metis add.commute add.left_commute add_add_bot mem_Collect_eq)
lemma agg_delta_1:
fixes f :: "'a::finite ⇒ 'b::aggregation_order"
shows "(∑⇩l if l = j then f l else bot) = f j + bot"
proof -
let ?f = "(λl . if l = j then f l else bot)"
let ?S = "{l::'a . True}"
show ?thesis
proof (cases "j ∈ ?S")
case False
thus ?thesis by simp
next
case True
let ?A = "?S - {j}"
let ?B = "{j}"
from True have eq: "?S = ?A ∪ ?B"
by blast
have dj: "?A ∩ ?B = {}"
by simp
have fAB: "finite ?A" "finite ?B"
by auto
have "aggregation.sum_0 ?f ?S = aggregation.sum_0 ?f ?A + aggregation.sum_0 ?f ?B"
using aggregation.sum_0.union_disjoint[OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
also have "... = aggregation.sum_0 (λl . bot) ?A + aggregation.sum_0 ?f ?B"
by (subst aggregation.sum_0.cong[where ?B="?A"]) simp_all
also have "... = zero + aggregation.sum_0 ?f ?B"
by (metis (no_types, lifting) add.commute add_add_bot aggregation.sum_0.F_g_one aggregation.sum_0.neutral)
also have "... = zero + (f j + zero)"
by simp
also have "... = f j + bot"
by (metis add.commute add.left_commute add_add_bot)
finally show ?thesis
.
qed
qed
lemma agg_delta_2:
fixes f :: "('a::finite,'b::aggregation_order) square"
shows "(∑⇩k ∑⇩l if k = i ∧ l = j then f (k,l) else bot) = f (i,j) + bot"
proof -
have "∀k . (∑⇩l if k = i ∧ l = j then f (k,l) else bot) = (if k = i then f (k,j) + bot else zero)"
proof
fix k
have "(∑⇩l if k = i ∧ l = j then f (k,l) else bot) = (∑⇩l if l = j then if k = i then f (k,l) else bot else bot)"
by meson
also have "... = (if k = i then f (k,j) else bot) + bot"
by (rule agg_delta_1)
finally show "(∑⇩l if k = i ∧ l = j then f (k,l) else bot) = (if k = i then f (k,j) + bot else zero)"
by simp
qed
hence "(∑⇩k ∑⇩l if k = i ∧ l = j then f (k,l) else bot) = (∑⇩k if k = i then f (k,j) + bot else zero)"
using aggregation.sum_0.cong by auto
also have "... = f (i,j) + bot"
apply (subst agg_delta)
by simp
finally show ?thesis
.
qed
subsection ‹Matrix Aggregation›
text ‹
The following definitions introduce the matrix of unit elements, componentwise aggregation and aggregation on matrices.
The aggregation of a matrix is a single value, but because s-algebras are single-sorted the result has to be encoded as a matrix of the same type (size) as the input.
We store the aggregated matrix value in the `first' entry of a matrix, setting all other entries to the unit value.
The first entry is determined by requiring an enumeration of indices.
It does not have to be the first entry; any fixed location in the matrix would work as well.
›
definition zero_matrix :: "('a,'b::{plus,bot}) square" ("mzero") where "mzero = (λe . bot + bot)"
definition plus_matrix :: "('a,'b::plus) square ⇒ ('a,'b) square ⇒ ('a,'b) square" (infixl "⊕⇩M" 65) where "plus_matrix f g = (λe . f e + g e)"
definition sum_matrix :: "('a::enum,'b::{plus,bot}) square ⇒ ('a,'b) square" ("sum⇩M _" [80] 80) where "sum_matrix f = (λ(i,j) . if i = hd enum_class.enum ∧ j = i then ∑⇩k ∑⇩l f (k,l) else bot + bot)"
text ‹
Basic properties of these operations are given in the following.
›
lemma bot_plus_bot:
"mbot ⊕⇩M mbot = mzero"
by (simp add: plus_matrix_def bot_matrix_def zero_matrix_def)
lemma sum_bot:
"sum⇩M (mbot :: ('a::enum,'b::aggregation_order) square) = mzero"
proof (rule ext, rule prod_cases)
fix i j :: "'a"
have "(sum⇩M mbot :: ('a,'b) square) (i,j) = (if i = hd enum_class.enum ∧ j = i then ∑⇩(k::'a) ∑⇩(l::'a) bot else bot + bot)"
by (unfold sum_matrix_def bot_matrix_def) simp
also have "... = bot + bot"
using agg_sum_bot aggregation.sum_0.neutral by fastforce
also have "... = mzero (i,j)"
by (simp add: zero_matrix_def)
finally show "(sum⇩M mbot :: ('a,'b) square) (i,j) = mzero (i,j)"
.
qed
lemma sum_plus_bot:
fixes f :: "('a::enum,'b::aggregation_order) square"
shows "sum⇩M f ⊕⇩M mbot = sum⇩M f"
proof (rule ext, rule prod_cases)
let ?h = "hd enum_class.enum"
fix i j
have "(sum⇩M f ⊕⇩M mbot) (i,j) = (if i = ?h ∧ j = i then (∑⇩k ∑⇩l f (k,l)) + bot else zero + bot)"
by (simp add: plus_matrix_def bot_matrix_def sum_matrix_def)
also have "... = (if i = ?h ∧ j = i then ∑⇩k ∑⇩l f (k,l) else zero)"
by (metis (no_types, lifting) add_add_bot aggregation.sum_0.F_one)
also have "... = (sum⇩M f) (i,j)"
by (simp add: sum_matrix_def)
finally show "(sum⇩M f ⊕⇩M mbot) (i,j) = (sum⇩M f) (i,j)"
by simp
qed
lemma sum_plus_zero:
fixes f :: "('a::enum,'b::aggregation_order) square"
shows "sum⇩M f ⊕⇩M mzero = sum⇩M f"
by (rule ext, rule prod_cases) (simp add: plus_matrix_def zero_matrix_def sum_matrix_def)
lemma agg_matrix_bot:
fixes f :: "('a,'b::aggregation_order) square"
assumes "∀i j . f (i,j) = bot"
shows "f = mbot"
apply (unfold bot_matrix_def)
using assms by auto
text ‹
We consider a different implementation of matrix aggregation which stores the aggregated value in all entries of the matrix instead of a particular one.
This does not require an enumeration of the indices.
All results continue to hold using this alternative implementation.
›
definition sum_matrix_2 :: "('a,'b::{plus,bot}) square ⇒ ('a,'b) square" ("sum2⇩M _" [80] 80) where "sum_matrix_2 f = (λe . ∑⇩k ∑⇩l f (k,l))"
lemma sum_bot_2:
"sum2⇩M (mbot :: ('a,'b::aggregation_order) square) = mzero"
proof
fix e
have "(sum2⇩M mbot :: ('a,'b) square) e = (∑⇩(k::'a) ∑⇩(l::'a) bot)"
by (unfold sum_matrix_2_def bot_matrix_def) simp
also have "... = bot + bot"
using agg_sum_bot aggregation.sum_0.neutral by fastforce
also have "... = mzero e"
by (simp add: zero_matrix_def)
finally show "(sum2⇩M mbot :: ('a,'b) square) e = mzero e"
.
qed
lemma sum_plus_bot_2:
fixes f :: "('a,'b::aggregation_order) square"
shows "sum2⇩M f ⊕⇩M mbot = sum2⇩M f"
proof
fix e
have "(sum2⇩M f ⊕⇩M mbot) e = (∑⇩k ∑⇩l f (k,l)) + bot"
by (simp add: plus_matrix_def bot_matrix_def sum_matrix_2_def)
also have "... = (∑⇩k ∑⇩l f (k,l))"
by (metis (no_types, lifting) add_add_bot aggregation.sum_0.F_one)
also have "... = (sum2⇩M f) e"
by (simp add: sum_matrix_2_def)
finally show "(sum2⇩M f ⊕⇩M mbot) e = (sum2⇩M f) e"
by simp
qed
lemma sum_plus_zero_2:
fixes f :: "('a,'b::aggregation_order) square"
shows "sum2⇩M f ⊕⇩M mzero = sum2⇩M f"
by (simp add: plus_matrix_def zero_matrix_def sum_matrix_2_def)
subsection ‹Aggregation Lattices›
text ‹
We extend aggregation orders to dense bounded distributive lattices.
Axiom ‹add_lattice› implements the inclusion-exclusion principle at the level of edge weights.
›