Theory Linear_Order_Matrices

(* Title:      Matrices over Bounded Linear Orders
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Matrices over Bounded Linear Orders›

text ‹
In this theory we characterise relation-algebraic properties of matrices over bounded linear orders (for example, extended real numbers) in terms of the entries in the matrices.
We consider, in particular, the following properties: univalent, injective, total, surjective, mapping, bijective, vector, covector, point, arc, reflexive, coreflexive, irreflexive, symmetric, antisymmetric, asymmetric.
We also consider the effect of composition with the matrix of greatest elements and with coreflexives (tests).
›

theory Linear_Order_Matrices

imports Matrix_Relation_Algebras

begin

class non_trivial_linorder_stone_relation_algebra_expansion = linorder_stone_relation_algebra_expansion + non_trivial
begin

subclass non_trivial_bounded_order ..

end

text ‹
Before we look at matrices, we generalise selectivity to finite suprema.
›

lemma linorder_finite_sup_selective:
  fixes f :: "'a::finite  'b::linorder_stone_algebra_expansion"
  shows "i . (⨆⇩k f k) = f i"
  apply (induct rule: comp_inf.one_sup_induct)
  apply blast
  using sup_selective by fastforce

lemma linorder_top_finite_sup:
  fixes f :: "'a::finite  'b::linorder_stone_algebra_expansion"
  assumes "k . f k  top"
    shows "(⨆⇩k f k)  top"
  by (metis assms linorder_finite_sup_selective)

text ‹
The following results show the effect of composition with the top› matrix from the left and from the right.
›

lemma comp_top_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "(f  mtop) (i,j) = (⨆⇩k f (i,k))"
  apply (unfold times_matrix_def top_matrix_def)
  by (metis (no_types, lifting) case_prod_conv comp_right_one one_def sup_monoid.sum.cong)

lemma top_comp_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "(mtop  f) (i,j) = (⨆⇩k f (k,j))"
  apply (unfold times_matrix_def top_matrix_def)
  by (metis (no_types, lifting) case_prod_conv comp_left_one one_def sup_monoid.sum.cong)

text ‹
We characterise univalent matrices: in each row, at most one entry may be different from bot›.
›

lemma univalent_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.univalent f"
      and "f (i,j)  bot"
      and "f (i,k)  bot"
    shows "j = k"
proof -
  have "(ft  f) (j,k) = (⨆⇩l (ft) (j,l) * f (l,k))"
    by (simp add: times_matrix_def)
  also have "... = (⨆⇩l (f (l,j))T * f (l,k))"
    by (simp add: conv_matrix_def)
  also have "... = (⨆⇩l f (l,j) * f (l,k))"
    by simp
  also have "...  f (i,j) * f (i,k)"
    using comp_inf.ub_sum by fastforce
  finally have "(ft  f) (j,k)  bot"
    using assms(2,3) bot.extremum_uniqueI times_dense by fastforce
  hence "mone (j,k)  (bot::'b)"
    by (metis assms(1) bot.extremum_uniqueI less_eq_matrix_def)
  thus ?thesis
    by (metis (mono_tags, lifting) case_prod_conv one_matrix_def)
qed

lemma univalent_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "i j k . f (i,j)  bot  f (i,k)  bot  j = k"
    shows "matrix_stone_relation_algebra.univalent f"
proof -
  show "ft  f  mone"
  proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
    fix j k
    show "(ft  f) (j,k)  mone (j,k)"
    proof (cases "j = k")
      assume "j = k"
      thus ?thesis
        by (simp add: one_matrix_def)
    next
      assume "j  k"
      hence "(⨆⇩i f (i,j) * f (i,k)) = bot"
        by (metis (no_types, lifting) assms semiring.mult_not_zero sup_monoid.sum.neutral)
      thus ?thesis
        by (simp add: times_matrix_def conv_matrix_def)
    qed
  qed
qed

lemma univalent_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.univalent f  (i j k . f (i,j)  bot  f (i,k)  bot  j = k)"
  using univalent_linorder_matrix_1 univalent_linorder_matrix_2 by auto

text ‹
Injective matrices can then be characterised by applying converse: in each column, at most one entry may be different from bot›.
›

lemma injective_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.injective f  (i j k . f (j,i)  bot  f (k,i)  bot  j = k)"
  by (unfold matrix_stone_relation_algebra.injective_conv_univalent univalent_linorder_matrix) (simp add: conv_matrix_def)

text ‹
Next come total matrices: each row has a top› entry.
›

lemma total_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.total_var f"
    shows "j . f (i,j) = top"
proof -
  have "mone (i,i)  (f  ft) (i,i)"
    using assms less_eq_matrix_def by blast
  hence "top = (f  ft) (i,i)"
    by (simp add: one_matrix_def top.extremum_unique)
  also have "... = (⨆⇩j f (i,j) * (ft) (j,i))"
    by (simp add: times_matrix_def)
  also have "... = (⨆⇩j f (i,j) * f (i,j))"
    by (simp add: conv_matrix_def)
  also have "... = (⨆⇩j f (i,j))"
    by simp
  finally show ?thesis
    by (metis linorder_top_finite_sup)
qed

lemma total_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "i . j . f (i,j) = top"
    shows "matrix_stone_relation_algebra.total_var f"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
  fix j k
  show "mone (j,k)  (f  ft) (j,k)"
  proof (cases "j = k")
    assume "j = k"
    hence "(⨆⇩i f (j,i) * (ft) (i,k)) = (⨆⇩i f (j,i))"
      by (simp add: conv_matrix_def)
    also have "... = top"
      by (metis (no_types) assms comp_inf.ub_sum sup.absorb2 sup_top_left)
    finally show ?thesis
      by (simp add: times_matrix_def)
  next
    assume "j  k"
    thus ?thesis
      by (simp add: one_matrix_def)
  qed
qed

lemma total_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.total f  (i . j . f (i,j) = top)"
  using total_linorder_matrix_1 total_linorder_matrix_2 matrix_stone_relation_algebra.total_var by auto

text ‹
Surjective matrices are again characterised by applying converse: each column has a top› entry.
›

lemma surjective_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.surjective f  (j . i . f (i,j) = top)"
  by (unfold matrix_stone_relation_algebra.surjective_conv_total total_linorder_matrix) (simp add: conv_matrix_def)

text ‹
A mapping therefore means that each row has exactly one top› entry and all others are bot›.
›

lemma mapping_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.mapping f  (i . j . f (i,j) = top  (k . j  k  f (i,k) = bot))"
  by (unfold total_linorder_matrix univalent_linorder_matrix) (metis (mono_tags, opaque_lifting) comp_inf.mult_1_right comp_inf.mult_right_zero)

lemma mapping_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.mapping f  (i . ∃!j . f (i,j) = top  (k . j  k  f (i,k) = bot))"
  apply (unfold mapping_linorder_matrix)
  using bot_not_top by auto

text ‹
Conversely, bijective means that each column has exactly one top› entry and all others are bot›.
›

lemma bijective_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.bijective f  (j . i . f (i,j) = top  (k . i  k  f (k,j) = bot))"
  by (unfold matrix_stone_relation_algebra.bijective_conv_mapping mapping_linorder_matrix) (simp add: conv_matrix_def)

lemma bijective_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.bijective f  (j . ∃!i . f (i,j) = top  (k . i  k  f (k,j) = bot))"
  by (unfold matrix_stone_relation_algebra.bijective_conv_mapping mapping_linorder_matrix_unique) (simp add: conv_matrix_def)

text ‹
We derive algebraic characterisations of matrices in which each row has an entry that is different from bot›.
›

lemma pp_total_linorder_matrix_1:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  assumes "(f  mtop) = mbot"
    shows "j . f (i,j)  bot"
proof -
  have "¬(j . f (i,j)  bot)  (f  mtop)  mbot"
  proof -
    assume "¬(j . f (i,j)  bot)"
    hence "top = -(f  mtop) (i,i)"
      by (simp add: comp_top_linorder_matrix linorder_finite_sup_selective)
    also have "... = ((f  mtop)) (i,i)"
      by (simp add: uminus_matrix_def)
    finally show "(f  mtop)  mbot"
      by (metis bot_matrix_def bot_not_top)
  qed
  thus ?thesis
    using assms by blast
qed

lemma pp_total_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "i . j . f (i,j)  bot"
    shows "(f  mtop) = mbot"
proof (rule ext, rule prod_cases)
  fix i j
  have "((f  mtop)) (i,j) = -(⨆⇩k f (i,k))"
    by (simp add: comp_top_linorder_matrix uminus_matrix_def)
  also have "... = bot"
    by (metis antisym assms bot.extremum comp_inf.ub_sum uminus_def)
  finally show "((f  mtop)) (i,j) = mbot (i,j)"
    by (simp add: bot_matrix_def)
qed

lemma pp_total_linorder_matrix_3:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "(f  mtop) = mbot  (i . j . f (i,j)  bot)"
  using pp_total_linorder_matrix_1 pp_total_linorder_matrix_2 by auto

lemma pp_total_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.total (f)  (i . j . f (i,j)  bot)"
  using matrix_stone_relation_algebra.pp_total pp_total_linorder_matrix_1 pp_total_linorder_matrix_2 by auto

lemma pp_mapping_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_mapping f  (i . j . f (i,j)  bot  (k . j  k  f (i,k) = bot))"
  by (metis (mono_tags, opaque_lifting) pp_total_linorder_matrix univalent_linorder_matrix_1 univalent_linorder_matrix_2)

lemma pp_mapping_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_mapping f  (i . ∃!j . f (i,j)  bot  (k . j  k  f (i,k) = bot))"
  apply (rule iffI)
  using pp_mapping_linorder_matrix apply blast
  by (metis pp_total_linorder_matrix univalent_linorder_matrix)

text ‹
Next follow matrices in which each column has an entry that is different from bot›.
›

lemma pp_surjective_linorder_matrix_1:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "(mtop  f) = mbot  (j . i . f (i,j)  bot)"
proof -
  have "(mtop  f) = mbot  ((mtop  f))t = mbott"
    by (metis matrix_stone_relation_algebra.conv_involutive)
  also have "...  (ft  mtop) = mbot"
    by (simp add: matrix_stone_relation_algebra.conv_complement matrix_stone_relation_algebra.conv_dist_comp)
  also have "...  (i . j . (ft) (i,j)  bot)"
    using pp_total_linorder_matrix_3 by auto
  also have "...  (j . i . f (i,j)  bot)"
    by (simp add: conv_matrix_def)
  finally show ?thesis
    .
qed

lemma pp_surjective_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.surjective (f)  (j . i . f (i,j)  bot)"
  using matrix_stone_relation_algebra.pp_surjective pp_surjective_linorder_matrix_1 by auto

lemma pp_bijective_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_bijective f  (j . i . f (i,j)  bot  (k . i  k  f (k,j) = bot))"
  by (unfold matrix_stone_relation_algebra.pp_bijective_conv_mapping pp_mapping_linorder_matrix) (simp add: conv_matrix_def)

lemma pp_bijective_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_bijective f  (j . ∃!i . f (i,j)  bot  (k . i  k  f (k,j) = bot))"
  by (unfold matrix_stone_relation_algebra.pp_bijective_conv_mapping pp_mapping_linorder_matrix_unique) (simp add: conv_matrix_def)

text ‹
The regular matrices are those which contain only bot› or top› entries.
›

lemma regular_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_p_algebra.regular f  (e . f e = bot  f e = top)"
proof -
  have "matrix_p_algebra.regular f  (f = f)"
    by auto
  also have "...  (e . --f e = f e)"
    by (metis uminus_matrix_def ext)
  also have "...  (e . f e = bot  f e = top)"
    by force
  finally show ?thesis
    .
qed

text ‹
Vectors are precisely the row-constant matrices.
›

lemma vector_linorder_matrix_0:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_bounded_idempotent_semiring.vector f"
    shows "f (i,j) = (⨆⇩k f (i,k))"
  by (metis assms comp_top_linorder_matrix)

lemma vector_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_bounded_idempotent_semiring.vector f"
    shows "f (i,j) = f (i,k)"
  by (metis assms vector_linorder_matrix_0)

lemma vector_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "i j k . f (i,j) = f (i,k)"
    shows "matrix_bounded_idempotent_semiring.vector f"
proof (rule ext, rule prod_cases)
  fix i j
  have "(f  mtop) (i,j) = (⨆⇩k f (i,k))"
    by (simp add: comp_top_linorder_matrix)
  also have "... = f (i,j)"
    by (metis assms linorder_finite_sup_selective)
  finally show "(f  mtop) (i,j) = f (i,j)"
    .
qed

lemma vector_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.vector f  (i j k . f (i,j) = f (i,k))"
  using vector_linorder_matrix_1 vector_linorder_matrix_2 by auto

text ‹
Hence covectors are precisely the column-constant matrices.
›

lemma covector_linorder_matrix_0:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_bounded_idempotent_semiring.covector f"
    shows "f (i,j) = (⨆⇩k f (k,j))"
  by (metis assms top_comp_linorder_matrix)

lemma covector_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.covector f  (i j k . f (i,j) = f (k,j))"
  by (unfold matrix_stone_relation_algebra.covector_conv_vector vector_linorder_matrix) (metis (no_types, lifting) case_prod_conv conv_matrix_def conv_def)

text ‹
A point is a matrix that has exactly one row, which is constant top›, and all other rows are constant bot›.
›

lemma point_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.point f  (i . j . f (i,j) = top  (k . i  k  f (k,j) = bot))"
  apply (unfold vector_linorder_matrix bijective_linorder_matrix)
  apply (rule iffI)
  apply metis
  by metis

lemma point_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.point f  (∃!i . j . f (i,j) = top  (k . i  k  f (k,j) = bot))"
  apply (unfold vector_linorder_matrix bijective_linorder_matrix)
  apply (rule iffI)
  apply (metis bot_not_top)
  by metis

lemma pp_point_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_point f  (i . j . f (i,j)  bot  (k . f (i,j) = f (i,k))  (k . i  k  f (k,j) = bot))"
  apply (unfold vector_linorder_matrix pp_bijective_linorder_matrix)
  apply (rule iffI)
  apply metis
  by metis

lemma pp_point_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_point f  (∃!i . j . f (i,j)  bot  (k . f (i,j) = f (i,k))  (k . i  k  f (k,j) = bot))"
  apply (unfold vector_linorder_matrix pp_bijective_linorder_matrix)
  apply (rule iffI)
  apply metis
  by metis

text ‹
An arc is a matrix that has exactly one top› entry and all other entries are bot›.
›

lemma arc_linorder_matrix_1:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.arc f"
    shows "e . f e = top  (d . e  d  f d = bot)"
proof -
  have "matrix_stone_relation_algebra.point (f  mtop)"
    by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
  from this obtain i where 1: "j . (f  mtop) (i,j) = top  (k . i  k  (f  mtop) (k,j) = bot)"
    using point_linorder_matrix by blast
  have "matrix_stone_relation_algebra.point (ft  mtop)"
    by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
  from this obtain j where "i . (ft  mtop) (j,i) = top  (k . j  k  (ft  mtop) (k,i) = bot)"
    using point_linorder_matrix by blast
  hence 2: "i . (mtop  f) (i,j) = top  (k . j  k  (mtop  f) (i,k) = bot)"
    by (metis (no_types) old.prod.case conv_matrix_def conv_def matrix_stone_relation_algebra.conv_dist_comp matrix_stone_relation_algebra.conv_top)
  have 3: "i k . j  k  f (i,k) = bot"
  proof (intro allI, rule impI)
    fix i k
    assume "j  k"
    hence "(⨆⇩l f (l,k)) = bot"
      using 2 by (simp add: top_comp_linorder_matrix)
    thus "f (i,k) = bot"
      by (metis bot.extremum_uniqueI comp_inf.ub_sum)
  qed
  have "(⨆⇩k f (i,k)) = top"
    using 1 by (simp add: comp_top_linorder_matrix)
  hence 4: "f (i,j) = top"
    using 3 by (metis bot_not_top linorder_finite_sup_selective)
  have "k l . k  i  l  j  f (k,l) = bot"
  proof (intro allI, unfold imp_disjL, rule conjI)
    fix k l
    show "k  i  f (k,l) = bot"
    proof
      assume "k  i"
      hence "(⨆⇩m f (k,m)) = bot"
        using 1 by (simp add: comp_top_linorder_matrix)
      thus "f (k,l) = bot"
        by (metis bot.extremum_uniqueI comp_inf.ub_sum)
    qed
    show "l  j  f (k,l) = bot"
      using 3 by simp
  qed
  thus ?thesis using 4
    by (metis old.prod.exhaust)
qed

lemma pp_arc_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "e . f e  bot  (d . e  d  f d = bot)"
    shows "matrix_stone_relation_algebra.pp_arc f"
proof (unfold matrix_stone_relation_algebra.pp_arc_expanded, intro conjI)
  show "f  mtop  ft  mone"
  proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
    fix i j
    show "(f  mtop  ft) (i,j)  mone (i,j)"
    proof (cases "i = j")
      assume "i = j"
      thus ?thesis
        by (simp add: one_matrix_def)
    next
      assume "i  j"
      hence 1: "k l . f (i,k) * f (j,l) = bot"
        by (metis assms Pair_inject semiring.mult_not_zero)
      have "(f  mtop  ft) (i,j) = (⨆⇩l (f  mtop) (i,l) * (ft) (l,j))"
        by (simp add: times_matrix_def)
      also have "... = (⨆⇩l (f  mtop) (i,l) * f (j,l))"
        by (simp add: conv_matrix_def)
      also have "... = (⨆⇩l (⨆⇩k f (i,k)) * f (j,l))"
        by (simp add: comp_top_linorder_matrix)
      also have "... = (⨆⇩l ⨆⇩k f (i,k) * f (j,l))"
        by (metis comp_right_dist_sum)
      also have "... = bot"
        using 1 linorder_finite_sup_selective by simp
      finally show ?thesis
        by simp
    qed
  qed
next
  show "ft  mtop  f  mone"
  proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
    fix i j
    show "(ft  mtop  f) (i,j)  mone (i,j)"
    proof (cases "i = j")
      assume "i = j"
      thus ?thesis
        by (simp add: one_matrix_def)
    next
      assume "i  j"
      hence 2: "k l . f (k,i) * f (l,j) = bot"
        by (metis assms Pair_inject semiring.mult_not_zero)
      have "(ft  mtop  f) (i,j) = (⨆⇩l (ft  mtop) (i,l) * f (l,j))"
        by (simp add: times_matrix_def)
      also have "... = (⨆⇩l (⨆⇩k (ft) (i,k)) * f (l,j))"
        by (simp add: comp_top_linorder_matrix)
      also have "... = (⨆⇩l (⨆⇩k f (k,i)) * f (l,j))"
        by (simp add: conv_matrix_def)
      also have "... = (⨆⇩l ⨆⇩k f (k,i) * f (l,j))"
        by (metis comp_right_dist_sum)
      also have "... = bot"
        using 2 linorder_finite_sup_selective by simp
      finally show ?thesis
        by simp
    qed
  qed
next
  show "mtop  f  mtop = mtop"
  proof (rule ext, rule prod_cases)
    fix i j
    from assms obtain k l where "f (k,l)  bot"
      using prod.collapse by auto
    hence "top = --f (k,l)"
      by simp
    also have "...  (⨆⇩k --f (k,l))"
      using comp_inf.ub_sum by metis
    also have "...  (⨆⇩l ⨆⇩k --f (k,l))"
      using comp_inf.ub_sum by simp
    finally have 3: "top  (⨆⇩l ⨆⇩k --f (k,l))"
      by simp
    have "(mtop  f  mtop) (i,j) = (⨆⇩l (⨆⇩k top * --f (k,l)) * top)"
      by (simp add: times_matrix_def top_matrix_def uminus_matrix_def)
    also have "... = (⨆⇩l ⨆⇩k --f (k,l))"
      by (metis (no_types, lifting) sup_monoid.sum.cong comp_inf.mult_1_left times_inf comp_inf.mult_1_right)
    also have "... = top"
      using 3 top.extremum_unique by blast
    finally show "(mtop  f  mtop) (i,j) = mtop (i,j)"
      by (simp add: top_matrix_def)
  qed
qed

lemma arc_linorder_matrix_2:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  assumes "e . f e = top  (d . e  d  f d = bot)"
    shows "matrix_stone_relation_algebra.arc f"
proof (unfold matrix_stone_relation_algebra.arc_expanded, intro conjI)
  show "f  mtop  ft  mone"
    by (metis (no_types, lifting) assms bot_not_top matrix_stone_relation_algebra.pp_arc_expanded pp_arc_linorder_matrix_2)
next
  show "ft  mtop  f  mone"
    by (metis (no_types, lifting) assms bot_not_top matrix_stone_relation_algebra.pp_arc_expanded pp_arc_linorder_matrix_2)
next
  show "mtop  f  mtop = mtop"
  proof (rule ext, rule prod_cases)
    fix i j
    from assms obtain k l where "f (k,l) = top"
      using prod.collapse by auto
    hence "(⨆⇩k f (k,l)) = top"
      by (metis (mono_tags) comp_inf.ub_sum top_unique)
    hence 3: "top  (⨆⇩l ⨆⇩k f (k,l))"
      by (metis (no_types) comp_inf.ub_sum)
    have "(mtop  f  mtop) (i,j) = (⨆⇩l (⨆⇩k top * f (k,l)) * top)"
      by (simp add: times_matrix_def top_matrix_def)
    also have "... = (⨆⇩l ⨆⇩k f (k,l))"
      by (metis (no_types, lifting) sup_monoid.sum.cong comp_inf.mult_1_left times_inf comp_inf.mult_1_right)
    also have "... = top"
      using 3 top.extremum_unique by blast
    finally show "(mtop  f  mtop) (i,j) = mtop (i,j)"
      by (simp add: top_matrix_def)
  qed
qed

lemma arc_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.arc f  (e . f e = top  (d . e  d  f d = bot))"
  using arc_linorder_matrix_1 arc_linorder_matrix_2 by blast

lemma arc_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.arc f  (∃!e . f e = top  (d . e  d  f d = bot))"
  apply (rule iffI)
  apply (metis (no_types, opaque_lifting) arc_linorder_matrix bot_not_top)
  using arc_linorder_matrix by blast

lemma pp_arc_linorder_matrix_1:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.pp_arc f"
    shows "e . f e  bot  (d . e  d  f d = bot)"
proof -
  have "matrix_stone_relation_algebra.pp_point (f  mtop)"
    by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
  from this obtain i where 1: "j . (f  mtop) (i,j)  bot  (k . (f  mtop) (i,j) = (f  mtop) (i,k))  (k . i  k  (f  mtop) (k,j) = bot)"
    by (metis pp_point_linorder_matrix)
  have "matrix_stone_relation_algebra.pp_point (ft  mtop)"
    by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
  from this obtain j where "i . (ft  mtop) (j,i)  bot  (k . (ft  mtop) (j,i) = (ft  mtop) (j,k))  (k . j  k  (ft  mtop) (k,i) = bot)"
    by (metis pp_point_linorder_matrix)
  hence 2: "i . (mtop  f) (i,j)  bot  (k . (mtop  f) (i,j) = (mtop  f) (k,j))  (k . j  k  (mtop  f) (i,k) = bot)"
    by (metis (no_types) old.prod.case conv_matrix_def conv_def matrix_stone_relation_algebra.conv_dist_comp matrix_stone_relation_algebra.conv_top)
  have 3: "i k . j  k  f (i,k) = bot"
  proof (intro allI, rule impI)
    fix i k
    assume "j  k"
    hence "(⨆⇩l f (l,k)) = bot"
      using 2 by (simp add: top_comp_linorder_matrix)
    thus "f (i,k) = bot"
      by (metis bot.extremum_uniqueI comp_inf.ub_sum)
  qed
  have "(⨆⇩k f (i,k))  bot"
    using 1 by (simp add: comp_top_linorder_matrix)
  hence 4: "f (i,j)  bot"
    using 3 by (metis linorder_finite_sup_selective)
  have "k l . k  i  l  j  f (k,l) = bot"
  proof (intro allI, unfold imp_disjL, rule conjI)
    fix k l
    show "k  i  f (k,l) = bot"
    proof
      assume "k  i"
      hence "(⨆⇩m f (k,m)) = bot"
        using 1 by (simp add: comp_top_linorder_matrix)
      thus "f (k,l) = bot"
        by (metis bot.extremum_uniqueI comp_inf.ub_sum)
    qed
    show "l  j  f (k,l) = bot"
      using 3 by simp
  qed
  thus ?thesis using 4
    by (metis old.prod.exhaust)
qed

lemma pp_arc_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_arc f  (e . f e  bot  (d . e  d  f d = bot))"
  using pp_arc_linorder_matrix_1 pp_arc_linorder_matrix_2 by blast

lemma pp_arc_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_arc f  (∃!e . f e  bot  (d . e  d  f d = bot))"
  apply (rule iffI)
  apply (metis (no_types, opaque_lifting) pp_arc_linorder_matrix)
  using pp_arc_linorder_matrix by blast

text ‹
Reflexive matrices are those with a constant top› diagonal.
›

lemma reflexive_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_idempotent_semiring.reflexive f"
    shows "f (i,i) = top"
proof -
  have "(top::'b) = mone (i,i)"
    by (simp add: one_matrix_def)
  also have "...  f (i,i)"
    using assms less_eq_matrix_def by blast
  finally show ?thesis
    by (simp add: top.extremum_unique)
qed

lemma reflexive_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "i . f (i,i) = top"
    shows "matrix_idempotent_semiring.reflexive f"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
  fix i j
  show "mone (i,j)  f (i,j)"
  proof (cases "i = j")
    assume "i = j"
    thus ?thesis
      by (simp add: assms)
  next
    assume "i  j"
    hence "(bot::'b) = mone (i,j)"
      by (simp add: one_matrix_def)
    thus ?thesis
      by simp
  qed
qed

lemma reflexive_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_idempotent_semiring.reflexive f  (i . f (i,i) = top)"
  using reflexive_linorder_matrix_1 reflexive_linorder_matrix_2 by auto

text ‹
Coreflexive matrices are those in which all non-diagonal entries are bot›.
›

lemma coreflexive_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_idempotent_semiring.coreflexive f"
      and "i  j"
    shows "f (i,j) = bot"
proof -
  have "f (i,j)  mone (i,j)"
    using assms less_eq_matrix_def by blast
  also have "... = bot"
    by (simp add: assms one_matrix_def)
  finally show ?thesis
    by (simp add: bot.extremum_unique)
qed

lemma coreflexive_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "i j . i  j  f (i,j) = bot"
    shows "matrix_idempotent_semiring.coreflexive f"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
  fix i j
  show "f (i,j)  mone (i,j)"
  proof (cases "i = j")
    assume "i = j"
    hence "(top::'b) = mone (i,j)"
      by (simp add: one_matrix_def)
    thus ?thesis
      by simp
  next
    assume "i  j"
    thus ?thesis
      by (simp add: assms)
  qed
qed

lemma coreflexive_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_idempotent_semiring.coreflexive f  (i j . i  j  f (i,j) = bot)"
  using coreflexive_linorder_matrix_1 coreflexive_linorder_matrix_2 by auto

text ‹
Irreflexive matrices are those with a constant bot› diagonal.
›

lemma irreflexive_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.irreflexive f"
    shows "f (i,i) = bot"
proof -
  have "(top::'b) = mone (i,i)"
    by (simp add: one_matrix_def)
  hence "(bot::'b) = (mone) (i,i)"
    by (simp add: uminus_matrix_def)
  hence "f (i,i)  bot"
    by (metis assms less_eq_matrix_def)
  thus ?thesis
    by (simp add: bot.extremum_unique)
qed

lemma irreflexive_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "i . f (i,i) = bot"
    shows "matrix_stone_relation_algebra.irreflexive f"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
  fix i j
  show "f (i,j)  (mone) (i,j)"
  proof (cases "i = j")
    assume "i = j"
    thus ?thesis
      by (simp add: assms)
  next
    assume "i  j"
    hence "(bot::'b) = mone (i,j)"
      by (simp add: one_matrix_def)
    hence "(top::'b) = (mone) (i,j)"
      by (simp add: uminus_matrix_def)
    thus ?thesis
      by simp
  qed
qed

lemma irreflexive_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.irreflexive f  (i . f (i,i) = bot)"
  using irreflexive_linorder_matrix_1 irreflexive_linorder_matrix_2 by auto

text ‹
As usual, symmetric matrices are those which do not change under transposition.
›

lemma symmetric_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.symmetric f  (i j . f (i,j) = f (j,i))"
  by (metis (mono_tags, lifting) case_prod_conv cond_case_prod_eta conv_matrix_def conv_def)

text ‹
Antisymmetric matrices are characterised as follows: each entry not on the diagonal or its mirror entry across the diagonal must be bot›.
›

lemma antisymmetric_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.antisymmetric f  (i j . i  j  f (i,j) = bot  f (j,i) = bot)"
proof -
  have "matrix_stone_relation_algebra.antisymmetric f  (i j . i  j  f (i,j)  f (j,i)  bot)"
    by (simp add: conv_matrix_def inf_matrix_def less_eq_matrix_def one_matrix_def)
  thus ?thesis
    by (metis (no_types, opaque_lifting) inf.absorb_iff1 inf.cobounded1 inf_bot_right inf_dense)
qed

text ‹
For asymmetric matrices the diagonal is included: each entry or its mirror entry across the diagonal must be bot›.
›

lemma asymmetric_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.asymmetric f  (i j . f (i,j) = bot  f (j,i) = bot)"
proof -
  have "matrix_stone_relation_algebra.asymmetric f  (i j . f (i,j)  f (j,i)  bot)"
    apply (unfold conv_matrix_def inf_matrix_def conv_def id_def bot_matrix_def)
    by (metis (mono_tags, lifting) bot.extremum bot.extremum_uniqueI case_prod_conv old.prod.exhaust)
  thus ?thesis
    by (metis (no_types, opaque_lifting) inf.absorb_iff1 inf.cobounded1 inf_bot_right inf_dense)
qed

text ‹
In a transitive matrix, the weight of one of the edges on an indirect route must be below the weight of the direct edge.
›

lemma transitive_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_idempotent_semiring.transitive f  (i j k . f (i,k)  f (i,j)  f (k,j)  f (i,j))"
proof -
  have "matrix_idempotent_semiring.transitive f  (i j . (⨆⇩k f (i,k) * f (k,j))  f (i,j))"
    by (simp add: times_matrix_def less_eq_matrix_def)
  also have "...  (i j k . f (i,k) * f (k,j)  f (i,j))"
    by (simp add: lub_sum_iff)
  also have "...  (i j k . f (i,k)  f (i,j)  f (k,j)  f (i,j))"
    using inf_less_eq by fastforce
  finally show ?thesis
    .
qed

text ‹
We finally show the effect of composing with a coreflexive (test) from the left and from the right.
This amounts to a restriction of each row or column to the entry on the diagonal of the coreflexive.
In this case, restrictions are formed by meets.
›

lemma coreflexive_comp_linorder_matrix:
  fixes f g :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_idempotent_semiring.coreflexive f"
    shows "(f  g) (i,j) = f (i,i)  g (i,j)"
proof -
  have 1: "k . i  k  f (i,k) = bot"
    using assms coreflexive_linorder_matrix by auto
  have "(⨆⇩k f (i,k)) = f (i,i)  (⨆⇘kUNIV-{i}f (i,k))"
    by (metis (no_types) UNIV_def brouwer.inf_bot_right finite_UNIV insert_def sup_monoid.sum.insert_remove)
  hence 2: "(⨆⇩k f (i,k)) = f (i,i)"
    using 1 by (metis (no_types) linorder_finite_sup_selective sup_not_bot)
  have "(f  g) (i,j) = (f  mtop  g) (i,j)"
    by (metis assms matrix_stone_relation_algebra.coreflexive_comp_top_inf)
  also have "... = (⨆⇩k f (i,k))  g (i,j)"
    by (metis inf_matrix_def comp_top_linorder_matrix)
  finally show ?thesis
    using 2 by simp
qed

lemma comp_coreflexive_linorder_matrix:
  fixes f g :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_idempotent_semiring.coreflexive g"
    shows "(f  g) (i,j) = f (i,j)  g (j,j)"
proof -
  have "(f  g) (i,j) = ((f  g)t) (j,i)"
    by (simp add: conv_matrix_def)
  also have "... = (g  ft) (j,i)"
    by (simp add: assms matrix_stone_relation_algebra.conv_dist_comp matrix_stone_relation_algebra.coreflexive_symmetric)
  also have "... = g (j,j)  (ft) (j,i)"
    by (simp add: assms coreflexive_comp_linorder_matrix)
  also have "... = f (i,j)  g (j,j)"
    by (metis (no_types, lifting) conv_def old.prod.case conv_matrix_def inf_commute)
  finally show ?thesis
    .
qed

end