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" and "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)
syntax_consts
  "_sum_sup_monoid" "_sum_sup_monoid_bounded" ⇌ sup_monoid.sum
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

lemma sum_const:
  "(⨆⇩k::'b::finite f) = f"
  by (metis lub_sum sup.cobounded1 sup_monoid.add_0_right sup_same_context ub_sum)

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] 80)  where "⊖f    = (λe . -f e)"
definition conv_matrix    :: "('a,'b::conv) square ⇒ ('a,'b) square"                                                  (‹_t› [100] 100) where "ft      = (λ(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 "ftt = f"
  proof (rule ext, rule prod_cases)
    fix i j
    have "(ftt) (i,j) = ((ft) (j,i))T"
      by (simp add: conv_matrix_def)
    also have "... = f (i,j)"
      by (simp add: conv_matrix_def)
    finally show "(ftt) (i,j) = f (i,j)"
      .
  qed
next
  fix f g :: "('a,'b) square"
  show "(f ⊕ g)t = ft ⊕ gt"
  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 "... = (ft) (i,j) ⊔ (gt) (i,j)"
      by (simp add: conv_matrix_def conv_dist_sup)
    also have "... = (ft ⊕ gt) (i,j)"
      by (simp add: sup_matrix_def)
    finally show "((f ⊕ g)t) (i,j) = (ft ⊕ gt) (i,j)"
      .
  qed
next
  fix f g :: "('a,'b) square"
  show "(f ⊙ g)t = gt ⊙ ft"
  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 "... = (⨆⇩k (gt) (i,k) * (ft) (k,j))"
      by (simp add: conv_matrix_def)
    also have "... = (gt ⊙ ft) (i,j)"
      by (simp add: times_matrix_def)
    finally show "((f ⊙ g)t) (i,j) = (gt ⊙ ft) (i,j)"
      .
  qed
next
  fix f g h :: "('a,'b) square"
  show "(f ⊙ g) ⊗ h ≼ f ⊙ (g ⊗ (ft ⊙ h))"
  proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
    fix i j
    have "((f ⊙ g) ⊗ h) (i,j) = (f ⊙ g) (i,j) ⊓ h (i,j)"
      by (simp add: inf_matrix_def)
    also have "... = (⨆⇩k f (i,k) * g (k,j)) ⊓ h (i,j)"
      by (simp add: times_matrix_def)
    also have "... = (⨆⇩k f (i,k) * g (k,j) ⊓ h (i,j))"
      by (metis (no_types) inf_right_dist_sum)
    also have "... ≤ (⨆⇩k f (i,k) * (g (k,j) ⊓ (f (i,k))T * h (i,j)))"
      by (rule leq_sum, meson dedekind_1)
    also have "... = (⨆⇩k f (i,k) * (g (k,j) ⊓ (ft) (k,i) * h (i,j)))"
      by (simp add: conv_matrix_def)
    also have "... ≤ (⨆⇩k f (i,k) * (g (k,j) ⊓ (⨆⇩l (ft) (k,l) * h (l,j))))"
      by (rule leq_sum, rule allI, rule comp_right_isotone, rule inf.sup_right_isotone, rule ub_sum)
    also have "... = (⨆⇩k f (i,k) * (g (k,j) ⊓ (ft ⊙ h) (k,j)))"
      by (simp add: times_matrix_def)
    also have "... = (⨆⇩k f (i,k) * (g ⊗ (ft ⊙ h)) (k,j))"
      by (simp add: inf_matrix_def)
    also have "... = (f ⊙ (g ⊗ (ft ⊙ h))) (i,j)"
      by (simp add: times_matrix_def)
    finally show "((f ⊙ g) ⊗ h) (i,j) ≤ (f ⊙ (g ⊗ (ft ⊙ h))) (i,j)"
      .
  qed
