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 "(f⇧t ⊙ f) (j,k) = (⨆⇩l (f⇧t) (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 "(f⇧t ⊙ 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 "f⇧t ⊙ f ≼ mone"
  proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
    fix j k
    show "(f⇧t ⊙ 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 ⊙ f⇧t) (i,i)"
    using assms less_eq_matrix_def by blast
  hence "top = (f ⊙ f⇧t) (i,i)"
    by (simp add: one_matrix_def top.extremum_unique)
  also have "... = (⨆⇩j f (i,j) * (f⇧t) (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 ⊙ f⇧t) (j,k)"
  proof (cases "j = k")
    assume "j = k"
    hence "(⨆⇩i f (j,i) * (f⇧t) (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 = mbot⇧t"
    by (metis matrix_stone_relation_algebra.conv_involutive)
  also have "... ⟷ ⊖(f⇧t ⊙ mtop) = mbot"
    by (simp add: matrix_stone_relation_algebra.conv_complement matrix_stone_relation_algebra.conv_dist_comp)
  also have "... ⟷ (∀i . ∃j . (f⇧t) (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 (f⇧t ⊙ mtop)"
    by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
  from this obtain j where "∀i . (f⇧t ⊙ mtop) (j,i) = top ∧ (∀k . j ≠ k ⟶ (f⇧t ⊙ 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 ⊙ f⇧t ≼ mone"
  proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
    fix i j
    show "(f ⊙ mtop ⊙ f⇧t) (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 ⊙ f⇧t) (i,j) = (⨆⇩l (f ⊙ mtop) (i,l) * (f⇧t) (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 "f⇧t ⊙ mtop ⊙ f ≼ mone"
  proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
    fix i j
    show "(f⇧t ⊙ 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 "(f⇧t ⊙ mtop ⊙ f) (i,j) = (⨆⇩l (f⇧t ⊙ mtop) (i,l) * f (l,j))"
        by (simp add: times_matrix_def)
      also have "... = (⨆⇩l (⨆⇩k (f⇧t) (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 ⊙ f⇧t ≼ mone"
    by (metis (no_types, lifting) assms bot_not_top matrix_stone_relation_algebra.pp_arc_expanded pp_arc_linorder_matrix_2)
next
  show "f⇧t ⊙ 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 (f⇧t ⊙ mtop)"
    by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
  from this obtain j where "∀i . (f⇧t ⊙ mtop) (j,i) ≠ bot ∧ (∀k . (f⇧t ⊙ mtop) (j,i) = (f⇧t ⊙ mtop) (j,k)) ∧ (∀k . j ≠ k ⟶ (f⇧t ⊙ 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) ⊔ (⨆⇘k∈UNIV-{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 ⊙ f⇧t) (j,i)"
    by (simp add: assms matrix_stone_relation_algebra.conv_dist_comp matrix_stone_relation_algebra.coreflexive_symmetric)
  also have "... = g (j,j) ⊓ (f⇧t) (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