# Theory Matrix_Relation_Algebras

```(* Title:      Matrix Relation Algebras
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Matrix Relation Algebras›

text ‹
This theory gives matrix models of Stone relation algebras and more general structures.
We consider only square matrices.
The main result is that matrices over Stone relation algebras form a Stone relation algebra.

We use the monoid structure underlying semilattices to provide finite sums, which are necessary for defining the composition of two matrices.
See \cite{ArmstrongFosterStruthWeber2016,ArmstrongGomesStruthWeber2016} for similar liftings to matrices for semirings and relation algebras.
A technical difference is that those theories are mostly based on semirings whereas our hierarchy is mostly based on lattices (and our semirings directly inherit from semilattices).

Relation algebras have both a semiring and a lattice structure such that semiring addition and lattice join coincide.
In particular, finite sums and finite suprema coincide.
Isabelle/HOL has separate theories for semirings and lattices, based on separate addition and join operations and different operations for finite sums and finite suprema.
Reusing results from both theories is beneficial for relation algebras, but not always easy to realise.
›

theory Matrix_Relation_Algebras

imports Relation_Algebras

begin

subsection ‹Finite Suprema›

text ‹
We consider finite suprema in idempotent semirings and Stone relation algebras.
We mostly use the first of the following notations, which denotes the supremum of expressions ‹t(x)› over all ‹x› from the type of ‹x›.
For finite types, this is implemented in Isabelle/HOL as the repeated application of binary suprema.
›

syntax
"_sum_sup_monoid" :: "idt ⇒ 'a::bounded_semilattice_sup_bot ⇒ 'a" ("(⨆⇩_ _)" [0,10] 10)
"_sum_sup_monoid_bounded" :: "idt ⇒ 'b set ⇒ 'a::bounded_semilattice_sup_bot ⇒ 'a" ("(⨆⇘_∈_⇙ _)" [0,51,10] 10)
translations
"⨆⇩x t" => "XCONST sup_monoid.sum (λx . t) { x . CONST True }"
"⨆⇘x∈X⇙ t" => "XCONST sup_monoid.sum (λx . t) X"

context idempotent_semiring
begin

text ‹
The following induction principles are useful for comparing two suprema.
The first principle works because types are not empty.
›

lemma one_sup_induct [case_names one sup]:
fixes f g :: "'b::finite ⇒ 'a"
assumes one: "⋀i . P (f i) (g i)"
and sup: "⋀j I . j ∉ I ⟹ P (⨆⇘i∈I⇙ f i) (⨆⇘i∈I⇙ g i) ⟹ P (f j ⊔ (⨆⇘i∈I⇙ f i)) (g j ⊔ (⨆⇘i∈I⇙ g i))"
shows "P (⨆⇩k f k) (⨆⇩k g k)"
proof -
let ?X = "{ k::'b . True }"
have "finite ?X" and "?X ≠ {}"
by auto
thus ?thesis
proof (induct rule: finite_ne_induct)
case (singleton i) thus ?case
using one by simp
next
case (insert j I) thus ?case
using sup by simp
qed
qed

lemma bot_sup_induct [case_names bot sup]:
fixes f g :: "'b::finite ⇒ 'a"
assumes bot: "P bot bot"
and sup: "⋀j I . j ∉ I ⟹ P (⨆⇘i∈I⇙ f i) (⨆⇘i∈I⇙ g i) ⟹ P (f j ⊔ (⨆⇘i∈I⇙ f i)) (g j ⊔ (⨆⇘i∈I⇙ g i))"
shows "P (⨆⇩k f k) (⨆⇩k g k)"
apply (induct rule: one_sup_induct)
using bot sup apply fastforce
using sup by blast

text ‹
Now many properties of finite suprema follow by simple applications of the above induction rules.
In particular, we show distributivity of composition, isotonicity and the upper-bound property.
›

lemma comp_right_dist_sum:
fixes f :: "'b::finite ⇒ 'a"
shows "(⨆⇩k f k * x) = (⨆⇩k f k) * x"
proof (induct rule: one_sup_induct)
case one show ?case
by simp
next
case (sup j I) thus ?case
using mult_right_dist_sup by auto
qed

lemma comp_left_dist_sum:
fixes f :: "'b::finite ⇒ 'a"
shows "(⨆⇩k x * f k) = x * (⨆⇩k f k)"
proof (induct rule: one_sup_induct)
case one show ?case
by simp
next
case (sup j I) thus ?case
by (simp add: mult_left_dist_sup)
qed

lemma leq_sum:
fixes f g :: "'b::finite ⇒ 'a"
shows "(∀k . f k ≤ g k) ⟹ (⨆⇩k f k) ≤ (⨆⇩k g k)"
proof (induct rule: one_sup_induct)
case one thus ?case
by simp
next
case (sup j I) thus ?case
using sup_mono by blast
qed

lemma ub_sum:
fixes f :: "'b::finite ⇒ 'a"
shows "f i ≤ (⨆⇩k f k)"
proof -
have "i ∈ { k . True }"
by simp
thus "f i ≤ (⨆⇩k f (k::'b))"
by (metis finite_code sup_monoid.sum.insert sup_ge1 mk_disjoint_insert)
qed

lemma lub_sum:
fixes f :: "'b::finite ⇒ 'a"
assumes "∀k . f k ≤ x"
shows "(⨆⇩k f k) ≤ x"
proof (induct rule: one_sup_induct)
case one show ?case
by (simp add: assms)
next
case (sup j I) thus ?case
using assms le_supI by blast
qed

lemma lub_sum_iff:
fixes f :: "'b::finite ⇒ 'a"
shows "(∀k . f k ≤ x) ⟷ (⨆⇩k f k) ≤ x"
using order.trans ub_sum lub_sum by blast

end

context stone_relation_algebra
begin

text ‹
In Stone relation algebras, we can also show that converse,  double complement and meet distribute over finite suprema.
›

lemma conv_dist_sum:
fixes f :: "'b::finite ⇒ 'a"
shows "(⨆⇩k (f k)⇧T) = (⨆⇩k f k)⇧T"
proof (induct rule: one_sup_induct)
case one show ?case
by simp
next
case (sup j I) thus ?case
by (simp add: conv_dist_sup)
qed

lemma pp_dist_sum:
fixes f :: "'b::finite ⇒ 'a"
shows "(⨆⇩k --f k) = --(⨆⇩k f k)"
proof (induct rule: one_sup_induct)
case one show ?case
by simp
next
case (sup j I) thus ?case
by simp
qed

lemma inf_right_dist_sum:
fixes f :: "'b::finite ⇒ 'a"
shows "(⨆⇩k f k ⊓ x) = (⨆⇩k f k) ⊓ x"
by (rule comp_inf.comp_right_dist_sum)

end

subsection ‹Square Matrices›

text ‹
Because our semiring and relation algebra type classes only work for homogeneous relations, we only look at square matrices.
›

type_synonym ('a,'b) square = "'a × 'a ⇒ 'b"

text ‹
We use standard matrix operations.
The Stone algebra structure is lifted componentwise.
Composition is matrix multiplication using given composition and supremum operations.
Its unit lifts given zero and one elements into an identity matrix.
Converse is matrix transpose with an additional componentwise transpose.
›

definition less_eq_matrix :: "('a,'b::ord) square ⇒ ('a,'b) square ⇒ bool"                                           (infix "≼" 50)   where "f ≼ g = (∀e . f e ≤ g e)"
definition less_matrix    :: "('a,'b::ord) square ⇒ ('a,'b) square ⇒ bool"                                           (infix "≺" 50)   where "f ≺ g = (f ≼ g ∧ ¬ g ≼ f)"
definition sup_matrix     :: "('a,'b::sup) square ⇒ ('a,'b) square ⇒ ('a,'b) square"                                 (infixl "⊕" 65)  where "f ⊕ g = (λe . f e ⊔ g e)"
definition inf_matrix     :: "('a,'b::inf) square ⇒ ('a,'b) square ⇒ ('a,'b) square"                                 (infixl "⊗" 67)  where "f ⊗ g = (λe . f e ⊓ g e)"
definition minus_matrix   :: "('a,'b::{uminus,inf}) square ⇒ ('a,'b) square ⇒ ('a,'b) square"                        (infixl "⊖" 65)  where "f ⊖ g = (λe . f e ⊓ -g e)"
definition implies_matrix :: "('a,'b::implies) square ⇒ ('a,'b) square ⇒ ('a,'b) square"                             (infixl "⊘" 65)  where "f ⊘ g = (λe . f e ↝ g e)"
definition times_matrix   :: "('a,'b::{times,bounded_semilattice_sup_bot}) square ⇒ ('a,'b) square ⇒ ('a,'b) square" (infixl "⊙" 70)  where "f ⊙ g = (λ(i,j) . ⨆⇩k f (i,k) * g (k,j))"
definition uminus_matrix  :: "('a,'b::uminus) square ⇒ ('a,'b) square"                                                ("⊖ _"  80)  where "⊖f    = (λe . -f e)"
definition conv_matrix    :: "('a,'b::conv) square ⇒ ('a,'b) square"                                                  ("_⇧t"  100) where "f⇧t      = (λ(i,j) . (f (j,i))⇧T)"
definition bot_matrix     :: "('a,'b::bot) square"                                                                     ("mbot")         where "mbot   = (λe . bot)"
definition top_matrix     :: "('a,'b::top) square"                                                                     ("mtop")         where "mtop   = (λe . top)"
definition one_matrix     :: "('a,'b::{one,bot}) square"                                                               ("mone")         where "mone   = (λ(i,j) . if i = j then 1 else bot)"

subsection ‹Stone Algebras›

text ‹
We first lift the Stone algebra structure.
Because all operations are componentwise, this also works for infinite matrices.
›

interpretation matrix_order: order where less_eq = less_eq_matrix and less = "less_matrix :: ('a,'b::order) square ⇒ ('a,'b) square ⇒ bool"
apply unfold_locales
apply (simp add: less_matrix_def)
apply (simp add: less_eq_matrix_def)
apply (meson less_eq_matrix_def order_trans)
by (meson less_eq_matrix_def antisym ext)

interpretation matrix_semilattice_sup: semilattice_sup where sup = sup_matrix and less_eq = less_eq_matrix and less = "less_matrix :: ('a,'b::semilattice_sup) square ⇒ ('a,'b) square ⇒ bool"
apply unfold_locales
apply (simp add: sup_matrix_def less_eq_matrix_def)
apply (simp add: sup_matrix_def less_eq_matrix_def)
by (simp add: sup_matrix_def less_eq_matrix_def)

interpretation matrix_semilattice_inf: semilattice_inf where inf = inf_matrix and less_eq = less_eq_matrix and less = "less_matrix :: ('a,'b::semilattice_inf) square ⇒ ('a,'b) square ⇒ bool"
apply unfold_locales
apply (simp add: inf_matrix_def less_eq_matrix_def)
apply (simp add: inf_matrix_def less_eq_matrix_def)
by (simp add: inf_matrix_def less_eq_matrix_def)

interpretation matrix_bounded_semilattice_sup_bot: bounded_semilattice_sup_bot where sup = sup_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a,'b::bounded_semilattice_sup_bot) square"
apply unfold_locales
by (simp add: bot_matrix_def less_eq_matrix_def)

interpretation matrix_bounded_semilattice_inf_top: bounded_semilattice_inf_top where inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and top = "top_matrix :: ('a,'b::bounded_semilattice_inf_top) square"
apply unfold_locales
by (simp add: less_eq_matrix_def top_matrix_def)

interpretation matrix_lattice: lattice where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = "less_matrix :: ('a,'b::lattice) square ⇒ ('a,'b) square ⇒ bool" ..

interpretation matrix_distrib_lattice: distrib_lattice where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = "less_matrix :: ('a,'b::distrib_lattice) square ⇒ ('a,'b) square ⇒ bool"
apply unfold_locales
by (simp add: sup_inf_distrib1 sup_matrix_def inf_matrix_def)

interpretation matrix_bounded_lattice: bounded_lattice where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a,'b::bounded_lattice) square" and top = top_matrix ..

interpretation matrix_bounded_distrib_lattice: bounded_distrib_lattice where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a,'b::bounded_distrib_lattice) square" and top = top_matrix ..

interpretation matrix_p_algebra: p_algebra where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a,'b::p_algebra) square" and top = top_matrix and uminus = uminus_matrix
apply unfold_locales
apply (unfold inf_matrix_def bot_matrix_def less_eq_matrix_def uminus_matrix_def)
by (meson pseudo_complement)

interpretation matrix_pd_algebra: pd_algebra where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a,'b::pd_algebra) square" and top = top_matrix and uminus = uminus_matrix ..

text ‹
In particular, matrices over Stone algebras form a Stone algebra.
›

interpretation matrix_stone_algebra: stone_algebra where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a,'b::stone_algebra) square" and top = top_matrix and uminus = uminus_matrix
by unfold_locales (simp add: sup_matrix_def uminus_matrix_def top_matrix_def)

interpretation matrix_heyting_stone_algebra: heyting_stone_algebra where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a,'b::heyting_stone_algebra) square" and top = top_matrix and uminus = uminus_matrix and implies = implies_matrix
apply unfold_locales
apply (unfold inf_matrix_def sup_matrix_def bot_matrix_def top_matrix_def less_eq_matrix_def uminus_matrix_def implies_matrix_def)
apply (simp add: implies_galois)
apply (simp add: uminus_eq)
by simp

interpretation matrix_boolean_algebra: boolean_algebra where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a,'b::boolean_algebra) square" and top = top_matrix and uminus = uminus_matrix and minus = minus_matrix
apply unfold_locales
apply simp
apply (simp add: sup_matrix_def uminus_matrix_def top_matrix_def)
by (simp add: inf_matrix_def uminus_matrix_def minus_matrix_def)

subsection ‹Semirings›

text ‹
Next, we lift the semiring structure.
Because of composition, this requires a restriction to finite matrices.
›

interpretation matrix_monoid: monoid_mult where times = times_matrix and one = "one_matrix :: ('a::finite,'b::idempotent_semiring) square"
proof
fix f g h :: "('a,'b) square"
show "(f ⊙ g) ⊙ h = f ⊙ (g ⊙ h)"
proof (rule ext, rule prod_cases)
fix i j
have "((f ⊙ g) ⊙ h) (i,j) = (⨆⇩l (f ⊙ g) (i,l) * h (l,j))"
by (simp add: times_matrix_def)
also have "... = (⨆⇩l (⨆⇩k f (i,k) * g (k,l)) * h (l,j))"
by (simp add: times_matrix_def)
also have "... = (⨆⇩l ⨆⇩k (f (i,k) * g (k,l)) * h (l,j))"
by (metis (no_types) comp_right_dist_sum)
also have "... = (⨆⇩l ⨆⇩k f (i,k) * (g (k,l) * h (l,j)))"
by (simp add: mult.assoc)
also have "... = (⨆⇩k ⨆⇩l f (i,k) * (g (k,l) * h (l,j)))"
using sup_monoid.sum.swap by auto
also have "... = (⨆⇩k f (i,k) * (⨆⇩l g (k,l) * h (l,j)))"
by (metis (no_types) comp_left_dist_sum)
also have "... = (⨆⇩k f (i,k) * (g ⊙ h) (k,j))"
by (simp add: times_matrix_def)
also have "... = (f ⊙ (g ⊙ h)) (i,j)"
by (simp add: times_matrix_def)
finally show "((f ⊙ g) ⊙ h) (i,j) = (f ⊙ (g ⊙ h)) (i,j)"
.
qed
next
fix f :: "('a,'b) square"
show "mone ⊙ f = f"
proof (rule ext, rule prod_cases)
fix i j
have "(mone ⊙ f) (i,j) = (⨆⇩k mone (i,k) * f (k,j))"
by (simp add: times_matrix_def)
also have "... = (⨆⇩k (if i = k then 1 else bot) * f (k,j))"
by (simp add: one_matrix_def)
also have "... = (⨆⇩k if i = k then 1 * f (k,j) else bot * f (k,j))"
by (metis (full_types, opaque_lifting))
also have "... = (⨆⇩k if i = k then f (k,j) else bot)"
by (meson mult_left_one mult_left_zero)
also have "... = f (i,j)"
by simp
finally show "(mone ⊙ f) (i,j) = f (i,j)"
.
qed
next
fix f :: "('a,'b) square"
show "f ⊙ mone = f"
proof (rule ext, rule prod_cases)
fix i j
have "(f ⊙ mone) (i,j) = (⨆⇩k f (i,k) * mone (k,j))"
by (simp add: times_matrix_def)
also have "... = (⨆⇩k f (i,k) * (if k = j then 1 else bot))"
by (simp add: one_matrix_def)
also have "... = (⨆⇩k if k = j then f (i,k) * 1 else f (i,k) * bot)"
by (metis (full_types, opaque_lifting))
also have "... = (⨆⇩k if k = j then f (i,k) else bot)"
by (meson mult.right_neutral semiring.mult_zero_right)
also have "... = f (i,j)"
by simp
finally show "(f ⊙ mone) (i,j) = f (i,j)"
.
qed
qed

interpretation matrix_idempotent_semiring: idempotent_semiring where sup = sup_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a::finite,'b::idempotent_semiring) square" and one = one_matrix and times = times_matrix
proof
fix f g h :: "('a,'b) square"
show "f ⊙ g ⊕ f ⊙ h ≼ f ⊙ (g ⊕ h)"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
fix i j
have "(f ⊙ g ⊕ f ⊙ h) (i,j) = (f ⊙ g) (i,j) ⊔ (f ⊙ h) (i,j)"
by (simp add: sup_matrix_def)
also have "... = (⨆⇩k f (i,k) * g (k,j)) ⊔ (⨆⇩k f (i,k) * h (k,j))"
by (simp add: times_matrix_def)
also have "... = (⨆⇩k f (i,k) * g (k,j) ⊔ f (i,k) * h (k,j))"
by (simp add: sup_monoid.sum.distrib)
also have "... = (⨆⇩k f (i,k) * (g (k,j) ⊔ h (k,j)))"
by (simp add: mult_left_dist_sup)
also have "... = (⨆⇩k f (i,k) * (g ⊕ h) (k,j))"
by (simp add: sup_matrix_def)
also have "... = (f ⊙ (g ⊕ h)) (i,j)"
by (simp add: times_matrix_def)
finally show "(f ⊙ g ⊕ f ⊙ h) (i,j) ≤ (f ⊙ (g ⊕ h)) (i,j)"
by simp
qed
next
fix f g h :: "('a,'b) square"
show "(f ⊕ g) ⊙ h = f ⊙ h ⊕ g ⊙ h"
proof (rule ext, rule prod_cases)
fix i j
have "((f ⊕ g) ⊙ h) (i,j) = (⨆⇩k (f ⊕ g) (i,k) * h (k,j))"
by (simp add: times_matrix_def)
also have "... = (⨆⇩k (f (i,k) ⊔ g (i,k)) * h (k,j))"
by (simp add: sup_matrix_def)
also have "... = (⨆⇩k f (i,k) * h (k,j) ⊔ g (i,k) * h (k,j))"
by (meson mult_right_dist_sup)
also have "... = (⨆⇩k f (i,k) * h (k,j)) ⊔ (⨆⇩k g (i,k) * h (k,j))"
by (simp add: sup_monoid.sum.distrib)
also have "... = (f ⊙ h) (i,j) ⊔ (g ⊙ h) (i,j)"
by (simp add: times_matrix_def)
also have "... = (f ⊙ h ⊕ g ⊙ h) (i,j)"
by (simp add: sup_matrix_def)
finally show "((f ⊕ g) ⊙ h) (i,j) = (f ⊙ h ⊕ g ⊙ h) (i,j)"
.
qed
next
fix f :: "('a,'b) square"
show "mbot ⊙ f = mbot"
proof (rule ext, rule prod_cases)
fix i j
have "(mbot ⊙ f) (i,j) = (⨆⇩k mbot (i,k) * f (k,j))"
by (simp add: times_matrix_def)
also have "... = (⨆⇩k bot * f (k,j))"
by (simp add: bot_matrix_def)
also have "... = bot"
by simp
also have "... = mbot (i,j)"
by (simp add: bot_matrix_def)
finally show "(mbot ⊙ f) (i,j) = mbot (i,j)"
.
qed
next
fix f :: "('a,'b) square"
show "mone ⊙ f = f"
by simp
next
fix f :: "('a,'b) square"
show "f ≼ f ⊙ mone"
by simp
next
fix f g h :: "('a,'b) square"
show "f ⊙ (g ⊕ h) = f ⊙ g ⊕ f ⊙ h"
proof (rule ext, rule prod_cases)
fix i j
have "(f ⊙ (g ⊕ h)) (i,j) = (⨆⇩k f (i,k) * (g ⊕ h) (k,j))"
by (simp add: times_matrix_def)
also have "... = (⨆⇩k f (i,k) * (g (k,j) ⊔ h (k,j)))"
by (simp add: sup_matrix_def)
also have "... = (⨆⇩k f (i,k) * g (k,j) ⊔ f (i,k) * h (k,j))"
by (meson mult_left_dist_sup)
also have "... = (⨆⇩k f (i,k) * g (k,j)) ⊔ (⨆⇩k f (i,k) * h (k,j))"
by (simp add: sup_monoid.sum.distrib)
also have "... = (f ⊙ g) (i,j) ⊔ (f ⊙ h) (i,j)"
by (simp add: times_matrix_def)
also have "... = (f ⊙ g ⊕ f ⊙ h) (i,j)"
by (simp add: sup_matrix_def)
finally show "(f ⊙ (g ⊕ h)) (i,j) = (f ⊙ g ⊕ f ⊙ h) (i,j)"
.
qed
next
fix f :: "('a,'b) square"
show "f ⊙ mbot = mbot"
proof (rule ext, rule prod_cases)
fix i j
have "(f ⊙ mbot) (i,j) = (⨆⇩k f (i,k) * mbot (k,j))"
by (simp add: times_matrix_def)
also have "... = (⨆⇩k f (i,k) * bot)"
by (simp add: bot_matrix_def)
also have "... = bot"
by simp
also have "... = mbot (i,j)"
by (simp add: bot_matrix_def)
finally show "(f ⊙ mbot) (i,j) = mbot (i,j)"
.
qed
qed

interpretation matrix_bounded_idempotent_semiring: bounded_idempotent_semiring where sup = sup_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a::finite,'b::bounded_idempotent_semiring) square" and top = top_matrix and one = one_matrix and times = times_matrix
proof
fix f :: "('a,'b) square"
show "f ⊕ mtop = mtop"
proof
fix e
have "(f ⊕ mtop) e = f e ⊔ mtop e"
by (simp add: sup_matrix_def)
also have "... = f e ⊔ top"
by (simp add: top_matrix_def)
also have "... = top"
by simp
also have "... = mtop e"
by (simp add: top_matrix_def)
finally show "(f ⊕ mtop) e = mtop e"
.
qed
qed

subsection ‹Stone Relation Algebras›

text ‹
Finally, we show that matrices over Stone relation algebras form a Stone relation algebra.
›

interpretation matrix_stone_relation_algebra: stone_relation_algebra where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix :: ('a::finite,'b::stone_relation_algebra) square" and top = top_matrix and uminus = uminus_matrix and one = one_matrix and times = times_matrix and conv = conv_matrix
proof
fix f g h :: "('a,'b) square"
show "(f ⊙ g) ⊙ h = f ⊙ (g ⊙ h)"
by (simp add: matrix_monoid.mult_assoc)
next
fix f g h :: "('a,'b) square"
show "(f ⊕ g) ⊙ h = f ⊙ h ⊕ g ⊙ h"
by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
next
fix f :: "('a,'b) square"
show "mbot ⊙ f = mbot"
by simp
next
fix f :: "('a,'b) square"
show "mone ⊙ f = f"
by simp
next
fix f :: "('a,'b) square"
show "f⇧t⇧t = f"
proof (rule ext, rule prod_cases)
fix i j
have "(f⇧t⇧t) (i,j) = ((f⇧t) (j,i))⇧T"
by (simp add: conv_matrix_def)
also have "... = f (i,j)"
by (simp add: conv_matrix_def)
finally show "(f⇧t⇧t) (i,j) = f (i,j)"
.
qed
next
fix f g :: "('a,'b) square"
show "(f ⊕ g)⇧t = f⇧t ⊕ g⇧t"
proof (rule ext, rule prod_cases)
fix i j
have "((f ⊕ g)⇧t) (i,j) = ((f ⊕ g) (j,i))⇧T"
by (simp add: conv_matrix_def)
also have "... = (f (j,i) ⊔ g (j,i))⇧T"
by (simp add: sup_matrix_def)
also have "... = (f⇧t) (i,j) ⊔ (g⇧t) (i,j)"
by (simp add: conv_matrix_def conv_dist_sup)
also have "... = (f⇧t ⊕ g⇧t) (i,j)"
by (simp add: sup_matrix_def)
finally show "((f ⊕ g)⇧t) (i,j) = (f⇧t ⊕ g⇧t) (i,j)"
.
qed
next
fix f g :: "('a,'b) square"
show "(f ⊙ g)⇧t = g⇧t ⊙ f⇧t"
proof (rule ext, rule prod_cases)
fix i j
have "((f ⊙ g)⇧t) (i,j) = ((f ⊙ g) (j,i))⇧T"
by (simp add: conv_matrix_def)
also have "... = (⨆⇩k f (j,k) * g (k,i))⇧T"
by (simp add: times_matrix_def)
also have "... = (⨆⇩k (f (j,k) * g (k,i))⇧T)"
by (metis (no_types) conv_dist_sum)
also have "... = (⨆⇩k (g (k,i))⇧T * (f (j,k))⇧T)"
by (simp add: conv_dist_comp)
also have ```