next
  fix f g :: "('a,'b) square"
  show "⊖⊖(f ⊙ g) = ⊖⊖f ⊙ ⊖⊖g"
  proof (rule ext, rule prod_cases)
    fix i j
    have "(⊖⊖(f ⊙ g)) (i,j) = --((f ⊙ g) (i,j))"
      by (simp add: uminus_matrix_def)
    also have "... = --(⨆⇩k f (i,k) * g (k,j))"
      by (simp add: times_matrix_def)
    also have "... = (⨆⇩k --(f (i,k) * g (k,j)))"
      by (metis (no_types) pp_dist_sum)
    also have "... = (⨆⇩k --(f (i,k)) * --(g (k,j)))"
      by (meson pp_dist_comp)
    also have "... = (⨆⇩k (⊖⊖f) (i,k) * (⊖⊖g) (k,j))"
      by (simp add: uminus_matrix_def)
    also have "... = (⊖⊖f ⊙ ⊖⊖g) (i,j)"
      by (simp add: times_matrix_def)
    finally show "(⊖⊖(f ⊙ g)) (i,j) = (⊖⊖f ⊙ ⊖⊖g) (i,j)"
      .
  qed
next
  let ?o = "mone :: ('a,'b) square"
  show "⊖⊖?o = ?o"
  proof (rule ext, rule prod_cases)
    fix i j
    have "(⊖⊖?o) (i,j) = --(?o (i,j))"
      by (simp add: uminus_matrix_def)
    also have "... = --(if i = j then 1 else bot)"
      by (simp add: one_matrix_def)
    also have "... = (if i = j then --1 else --bot)"
      by simp
    also have "... = (if i = j then 1 else bot)"
      by auto
    also have "... = ?o (i,j)"
      by (simp add: one_matrix_def)
    finally show "(⊖⊖?o) (i,j) = ?o (i,j)"
      .
  qed
qed

interpretation matrix_stone_relation_algebra_consistent: stone_relation_algebra_consistent 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_consistent) square" and top = top_matrix and uminus = uminus_matrix and one = one_matrix and times = times_matrix and conv = conv_matrix
proof
  show "(mbot::('a,'b) square) ≠ mtop"
    by (metis consistent bot_matrix_def top_matrix_def)
qed

interpretation matrix_stone_relation_algebra_tarski: stone_relation_algebra_tarski 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_tarski) square" and top = top_matrix and uminus = uminus_matrix and one = one_matrix and times = times_matrix and conv = conv_matrix
proof
  fix x :: "('a,'b) square"
  assume 1: "matrix_p_algebra.regular x"
  assume "x ≠ mbot"
  from this obtain i j where "x (i,j) ≠ bot"
    by (metis bot_matrix_def ext surj_pair)
  hence 2: "top * x (i,j) * top = top"
    using 1 by (metis tarski uminus_matrix_def)
  show "matrix_bounded_idempotent_semiring.total (mtop ⊙ x)"
  proof (rule ext, rule prod_cases)
    fix k l
    have "top * x (i,j) * top ≤ (⨆⇩m top * x (m,j)) * top"
      using comp_inf.ub_sum comp_isotone by fastforce
    also have "... = (mtop ⊙ x) (k,j) * top"
      by (simp add: times_matrix_def top_matrix_def)
    also have "... ≤ (⨆⇩m (mtop ⊙ x) (k,m) * top)"
      using comp_inf.ub_sum by force
    also have "... = (mtop ⊙ x ⊙ mtop) (k,l)"
      by (simp add: times_matrix_def top_matrix_def)
    finally show "(mtop ⊙ x ⊙ mtop) (k,l) = mtop (k,l)"
      using 2 by (simp add: top_matrix_def inf.bot_unique)
  qed
qed

interpretation matrix_stone_relation_algebra_tarski_consistent: stone_relation_algebra_tarski_consistent 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_tarski_consistent) square" and top = top_matrix and uminus = uminus_matrix and one = one_matrix and times = times_matrix and conv = conv_matrix
  ..

end