Theory Matrix_Kleene_Algebras

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

section ‹Matrix Kleene Algebras›

text ‹
This theory gives a matrix model of Stone-Kleene relation algebras.
The main result is that matrices over Kleene algebras form Kleene algebras.
The automata-based construction is due to Conway \<^cite>‹"Conway1971"›.
An implementation of the construction in Isabelle/HOL that extends \<^cite>‹"ArmstrongGomesStruthWeber2016"› was given in \<^cite>‹"Asplund2014"› without a correctness proof.

For specifying the size of matrices, Isabelle/HOL's type system requires the use of types, not sets.
This creates two issues when trying to implement Conway's recursive construction directly.
First, the matrix size changes for recursive calls, which requires dependent types.
Second, some submatrices used in the construction are not square, which requires typed Kleene algebras \<^cite>‹"Kozen1998"›, that is, categories of Kleene algebras.

Because these instruments are not available in Isabelle/HOL, we use square matrices with a constant size given by the argument of the Kleene star operation.
Smaller, possibly rectangular submatrices are identified by two lists of indices: one for the rows to include and one for the columns to include.
Lists are used to make recursive calls deterministic; otherwise sets would be sufficient.
›

theory Matrix_Kleene_Algebras

imports Stone_Relation_Algebras.Matrix_Relation_Algebras Kleene_Relation_Algebras

begin

subsection ‹Matrix Restrictions›

text ‹
In this section we develop a calculus of matrix restrictions.
The restriction of a matrix to specific row and column indices is implemented by the following function, which keeps the size of the matrix and sets all unused entries to ‹bot›.
›

definition restrict_matrix :: "'a list ⇒ ('a,'b::bot) square ⇒ 'a list ⇒ ('a,'b) square" (‹_ ⟨_⟩ _› [90,41,90] 91)
  where "restrict_matrix as f bs = (λ(i,j) . if i ∈ set as ∧ j ∈ set bs then f (i,j) else bot)"

text ‹
The following function captures Conway's automata-based construction of the Kleene star of a matrix.
An index ‹k› is chosen and ‹s› contains all other indices.
The matrix is split into four submatrices ‹a›, ‹b›, ‹c›, ‹d› including/not including row/column ‹k›.
Four matrices are computed containing the entries given by Conway's construction.
These four matrices are added to obtain the result.
All matrices involved in the function have the same size, but matrix restriction is used to set irrelevant entries to ‹bot›.
›

primrec star_matrix' :: "'a list ⇒ ('a,'b::{star,times,bounded_semilattice_sup_bot}) square ⇒ ('a,'b) square" where
"star_matrix' Nil g = mbot" |
"star_matrix' (k#s) g = (
  let r = [k] in
  let a = r⟨g⟩r in
  let b = r⟨g⟩s in
  let c = s⟨g⟩r in
  let d = s⟨g⟩s in
  let as = r⟨star o a⟩r in
  let ds = star_matrix' s d in
  let e = a ⊕ b ⊙ ds ⊙ c in
  let es = r⟨star o e⟩r in
  let f = d ⊕ c ⊙ as ⊙ b in
  let fs = star_matrix' s f in
  es ⊕ as ⊙ b ⊙ fs ⊕ ds ⊙ c ⊙ es ⊕ fs
)"

text ‹
The Kleene star of the whole matrix is obtained by taking as indices all elements of the underlying type ‹'a›.
This is conveniently supplied by the ‹enum› class.
›

fun star_matrix :: "('a::enum,'b::{star,times,bounded_semilattice_sup_bot}) square ⇒ ('a,'b) square" (‹_⇧⊙› [100] 100) where "star_matrix f = star_matrix' (enum_class.enum::'a list) f"

text ‹
The following lemmas deconstruct matrices with non-empty restrictions.
›

lemma restrict_empty_left:
  "[]⟨f⟩ls = mbot"
  by (unfold restrict_matrix_def bot_matrix_def) auto

lemma restrict_empty_right:
  "ks⟨f⟩[] = mbot"
  by (unfold restrict_matrix_def bot_matrix_def) auto

lemma restrict_nonempty_left:
  fixes f :: "('a,'b::bounded_semilattice_sup_bot) square"
  shows "(k#ks)⟨f⟩ls = [k]⟨f⟩ls ⊕ ks⟨f⟩ls"
  by (unfold restrict_matrix_def sup_matrix_def) auto

lemma restrict_nonempty_right:
  fixes f :: "('a,'b::bounded_semilattice_sup_bot) square"
  shows "ks⟨f⟩(l#ls) = ks⟨f⟩[l] ⊕ ks⟨f⟩ls"
  by (unfold restrict_matrix_def sup_matrix_def) auto

lemma restrict_nonempty:
  fixes f :: "('a,'b::bounded_semilattice_sup_bot) square"
  shows "(k#ks)⟨f⟩(l#ls) = [k]⟨f⟩[l] ⊕ [k]⟨f⟩ls ⊕ ks⟨f⟩[l] ⊕ ks⟨f⟩ls"
  by (unfold restrict_matrix_def sup_matrix_def) auto

text ‹
The following predicate captures that two index sets are disjoint.
This has consequences for composition and the unit matrix.
›

abbreviation "disjoint ks ls ≡ ¬ (∃x . x ∈ set ks ∧ x ∈ set ls)"

lemma times_disjoint:
  fixes f g :: "('a,'b::idempotent_semiring) square"
  assumes "disjoint ls ms"
    shows "ks⟨f⟩ls ⊙ ms⟨g⟩ns = mbot"
proof (rule ext, rule prod_cases)
  fix i j
  have "(ks⟨f⟩ls ⊙ ms⟨g⟩ns) (i,j) = (⨆⇩k (ks⟨f⟩ls) (i,k) * (ms⟨g⟩ns) (k,j))"
    by (simp add: times_matrix_def)
  also have "... = (⨆⇩k (if i ∈ set ks ∧ k ∈ set ls then f (i,k) else bot)
    * (if k ∈ set ms ∧ j ∈ set ns then g (k,j) else bot))"
    by (simp add: restrict_matrix_def)
  also have "... = (⨆⇩k if k ∈ set ms ∧ j ∈ set ns then bot * g (k,j)
    else (if i ∈ set ks ∧ k ∈ set ls then f (i,k) else bot) * bot)"
    using assms by (auto intro: sup_monoid.sum.cong)
  also have "... = (⨆⇩(k::'a) bot)"
    by (simp add: sup_monoid.sum.neutral)
  also have "... = bot"
    by (simp add: eq_iff le_funI)
  also have "... = mbot (i,j)"
    by (simp add: bot_matrix_def)
  finally show "(ks⟨f⟩ls ⊙ ms⟨g⟩ns) (i,j) = mbot (i,j)"
    .
qed

lemma one_disjoint:
  assumes "disjoint ks ls"
    shows "ks⟨(mone::('a,'b::idempotent_semiring) square)⟩ls = mbot"
proof (rule ext, rule prod_cases)
  let ?o = "mone::('a,'b) square"
  fix i j
  have "(ks⟨?o⟩ls) (i,j) = (if i ∈ set ks ∧ j ∈ set ls then if i = j then 1 else bot else bot)"
    by (simp add: restrict_matrix_def one_matrix_def)
  also have "... = bot"
    using assms by auto
  also have "... = mbot (i,j)"
    by (simp add: bot_matrix_def)
  finally show "(ks⟨?o⟩ls) (i,j) = mbot (i,j)"
    .
qed

text ‹
The following predicate captures that an index set is a subset of another index set.
This has consequences for repeated restrictions.
›

abbreviation "is_sublist ks ls ≡ set ks ⊆ set ls"

lemma restrict_sublist:
  assumes "is_sublist ls ks"
      and "is_sublist ms ns"
    shows "ls⟨ks⟨f⟩ns⟩ms = ls⟨f⟩ms"
proof (rule ext, rule prod_cases)
  fix i j
  show "(ls⟨ks⟨f⟩ns⟩ms) (i,j) = (ls⟨f⟩ms) (i,j)"
  proof (cases "i ∈ set ls ∧ j ∈ set ms")
    case True
    with assms show ?thesis
      by (auto simp add: restrict_matrix_def)
  next
    case False
    with assms show ?thesis
      by (auto simp add: restrict_matrix_def)
  qed
qed

lemma restrict_superlist:
  assumes "is_sublist ls ks"
      and "is_sublist ms ns"
    shows "ks⟨ls⟨f⟩ms⟩ns = ls⟨f⟩ms"
proof (rule ext, rule prod_cases)
  fix i j
  show "(ks⟨ls⟨f⟩ms⟩ns) (i,j) = (ls⟨f⟩ms) (i,j)"
  proof (cases "i ∈ set ls ∧ j ∈ set ms")
    case True
    with assms show ?thesis
      by (auto simp add: restrict_matrix_def)
  next
    case False
    with assms show ?thesis
      by (auto simp add: restrict_matrix_def)
  qed
qed

text ‹
The following lemmas give the sizes of the results of some matrix operations.
›

lemma restrict_sup:
  fixes f g :: "('a,'b::bounded_semilattice_sup_bot) square"
  shows "ks⟨f ⊕ g⟩ls = ks⟨f⟩ls ⊕ ks⟨g⟩ls"
  by (unfold restrict_matrix_def sup_matrix_def) auto

lemma restrict_times:
  fixes f g :: "('a,'b::idempotent_semiring) square"
  shows "ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms = ks⟨f⟩ls ⊙ ls⟨g⟩ms"
proof (rule ext, rule prod_cases)
  fix i j
  have "(ks⟨(ks⟨f⟩ls ⊙ ls⟨g⟩ms)⟩ms) (i,j) = (if i ∈ set ks ∧ j ∈ set ms then (⨆⇩k (ks⟨f⟩ls) (i,k) * (ls⟨g⟩ms) (k,j)) else bot)"
    by (simp add: times_matrix_def restrict_matrix_def)
  also have "... = (if i ∈ set ks ∧ j ∈ set ms then (⨆⇩k (if i ∈ set ks ∧ k ∈ set ls then f (i,k) else bot) * (if k ∈ set ls ∧ j ∈ set ms then g (k,j) else bot)) else bot)"
    by (simp add: restrict_matrix_def)
  also have "... = (if i ∈ set ks ∧ j ∈ set ms then (⨆⇩k if k ∈ set ls then f (i,k) * g (k,j) else bot) else bot)"
    by (auto intro: sup_monoid.sum.cong)
  also have "... = (⨆⇩k if i ∈ set ks ∧ j ∈ set ms then (if k ∈ set ls then f (i,k) * g (k,j) else bot) else bot)"
    by auto
  also have "... = (⨆⇩k (if i ∈ set ks ∧ k ∈ set ls then f (i,k) else bot) * (if k ∈ set ls ∧ j ∈ set ms then g (k,j) else bot))"
    by (auto intro: sup_monoid.sum.cong)
  also have "... = (⨆⇩k (ks⟨f⟩ls) (i,k) * (ls⟨g⟩ms) (k,j))"
    by (simp add: restrict_matrix_def)
  also have "... = (ks⟨f⟩ls ⊙ ls⟨g⟩ms) (i,j)"
    by (simp add: times_matrix_def)
  finally show "(ks⟨(ks⟨f⟩ls ⊙ ls⟨g⟩ms)⟩ms) (i,j) = (ks⟨f⟩ls ⊙ ls⟨g⟩ms) (i,j)"
    .
qed

lemma restrict_star:
  fixes g :: "('a,'b::kleene_algebra) square"
  shows "t⟨star_matrix' t g⟩t = star_matrix' t g"
proof (induct arbitrary: g rule: list.induct)
  case Nil show ?case
    by (simp add: restrict_empty_left)
