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 List.member as i ∧ List.member bs j 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 List.member_def bot_matrix_def) auto

lemma restrict_empty_right:
  "ks⟨f⟩[] = mbot"
  by (unfold restrict_matrix_def List.member_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 List.member_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 List.member_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 List.member_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 . List.member ks x ∧ List.member ls x)"

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 List.member ks i ∧ List.member ls k then f (i,k) else bot) * (if List.member ms k ∧ List.member ns j then g (k,j) else bot))"
    by (simp add: restrict_matrix_def)
  also have "... = (⨆⇩k if List.member ms k ∧ List.member ns j then bot * g (k,j) else (if List.member ks i ∧ List.member ls k 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 List.member ks i ∧ List.member ls j 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 ≡ ∀x . List.member ks x ⟶ List.member ls x"

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 "List.member ls i ∧ List.member ms j")
    case True thus ?thesis
      by (simp add: assms restrict_matrix_def)
  next
    case False thus ?thesis
      by (unfold restrict_matrix_def) auto
  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 "List.member ls i ∧ List.member ms j")
    case True thus ?thesis
      by (simp add: assms restrict_matrix_def)
  next
    case False thus ?thesis
      by (unfold restrict_matrix_def) auto
  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 List.member ks i ∧ List.member ms j 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 List.member ks i ∧ List.member ms j then (⨆⇩k (if List.member ks i ∧ List.member ls k then f (i,k) else bot) * (if List.member ls k ∧ List.member ms j then g (k,j) else bot)) else bot)"
    by (simp add: restrict_matrix_def)
  also have "... = (if List.member ks i ∧ List.member ms j then (⨆⇩k if List.member ls k then f (i,k) * g (k,j) else bot) else bot)"
    by (auto intro: sup_monoid.sum.cong)
  also have "... = (⨆⇩k if List.member ks i ∧ List.member ms j then (if List.member ls k then f (i,k) * g (k,j) else bot) else bot)"
    by auto
  also have "... = (⨆⇩k (if List.member ks i ∧ List.member ls k then f (i,k) else bot) * (if List.member ls k ∧ List.member ms j 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"
  hence 1: "⋀g::('a,'b) square . ?t⟨star_matrix' s g⟩?t = star_matrix' s g"
    by (metis member_rec(1) restrict_superlist)
  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 member_def)
    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 "¬ List.member ks k"
    shows "(k#ks)⟨(mone::('a,'b::idempotent_semiring) square)⟩(k#ks) = [k]⟨mone⟩[k] ⊕ ks⟨mone⟩ks"
  by (subst restrict_nonempty) (simp add: assms member_rec 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 List.member ks i ∧ List.member ks k then ?o (i,k) else bot) * (if List.member ks k ∧ List.member ls j then f (k,j) else bot))"
    by (simp add: restrict_matrix_def)
  also have "... = (⨆⇩k (if List.member ks i ∧ List.member ks k then (if i = k then 1 else bot) else bot) * (if List.member ks k ∧ List.member ls j then f (k,j) else bot))"
    by (unfold one_matrix_def) auto
  also have "... = (⨆⇩k (if i = k then (if List.member ks i then 1 else bot) else bot) * (if List.member ks k ∧ List.member ls j then f (k,j) else bot))"
    by (auto intro: sup_monoid.sum.cong)
  also have "... = (⨆⇩k if i = k then (if List.member ks i then 1 else bot) * (if List.member ks i ∧ List.member ls j then f (i,j) else bot) else bot)"
    by (rule sup_monoid.sum.cong) simp_all
  also have "... = (if List.member ks i then 1 else bot) * (if List.member ks i ∧ List.member ls j then f (i,j) else bot)"
    by simp
  also have "... = (if List.member ks i ∧ List.member ls j 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 List.member_def)

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

lemma restrict_list_singleton:
  "(ks⟨f⟩[l]) (i,j) = (if List.member ks i ∧ j = l then f (i,j) else bot)"
  by (simp add: restrict_matrix_def List.member_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 List.member_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 "¬ List.member ls l"
    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: List.member_def 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 (simp add: member_rec)
  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: "List.member ls j ⟹ f (k,j) = g (k,j)"
      using 3 by (metis restrict_singleton_list)
    have 6: "List.member ks i ⟹ 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: "List.member ks i ⟹ List.member ls j ⟹ f (i,j) = g (i,j)"
      by (simp add: restrict_matrix_def)
    have "((k#ks)⟨f⟩(l#ls)) (i,j) = (if (i = k ∨ List.member ks i) ∧ (j = l ∨ List.member ls j) then f (i,j) else bot)"
      by (simp add: restrict_matrix_def List.member_def)
    also have "... = (if i = k ∧ j = l then f (i,j) else if i = k ∧ List.member ls j then f (i,j) else if List.member ks i ∧ j = l then f (i,j) else if List.member ks i ∧ List.member ls j then f (i,j) else bot)"
      by auto
    also have "... = (if i = k ∧ j = l then g (i,j) else if i = k ∧ List.member ls j then g (i,j) else if List.member ks i ∧ j = l then g (i,j) else if List.member ks i ∧ List.member ls j then g (i,j) else bot)"
      using 4 5 6 7 by simp
    also have "... = (if (i = k ∨ List.member ks i) ∧ (j = l ∨ List.member ls j) then g (i,j) else bot)"
      by auto
    also have "... = ((k#ks)⟨g⟩(l#ls)) (i,j)"
      by (simp add: restrict_matrix_def List.member_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 List.member ms i ∧ List.member ns j then if List.member ks i ∧ List.member ls j 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

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 List.member ms i ∧ List.member ns j then if List.member ks i ∧ List.member ls j 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 "¬ List.member ks k"
      and "¬ List.member ls l"
      and "¬ List.member ms m"
    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 (simp add: assms(1,3) member_rec)
  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 (simp add: 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 (simp add: 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 (simp add: 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 (simp add: 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 "¬ List.member ks k"
      and "¬ List.member ls l"
      and "¬ List.member ms m"
    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) matrix_semilattice_sup.sup.bounded_iff member_def member_rec(2) 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) matrix_semilattice_sup.sup.bounded_iff member_def member_rec(2) 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 (no_types, opaque_lifting) matrix_idempotent_semiring.mult_right_dist_sup matrix_semilattice_sup.sup.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 add: in_set_member member_rec)
      hence 5: "?t⟨?o⟩?t = ?r⟨?o⟩?r ⊕ s⟨?o⟩s"
        by (meson member_rec(1) 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 (no_types, lifting) distinct.simps(2) restrict_superlist)
      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 ∧ ¬ List.member s k ∧ ¬ List.member ys y"
            using 2 by (simp add: List.member_def)
          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 add: 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 add: in_set_member member_rec(1) member_rec(2))
          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 member_rec(2) 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 ∧ ¬ List.member s k ∧ ¬ List.member ys y"
            using 2 by (simp add: List.member_def)
          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 by (simp add: 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 add: in_set_member member_rec)
          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