next
  case (Cons k s)
  let ?t = "k#s"
  assume "⋀g::('a,'b) square . s⟨star_matrix' s g⟩s = star_matrix' s g"
  then have 1: "?t⟨star_matrix' s g⟩?t = star_matrix' s g" for g :: ‹('a, 'b) square›
    using restrict_superlist [of s ‹k # s› s ‹k # s› ‹star_matrix' s g›]
    by auto
  show "?t⟨star_matrix' ?t g⟩?t = star_matrix' ?t g"
  proof -
    let ?r = "[k]"
    let ?a = "?r⟨g⟩?r"
    let ?b = "?r⟨g⟩s"
    let ?c = "s⟨g⟩?r"
    let ?d = "s⟨g⟩s"
    let ?as = "?r⟨star o ?a⟩?r"
    let ?ds = "star_matrix' s ?d"
    let ?e = "?a ⊕ ?b ⊙ ?ds ⊙ ?c"
    let ?es = "?r⟨star o ?e⟩?r"
    let ?f = "?d ⊕ ?c ⊙ ?as ⊙ ?b"
    let ?fs = "star_matrix' s ?f"
    have 2: "?t⟨?as⟩?t = ?as ∧ ?t⟨?b⟩?t = ?b ∧ ?t⟨?c⟩?t = ?c ∧ ?t⟨?es⟩?t = ?es"
      by (simp add: restrict_superlist subset_eq)
    have 3: "?t⟨?ds⟩?t = ?ds ∧ ?t⟨?fs⟩?t = ?fs"
      using 1 by simp
    have 4: "?t⟨?t⟨?as⟩?t ⊙ ?t⟨?b⟩?t ⊙ ?t⟨?fs⟩?t⟩?t = ?t⟨?as⟩?t ⊙ ?t⟨?b⟩?t ⊙ ?t⟨?fs⟩?t"
      by (metis (no_types) restrict_times)
    have 5: "?t⟨?t⟨?ds⟩?t ⊙ ?t⟨?c⟩?t ⊙ ?t⟨?es⟩?t⟩?t = ?t⟨?ds⟩?t ⊙ ?t⟨?c⟩?t ⊙ ?t⟨?es⟩?t"
      by (metis (no_types) restrict_times)
    have "?t⟨star_matrix' ?t g⟩?t = ?t⟨?es ⊕ ?as ⊙ ?b ⊙ ?fs ⊕ ?ds ⊙ ?c ⊙ ?es ⊕ ?fs⟩?t"
      by (metis star_matrix'.simps(2))
    also have "... = ?t⟨?es⟩?t ⊕ ?t⟨?as ⊙ ?b ⊙ ?fs⟩?t ⊕ ?t⟨?ds ⊙ ?c ⊙ ?es⟩?t ⊕ ?t⟨?fs⟩?t"
      by (simp add: restrict_sup)
    also have "... = ?es ⊕ ?as ⊙ ?b ⊙ ?fs ⊕ ?ds ⊙ ?c ⊙ ?es ⊕ ?fs"
      using 2 3 4 5 by simp
    also have "... = star_matrix' ?t g"
      by (metis star_matrix'.simps(2))
    finally show ?thesis
      .
  qed
qed

lemma restrict_one:
  assumes "¬ k ∈ set ks"
    shows "(k#ks)⟨(mone::('a,'b::idempotent_semiring) square)⟩(k#ks) = [k]⟨mone⟩[k] ⊕ ks⟨mone⟩ks"
  by (subst restrict_nonempty) (simp add: assms one_disjoint)

lemma restrict_one_left_unit:
  "ks⟨(mone::('a::finite,'b::idempotent_semiring) square)⟩ks ⊙ ks⟨f⟩ls = ks⟨f⟩ls"
proof (rule ext, rule prod_cases)
  let ?o = "mone::('a,'b::idempotent_semiring) square"
  fix i j
  have "(ks⟨?o⟩ks ⊙ ks⟨f⟩ls) (i,j) = (⨆⇩k (ks⟨?o⟩ks) (i,k) * (ks⟨f⟩ls) (k,j))"
    by (simp add: times_matrix_def)
  also have "... = (⨆⇩k (if i ∈ set ks ∧ k ∈ set ks then ?o (i,k) else bot) * (if k ∈ set ks ∧ j ∈ set ls then f (k,j) else bot))"
    by (simp add: restrict_matrix_def)
  also have "... = (⨆⇩k (if i ∈ set ks ∧ k ∈ set ks then (if i = k then 1 else bot) else bot) * (if k ∈ set ks ∧ j ∈ set ls then f (k,j) else bot))"
    by (unfold one_matrix_def) auto
  also have "... = (⨆⇩k (if i = k then (if i ∈ set ks then 1 else bot) else bot) * (if k ∈ set ks ∧ j ∈ set ls then f (k,j) else bot))"
    by (auto intro: sup_monoid.sum.cong)
  also have "... = (⨆⇩k if i = k then (if i ∈ set ks then 1 else bot) * (if i ∈ set ks ∧ j ∈ set ls then f (i,j) else bot) else bot)"
    by (rule sup_monoid.sum.cong) simp_all
  also have "... = (if i ∈ set ks then 1 else bot) * (if i ∈ set ks ∧ j ∈ set ls then f (i,j) else bot)"
    by simp
  also have "... = (if i ∈ set ks ∧ j ∈ set ls then f (i,j) else bot)"
    by simp
  also have "... = (ks⟨f⟩ls) (i,j)"
    by (simp add: restrict_matrix_def)
  finally show "(ks⟨?o⟩ks ⊙ ks⟨f⟩ls) (i,j) = (ks⟨f⟩ls) (i,j)"
    .
qed

text ‹
The following lemmas consider restrictions to singleton index sets.
›

lemma restrict_singleton:
  "([k]⟨f⟩[l]) (i,j) = (if i = k ∧ j = l then f (i,j) else bot)"
  by (simp add: restrict_matrix_def)

lemma restrict_singleton_list:
  "([k]⟨f⟩ls) (i,j) = (if i = k ∧ j ∈ set ls then f (i,j) else bot)"
  by (simp add: restrict_matrix_def)

lemma restrict_list_singleton:
  "(ks⟨f⟩[l]) (i,j) = (if i ∈ set ks ∧ j = l then f (i,j) else bot)"
  by (simp add: restrict_matrix_def)

lemma restrict_singleton_product:
  fixes f g :: "('a::finite,'b::kleene_algebra) square"
  shows "([k]⟨f⟩[l] ⊙ [m]⟨g⟩[n]) (i,j) = (if i = k ∧ l = m ∧ j = n then f (i,l) * g (m,j) else bot)"
proof -
  have "([k]⟨f⟩[l] ⊙ [m]⟨g⟩[n]) (i,j) = (⨆⇩h ([k]⟨f⟩[l]) (i,h) * ([m]⟨g⟩[n]) (h,j))"
    by (simp add: times_matrix_def)
  also have "... = (⨆⇩h (if i = k ∧ h = l then f (i,h) else bot) * (if h = m ∧ j = n then g (h,j) else bot))"
    by (simp add: restrict_singleton)
  also have "... = (⨆⇩h if h = l then (if i = k then f (i,h) else bot) * (if h = m ∧ j = n then g (h,j) else bot) else bot)"
    by (rule sup_monoid.sum.cong) auto
  also have "... = (if i = k then f (i,l) else bot) * (if l = m ∧ j = n then g (l,j) else bot)"
    by simp
  also have "... = (if i = k ∧ l = m ∧ j = n then f (i,l) * g (m,j) else bot)"
    by simp
  finally show ?thesis
    .
qed

text ‹
The Kleene star unfold law holds for matrices with a single entry on the diagonal.
›

lemma restrict_star_unfold:
  "[l]⟨(mone::('a::finite,'b::kleene_algebra) square)⟩[l] ⊕ [l]⟨f⟩[l] ⊙ [l]⟨star o f⟩[l] = [l]⟨star o f⟩[l]"
proof (rule ext, rule prod_cases)
  let ?o = "mone::('a,'b::kleene_algebra) square"
  fix i j
  have "([l]⟨?o⟩[l] ⊕ [l]⟨f⟩[l] ⊙ [l]⟨star o f⟩[l]) (i,j) = ([l]⟨?o⟩[l]) (i,j) ⊔ ([l]⟨f⟩[l] ⊙ [l]⟨star o f⟩[l]) (i,j)"
    by (simp add: sup_matrix_def)
  also have "... = ([l]⟨?o⟩[l]) (i,j) ⊔ (⨆⇩k ([l]⟨f⟩[l]) (i,k) * ([l]⟨star o f⟩[l]) (k,j))"
    by (simp add: times_matrix_def)
  also have "... = ([l]⟨?o⟩[l]) (i,j) ⊔ (⨆⇩k (if i = l ∧ k = l then f (i,k) else bot) * (if k = l ∧ j = l then (f (k,j))⇧⋆ else bot))"
    by (simp add: restrict_singleton o_def)
  also have "... = ([l]⟨?o⟩[l]) (i,j) ⊔ (⨆⇩k if k = l then (if i = l then f (i,k) else bot) * (if j = l then (f (k,j))⇧⋆ else bot) else bot)"
    apply (rule arg_cong2[where f=sup])
    apply simp
    by (rule sup_monoid.sum.cong) auto
  also have "... = ([l]⟨?o⟩[l]) (i,j) ⊔ (if i = l then f (i,l) else bot) * (if j = l then (f (l,j))⇧⋆ else bot)"
    by simp
  also have "... = (if i = l ∧ j = l then 1 ⊔ f (l,l) * (f (l,l))⇧⋆ else bot)"
    by (simp add: restrict_singleton one_matrix_def)
  also have "... = (if i = l ∧ j = l then (f (l,l))⇧⋆ else bot)"
    by (simp add: star_left_unfold_equal)
  also have "... = ([l]⟨star o f⟩[l]) (i,j)"
    by (simp add: restrict_singleton o_def)
  finally show "([l]⟨?o⟩[l] ⊕ [l]⟨f⟩[l] ⊙ [l]⟨star o f⟩[l]) (i,j) = ([l]⟨star o f⟩[l]) (i,j)"
    .
qed

lemma restrict_all:
  "enum_class.enum⟨f⟩enum_class.enum = f"
  by (simp add: restrict_matrix_def enum_UNIV)

text ‹
The following shows the various components of a matrix product.
It is essentially a recursive implementation of the product.
›

lemma restrict_nonempty_product:
  fixes f g :: "('a::finite,'b::idempotent_semiring) square"
  assumes "¬ l ∈ set ls"
    shows "(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms) = ([k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ ([k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms)"
proof -
  have "(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms) = ([k]⟨f⟩[l] ⊕ [k]⟨f⟩ls ⊕ ks⟨f⟩[l] ⊕ ks⟨f⟩ls) ⊙ ([l]⟨g⟩[m] ⊕ [l]⟨g⟩ms ⊕ ls⟨g⟩[m] ⊕ ls⟨g⟩ms)"
    by (metis restrict_nonempty)
  also have "... = [k]⟨f⟩[l] ⊙ ([l]⟨g⟩[m] ⊕ [l]⟨g⟩ms ⊕ ls⟨g⟩[m] ⊕ ls⟨g⟩ms) ⊕ [k]⟨f⟩ls ⊙ ([l]⟨g⟩[m] ⊕ [l]⟨g⟩ms ⊕ ls⟨g⟩[m] ⊕ ls⟨g⟩ms) ⊕ ks⟨f⟩[l] ⊙ ([l]⟨g⟩[m] ⊕ [l]⟨g⟩ms ⊕ ls⟨g⟩[m] ⊕ ls⟨g⟩ms) ⊕ ks⟨f⟩ls ⊙ ([l]⟨g⟩[m] ⊕ [l]⟨g⟩ms ⊕ ls⟨g⟩[m] ⊕ ls⟨g⟩ms)"
    by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
  also have "... = ([k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩[l] ⊙ ls⟨g⟩[m] ⊕ [k]⟨f⟩[l] ⊙ ls⟨g⟩ms) ⊕ ([k]⟨f⟩ls ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩[l] ⊙ ls⟨g⟩[m] ⊕ ks⟨f⟩[l] ⊙ ls⟨g⟩ms) ⊕ (ks⟨f⟩ls ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms)"
    by (simp add: matrix_idempotent_semiring.mult_left_dist_sup)
  also have "... = ([k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms) ⊕ ([k]⟨f⟩ls ⊙ ls⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩[l] ⊙ [l]⟨g⟩ms) ⊕ (ks⟨f⟩ls ⊙ ls⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms)"
    using assms by (simp add: times_disjoint)
  also have "... = ([k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ ([k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms)"
    by (simp add: matrix_bounded_semilattice_sup_bot.sup_monoid.add_assoc matrix_semilattice_sup.sup_left_commute)
  finally show ?thesis
    .
qed

text ‹
Equality of matrices is componentwise.
›

lemma restrict_nonempty_eq:
  "(k#ks)⟨f⟩(l#ls) = (k#ks)⟨g⟩(l#ls) ⟷ [k]⟨f⟩[l] = [k]⟨g⟩[l] ∧ [k]⟨f⟩ls = [k]⟨g⟩ls ∧ ks⟨f⟩[l] = ks⟨g⟩[l] ∧ ks⟨f⟩ls = ks⟨g⟩ls"
proof
  assume 1: "(k#ks)⟨f⟩(l#ls) = (k#ks)⟨g⟩(l#ls)"
  have 2: "is_sublist [k] (k#ks) ∧ is_sublist ks (k#ks) ∧ is_sublist [l] (l#ls) ∧ is_sublist ls (l#ls)"
    by auto
  hence "[k]⟨f⟩[l] = [k]⟨(k#ks)⟨f⟩(l#ls)⟩[l] ∧ [k]⟨f⟩ls = [k]⟨(k#ks)⟨f⟩(l#ls)⟩ls ∧ ks⟨f⟩[l] = ks⟨(k#ks)⟨f⟩(l#ls)⟩[l] ∧ ks⟨f⟩ls = ks⟨(k#ks)⟨f⟩(l#ls)⟩ls"
    by (simp add: restrict_sublist)
  thus "[k]⟨f⟩[l] = [k]⟨g⟩[l] ∧ [k]⟨f⟩ls = [k]⟨g⟩ls ∧ ks⟨f⟩[l] = ks⟨g⟩[l] ∧ ks⟨f⟩ls = ks⟨g⟩ls"
    using 1 2 by (simp add: restrict_sublist)
next
  assume 3: "[k]⟨f⟩[l] = [k]⟨g⟩[l] ∧ [k]⟨f⟩ls = [k]⟨g⟩ls ∧ ks⟨f⟩[l] = ks⟨g⟩[l] ∧ ks⟨f⟩ls = ks⟨g⟩ls"
  show "(k#ks)⟨f⟩(l#ls) = (k#ks)⟨g⟩(l#ls)"
  proof (rule ext, rule prod_cases)
    fix i j
    have 4: "f (k,l) = g (k,l)"
      using 3 by (metis restrict_singleton)
    have 5: "j ∈ set ls ⟹ f (k,j) = g (k,j)"
      using 3 by (metis restrict_singleton_list)
    have 6: "i ∈ set ks ⟹ f (i,l) = g (i,l)"
      using 3 by (metis restrict_list_singleton)
    have "(ks⟨f⟩ls) (i,j) = (ks⟨g⟩ls) (i,j)"
      using 3 by simp
    hence 7: "i ∈ set ks ⟹ j ∈ set ls ⟹ f (i,j) = g (i,j)"
      by (simp add: restrict_matrix_def)
    have "((k#ks)⟨f⟩(l#ls)) (i,j) = (if (i = k ∨ i ∈ set ks) ∧ (j = l ∨ j ∈ set ls) then f (i,j) else bot)"
      by (simp add: restrict_matrix_def)
    also have "... = (if i = k ∧ j = l then f (i,j) else if i = k ∧ j ∈ set ls then f (i,j) else if i ∈ set ks ∧ j = l then f (i,j) else if i ∈ set ks ∧ j ∈ set ls then f (i,j) else bot)"
      by auto
    also have "... = (if i = k ∧ j = l then g (i,j) else if i = k ∧ j ∈ set ls then g (i,j) else if i ∈ set ks ∧ j = l then g (i,j) else if i ∈ set ks ∧ j ∈ set ls then g (i,j) else bot)"
      using 4 5 6 7 by simp
    also have "... = (if (i = k ∨ i ∈ set ks) ∧ (j = l ∨ j ∈ set ls) then g (i,j) else bot)"
      by auto
    also have "... = ((k#ks)⟨g⟩(l#ls)) (i,j)"
      by (simp add: restrict_matrix_def)
    finally show "((k#ks)⟨f⟩(l#ls)) (i,j) = ((k#ks)⟨g⟩(l#ls)) (i,j)"
      .
  qed
qed

text ‹
Inequality of matrices is componentwise.
›

lemma restrict_nonempty_less_eq:
  fixes f g :: "('a,'b::idempotent_semiring) square"
  shows "(k#ks)⟨f⟩(l#ls) ≼ (k#ks)⟨g⟩(l#ls) ⟷ [k]⟨f⟩[l] ≼ [k]⟨g⟩[l] ∧ [k]⟨f⟩ls ≼ [k]⟨g⟩ls ∧ ks⟨f⟩[l] ≼ ks⟨g⟩[l] ∧ ks⟨f⟩ls ≼ ks⟨g⟩ls"
  by (unfold matrix_semilattice_sup.sup.order_iff) (metis (no_types, lifting) restrict_nonempty_eq restrict_sup)

text ‹
The following lemmas treat repeated restrictions to disjoint index sets.
›

lemma restrict_disjoint_left:
  assumes "disjoint ks ms"
    shows "ms⟨ks⟨f⟩ls⟩ns = mbot"
proof (rule ext, rule prod_cases)
  fix i j
  have "(ms⟨ks⟨f⟩ls⟩ns) (i,j) = (if i ∈ set ms ∧ j ∈ set ns then if i ∈ set ks ∧ j ∈ set ls then f (i,j) else bot else bot)"
    by (auto simp add: restrict_matrix_def)
  thus "(ms⟨ks⟨f⟩ls⟩ns) (i,j) = mbot (i,j)"
    using assms by (simp add: bot_matrix_def)
qed

lemma restrict_disjoint_right:
  assumes "disjoint ls ns"
    shows "ms⟨ks⟨f⟩ls⟩ns = mbot"
proof (rule ext, rule prod_cases)
  fix i j
  have "(ms⟨ks⟨f⟩ls⟩ns) (i,j) = (if i ∈ set ms ∧ j ∈ set ns then if i ∈ set ks ∧ j ∈ set ls then f (i,j) else bot else bot)"
    by (simp add: restrict_matrix_def)
  thus "(ms⟨ks⟨f⟩ls⟩ns) (i,j) = mbot (i,j)"
    using assms by (simp add: bot_matrix_def)
qed

text ‹
The following lemma expresses the equality of a matrix and a product of two matrices componentwise.
›

lemma restrict_nonempty_product_eq:
  fixes f g h :: "('a::finite,'b::idempotent_semiring) square"
  assumes "¬ k ∈ set ks"
      and "¬ l ∈ set ls"
      and "¬ m ∈ set ms"
    shows "(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms) = (k#ks)⟨h⟩(m#ms) ⟷ [k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m] = [k]⟨h⟩[m] ∧ [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms = [k]⟨h⟩ms ∧ ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m] = ks⟨h⟩[m] ∧ ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms = ks⟨h⟩ms"
proof -
  have 1: "disjoint [k] ks ∧ disjoint [m] ms"
    by (auto simp add: assms(1,3))
  have 2: "[k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] = [k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m]"
  proof -
    have "[k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] = [k]⟨([k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ ([k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms)⟩[m]"
      by (metis assms(2) restrict_nonempty_product)
    also have "... = [k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m] ⊕ [k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m] ⊕ [k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩[m] ⊕ [k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩ms⟩[m] ⊕ [k]⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m] ⊕ [k]⟨ks⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m] ⊕ [k]⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩[m] ⊕ [k]⟨ks⟨f⟩ls ⊙ ls⟨g⟩ms⟩[m]"
      by (simp add: matrix_bounded_semilattice_sup_bot.sup_monoid.add_assoc restrict_sup)
    also have "... = [k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m] ⊕ [k]⟨[k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms⟩[m] ⊕ [k]⟨[k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms⟩[m] ⊕ [k]⟨ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m]⟩[m] ⊕ [k]⟨ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m]⟩[m] ⊕ [k]⟨ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms⟩[m] ⊕ [k]⟨ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms⟩[m]"
      by (simp add: restrict_times)
    also have "... = [k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m]"
      using 1 by (metis restrict_disjoint_left restrict_disjoint_right matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_right)
    finally show ?thesis
      .
  qed
  have 3: "[k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms = [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms"
  proof -
    have "[k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms = [k]⟨([k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ ([k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms)⟩ms"
      by (metis assms(2) restrict_nonempty_product)
    also have "... = [k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩ms ⊕ [k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩[m]⟩ms ⊕ [k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms ⊕ [k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms ⊕ [k]⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩ms ⊕ [k]⟨ks⟨f⟩ls ⊙ ls⟨g⟩[m]⟩ms ⊕ [k]⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms ⊕ [k]⟨ks⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms"
      by (simp add: matrix_bounded_semilattice_sup_bot.sup_monoid.add_assoc restrict_sup)
    also have "... = [k]⟨[k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m]⟩ms ⊕ [k]⟨[k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m]⟩ms ⊕ [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms ⊕ [k]⟨ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m]⟩ms ⊕ [k]⟨ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m]⟩ms ⊕ [k]⟨ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms⟩ms ⊕ [k]⟨ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms⟩ms"
      by (simp add: restrict_times)
    also have "... = [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms"
      using 1 by (metis restrict_disjoint_left restrict_disjoint_right matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_right matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_left)
    finally show ?thesis
      .
  qed
  have 4: "ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] = ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m]"
  proof -
    have "ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] = ks⟨([k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ ([k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms)⟩[m]"
      by (metis assms(2) restrict_nonempty_product)
    also have "... = ks⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m] ⊕ ks⟨[k]⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m] ⊕ ks⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩[m] ⊕ ks⟨[k]⟨f⟩ls ⊙ ls⟨g⟩ms⟩[m] ⊕ ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m] ⊕ ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m] ⊕ ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩[m] ⊕ ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩ms⟩[m]"
      by (simp add: matrix_bounded_semilattice_sup_bot.sup_monoid.add_assoc restrict_sup)
    also have "... = ks⟨[k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m]⟩[m] ⊕ ks⟨[k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m]⟩[m] ⊕ ks⟨[k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms⟩[m] ⊕ ks⟨[k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms⟩[m] ⊕ ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m] ⊕ ks⟨ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms⟩[m] ⊕ ks⟨ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms⟩[m]"
      by (simp add: restrict_times)
    also have "... = ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m]"
      using 1 by (metis restrict_disjoint_left restrict_disjoint_right matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_right matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_left)
    finally show ?thesis
      .
  qed
  have 5: "ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms = ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms"
  proof -
    have "ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms = ks⟨([k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ ([k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m]) ⊕ (ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms)⟩ms"
      by (metis assms(2) restrict_nonempty_product)
    also have "... = ks⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩ms ⊕ ks⟨[k]⟨f⟩ls ⊙ ls⟨g⟩[m]⟩ms ⊕ ks⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms ⊕ ks⟨[k]⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms ⊕ ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩ms ⊕ ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩[m]⟩ms ⊕ ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms ⊕ ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms"
      by (simp add: matrix_bounded_semilattice_sup_bot.sup_monoid.add_assoc restrict_sup)
    also have "... = ks⟨[k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m]⟩ms ⊕ ks⟨[k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m]⟩ms ⊕ ks⟨[k]⟨[k]⟨f⟩[l] ⊙ [l]⟨g⟩ms⟩ms⟩ms ⊕ ks⟨[k]⟨[k]⟨f⟩ls ⊙ ls⟨g⟩ms⟩ms⟩ms ⊕ ks⟨ks⟨ks⟨f⟩[l] ⊙ [l]⟨g⟩[m]⟩[m]⟩ms ⊕ ks⟨ks⟨ks⟨f⟩ls ⊙ ls⟨g⟩[m]⟩[m]⟩ms ⊕ ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms"
      by (simp add: restrict_times)
    also have "... = ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms"
      using 1 by (metis restrict_disjoint_left restrict_disjoint_right matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_left)
    finally show ?thesis
      .
  qed
  have "(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms) = (k#ks)⟨h⟩(m#ms) ⟷ (k#ks)⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩(m#ms) = (k#ks)⟨h⟩(m#ms)"
    by (simp add: restrict_times)
  also have "... ⟷ [k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] = [k]⟨h⟩[m] ∧ [k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms = [k]⟨h⟩ms ∧ ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] = ks⟨h⟩[m] ∧ ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms = ks⟨h⟩ms"
    by (meson restrict_nonempty_eq)
  also have "... ⟷ [k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m] = [k]⟨h⟩[m] ∧ [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms = [k]⟨h⟩ms ∧ ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m] = ks⟨h⟩[m] ∧ ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms = ks⟨h⟩ms"
    using 2 3 4 5 by simp
  finally show ?thesis
    by simp
qed

text ‹
The following lemma gives a componentwise characterisation of the inequality of a matrix and a product of two matrices.
›

lemma restrict_nonempty_product_less_eq:
  fixes f g h :: "('a::finite,'b::idempotent_semiring) square"
  assumes "¬ k ∈ set ks"
      and "¬ l ∈ set ls"
      and "¬ m ∈ set ms"
    shows "(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms) ≼ (k#ks)⟨h⟩(m#ms) ⟷ [k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m] ≼ [k]⟨h⟩[m] ∧ [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms ≼ [k]⟨h⟩ms ∧ ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m] ≼ ks⟨h⟩[m] ∧ ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms ≼ ks⟨h⟩ms"
proof -
  have 1: "[k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] = [k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m]"
    by (metis assms restrict_nonempty_product_eq restrict_times)
  have 2: "[k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms = [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms"
    by (metis assms restrict_nonempty_product_eq restrict_times)
  have 3: "ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] = ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m]"
    by (metis assms restrict_nonempty_product_eq restrict_times)
  have 4: "ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms = ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms"
    by (metis assms restrict_nonempty_product_eq restrict_times)
  have "(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms) ≼ (k#ks)⟨h⟩(m#ms) ⟷ (k#ks)⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩(m#ms) ≼ (k#ks)⟨h⟩(m#ms)"
    by (simp add: restrict_times)
  also have "... ⟷ [k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] ≼ [k]⟨h⟩[m] ∧ [k]⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms ≼ [k]⟨h⟩ms ∧ ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩[m] ≼ ks⟨h⟩[m] ∧ ks⟨(k#ks)⟨f⟩(l#ls) ⊙ (l#ls)⟨g⟩(m#ms)⟩ms ≼ ks⟨h⟩ms"
    by (meson restrict_nonempty_less_eq)
  also have "... ⟷ [k]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩[m] ≼ [k]⟨h⟩[m] ∧ [k]⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ [k]⟨f⟩ls ⊙ ls⟨g⟩ms ≼ [k]⟨h⟩ms ∧ ks⟨f⟩[l] ⊙ [l]⟨g⟩[m] ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩[m] ≼ ks⟨h⟩[m] ∧ ks⟨f⟩[l] ⊙ [l]⟨g⟩ms ⊕ ks⟨f⟩ls ⊙ ls⟨g⟩ms ≼ ks⟨h⟩ms"
    using 1 2 3 4 by simp
  finally show ?thesis
    by simp
qed

text ‹
The Kleene star induction laws hold for matrices with a single entry on the diagonal.
The matrix ‹g› can actually contain a whole row/colum at the appropriate index.
›

lemma restrict_star_left_induct:
  fixes f g :: "('a::finite,'b::kleene_algebra) square"
  shows "distinct ms ⟹ [l]⟨f⟩[l] ⊙ [l]⟨g⟩ms ≼ [l]⟨g⟩ms ⟹ [l]⟨star o f⟩[l] ⊙ [l]⟨g⟩ms ≼ [l]⟨g⟩ms"
proof (induct ms)
  case Nil thus ?case
    by (simp add: restrict_empty_right)
next
  case (Cons m ms)
  assume 1: "distinct ms ⟹ [l]⟨f⟩[l] ⊙ [l]⟨g⟩ms ≼ [l]⟨g⟩ms ⟹ [l]⟨star o f⟩[l] ⊙ [l]⟨g⟩ms ≼ [l]⟨g⟩ms"
  assume 2: "distinct (m#ms)"
  assume 3: "[l]⟨f⟩[l] ⊙ [l]⟨g⟩(m#ms) ≼ [l]⟨g⟩(m#ms)"
  have 4: "[l]⟨f⟩[l] ⊙ [l]⟨g⟩[m] ≼ [l]⟨g⟩[m] ∧ [l]⟨f⟩[l] ⊙ [l]⟨g⟩ms ≼ [l]⟨g⟩ms"
    using 2 3
    by (metis distinct.simps(2) distinct_singleton matrix_semilattice_sup.le_sup_iff
        restrict_nonempty_product_less_eq)
  hence 5: "[l]⟨star o f⟩[l] ⊙ [l]⟨g⟩ms ≼ [l]⟨g⟩ms"
    using 1 2 by simp
  have "f (l,l) * g (l,m) ≤ g (l,m)"
    using 4 by (metis restrict_singleton_product restrict_singleton less_eq_matrix_def)
  hence 6: "(f (l,l))⇧⋆ * g (l,m) ≤ g (l,m)"
    by (simp add: star_left_induct_mult)
  have "[l]⟨star o f⟩[l] ⊙ [l]⟨g⟩[m] ≼ [l]⟨g⟩[m]"
  proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
    fix i j
    have "([l]⟨star o f⟩[l] ⊙ [l]⟨g⟩[m]) (i,j) = (⨆⇩k ([l]⟨star o f⟩[l]) (i,k) * ([l]⟨g⟩[m]) (k,j))"
      by (simp add: times_matrix_def)
    also have "... = (⨆⇩k (if i = l ∧ k = l then (f (i,k))⇧⋆ else bot) * (if k = l ∧ j = m then g (k,j) else bot))"
      by (simp add: restrict_singleton o_def)
    also have "... = (⨆⇩k if k = l then (if i = l then (f (i,k))⇧⋆ else bot) * (if j = m then g (k,j) else bot) else bot)"
      by (rule sup_monoid.sum.cong) auto
    also have "... = (if i = l then (f (i,l))⇧⋆ else bot) * (if j = m then g (l,j) else bot)"
      by simp
    also have "... = (if i = l ∧ j = m then (f (l,l))⇧⋆ * g (l,m) else bot)"
      by simp
    also have "... ≤ ([l]⟨g⟩[m]) (i,j)"
      using 6 by (simp add: restrict_singleton)
    finally show "([l]⟨star o f⟩[l] ⊙ [l]⟨g⟩[m]) (i,j) ≤ ([l]⟨g⟩[m]) (i,j)"
      .
  qed
  thus "[l]⟨star o f⟩[l] ⊙ [l]⟨g⟩(m#ms) ≼ [l]⟨g⟩(m#ms)"
    using 2 5 by (metis (no_types, opaque_lifting) matrix_idempotent_semiring.mult_left_dist_sup matrix_semilattice_sup.sup.mono restrict_nonempty_right)
qed

lemma restrict_star_right_induct:
  fixes f g :: "('a::finite,'b::kleene_algebra) square"
  shows "distinct ms ⟹ ms⟨g⟩[l] ⊙ [l]⟨f⟩[l] ≼ ms⟨g⟩[l] ⟹ ms⟨g⟩[l] ⊙ [l]⟨star o f⟩[l] ≼ ms⟨g⟩[l]"
proof (induct ms)
  case Nil thus ?case
    by (simp add: restrict_empty_left)
next
  case (Cons m ms)
  assume 1: "distinct ms ⟹ ms⟨g⟩[l] ⊙ [l]⟨f⟩[l] ≼ ms⟨g⟩[l] ⟹ ms⟨g⟩[l] ⊙ [l]⟨star o f⟩[l] ≼ ms⟨g⟩[l]"
  assume 2: "distinct (m#ms)"
  assume 3: "(m#ms)⟨g⟩[l] ⊙ [l]⟨f⟩[l] ≼ (m#ms)⟨g⟩[l]"
  have 4: "[m]⟨g⟩[l] ⊙ [l]⟨f⟩[l] ≼ [m]⟨g⟩[l] ∧ ms⟨g⟩[l] ⊙ [l]⟨f⟩[l] ≼ ms⟨g⟩[l]"
    using 2 3
    by (metis distinct.simps(2) distinct_singleton matrix_semilattice_sup.le_sup_iff
        restrict_nonempty_product_less_eq) 
  hence 5: "ms⟨g⟩[l] ⊙ [l]⟨star o f⟩[l] ≼ ms⟨g⟩[l]"
    using 1 2  by simp
  have "g (m,l) * f (l,l) ≤ g (m,l)"
    using 4 by (metis restrict_singleton_product restrict_singleton less_eq_matrix_def)
  hence 6: "g (m,l) * (f (l,l))⇧⋆ ≤ g (m,l)"
    by (simp add: star_right_induct_mult)
  have "[m]⟨g⟩[l] ⊙ [l]⟨star o f⟩[l] ≼ [m]⟨g⟩[l]"
  proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
    fix i j
    have "([m]⟨g⟩[l] ⊙ [l]⟨star o f⟩[l]) (i,j) = (⨆⇩k ([m]⟨g⟩[l]) (i,k) * ([l]⟨star o f⟩[l]) (k,j))"
      by (simp add: times_matrix_def)
    also have "... = (⨆⇩k (if i = m ∧ k = l then g (i,k) else bot) * (if k = l ∧ j = l then (f (k,j))⇧⋆ else bot))"
      by (simp add: restrict_singleton o_def)
    also have "... = (⨆⇩k if k = l then (if i = m then g (i,k) else bot) * (if j = l then (f (k,j))⇧⋆ else bot) else bot)"
      by (rule sup_monoid.sum.cong) auto
    also have "... = (if i = m then g (i,l) else bot) * (if j = l then (f (l,j))⇧⋆ else bot)"
      by simp
    also have "... = (if i = m ∧ j = l then g (m,l) * (f (l,l))⇧⋆ else bot)"
      by simp
    also have "... ≤ ([m]⟨g⟩[l]) (i,j)"
      using 6 by (simp add: restrict_singleton)
    finally show "([m]⟨g⟩[l] ⊙ [l]⟨star o f⟩[l]) (i,j) ≤ ([m]⟨g⟩[l]) (i,j)"
      .
  qed
  thus "(m#ms)⟨g⟩[l] ⊙ [l]⟨star o f⟩[l] ≼ (m#ms)⟨g⟩[l]"
    using 2 5
    by (metis matrix_idempotent_semiring.mult_right_dist_sup
        matrix_idempotent_semiring.semiring.add_mono restrict_nonempty_left) 
qed

lemma restrict_pp:
  fixes f :: "('a,'b::p_algebra) square"
  shows "ks⟨⊖⊖f⟩ls = ⊖⊖(ks⟨f⟩ls)"
  by (unfold restrict_matrix_def uminus_matrix_def) auto

lemma pp_star_commute:
  fixes f :: "('a,'b::stone_kleene_relation_algebra) square"
  shows "⊖⊖(star o f) = star o ⊖⊖f"
  by (simp add: uminus_matrix_def o_def pp_dist_star)

subsection ‹Matrices form a Kleene Algebra›

text ‹
Matrices over Kleene algebras form a Kleene algebra using Conway's construction.
It remains to prove one unfold and two induction axioms of the Kleene star.
Each proof is by induction over the size of the matrix represented by an index list.
›

interpretation matrix_kleene_algebra: kleene_algebra_var where sup = sup_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix::('a::enum,'b::kleene_algebra) square" and one = one_matrix and times = times_matrix and star = star_matrix
proof
  fix y :: "('a,'b) square"
  let ?e = "enum_class.enum::'a list"
  let ?o = "mone :: ('a,'b) square"
  have "∀g :: ('a,'b) square . distinct ?e ⟶ (?e⟨?o⟩?e ⊕ ?e⟨g⟩?e ⊙ star_matrix' ?e g) = (star_matrix' ?e g)"
  proof (induct rule: list.induct)
    case Nil thus ?case
      by (simp add: restrict_empty_left)
  next
    case (Cons k s)
    let ?t = "k#s"
    assume 1: "∀g :: ('a,'b) square . distinct s ⟶ (s⟨?o⟩s ⊕ s⟨g⟩s ⊙ star_matrix' s g) = (star_matrix' s g)"
    show "∀g :: ('a,'b) square . distinct ?t ⟶ (?t⟨?o⟩?t ⊕ ?t⟨g⟩?t ⊙ star_matrix' ?t g) = (star_matrix' ?t g)"
    proof (rule allI, rule impI)
      fix g :: "('a,'b) square"
      assume 2: "distinct ?t"
      let ?r = "[k]"
      let ?a = "?r⟨g⟩?r"
      let ?b = "?r⟨g⟩s"
      let ?c = "s⟨g⟩?r"
      let ?d = "s⟨g⟩s"
      let ?as = "?r⟨star o ?a⟩?r"
      let ?ds = "star_matrix' s ?d"
      let ?e = "?a ⊕ ?b ⊙ ?ds ⊙ ?c"
      let ?es = "?r⟨star o ?e⟩?r"
      let ?f = "?d ⊕ ?c ⊙ ?as ⊙ ?b"
      let ?fs = "star_matrix' s ?f"
      have "s⟨?ds⟩s = ?ds ∧ s⟨?fs⟩s = ?fs"
        by (simp add: restrict_star)
      hence 3: "?r⟨?e⟩?r = ?e ∧ s⟨?f⟩s = ?f"
        by (metis (no_types, lifting) restrict_one_left_unit restrict_sup restrict_times)
      have 4: "disjoint s ?r ∧ disjoint ?r s"
        using 2 by simp
      hence 5: "?t⟨?o⟩?t = ?r⟨?o⟩?r ⊕ s⟨?o⟩s"
        by (auto intro: restrict_one)
      have 6: "?t⟨g⟩?t ⊙ ?es = ?a ⊙ ?es ⊕ ?c ⊙ ?es"
      proof -
        have "?t⟨g⟩?t ⊙ ?es = (?a ⊕ ?b ⊕ ?c ⊕ ?d) ⊙ ?es"
          by (metis restrict_nonempty)
        also have "... = ?a ⊙ ?es ⊕ ?b ⊙ ?es ⊕ ?c ⊙ ?es ⊕ ?d ⊙ ?es"
          by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
        also have "... = ?a ⊙ ?es ⊕ ?c ⊙ ?es"
          using 4 by (simp add: times_disjoint)
        finally show ?thesis
          .
      qed
      have 7: "?t⟨g⟩?t ⊙ ?as ⊙ ?b ⊙ ?fs = ?a ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?c ⊙ ?as ⊙ ?b ⊙ ?fs"
      proof -
        have "?t⟨g⟩?t ⊙ ?as ⊙ ?b ⊙ ?fs = (?a ⊕ ?b ⊕ ?c ⊕ ?d) ⊙ ?as ⊙ ?b ⊙ ?fs"
          by (metis restrict_nonempty)
        also have "... = ?a ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?b ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?c ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?d ⊙ ?as ⊙ ?b ⊙ ?fs"
          by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
        also have "... = ?a ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?c ⊙ ?as ⊙ ?b ⊙ ?fs"
          using 4 by (simp add: times_disjoint)
        finally show ?thesis
          .
      qed
      have 8: "?t⟨g⟩?t ⊙ ?ds ⊙ ?c ⊙ ?es = ?b ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?d ⊙ ?ds ⊙ ?c ⊙ ?es"
      proof -
        have "?t⟨g⟩?t ⊙ ?ds ⊙ ?c ⊙ ?es = (?a ⊕ ?b ⊕ ?c ⊕ ?d) ⊙ ?ds ⊙ ?c ⊙ ?es"
          by (metis restrict_nonempty)
        also have "... = ?a ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?b ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?c ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?d ⊙ ?ds ⊙ ?c ⊙ ?es"
          by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
        also have "... = ?b ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?d ⊙ ?ds ⊙ ?c ⊙ ?es"
          using 4 by (metis (no_types, lifting) times_disjoint matrix_idempotent_semiring.mult_left_zero restrict_star matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_right matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_left)
        finally show ?thesis
          .
      qed
      have 9: "?t⟨g⟩?t ⊙ ?fs = ?b ⊙ ?fs ⊕ ?d ⊙ ?fs"
      proof -
        have "?t⟨g⟩?t ⊙ ?fs = (?a ⊕ ?b ⊕ ?c ⊕ ?d) ⊙ ?fs"
          by (metis restrict_nonempty)
        also have "... = ?a ⊙ ?fs ⊕ ?b ⊙ ?fs ⊕ ?c ⊙ ?fs ⊕ ?d ⊙ ?fs"
          by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
        also have "... = ?b ⊙ ?fs ⊕ ?d ⊙ ?fs"
          using 4 by (metis (no_types, lifting) times_disjoint restrict_star matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_right matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_left)
        finally show ?thesis
          .
      qed
      have "?t⟨?o⟩?t ⊕ ?t⟨g⟩?t ⊙ star_matrix' ?t g = ?t⟨?o⟩?t ⊕ ?t⟨g⟩?t ⊙ (?es ⊕ ?as ⊙ ?b ⊙ ?fs ⊕ ?ds ⊙ ?c ⊙ ?es ⊕ ?fs)"
        by (metis star_matrix'.simps(2))
      also have "... = ?t⟨?o⟩?t ⊕ ?t⟨g⟩?t ⊙ ?es ⊕ ?t⟨g⟩?t ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?t⟨g⟩?t ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?t⟨g⟩?t ⊙ ?fs"
        by (simp add: matrix_idempotent_semiring.mult_left_dist_sup matrix_monoid.mult_assoc matrix_semilattice_sup.sup_assoc)
      also have "... = ?r⟨?o⟩?r ⊕ s⟨?o⟩s ⊕ ?a ⊙ ?es ⊕ ?c ⊙ ?es ⊕ ?a ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?c ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?b ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?d ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?b ⊙ ?fs ⊕ ?d ⊙ ?fs"
        using 5 6 7 8 9 by (simp add: matrix_semilattice_sup.sup.assoc)
      also have "... = (?r⟨?o⟩?r ⊕ (?a ⊙ ?es ⊕ ?b ⊙ ?ds ⊙ ?c ⊙ ?es)) ⊕ (?b ⊙ ?fs ⊕ ?a ⊙ ?as ⊙ ?b ⊙ ?fs) ⊕ (?c ⊙ ?es ⊕ ?d ⊙ ?ds ⊙ ?c ⊙ ?es) ⊕ (s⟨?o⟩s ⊕ (?d ⊙ ?fs ⊕ ?c ⊙ ?as ⊙ ?b ⊙ ?fs))"
        by (simp only: matrix_semilattice_sup.sup_assoc matrix_semilattice_sup.sup_commute matrix_semilattice_sup.sup_left_commute)
      also have "... = (?r⟨?o⟩?r ⊕ (?a ⊙ ?es ⊕ ?b ⊙ ?ds ⊙ ?c ⊙ ?es)) ⊕ (?r⟨?o⟩?r ⊙ ?b ⊙ ?fs ⊕ ?a ⊙ ?as ⊙ ?b ⊙ ?fs) ⊕ (s⟨?o⟩s ⊙ ?c ⊙ ?es ⊕ ?d ⊙ ?ds ⊙ ?c ⊙ ?es) ⊕ (s⟨?o⟩s ⊕ (?d ⊙ ?fs ⊕ ?c ⊙ ?as ⊙ ?b ⊙ ?fs))"
        by (simp add: restrict_one_left_unit)
      also have "... = (?r⟨?o⟩?r ⊕ ?e ⊙ ?es) ⊕ ((?r⟨?o⟩?r ⊕ ?a ⊙ ?as) ⊙ ?b ⊙ ?fs) ⊕ ((s⟨?o⟩s ⊕ ?d ⊙ ?ds) ⊙ ?c ⊙ ?es) ⊕ (s⟨?o⟩s ⊕ ?f ⊙ ?fs)"
        by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
      also have "... = (?r⟨?o⟩?r ⊕ ?e ⊙ ?es) ⊕ ((?r⟨?o⟩?r ⊕ ?a ⊙ ?as) ⊙ ?b ⊙ ?fs) ⊕ ((s⟨?o⟩s ⊕ ?d ⊙ ?ds) ⊙ ?c ⊙ ?es) ⊕ ?fs"
        using 1 2 3 by (metis distinct.simps(2))
      also have "... = (?r⟨?o⟩?r ⊕ ?e ⊙ ?es) ⊕ ((?r⟨?o⟩?r ⊕ ?a ⊙ ?as) ⊙ ?b ⊙ ?fs) ⊕ (?ds ⊙ ?c ⊙ ?es) ⊕ ?fs"
        using 1 2
        by (metis distinct.simps(2) restrict_one_left_unit restrict_times) 
      also have "... = ?es ⊕ ((?r⟨?o⟩?r ⊕ ?a ⊙ ?as) ⊙ ?b ⊙ ?fs) ⊕ (?ds ⊙ ?c ⊙ ?es) ⊕ ?fs"
        using 3 by (metis restrict_star_unfold)
      also have "... = ?es ⊕ ?as ⊙ ?b ⊙ ?fs ⊕ ?ds ⊙ ?c ⊙ ?es ⊕ ?fs"
        by (metis (no_types, lifting) restrict_one_left_unit restrict_star_unfold restrict_times)
      also have "... = star_matrix' ?t g"
        by (metis star_matrix'.simps(2))
      finally show "?t⟨?o⟩?t ⊕ ?t⟨g⟩?t ⊙ star_matrix' ?t g = star_matrix' ?t g"
        .
    qed
  qed
  thus "?o ⊕ y ⊙ y⇧⊙ ≼ y⇧⊙"
    by (simp add: enum_distinct restrict_all)
next
  fix x y z :: "('a,'b) square"
  let ?e = "enum_class.enum::'a list"
  have "∀g h :: ('a,'b) square . ∀zs . distinct ?e ∧ distinct zs ⟶ (?e⟨g⟩?e ⊙ ?e⟨h⟩zs ≼ ?e⟨h⟩zs ⟶ star_matrix' ?e g ⊙ ?e⟨h⟩zs ≼ ?e⟨h⟩zs)"
  proof (induct rule: list.induct)
    case Nil thus ?case
      by (simp add: restrict_empty_left)
    case (Cons k s)
    let ?t = "k#s"
    assume 1: "∀g h :: ('a,'b) square . ∀zs . distinct s ∧ distinct zs ⟶ (s⟨g⟩s ⊙ s⟨h⟩zs ≼ s⟨h⟩zs ⟶ star_matrix' s g ⊙ s⟨h⟩zs ≼ s⟨h⟩zs)"
    show "∀g h :: ('a,'b) square . ∀zs . distinct ?t ∧ distinct zs ⟶ (?t⟨g⟩?t ⊙ ?t⟨h⟩zs ≼ ?t⟨h⟩zs ⟶ star_matrix' ?t g ⊙ ?t⟨h⟩zs ≼ ?t⟨h⟩zs)"
    proof (intro allI)
      fix g h :: "('a,'b) square"
      fix zs :: "'a list"
      show "distinct ?t ∧ distinct zs ⟶ (?t⟨g⟩?t ⊙ ?t⟨h⟩zs ≼ ?t⟨h⟩zs ⟶ star_matrix' ?t g ⊙ ?t⟨h⟩zs ≼ ?t⟨h⟩zs)"
      proof (cases zs)
        case Nil thus ?thesis
          by (metis restrict_empty_right restrict_star restrict_times)
      next
        case (Cons y ys)
        assume 2: "zs = y#ys"
        show "distinct ?t ∧ distinct zs ⟶ (?t⟨g⟩?t ⊙ ?t⟨h⟩zs ≼ ?t⟨h⟩zs ⟶ star_matrix' ?t g ⊙ ?t⟨h⟩zs ≼ ?t⟨h⟩zs)"
        proof (intro impI)
          let ?y = "[y]"
          assume 3: "distinct ?t ∧ distinct zs"
          hence 4: "distinct s ∧ distinct ys ∧ ¬ k ∈ set s ∧ ¬ y ∈ set ys"
            using 2 by simp
          let ?r = "[k]"
          let ?a = "?r⟨g⟩?r"
          let ?b = "?r⟨g⟩s"
          let ?c = "s⟨g⟩?r"
          let ?d = "s⟨g⟩s"
          let ?as = "?r⟨star o ?a⟩?r"
          let ?ds = "star_matrix' s ?d"
          let ?e = "?a ⊕ ?b ⊙ ?ds ⊙ ?c"
          let ?es = "?r⟨star o ?e⟩?r"
          let ?f = "?d ⊕ ?c ⊙ ?as ⊙ ?b"
          let ?fs = "star_matrix' s ?f"
          let ?ha = "?r⟨h⟩?y"
          let ?hb = "?r⟨h⟩ys"
          let ?hc = "s⟨h⟩?y"
          let ?hd = "s⟨h⟩ys"
          assume "?t⟨g⟩?t ⊙ ?t⟨h⟩zs ≼ ?t⟨h⟩zs"
          hence 5: "?a ⊙ ?ha ⊕ ?b ⊙ ?hc ≼ ?ha ∧ ?a ⊙ ?hb ⊕ ?b ⊙ ?hd ≼ ?hb ∧ ?c ⊙ ?ha ⊕ ?d ⊙ ?hc ≼ ?hc ∧ ?c ⊙ ?hb ⊕ ?d ⊙ ?hd ≼ ?hd"
            using 2 3 4 by simp
              (meson matrix_semilattice_sup.le_sup_iff restrict_nonempty_product_less_eq) 
          have 6: "s⟨?ds⟩s = ?ds ∧ s⟨?fs⟩s = ?fs"
            by (simp add: restrict_star)
          hence 7: "?r⟨?e⟩?r = ?e ∧ s⟨?f⟩s = ?f"
            by (metis (no_types, lifting) restrict_one_left_unit restrict_sup restrict_times)
          have 8: "disjoint s ?r ∧ disjoint ?r s"
            using 3 by simp
          have 9: "?es ⊙ ?t⟨h⟩zs = ?es ⊙ ?ha ⊕ ?es ⊙ ?hb"
          proof -
            have "?es ⊙ ?t⟨h⟩zs = ?es ⊙ (?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd)"
              using 2 by (metis restrict_nonempty)
            also have "... = ?es ⊙ ?ha ⊕ ?es ⊙ ?hb ⊕ ?es ⊙ ?hc ⊕ ?es ⊙ ?hd"
              by (simp add: matrix_idempotent_semiring.mult_left_dist_sup)
            also have "... = ?es ⊙ ?ha ⊕ ?es ⊙ ?hb"
              using 8 by (simp add: times_disjoint)
            finally show ?thesis
              .
          qed
          have 10: "?as ⊙ ?b ⊙ ?fs ⊙ ?t⟨h⟩zs = ?as ⊙ ?b ⊙ ?fs ⊙ ?hc ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hd"
          proof -
            have "?as ⊙ ?b ⊙ ?fs ⊙ ?t⟨h⟩zs = ?as ⊙ ?b ⊙ ?fs ⊙ (?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd)"
              using 2 by (metis restrict_nonempty)
            also have "... = ?as ⊙ ?b ⊙ ?fs ⊙ ?ha ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hb ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hc ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hd"
              by (simp add: matrix_idempotent_semiring.mult_left_dist_sup)
            also have "... = ?as ⊙ ?b ⊙ (?fs ⊙ ?ha) ⊕ ?as ⊙ ?b ⊙ (?fs ⊙ ?hb) ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hc ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hd"
              by (simp add: matrix_monoid.mult_assoc)
            also have "... = ?as ⊙ ?b ⊙ mbot ⊕ ?as ⊙ ?b ⊙ mbot ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hc ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hd"
              using 6 8 by (metis (no_types) times_disjoint)
            also have "... = ?as ⊙ ?b ⊙ ?fs ⊙ ?hc ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hd"
              by simp
            finally show ?thesis
              .
          qed
          have 11: "?ds ⊙ ?c ⊙ ?es ⊙ ?t⟨h⟩zs = ?ds ⊙ ?c ⊙ ?es ⊙ ?ha ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?hb"
          proof -
            have "?ds ⊙ ?c ⊙ ?es ⊙ ?t⟨h⟩zs = ?ds ⊙ ?c ⊙ ?es ⊙ (?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd)"
              using 2 by (metis restrict_nonempty)
            also have "... = ?ds ⊙ ?c ⊙ ?es ⊙ ?ha ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?hb ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?hc ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?hd"
              by (simp add: matrix_idempotent_semiring.mult_left_dist_sup)
            also have "... = ?ds ⊙ ?c ⊙ ?es ⊙ ?ha ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?hb ⊕ ?ds ⊙ ?c ⊙ (?es ⊙ ?hc) ⊕ ?ds ⊙ ?c ⊙ (?es ⊙ ?hd)"
              by (simp add: matrix_monoid.mult_assoc)
            also have "... = ?ds ⊙ ?c ⊙ ?es ⊙ ?ha ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?hb ⊕ ?ds ⊙ ?c ⊙ mbot ⊕ ?ds ⊙ ?c ⊙ mbot"
              using 8 by (metis times_disjoint)
            also have "... = ?ds ⊙ ?c ⊙ ?es ⊙ ?ha ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?hb"
              by simp
            finally show ?thesis
              .
          qed
          have 12: "?fs ⊙ ?t⟨h⟩zs = ?fs ⊙ ?hc ⊕ ?fs ⊙ ?hd"
          proof -
            have "?fs ⊙ ?t⟨h⟩zs = ?fs ⊙ (?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd)"
              using 2 by (metis restrict_nonempty)
            also have "... = ?fs ⊙ ?ha ⊕ ?fs ⊙ ?hb ⊕ ?fs ⊙ ?hc ⊕ ?fs ⊙ ?hd"
              by (simp add: matrix_idempotent_semiring.mult_left_dist_sup)
            also have "... = ?fs ⊙ ?hc ⊕ ?fs ⊙ ?hd"
              using 6 8 by (metis (no_types) times_disjoint matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_left)
            finally show ?thesis
              .
          qed
          have 13: "?es ⊙ ?ha ≼ ?ha"
          proof -
            have "?b ⊙ ?ds ⊙ ?c ⊙ ?ha ≼ ?b ⊙ ?ds ⊙ ?hc"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?b ⊙ ?hc"
              using 1 3 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc restrict_sublist)
            also have "... ≼ ?ha"
              using 5 by simp
            finally have "?e ⊙ ?ha ≼ ?ha"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
            thus ?thesis
              using 7 by (simp add: restrict_star_left_induct)
          qed
          have 14: "?es ⊙ ?hb ≼ ?hb"
          proof -
            have "?b ⊙ ?ds ⊙ ?c ⊙ ?hb ≼ ?b ⊙ ?ds ⊙ ?hd"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?b ⊙ ?hd"
              using 1 4 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc restrict_sublist)
            also have "... ≼ ?hb"
              using 5 by simp
            finally have "?e ⊙ ?hb ≼ ?hb"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
            thus ?thesis
              using 4 7 by (simp add: restrict_star_left_induct)
          qed
          have 15: "?fs ⊙ ?hc ≼ ?hc"
          proof -
            have "?c ⊙ ?as ⊙ ?b ⊙ ?hc ≼ ?c ⊙ ?as ⊙ ?ha"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?c ⊙ ?ha"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc restrict_star_left_induct restrict_sublist)
            also have "... ≼ ?hc"
              using 5 by simp
            finally have "?f ⊙ ?hc ≼ ?hc"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
            thus ?thesis
              using 1 3 7 by simp
          qed
          have 16: "?fs ⊙ ?hd ≼ ?hd"
          proof -
            have "?c ⊙ ?as ⊙ ?b ⊙ ?hd ≼ ?c ⊙ ?as ⊙ ?hb"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?c ⊙ ?hb"
              using 4 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc restrict_star_left_induct restrict_sublist)
            also have "... ≼ ?hd"
              using 5 by simp
            finally have "?f ⊙ ?hd ≼ ?hd"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
            thus ?thesis
              using 1 4 7 by simp
          qed
          have 17: "?as ⊙ ?b ⊙ ?fs ⊙ ?hc ≼ ?ha"
          proof -
            have "?as ⊙ ?b ⊙ ?fs ⊙ ?hc ≼ ?as ⊙ ?b ⊙ ?hc"
              using 15 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?as ⊙ ?ha"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?ha"
              using 5 by (simp add: restrict_star_left_induct restrict_sublist)
            finally show ?thesis
              .
          qed
          have 18: "?as ⊙ ?b ⊙ ?fs ⊙ ?hd ≼ ?hb"
          proof -
            have "?as ⊙ ?b ⊙ ?fs ⊙ ?hd ≼ ?as ⊙ ?b ⊙ ?hd"
              using 16 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?as ⊙ ?hb"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?hb"
              using 4 5 by (simp add: restrict_star_left_induct restrict_sublist)
            finally show ?thesis
              .
          qed
          have 19: "?ds ⊙ ?c ⊙ ?es ⊙ ?ha ≼ ?hc"
          proof -
            have "?ds ⊙ ?c ⊙ ?es ⊙ ?ha ≼ ?ds ⊙ ?c ⊙ ?ha"
              using 13 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?ds ⊙ ?hc"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?hc"
              using 1 3 5 by (simp add: restrict_sublist)
            finally show ?thesis
              .
          qed
          have 20: "?ds ⊙ ?c ⊙ ?es ⊙ ?hb ≼ ?hd"
          proof -
            have "?ds ⊙ ?c ⊙ ?es ⊙ ?hb ≼ ?ds ⊙ ?c ⊙ ?hb"
              using 14 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?ds ⊙ ?hd"
              using 5 by (simp add: matrix_idempotent_semiring.mult_right_isotone matrix_monoid.mult_assoc)
            also have "... ≼ ?hd"
              using 1 4 5 by (simp add: restrict_sublist)
            finally show ?thesis
              .
          qed
          have 21: "?es ⊙ ?ha ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hc ≼ ?ha"
            using 13 17 matrix_semilattice_sup.le_supI by blast
          have 22: "?es ⊙ ?hb ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hd ≼ ?hb"
            using 14 18 matrix_semilattice_sup.le_supI by blast
          have 23: "?ds ⊙ ?c ⊙ ?es ⊙ ?ha ⊕ ?fs ⊙ ?hc ≼ ?hc"
            using 15 19 matrix_semilattice_sup.le_supI by blast
          have 24: "?ds ⊙ ?c ⊙ ?es ⊙ ?hb ⊕ ?fs ⊙ ?hd ≼ ?hd"
            using 16 20 matrix_semilattice_sup.le_supI by blast
          have "star_matrix' ?t g ⊙ ?t⟨h⟩zs = (?es ⊕ ?as ⊙ ?b ⊙ ?fs ⊕ ?ds ⊙ ?c ⊙ ?es ⊕ ?fs) ⊙ ?t⟨h⟩zs"
            by (metis star_matrix'.simps(2))
          also have "... = ?es ⊙ ?t⟨h⟩zs ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?t⟨h⟩zs ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?t⟨h⟩zs ⊕ ?fs ⊙ ?t⟨h⟩zs"
            by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
          also have "... = ?es ⊙ ?ha ⊕ ?es ⊙ ?hb ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hc ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hd ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?ha ⊕ ?ds ⊙ ?c ⊙ ?es ⊙ ?hb ⊕ ?fs ⊙ ?hc ⊕ ?fs ⊙ ?hd"
            using 9 10 11 12 by (simp only: matrix_semilattice_sup.sup_assoc)
          also have "... = (?es ⊙ ?ha ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hc) ⊕ (?es ⊙ ?hb ⊕ ?as ⊙ ?b ⊙ ?fs ⊙ ?hd) ⊕ (?ds ⊙ ?c ⊙ ?es ⊙ ?ha ⊕ ?fs ⊙ ?hc) ⊕ (?ds ⊙ ?c ⊙ ?es ⊙ ?hb ⊕ ?fs ⊙ ?hd)"
            by (simp only: matrix_semilattice_sup.sup_assoc matrix_semilattice_sup.sup_commute matrix_semilattice_sup.sup_left_commute)
          also have "... ≼ ?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd"
            using 21 22 23 24 matrix_semilattice_sup.sup.mono by blast
          also have "... = ?t⟨h⟩zs"
            using 2 by (metis restrict_nonempty)
          finally show "star_matrix' ?t g ⊙ ?t⟨h⟩zs ≼ ?t⟨h⟩zs"
            .
        qed
      qed
    qed
  qed
  hence "∀zs . distinct zs ⟶ (y ⊙ ?e⟨x⟩zs ≼ ?e⟨x⟩zs ⟶ y⇧⊙ ⊙ ?e⟨x⟩zs ≼ ?e⟨x⟩zs)"
    by (simp add: enum_distinct restrict_all)
  thus "y ⊙ x ≼ x ⟶ y⇧⊙ ⊙ x ≼ x"
    by (metis restrict_all enum_distinct)
next
  fix x y z :: "('a,'b) square"
  let ?e = "enum_class.enum::'a list"
  have "∀g h :: ('a,'b) square . ∀zs . distinct ?e ∧ distinct zs ⟶ (zs⟨h⟩?e ⊙ ?e⟨g⟩?e ≼ zs⟨h⟩?e ⟶ zs⟨h⟩?e ⊙ star_matrix' ?e g ≼ zs⟨h⟩?e)"
  proof (induct rule:list.induct)
    case Nil thus ?case
      by (simp add: restrict_empty_left)
    case (Cons k s)
    let ?t = "k#s"
    assume 1: "∀g h :: ('a,'b) square . ∀zs . distinct s ∧ distinct zs ⟶ (zs⟨h⟩s ⊙ s⟨g⟩s ≼ zs⟨h⟩s ⟶ zs⟨h⟩s ⊙ star_matrix' s g ≼ zs⟨h⟩s)"
    show "∀g h :: ('a,'b) square . ∀zs . distinct ?t ∧ distinct zs ⟶ (zs⟨h⟩?t ⊙ ?t⟨g⟩?t ≼ zs⟨h⟩?t ⟶ zs⟨h⟩?t ⊙ star_matrix' ?t g ≼ zs⟨h⟩?t)"
    proof (intro allI)
      fix g h :: "('a,'b) square"
      fix zs :: "'a list"
      show "distinct ?t ∧ distinct zs ⟶ (zs⟨h⟩?t ⊙ ?t⟨g⟩?t ≼ zs⟨h⟩?t ⟶ zs⟨h⟩?t ⊙ star_matrix' ?t g ≼ zs⟨h⟩?t)"
      proof (cases zs)
        case Nil thus ?thesis
          by (metis restrict_empty_left restrict_star restrict_times)
      next
        case (Cons y ys)
        assume 2: "zs = y#ys"
        show "distinct ?t ∧ distinct zs ⟶ (zs⟨h⟩?t ⊙ ?t⟨g⟩?t ≼ zs⟨h⟩?t ⟶ zs⟨h⟩?t ⊙ star_matrix' ?t g ≼ zs⟨h⟩?t)"
        proof (intro impI)
          let ?y = "[y]"
          assume 3: "distinct ?t ∧ distinct zs"
          hence 4: "distinct s ∧ distinct ys ∧ ¬ k ∈ set s ∧ ¬ y ∈ set ys"
            using 2 by simp
          let ?r = "[k]"
          let ?a = "?r⟨g⟩?r"
          let ?b = "?r⟨g⟩s"
          let ?c = "s⟨g⟩?r"
          let ?d = "s⟨g⟩s"
          let ?as = "?r⟨star o ?a⟩?r"
          let ?ds = "star_matrix' s ?d"
          let ?e = "?a ⊕ ?b ⊙ ?ds ⊙ ?c"
          let ?es = "?r⟨star o ?e⟩?r"
          let ?f = "?d ⊕ ?c ⊙ ?as ⊙ ?b"
          let ?fs = "star_matrix' s ?f"
          let ?ha = "?y⟨h⟩?r"
          let ?hb = "?y⟨h⟩s"
          let ?hc = "ys⟨h⟩?r"
          let ?hd = "ys⟨h⟩s"
          assume "zs⟨h⟩?t ⊙ ?t⟨g⟩?t ≼ zs⟨h⟩?t"
          hence 5: "?ha ⊙ ?a ⊕ ?hb ⊙ ?c ≼ ?ha ∧ ?ha ⊙ ?b ⊕ ?hb ⊙ ?d ≼ ?hb ∧ ?hc ⊙ ?a ⊕ ?hd ⊙ ?c ≼ ?hc ∧ ?hc ⊙ ?b ⊕ ?hd ⊙ ?d ≼ ?hd"
            using 2 3 4
            using restrict_nonempty_product_less_eq by blast 
          have 6: "s⟨?ds⟩s = ?ds ∧ s⟨?fs⟩s = ?fs"
            by (simp add: restrict_star)
          hence 7: "?r⟨?e⟩?r = ?e ∧ s⟨?f⟩s = ?f"
            by (metis (no_types, lifting) restrict_one_left_unit restrict_sup restrict_times)
          have 8: "disjoint s ?r ∧ disjoint ?r s"
            using 3 by simp
          have 9: "zs⟨h⟩?t ⊙ ?es = ?ha ⊙ ?es ⊕ ?hc ⊙ ?es"
          proof -
            have "zs⟨h⟩?t ⊙ ?es = (?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd) ⊙ ?es"
              using 2 by (metis restrict_nonempty)
            also have "... = ?ha ⊙ ?es ⊕ ?hb ⊙ ?es ⊕ ?hc ⊙ ?es ⊕ ?hd ⊙ ?es"
              by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
            also have "... = ?ha ⊙ ?es ⊕ ?hc ⊙ ?es"
              using 8 by (simp add: times_disjoint)
            finally show ?thesis
              .
          qed
          have 10: "zs⟨h⟩?t ⊙ ?as ⊙ ?b ⊙ ?fs = ?ha ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hc ⊙ ?as ⊙ ?b ⊙ ?fs"
          proof -
            have "zs⟨h⟩?t ⊙ ?as ⊙ ?b ⊙ ?fs = (?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd) ⊙ ?as ⊙ ?b ⊙ ?fs"
              using 2 by (metis restrict_nonempty)
            also have "... = ?ha ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hb ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hc ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hd ⊙ ?as ⊙ ?b ⊙ ?fs"
              by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
            also have "... = ?ha ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ mbot ⊙ ?b ⊙ ?fs ⊕ ?hc ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ mbot ⊙ ?b ⊙ ?fs"
              using 8 by (metis (no_types) times_disjoint)
            also have "... = ?ha ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hc ⊙ ?as ⊙ ?b ⊙ ?fs"
              by simp
            finally show ?thesis
              .
          qed
          have 11: "zs⟨h⟩?t ⊙ ?ds ⊙ ?c ⊙ ?es = ?hb ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?hd ⊙ ?ds ⊙ ?c ⊙ ?es"
          proof -
            have "zs⟨h⟩?t ⊙ ?ds ⊙ ?c ⊙ ?es = (?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd) ⊙ ?ds ⊙ ?c ⊙ ?es"
              using 2 by (metis restrict_nonempty)
            also have "... = ?ha ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?hb ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?hc ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?hd ⊙ ?ds ⊙ ?c ⊙ ?es"
              by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
            also have "... = mbot ⊙ ?c ⊙ ?es ⊕ ?hb ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ mbot ⊙ ?c ⊙ ?es ⊕ ?hd ⊙ ?ds ⊙ ?c ⊙ ?es"
              using 6 8 by (metis (no_types) times_disjoint)
            also have "... = ?hb ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?hd ⊙ ?ds ⊙ ?c ⊙ ?es"
              by simp
            finally show ?thesis
              .
          qed
          have 12: "zs⟨h⟩?t ⊙ ?fs = ?hb ⊙ ?fs ⊕ ?hd ⊙ ?fs"
          proof -
            have "zs⟨h⟩?t ⊙ ?fs = (?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd) ⊙ ?fs"
              using 2 by (metis restrict_nonempty)
            also have "... = ?ha ⊙ ?fs ⊕ ?hb ⊙ ?fs ⊕ ?hc ⊙ ?fs ⊕ ?hd ⊙ ?fs"
              by (simp add: matrix_idempotent_semiring.mult_right_dist_sup)
            also have "... = ?hb ⊙ ?fs ⊕ ?hd ⊙ ?fs"
              using 6 8 by (metis (no_types) times_disjoint matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_right matrix_bounded_semilattice_sup_bot.sup_monoid.add_0_left)
            finally show ?thesis
              .
          qed
          have 13: "?ha ⊙ ?es ≼ ?ha"
          proof -
            have "?ha ⊙ ?b ⊙ ?ds ⊙ ?c ≼ ?hb ⊙ ?ds ⊙ ?c"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone)
            also have "... ≼ ?hb ⊙ ?c"
              using 1 4 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone restrict_sublist)
            also have "... ≼ ?ha"
              using 5 by simp
            finally have "?ha ⊙ ?e ≼ ?ha"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_dist_sup matrix_monoid.mult_assoc)
            thus ?thesis
              using 7 by (simp add: restrict_star_right_induct)
          qed
          have 14: "?hb ⊙ ?fs ≼ ?hb"
          proof -
            have "?hb ⊙ ?c ⊙ ?as ⊙ ?b ≼ ?ha ⊙ ?as ⊙ ?b"
              using 5 by (metis matrix_semilattice_sup.le_supE matrix_idempotent_semiring.mult_left_isotone)
            also have "... ≼ ?ha ⊙ ?b"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone restrict_star_right_induct restrict_sublist)
            also have "... ≼ ?hb"
              using 5 by simp
            finally have "?hb ⊙ ?f ≼ ?hb"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_dist_sup matrix_monoid.mult_assoc)
            thus ?thesis
              using 1 3 7 by simp
          qed
          have 15: "?hc ⊙ ?es ≼ ?hc"
          proof -
            have "?hc ⊙ ?b ⊙ ?ds ⊙ ?c ≼ ?hd ⊙ ?ds ⊙ ?c"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone)
            also have "... ≼ ?hd ⊙ ?c"
              using 1 4 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone restrict_sublist)
            also have "... ≼ ?hc"
              using 5 by simp
            finally have "?hc ⊙ ?e ≼ ?hc"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_dist_sup matrix_monoid.mult_assoc)
            thus ?thesis
              using 4 7 by (simp add: restrict_star_right_induct)
          qed
          have 16: "?hd ⊙ ?fs ≼ ?hd"
          proof -
            have "?hd ⊙ ?c ⊙ ?as ⊙ ?b ≼ ?hc ⊙ ?as ⊙ ?b"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone)
            also have "... ≼ ?hc ⊙ ?b"
              using 4 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone restrict_star_right_induct restrict_sublist)
            also have "... ≼ ?hd"
              using 5 by simp
            finally have "?hd ⊙ ?f ≼ ?hd"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_dist_sup matrix_monoid.mult_assoc)
            thus ?thesis
              using 1 4 7 by simp
          qed
          have 17: "?hb ⊙ ?ds ⊙ ?c ⊙ ?es ≼ ?ha"
          proof -
            have "?hb ⊙ ?ds ⊙ ?c ⊙ ?es ≼ ?hb ⊙ ?c ⊙ ?es"
              using 1 4 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone restrict_sublist)
            also have "... ≼ ?ha ⊙ ?es"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone)
            also have "... ≼ ?ha"
              using 13 by simp
            finally show ?thesis
              .
          qed
          have 18: "?ha ⊙ ?as ⊙ ?b ⊙ ?fs ≼ ?hb"
          proof -
            have "?ha ⊙ ?as ⊙ ?b ⊙ ?fs ≼ ?ha ⊙ ?b ⊙ ?fs"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone restrict_star_right_induct restrict_sublist)
            also have "... ≼ ?hb ⊙ ?fs"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone)
            also have "... ≼ ?hb"
              using 14 by simp
            finally show ?thesis
              by simp
          qed
          have 19: "?hd ⊙ ?ds ⊙ ?c ⊙ ?es ≼ ?hc"
          proof -
            have "?hd ⊙ ?ds ⊙ ?c ⊙ ?es ≼ ?hd ⊙ ?c ⊙ ?es"
              using 1 4 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone restrict_sublist)
            also have "... ≼ ?hc ⊙ ?es"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone)
            also have "... ≼ ?hc"
              using 15 by simp
            finally show ?thesis
              by simp
          qed
          have 20: "?hc ⊙ ?as ⊙ ?b ⊙ ?fs ≼ ?hd"
          proof -
            have "?hc ⊙ ?as ⊙ ?b ⊙ ?fs ≼ ?hc ⊙ ?b ⊙ ?fs"
              using 4 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone restrict_star_right_induct restrict_sublist)
            also have "... ≼ ?hd ⊙ ?fs"
              using 5 by (simp add: matrix_idempotent_semiring.mult_left_isotone)
            also have "... ≼ ?hd"
              using 16 by simp
            finally show ?thesis
              by simp
          qed
          have 21: "?ha ⊙ ?es ⊕ ?hb ⊙ ?ds ⊙ ?c ⊙ ?es ≼ ?ha"
            using 13 17 matrix_semilattice_sup.le_supI by blast
          have 22: "?ha ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hb ⊙ ?fs ≼ ?hb"
            using 14 18 matrix_semilattice_sup.le_supI by blast
          have 23: "?hc ⊙ ?es ⊕ ?hd ⊙ ?ds ⊙ ?c ⊙ ?es ≼ ?hc"
            using 15 19 matrix_semilattice_sup.le_supI by blast
          have 24: "?hc ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hd ⊙ ?fs ≼ ?hd"
            using 16 20 matrix_semilattice_sup.le_supI by blast
          have "zs⟨h⟩?t ⊙ star_matrix' ?t g = zs⟨h⟩?t ⊙ (?es ⊕ ?as ⊙ ?b ⊙ ?fs ⊕ ?ds ⊙ ?c ⊙ ?es ⊕ ?fs)"
            by (metis star_matrix'.simps(2))
          also have "... = zs⟨h⟩?t ⊙ ?es ⊕ zs⟨h⟩?t ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ zs⟨h⟩?t ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ zs⟨h⟩?t ⊙ ?fs"
            by (simp add: matrix_idempotent_semiring.mult_left_dist_sup matrix_monoid.mult_assoc)
          also have "... = ?ha ⊙ ?es ⊕ ?hc ⊙ ?es ⊕ ?ha ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hc ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hb ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?hd ⊙ ?ds ⊙ ?c ⊙ ?es ⊕ ?hb ⊙ ?fs ⊕ ?hd ⊙ ?fs"
            using 9 10 11 12 by (simp add: matrix_semilattice_sup.sup_assoc)
          also have "... = (?ha ⊙ ?es ⊕ ?hb ⊙ ?ds ⊙ ?c ⊙ ?es) ⊕ (?ha ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hb ⊙ ?fs) ⊕ (?hc ⊙ ?es ⊕ ?hd ⊙ ?ds ⊙ ?c ⊙ ?es) ⊕ (?hc ⊙ ?as ⊙ ?b ⊙ ?fs ⊕ ?hd ⊙ ?fs)"
            using 9 10 11 12 by (simp only: matrix_semilattice_sup.sup_assoc matrix_semilattice_sup.sup_commute matrix_semilattice_sup.sup_left_commute)
          also have "... ≼ ?ha ⊕ ?hb ⊕ ?hc ⊕ ?hd"
            using 21 22 23 24 matrix_semilattice_sup.sup.mono by blast
          also have "... = zs⟨h⟩?t"
            using 2 by (metis restrict_nonempty)
          finally show "zs⟨h⟩?t ⊙ star_matrix' ?t g ≼ zs⟨h⟩?t"
            .
        qed
      qed
    qed
  qed
  hence "∀zs . distinct zs ⟶ (zs⟨x⟩?e ⊙ y ≼ zs⟨x⟩?e ⟶ zs⟨x⟩?e ⊙ y⇧⊙ ≼ zs⟨x⟩?e)"
    by (simp add: enum_distinct restrict_all)
  thus "x ⊙ y ≼ x ⟶ x ⊙ y⇧⊙ ≼ x"
    by (metis restrict_all enum_distinct)
qed

subsection ‹Matrices form a Stone-Kleene Relation Algebra›

text ‹
Matrices over Stone-Kleene relation algebras form a Stone-Kleene relation algebra.
It remains to prove the axiom about the interaction of Kleene star and double complement.
›

interpretation matrix_stone_kleene_relation_algebra: stone_kleene_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::enum,'b::stone_kleene_relation_algebra) square" and top = top_matrix and uminus = uminus_matrix and one = one_matrix and times = times_matrix and conv = conv_matrix and star = star_matrix
proof
  fix x :: "('a,'b) square"
  let ?e = "enum_class.enum::'a list"
  let ?o = "mone :: ('a,'b) square"
  show "⊖⊖(x⇧⊙) = (⊖⊖x)⇧⊙"
  proof (rule matrix_order.order_antisym)
    have "∀g :: ('a,'b) square . distinct ?e ⟶ ⊖⊖(star_matrix' ?e (⊖⊖g)) = star_matrix' ?e (⊖⊖g)"
    proof (induct rule: list.induct)
      case Nil thus ?case
        by simp
    next
      case (Cons k s)
      let ?t = "k#s"
      assume 1: "∀g :: ('a,'b) square . distinct s ⟶ ⊖⊖(star_matrix' s (⊖⊖g)) = star_matrix' s (⊖⊖g)"
      show "∀g :: ('a,'b) square . distinct ?t ⟶ ⊖⊖(star_matrix' ?t (⊖⊖g)) = star_matrix' ?t (⊖⊖g)"
      proof (rule allI, rule impI)
        fix g :: "('a,'b) square"
        assume 2: "distinct ?t"
        let ?r = "[k]"
        let ?a = "?r⟨⊖⊖g⟩?r"
        let ?b = "?r⟨⊖⊖g⟩s"
        let ?c = "s⟨⊖⊖g⟩?r"
        let ?d = "s⟨⊖⊖g⟩s"
        let ?as = "?r⟨star o ?a⟩?r"
        let ?ds = "star_matrix' s ?d"
        let ?e = "?a ⊕ ?b ⊙ ?ds ⊙ ?c"
        let ?es = "?r⟨star o ?e⟩?r"
        let ?f = "?d ⊕ ?c ⊙ ?as ⊙ ?b"
        let ?fs = "star_matrix' s ?f"
        have "s⟨?ds⟩s = ?ds ∧ s⟨?fs⟩s = ?fs"
          by (simp add: restrict_star)
        have 3: "⊖⊖?a = ?a ∧ ⊖⊖?b = ?b ∧ ⊖⊖?c = ?c ∧ ⊖⊖?d = ?d"
          by (metis matrix_p_algebra.regular_closed_p restrict_pp)
        hence 4: "⊖⊖?as = ?as"
          by (metis pp_star_commute restrict_pp)
        hence "⊖⊖?f = ?f"
          using 3 by (metis matrix_stone_algebra.regular_closed_sup matrix_stone_relation_algebra.regular_mult_closed)
        hence 5: "⊖⊖?fs = ?fs"
          using 1 2 by (metis distinct.simps(2))
        have 6: "⊖⊖?ds = ?ds"
          using 1 2 by (simp add: restrict_pp)
        hence "⊖⊖?e = ?e"
          using 3 by (metis matrix_stone_algebra.regular_closed_sup matrix_stone_relation_algebra.regular_mult_closed)
        hence 7: "⊖⊖?es = ?es"
          by (metis pp_star_commute restrict_pp)
        have "⊖⊖(star_matrix' ?t (⊖⊖g)) = ⊖⊖(?es ⊕ ?as ⊙ ?b ⊙ ?fs ⊕ ?ds ⊙ ?c ⊙ ?es ⊕ ?fs)"
          by (metis star_matrix'.simps(2))
        also have "... = ⊖⊖?es ⊕ ⊖⊖?as ⊙ ⊖⊖?b ⊙ ⊖⊖?fs ⊕ ⊖⊖?ds ⊙ ⊖⊖?c ⊙ ⊖⊖?es ⊕ ⊖⊖?fs"
          by (simp add: matrix_stone_relation_algebra.pp_dist_comp)
        also have "... = ?es ⊕ ?as ⊙ ?b ⊙ ?fs ⊕ ?ds ⊙ ?c ⊙ ?es ⊕ ?fs"
          using 3 4 5 6 7 by simp
        finally show "⊖⊖(star_matrix' ?t (⊖⊖g)) = star_matrix' ?t (⊖⊖g)"
          by (metis star_matrix'.simps(2))
      qed
    qed
    hence "(⊖⊖x)⇧⊙ = ⊖⊖((⊖⊖x)⇧⊙)"
      by (simp add: enum_distinct restrict_all)
    thus "⊖⊖(x⇧⊙) ≼ (⊖⊖x)⇧⊙"
      by (metis matrix_kleene_algebra.star.circ_isotone matrix_p_algebra.pp_increasing matrix_p_algebra.pp_isotone)
  next
    have "?o ⊕ ⊖⊖x ⊙ ⊖⊖(x⇧⊙) ≼ ⊖⊖(x⇧⊙)"
      by (metis matrix_kleene_algebra.star_left_unfold_equal matrix_p_algebra.sup_pp_semi_commute matrix_stone_relation_algebra.pp_dist_comp)
    thus "(⊖⊖x)⇧⊙ ≼ ⊖⊖(x⇧⊙)"
      using matrix_kleene_algebra.star_left_induct by fastforce
  qed
qed

interpretation matrix_stone_kleene_relation_algebra_consistent: stone_kleene_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::enum,'b::stone_kleene_relation_algebra_consistent) square" and top = top_matrix and uminus = uminus_matrix and one = one_matrix and times = times_matrix and conv = conv_matrix and star = star_matrix
  ..

interpretation matrix_stone_kleene_relation_algebra_tarski: stone_kleene_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::enum,'b::stone_kleene_relation_algebra_tarski) square" and top = top_matrix and uminus = uminus_matrix and one = one_matrix and times = times_matrix and conv = conv_matrix and star = star_matrix
  ..

interpretation matrix_stone_kleene_relation_algebra_tarski_consistent: stone_kleene_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::enum,'b::stone_kleene_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 and star = star_matrix
  ..

end