# Theory Matrix_Peano_Algebras

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

section ‹Matrix Peano Algebras›

text ‹
We define a Boolean matrix representation of natural numbers up to ‹n›, where ‹n› the size of an enumeration type ‹'a::enum›.
Numbers (obtained by ‹Z_matrix› for ‹0› and ‹N_matrix n› for ‹n›) are represented as relational vectors.
The total successor function (‹S_matrix›, modulo ‹n›) and the partial successor function (‹S'_matrix›, for numbers up to ‹n-1›) are relations that are (partial) functions.

We give an order-embedding of ‹nat› into this representation.
We show that this representation satisfies a relational version of the Peano axioms.
We also implement a function ‹CP_matrix› that chooses a number in a non-empty set.
›

theory Matrix_Peano_Algebras

imports Aggregation_Algebras.M_Choose_Component Relational_Disjoint_Set_Forests.More_Disjoint_Set_Forests

begin

no_notation
uminus ("- _" [81] 80) and
minus_class.minus (infixl "-" 65)

definition Z_matrix :: "('a::enum,'b::{bot,top}) square" ("mZero") where "mZero = (λ(i,j) . if i = hd enum_class.enum then top else bot)"
definition S_matrix :: "('a::enum,'b::{bot,top}) square" ("msuccmod") where "msuccmod = (λ(i,j) . let e = (enum_class.enum :: 'a list) in if (∃k . Suc k<length e ∧ i = e ! k ∧ j = e ! Suc k) ∨ (i = e ! minus_class.minus (length e) 1 ∧ j = hd e) then top else bot)"
definition S'_matrix :: "('a::enum,'b::{bot,top}) square" ("msucc") where "msucc = (λ(i,j) . let e = (enum_class.enum :: 'a list) in if ∃k . Suc k<length e ∧ i = e ! k ∧ j = e ! Suc k then top else bot)"
definition N_matrix :: "nat ⇒ ('a::enum,'b::{bot,top}) square" ("mnat") where "mnat n = (λ(i,j) . if i = enum_class.enum ! n then top else bot)"
definition CP_matrix  :: "('a::enum,'b::{bot,uminus}) square ⇒ ('a,'b) square" ("mcp") where "mcp f = (λ(i,j) . if Some i = find (λx . f (x,x) ≠ bot) enum_class.enum then uminus_class.uminus (uminus_class.uminus (f (i,j))) else bot)"

lemma S'_matrix_S_matrix:
"(msucc :: ('a::enum,'b::stone_relation_algebra) square) = msuccmod ⊖ mZero⇧t"
proof (rule ext, rule prod_cases)
let ?e = "enum_class.enum :: 'a list"
let ?h = "hd ?e"
let ?s = "msuccmod :: ('a,'b) square"
let ?s' = "msucc :: ('a,'b) square"
let ?z = "mZero :: ('a,'b) square"
fix i j
have "?s' (i,j) = ?s (i,j) - ?z (j,i)"
proof (cases "j = ?h")
case True
have "?s' (i,j) = bot"
proof (unfold S'_matrix_def, clarsimp)
fix k
assume 1: "Suc k < length ?e" "j = ?e ! Suc k"
have "(UNIV :: 'a set) ≠ {}"
by simp
hence "?e ! Suc k = ?e ! 0"
using 1 by (simp add: hd_conv_nth UNIV_enum True)
hence "Suc k = 0"
apply (subst nth_eq_iff_index_eq[THEN sym, of ?e])
using 1 enum_distinct by auto
thus "top = bot"
by simp
qed
thus ?thesis
next
case False
thus ?thesis
by (simp add: Z_matrix_def S_matrix_def S'_matrix_def)
qed
thus "?s' (i,j) = (?s ⊖ ?z⇧t) (i,j)"
by (simp add: minus_matrix_def conv_matrix_def Z_matrix_def)
qed

lemma N_matrix_power_S:
"n < length (enum_class.enum :: 'a list) ⟶ mnat n = matrix_monoid.power (msuccmod⇧t) n ⊙ (mZero :: ('a::enum,'b::stone_relation_algebra) square)"
proof (induct n)
let ?z = "mZero :: ('a,'b) square"
let ?s = "msuccmod :: ('a,'b) square"
let ?e = "enum_class.enum :: 'a list"
let ?h = "hd ?e"
let ?l = "length ?e"
let ?g = "?e ! minus_class.minus ?l 1"
let ?p = "matrix_monoid.power (?s⇧t)"
case 0
have "(UNIV :: 'a set) ≠ {}"
by simp
hence "?h = ?e ! 0"
thus ?case
case (Suc n)
assume 1: "n < ?l ⟶ mnat n = ?p n ⊙ ?z"
show "Suc n < ?l ⟶ mnat (Suc n) = ?p (Suc n) ⊙ ?z"
proof
assume 2: "Suc n < ?l"
hence "n < ?l"
by simp
hence "∀l<?l . (?e ! l = ?e ! n ⟶ l = n)"
using nth_eq_iff_index_eq enum_distinct by auto
hence 3: "⋀i . (∃l<?l . ?e ! n = ?e ! l ∧ i = ?e ! Suc l) ⟶ (i = ?e ! Suc n)"
by auto
have 4: "⋀i . (∃l . Suc l<?l ∧ ?e ! n = ?e ! l ∧ i = ?e ! Suc l) ⟷ (i = ?e ! Suc n)"
apply (rule iffI)
using 3 apply (metis Suc_lessD)
using 2 by auto
show "mnat (Suc n) = ?p (Suc n) ⊙ ?z"
proof (rule ext, rule prod_cases)
fix i j :: 'a
have "(?p (Suc n) ⊙ ?z) (i,j) = (?s⇧t ⊙ mnat n) (i,j)"
using 1 2 by (simp add: matrix_monoid.mult_assoc)
also have "... = (⨆⇩k ((?s (k,i))⇧T * mnat n (k,j)))"
also have "... = (⨆⇩k ((if (∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l) ∨ (k = ?g ∧ i = ?h) then top else bot)⇧T * (if k = ?e ! n then top else bot)))"
also have "... = (⨆⇩k ((if (∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l) ∨ (k = ?g ∧ i = ?h) then top else bot) * (if k = ?e ! n then top else bot)))"
by (smt (verit, best) sup_monoid.sum.cong symmetric_bot_closed symmetric_top_closed)
also have "... = (⨆⇩k (if (∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! n) ∨ (k = ?g ∧ i = ?h ∧ k = ?e ! n) then top else bot))"
by (smt (verit, best) covector_bot_closed idempotent_bot_closed sup_monoid.sum.cong surjective_top_closed vector_bot_closed)
also have "... = (if ∃l . Suc l<length ?e ∧ ?e ! n = ?e ! l ∧ i = ?e ! Suc l then top else bot)"
proof -
have "⋀k . ¬(k = ?g ∧ i = ?h ∧ k = ?e ! n)"
using 2 distinct_conv_nth[of ?e] enum_distinct by auto
thus ?thesis
by (smt (verit, del_insts) comp_inf.ub_sum sup.order_iff sup_monoid.sum.neutral sup_top_right)
qed
also have "... = (if i = ?e ! Suc n then top else bot)"
using 4 by simp
also have "... = mnat (Suc n) (i,j)"
finally show "mnat (Suc n) (i,j) = (?p (Suc n) ⊙ ?z) (i,j)"
by simp
qed
qed
qed

lemma N_matrix_power_S':
"n < length (enum_class.enum :: 'a list) ⟶ mnat n = matrix_monoid.power (msucc⇧t) n ⊙ (mZero :: ('a::enum,'b::stone_relation_algebra) square)"
proof (induct n)
let ?z = "mZero :: ('a,'b) square"
let ?s = "msucc :: ('a,'b) square"
let ?e = "enum_class.enum :: 'a list"
let ?h = "hd ?e"
let ?l = "length ?e"
let ?p = "matrix_monoid.power (?s⇧t)"
case 0
have "(UNIV :: 'a set) ≠ {}"
by simp
hence "?h = ?e ! 0"
thus ?case
case (Suc n)
assume 1: "n < ?l ⟶ mnat n = ?p n ⊙ ?z"
show "Suc n < ?l ⟶ mnat (Suc n) = ?p (Suc n) ⊙ ?z"
proof
assume 2: "Suc n < ?l"
hence "n < ?l"
by simp
hence "∀l<?l . (?e ! l = ?e ! n ⟶ l = n)"
using nth_eq_iff_index_eq enum_distinct by auto
hence 3: "⋀i . (∃l<?l . ?e ! n = ?e ! l ∧ i = ?e ! Suc l) ⟶ (i = ?e ! Suc n)"
by auto
have 4: "⋀i . (∃l . Suc l<?l ∧ ?e ! n = ?e ! l ∧ i = ?e ! Suc l) ⟷ (i = ?e ! Suc n)"
apply (rule iffI)
using 3 apply (metis Suc_lessD)
using 2 by auto
show "mnat (Suc n) = ?p (Suc n) ⊙ ?z"
proof (rule ext, rule prod_cases)
fix i j :: 'a
have "(?p (Suc n) ⊙ ?z) (i,j) = (?s⇧t ⊙ mnat n) (i,j)"
using 1 2 by (simp add: matrix_monoid.mult_assoc)
also have "... = (⨆⇩k ((?s (k,i))⇧T * mnat n (k,j)))"
also have "... = (⨆⇩k ((if ∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l then top else bot)⇧T * (if k = ?e ! n then top else bot)))"
also have "... = (⨆⇩k ((if ∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l then top else bot) * (if k = ?e ! n then top else bot)))"
by (smt (verit, best) sup_monoid.sum.cong symmetric_bot_closed symmetric_top_closed)
also have "... = (⨆⇩k (if ∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! n then top else bot))"
by (smt (verit, best) covector_bot_closed idempotent_bot_closed sup_monoid.sum.cong surjective_top_closed vector_bot_closed)
also have "... = (if ∃l . Suc l<length ?e ∧ ?e ! n = ?e ! l ∧ i = ?e ! Suc l then top else bot)"
by (smt (verit, del_insts) comp_inf.ub_sum sup.order_iff sup_monoid.sum.neutral sup_top_right)
also have "... = (if i = ?e ! Suc n then top else bot)"
using 4 by simp
also have "... = mnat (Suc n) (i,j)"
finally show "mnat (Suc n) (i,j) = (?p (Suc n) ⊙ ?z) (i,j)"
by simp
qed
qed
qed

lemma N_matrix_power_S'_hom_zero:
"mnat 0 = (mZero :: ('a::enum,'b::stone_relation_algebra) square)"
proof -
let ?e = "enum_class.enum :: 'a list"
have "(UNIV :: 'a set) = set ?e"
using UNIV_enum by simp
hence "0 < length ?e"
by auto
thus ?thesis
using N_matrix_power_S' by force
qed

lemma N_matrix_power_S'_hom_succ:
assumes "Suc n < length (enum_class.enum :: 'a list)"
shows "mnat (Suc n) = msucc⇧t ⊙ (mnat n :: ('a::enum,'b::stone_relation_algebra) square)"
proof -
let ?e = "enum_class.enum :: 'a list"
let ?z = "mZero :: ('a,'b) square"
have 1: "n < length ?e"
using assms by simp
have "mnat (Suc n) = matrix_monoid.power (msucc⇧t) (Suc n) ⊙ ?z"
using assms N_matrix_power_S' by blast
also have "... = msucc⇧t ⊙ matrix_monoid.power (msucc⇧t) n ⊙ ?z"
by simp
also have "... = msucc⇧t ⊙ (matrix_monoid.power (msucc⇧t) n ⊙ ?z)"
also have "... = msucc⇧t ⊙ mnat n"
using 1 by (metis N_matrix_power_S')
finally show ?thesis
.
qed

lemma N_matrix_power_S'_hom_inj:
assumes "m < length (enum_class.enum :: 'a list)"
and "n < length (enum_class.enum :: 'a list)"
and "m ≠ n"
shows "mnat m ≠ (mnat n :: ('a::enum,'b::stone_relation_algebra_consistent) square)"
proof -
let ?e = "enum_class.enum :: 'a list"
let ?m = "?e ! m"
have 1: "mnat m (?m,?m) = top"
have "mnat n (?m,?m) = bot"
apply (unfold N_matrix_def)
using assms enum_distinct nth_eq_iff_index_eq by auto
thus ?thesis
using 1 by (metis consistent)
qed

syntax
"_sum_sup_monoid" :: "idt ⇒ nat ⇒ 'a::bounded_semilattice_sup_bot ⇒ 'a" ("(⨆_<_ . _)" [0,51,10] 10)
translations
"⨆x<y . t" => "XCONST sup_monoid.sum (λx . t) { x . x < y }"

context bounded_semilattice_sup_bot
begin

lemma ub_sum_nat:
fixes f :: "nat ⇒ 'a"
assumes "i < l"
shows "f i ≤ (⨆k<l . f k)"
by (metis (no_types, lifting) assms finite_Collect_less_nat sup_ge1 sup_monoid.sum.remove mem_Collect_eq)

lemma lub_sum_nat:
fixes f :: "nat ⇒ 'a"
assumes "∀k<l . f k ≤ x"
shows "(⨆k<l . f k) ≤ x"
apply (rule finite_subset_induct[where A="{k . k < l}"])

end

lemma ext_sum_nat:
fixes l :: nat
shows "(⨆k<l . f k x) = (⨆k<l . f k) x"
apply (rule finite_subset_induct[where A="{k . k < l}"])
apply simp
apply simp
apply (metis (no_types, lifting) bot_apply sup_monoid.sum.empty)
by (metis (mono_tags, lifting) sup_apply sup_monoid.sum.insert)

interpretation matrix_skra_peano_1: skra_peano_1 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::linorder_stone_kleene_relation_algebra_tarski_consistent_expansion) 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 and Z = Z_matrix and S = S_matrix
proof
let ?z = "mZero :: ('a,'b) square"
let ?s = "msuccmod :: ('a,'b) square"
let ?e = "enum_class.enum :: 'a list"
let ?h = "hd ?e"
let ?l = "length ?e"
let ?g = "?e ! minus_class.minus ?l 1"
let ?p = "matrix_monoid.power (?s⇧t)"
have 1: "?z ⊙ mtop = ?z"
proof (rule ext, rule prod_cases)
fix i j :: 'a
have "(?z ⊙ mtop) (i,j) = (⨆⇩k (?z (i,k) * top))"
also have "... = (⨆⇩k::'a (if i = ?h then top else bot) * top)"
also have "... = (if i = ?h then top else bot) * (top :: 'b)"
using sum_const by blast
also have "... = ?z (i,j)"
finally show "(?z ⊙ mtop) (i,j) = ?z (i,j)"
.
qed
have 2: "?z ⊙ ?z⇧t ≼ mone"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
fix i j :: 'a
have "(?z ⊙ ?z⇧t) (i,j) = (⨆⇩k (?z (i,k) * (?z (j,k))⇧T))"
also have "... = (⨆⇩k::'a (if i = ?h then top else bot) * (if j = ?h then top else bot))"
also have "... = (if i = ?h then top else bot) * (if j = ?h then top else bot)"
using sum_const by blast
also have "... ≤ mone (i,j)"
finally show "(?z ⊙ ?z⇧t) (i,j) ≤ mone (i,j)"
.
qed
have 3: "mtop ⊙ ?z = mtop"
proof (rule ext, rule prod_cases)
fix i j :: 'a
have "mtop (i,j) = (top::'b) * (if ?h = ?h then top else bot)"
also have "... ≤ (⨆⇩k::'a (top * (if k = ?h then top else bot)))"
by (rule ub_sum)
also have "... = (⨆⇩k (top * ?z (k,j)))"
also have "... = (mtop ⊙ ?z) (i,j)"
finally show "(mtop ⊙ ?z) (i,j) = mtop (i,j)"
qed
show "matrix_stone_relation_algebra.point ?z"
using 1 2 3 by simp
have "∀i (j::'a) (k::'a) . (∃l<?l . ∃m<?l . k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! m ∧ j = ?e ! Suc m) ⟶ i = j"
using distinct_conv_nth enum_distinct by auto
hence 4: "∀i (j::'a) (k::'a) . (∃l m . Suc l<?l ∧ Suc m<?l ∧ k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! m ∧ j = ?e ! Suc m) ⟶ i = j"
by (metis Suc_lessD)
show "?s⇧t ⊙ ?s ≼ mone"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
fix i j :: 'a
have "(?s⇧t ⊙ ?s) (i,j) = (⨆⇩k (?s (k,i) * ?s (k,j)))"
also have "... = (⨆⇩k::'a ((if (∃l . Suc l<?l ∧ k = ?e ! l ∧ i = ?e ! Suc l) ∨ (k = ?g ∧ i = ?h) then top else bot) * (if (∃m . Suc m<?l ∧ k = ?e ! m ∧ j = ?e ! Suc m) ∨ (k = ?g ∧ j = ?h) then top else bot)))"
also have "... = (⨆⇩k::'a (if (∃l m . Suc l<?l ∧ Suc m<?l ∧ k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! m ∧ j = ?e ! Suc m) ∨ (k = ?g ∧ i = ?h ∧ j = ?h) then top else bot))"
proof -
have 5: "⋀k . ¬((∃l . Suc l<?l ∧ k = ?e ! l ∧ i = ?e ! Suc l) ∧ (k = ?g ∧ j = ?h))"
using distinct_conv_nth[of ?e] enum_distinct by auto
have "⋀k . ¬((k = ?g ∧ i = ?h) ∧ (∃m . Suc m<?l ∧ k = ?e ! m ∧ j = ?e ! Suc m))"
using distinct_conv_nth[of ?e] enum_distinct by auto
thus ?thesis
using 5 by (smt (verit) covector_bot_closed idempotent_bot_closed sup_monoid.sum.cong surjective_top_closed vector_bot_closed)
qed
also have "... ≤ (⨆⇩k::'a (if i = j then top else bot))"
using 4 by (smt (verit, best) comp_inf.ub_sum order_top_class.top_greatest sup_monoid.sum.not_neutral_contains_not_neutral top.extremum_uniqueI)
also have "... ≤ (if i = j then top else bot)"
also have "... = mone (i,j)"
finally show "(?s⇧t ⊙ ?s) (i,j) ≤ mone (i,j)"
.
qed
have 6: "∀i (j::'a) (k::'a) . (∃l m . Suc l<?l ∧ Suc m<?l ∧ i = ?e ! l ∧ k = ?e ! Suc l ∧ j = ?e ! m ∧ k = ?e ! Suc m) ⟶ i = j"
using distinct_conv_nth enum_distinct by auto
show "?s ⊙ ?s⇧t ≼ mone"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
fix i j :: 'a
have "(?s ⊙ ?s⇧t) (i,j) = (⨆⇩k (?s (i,k) * ?s (j,k)))"
also have "... = (⨆⇩k::'a ((if (∃l . Suc l<?l ∧ i = ?e ! l ∧ k = ?e ! Suc l) ∨ (i = ?g ∧ k = ?h) then top else bot) * (if (∃m . Suc m<?l ∧ j = ?e ! m ∧ k = ?e ! Suc m) ∨ (j = ?g ∧ k = ?h) then top else bot)))"
also have "... = (⨆⇩k::'a (if (∃l m . Suc l<?l ∧ Suc m<?l ∧ i = ?e ! l ∧ k = ?e ! Suc l ∧ j = ?e ! m ∧ k = ?e ! Suc m) ∨ (i = ?g ∧ k = ?h ∧ j = ?g) then top else bot))"
proof -
have 7: "⋀l . Suc l<?l ⟶ 0<?l"
by auto
have 8: "?h = ?e ! 0"
proof (rule hd_conv_nth, rule)
assume "?e = []"
hence "(UNIV::'a set) = {}"
thus "False"
by simp
qed
have 9: "⋀k . ¬((∃l . Suc l<?l ∧ i = ?e ! l ∧ k = ?e ! Suc l) ∧ (j = ?g ∧ k = ?h))"
using 7 8 distinct_conv_nth[of ?e] enum_distinct by auto
have "⋀k . ¬((i = ?g ∧ k = ?h) ∧ (∃m . Suc m<?l ∧ j = ?e ! m ∧ k = ?e ! Suc m))"
using 7 8 distinct_conv_nth[of ?e] enum_distinct by auto
thus ?thesis
using 9 by (smt (verit) covector_bot_closed idempotent_bot_closed sup_monoid.sum.cong surjective_top_closed vector_bot_closed)
qed
also have "... ≤ (⨆⇩k::'a (if i = j then top else bot))"
using 6 by (smt (verit, best) comp_inf.ub_sum order_top_class.top_greatest sup_monoid.sum.not_neutral_contains_not_neutral top.extremum_uniqueI)
also have "... ≤ (if i = j then top else bot)"
by simp
also have "... = mone (i,j)"
finally show "(?s ⊙ ?s⇧t) (i,j) ≤ mone (i,j)"
.
qed
have "(mtop :: ('a,'b) square) = (⨆k<?l . mnat k)"
proof (rule ext, rule prod_cases)
fix i j :: 'a
have "mtop (i,j) = (top :: 'b)"
also have "... = (⨆k<?l . (if i = ?e ! k then top else bot))"
proof -
have "i ∈ set ?e"
using UNIV_enum by auto
from this obtain k where 6: "k < ?l ∧ i = ?e ! k"
by (metis in_set_conv_nth)
hence "(λk . if i = ?e ! k then top else bot) k ≤ (⨆k<?l . (if i = ?e ! k then top else bot :: 'b))"
by (metis ub_sum_nat)
hence "top ≤ (⨆k<?l . (if i = ?e ! k then top else bot :: 'b))"
using 6 by simp
thus ?thesis
using top.extremum_uniqueI by force
qed
also have "... = (⨆k<?l . mnat k (i,j))"
also have "... = (⨆k<?l . mnat k) (i,j)"
finally show "(mtop (i,j) :: 'b) = (⨆k<?l . mnat k) (i,j)"
.
qed
also have "... = (⨆k<?l . ?p k ⊙ ?z)"
proof -
have "⋀k . k<?l ⟶ mnat k = ?p k ⊙ ?z"
using N_matrix_power_S by auto
thus ?thesis
by (metis (no_types, lifting) mem_Collect_eq sup_monoid.sum.cong)
qed
also have "... ≼ ?s⇧t⇧⊙ ⊙ ?z"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
fix i j :: 'a
have "(⨆k<?l . ?p k ⊙ ?z) (i,j) = (⨆k<?l . (?p k ⊙ ?z) (i,j))"
by (metis ext_sum_nat)
also have "... ≤ (?s⇧t⇧⊙ ⊙ ?z) (i,j)"
apply (rule lub_sum_nat)
by (metis less_eq_matrix_def matrix_idempotent_semiring.mult_left_isotone matrix_kleene_algebra.star.power_below_circ)
finally show "(⨆k<?l . ?p k ⊙ ?z) (i,j) ≤ (?s⇧t⇧⊙ ⊙ ?z) (i,j)"
.
qed
finally show "?s⇧t⇧⊙ ⊙ ?z = mtop"
qed

interpretation matrix_skra_peano_2: skra_peano_2 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::linorder_stone_kleene_relation_algebra_tarski_consistent_expansion) 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 and Z = Z_matrix and S = S_matrix
proof
let ?s = "msuccmod :: ('a,'b) square"
let ?e = "enum_class.enum :: 'a list"
let ?h = "hd ?e"
let ?l = "length ?e"
let ?g = "?e ! minus_class.minus ?l 1"
show "matrix_bounded_idempotent_semiring.total ?s"
proof (rule ext, rule prod_cases)
fix i j :: 'a
have "(?s ⊙ mtop) (i,j) = (⨆⇩k (?s (i,k) * top))"
also have "... = (⨆⇩k::'a if (∃l . Suc l<?l ∧ i = ?e ! l ∧ k = ?e ! Suc l) ∨ (i = ?g ∧ k = ?h) then top else bot)"
also have "... = top"
proof -
have "⋀i . (∃l . Suc l<?l ∧ i = ?e ! l) ∨ i = ?g"
by (metis in_set_conv_nth in_enum Suc_lessI diff_Suc_1)
hence "⋀i . ∃k . (∃l . Suc l<?l ∧ i = ?e ! l ∧ k = ?e ! Suc l) ∨ (i = ?g ∧ k = ?h)"
by blast
thus ?thesis
by (smt (verit, ccfv_threshold) comp_inf.ub_sum top.extremum_uniqueI)
qed
finally show "(?s ⊙ mtop) (i,j) = mtop (i,j)"
qed
qed

interpretation matrix_skra_peano_3: skra_peano_3 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::linorder_stone_kleene_relation_algebra_tarski_consistent_expansion) 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 and Z = Z_matrix and S = S_matrix
proof (unfold_locales, rule finite_surj)
show "finite (UNIV :: 'a rel set)"
by simp
let ?f = "λR p . if p ∈ R then top else bot"
show "{ f :: ('a,'b) square . matrix_p_algebra.regular f } ⊆ range ?f"
proof
fix f :: "('a,'b) square"
let ?R = "{ (x,y) . f (x,y) = top }"
assume "f ∈ { f . matrix_p_algebra.regular f }"
hence "matrix_p_algebra.regular f"
by simp
hence "⋀p . f p ≠ top ⟶ f p = bot"
by (metis linorder_stone_algebra_expansion_class.uminus_def uminus_matrix_def)
hence "f = ?f ?R"
by fastforce
thus "f ∈ range ?f"
by blast
qed
qed

interpretation matrix_skra_peano_4: skra_peano_4 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::linorder_stone_kleene_relation_algebra_tarski_consistent_plus_expansion) 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 and Z = Z_matrix and S = S_matrix and choose_point = agg_square_m_kleene_algebra_2.m_choose_component_algebra_tarski.choose_component_point
apply unfold_locales

interpretation matrix'_skra_peano_1: skra_peano_1 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::linorder_stone_kleene_relation_algebra_tarski_consistent_expansion) 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 and Z = Z_matrix and S = S'_matrix
proof
let ?z = "mZero :: ('a,'b) square"
let ?s = "msucc :: ('a,'b) square"
let ?e = "enum_class.enum :: 'a list"
let ?l = "length ?e"
let ?p = "matrix_monoid.power (?s⇧t)"
show "matrix_stone_relation_algebra.point ?z"
using matrix_skra_peano_1.Z_point by auto
have "∀i (j::'a) (k::'a) . (∃l<?l . ∃m<?l . k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! m ∧ j = ?e ! Suc m) ⟶ i = j"
using distinct_conv_nth enum_distinct by auto
hence 4: "∀i (j::'a) (k::'a) . (∃l m . Suc l<?l ∧ Suc m<?l ∧ k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! m ∧ j = ?e ! Suc m) ⟶ i = j"
by (metis Suc_lessD)
show "?s⇧t ⊙ ?s ≼ mone"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
fix i j :: 'a
have "(?s⇧t ⊙ ?s) (i,j) = (⨆⇩k (?s (k,i) * ?s (k,j)))"
also have "... = (⨆⇩k::'a ((if ∃l . Suc l<?l ∧ k = ?e ! l ∧ i = ?e ! Suc l then top else bot) * (if ∃m . Suc m<?l ∧ k = ?e ! m ∧ j = ?e ! Suc m then top else bot)))"
also have "... = (⨆⇩k::'a (if (∃l m . Suc l<?l ∧ Suc m<?l ∧ k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! m ∧ j = ?e ! Suc m) then top else bot))"
by (smt (verit) covector_bot_closed idempotent_bot_closed sup_monoid.sum.cong surjective_top_closed vector_bot_closed)
also have "... ≤ (⨆⇩k::'a (if i = j then top else bot))"
using 4 by (smt (verit, best) comp_inf.ub_sum order_top_class.top_greatest sup_monoid.sum.not_neutral_contains_not_neutral top.extremum_uniqueI)
also have "... ≤ (if i = j then top else bot)"
also have "... = mone (i,j)"
finally show "(?s⇧t ⊙ ?s) (i,j) ≤ mone (i,j)"
.
qed
have 5: "∀i (j::'a) (k::'a) . (∃l m . Suc l<?l ∧ Suc m<?l ∧ i = ?e ! l ∧ k = ?e ! Suc l ∧ j = ?e ! m ∧ k = ?e ! Suc m) ⟶ i = j"
using distinct_conv_nth enum_distinct by auto
show "?s ⊙ ?s⇧t ≼ mone"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
fix i j :: 'a
have "(?s ⊙ ?s⇧t) (i,j) = (⨆⇩k (?s (i,k) * ?s (j,k)))"
also have "... = (⨆⇩k::'a ((if ∃l . Suc l<?l ∧ i = ?e ! l ∧ k = ?e ! Suc l then top else bot) * (if ∃m . Suc m<?l ∧ j = ?e ! m ∧ k = ?e ! Suc m then top else bot)))"
also have "... = (⨆⇩k::'a (if (∃l m . Suc l<?l ∧ Suc m<?l ∧ i = ?e ! l ∧ k = ?e ! Suc l ∧ j = ?e ! m ∧ k = ?e ! Suc m) then top else bot))"
by (smt (verit) covector_bot_closed idempotent_bot_closed sup_monoid.sum.cong surjective_top_closed vector_bot_closed)
also have "... ≤ (⨆⇩k::'a (if i = j then top else bot))"
using 5 by (smt (verit, best) comp_inf.ub_sum order_top_class.top_greatest sup_monoid.sum.not_neutral_contains_not_neutral top.extremum_uniqueI)
also have "... ≤ (if i = j then top else bot)"
by simp
also have "... = mone (i,j)"
finally show "(?s ⊙ ?s⇧t) (i,j) ≤ mone (i,j)"
.
qed
have "(mtop :: ('a,'b) square) = (⨆k<?l . mnat k)"
proof (rule ext, rule prod_cases)
fix i j :: 'a
have "mtop (i,j) = (top :: 'b)"
also have "... = (⨆k<?l . (if i = ?e ! k then top else bot))"
proof -
have "i ∈ set ?e"
using UNIV_enum by auto
from this obtain k where 6: "k < ?l ∧ i = ?e ! k"
by (metis in_set_conv_nth)
hence "(λk . if i = ?e ! k then top else bot) k ≤ (⨆k<?l . (if i = ?e ! k then top else bot :: 'b))"
by (metis ub_sum_nat)
hence "top ≤ (⨆k<?l . (if i = ?e ! k then top else bot :: 'b))"
using 6 by simp
thus ?thesis
using top.extremum_uniqueI by force
qed
also have "... = (⨆k<?l . mnat k (i,j))"
also have "... = (⨆k<?l . mnat k) (i,j)"
finally show "(mtop (i,j) :: 'b) = (⨆k<?l . mnat k) (i,j)"
.
qed
also have "... = (⨆k<?l . ?p k ⊙ ?z)"
proof -
have "⋀k . k<?l ⟶ mnat k = ?p k ⊙ ?z"
using N_matrix_power_S' by auto
thus ?thesis
by (metis (no_types, lifting) mem_Collect_eq sup_monoid.sum.cong)
qed
also have "... ≼ ?s⇧t⇧⊙ ⊙ ?z"
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
fix i j :: 'a
have "(⨆k<?l . ?p k ⊙ ?z) (i,j) = (⨆k<?l . (?p k ⊙ ?z) (i,j))"
by (metis ext_sum_nat)
also have "... ≤ (?s⇧t⇧⊙ ⊙ ?z) (i,j)"
apply (rule lub_sum_nat)
by (metis less_eq_matrix_def matrix_idempotent_semiring.mult_left_isotone matrix_kleene_algebra.star.power_below_circ)
finally show "(⨆k<?l . ?p k ⊙ ?z) (i,j) ≤ (?s⇧t⇧⊙ ⊙ ?z) (i,j)"
.
qed
finally show "?s⇧t⇧⊙ ⊙ ?z = mtop"
qed

lemma nat_less_lesseq_pred:
"(m :: nat) < n ⟹ m ≤ minus_class.minus n 1"
by simp

lemma S'_matrix_acyclic:
"matrix_stone_kleene_relation_algebra.acyclic (msucc :: ('a::enum,'b::linorder_stone_kleene_relation_algebra_tarski_consistent_expansion) square)"
proof (rule ccontr)
let ?e = "enum_class.enum :: 'a list"
let ?l = "length ?e"
let ?l1 = "minus_class.minus ?l 1"
let ?s = "msucc :: ('a,'b) square"
have "(UNIV :: 'a set) ≠ {}"
by simp
hence 1: "?e ≠ []"
hence 2: "?l ≠ 0"
by simp
assume "¬ matrix_stone_kleene_relation_algebra.acyclic ?s"
hence "?s ⊙ ?s⇧⊙ ⊗ mone ≠ mbot"
from this obtain i1 i2 where "(?s ⊙ ?s⇧⊙ ⊗ mone) (i1,i2) ≠ bot"
by (metis bot_matrix_def ext surj_pair)
hence 3: "(?s ⊙ ?s⇧⊙) (i1,i2) ⊓ mone (i1,i2) ≠ bot"
hence "mone (i1,i2) ≠ (bot :: 'b)"
by force
hence "i1 = i2"
by (metis (mono_tags, lifting) prod.simps(2) one_matrix_def)
hence "(?s ⊙ ?s⇧⊙) (i1,i1) ≠ bot"
using 3 by force
hence "(⨆⇩k ?s (i1,k) * (?s⇧⊙) (k,i1)) ≠ bot"
by (smt (verit, best) times_matrix_def case_prod_conv sup_monoid.sum.cong)
from this obtain i3 where 4: "?s (i1,i3) * (?s⇧⊙) (i3,i1) ≠ bot"
by force
hence "?s (i1,i3) ≠ bot"
by force
hence "(if ∃j1 . Suc j1<?l ∧ i1 = ?e ! j1 ∧ i3 = ?e ! Suc j1 then top else bot :: 'b) ≠ bot"
from this obtain j1 where 5: "Suc j1 < ?l ∧ i1 = ?e ! j1 ∧ i3 = ?e ! Suc j1"
by meson
have "j1 ≠ ?l1"
using 5 enum_distinct by auto
hence "i1 ≠ last ?e"
apply (subst last_conv_nth)
using 1 apply simp
apply (subst 5)
apply (subst nth_eq_iff_index_eq[of ?e])
using 1 5 enum_distinct by auto
hence 6: "mone (last ?e,i1) = (bot :: 'b)"
have 7: "(?s⇧⊙) (i3,i1) ≠ bot"
using 4 by force
have "⋀j2 . Suc j1 + j2 < ?l ⟶ (?s⇧⊙) (?e ! (Suc j1 + j2),i1) ≠ bot"
proof -
fix j2
show "Suc j1 + j2 < ?l ⟶ (?s⇧⊙) (?e ! (Suc j1 + j2),i1) ≠ bot"
proof (induct j2)
case 0
show ?case
using 5 7 by simp
next
case (Suc j3)
show ?case
proof
assume 8: "Suc j1 + Suc j3 < ?l"
hence "(?s⇧⊙) (?e ! (Suc j1 + j3),i1) ≠ bot"
using Suc by simp
hence "(mone ⊕ ?s ⊙ ?s⇧⊙) (?e ! (Suc j1 + j3),i1) ≠ bot"
by (metis matrix_kleene_algebra.star_left_unfold_equal)
hence 9: "mone (?e ! (Suc j1 + j3),i1) ⊔ (?s ⊙ ?s⇧⊙) (?e ! (Suc j1 + j3),i1) ≠ bot"
have "?e ! (Suc j1 + j3) ≠ i1"
using 5 8 distinct_conv_nth[of ?e] enum_distinct by auto
hence "mone (?e ! (Suc j1 + j3),i1) = (bot :: 'b)"
hence "(?s ⊙ ?s⇧⊙) (?e ! (Suc j1 + j3),i1) ≠ bot"
using 9 by simp
hence "(⨆⇩k ?s (?e ! (Suc j1 + j3),k) * (?s⇧⊙) (k,i1)) ≠ bot"
by (smt (verit, best) times_matrix_def case_prod_conv sup_monoid.sum.cong)
from this obtain i4 where 10: "?s (?e ! (Suc j1 + j3),i4) * (?s⇧⊙) (i4,i1) ≠ bot"
by force
hence "?s (?e ! (Suc j1 + j3),i4) ≠ bot"
by force
hence "(if ∃j4 . Suc j4<?l ∧ ?e ! (Suc j1 + j3) = ?e ! j4 ∧ i4 = ?e ! Suc j4 then top else bot :: 'b) ≠ bot"
from this obtain j4 where 11: "Suc j4<?l ∧ ?e ! (Suc j1 + j3) = ?e ! j4 ∧ i4 = ?e ! Suc j4"
by meson
hence "Suc j1 + j3 = j4"
apply (subst nth_eq_iff_index_eq[of ?e, THEN sym])
using 8 enum_distinct by auto
hence "i4 = ?e ! (Suc j1 + Suc j3)"
using 11 by simp
thus "(?s⇧⊙) (?e ! (Suc j1 + Suc j3),i1) ≠ bot"
using 10 by force
qed
qed
qed
hence "⋀j5 . Suc j1 ≤ j5 ∧ j5 < ?l ⟶ (?s⇧⊙) (?e ! j5,i1) ≠ bot"
using le_Suc_ex by blast
hence "(?s⇧⊙) (last ?e,i1) ≠ bot"
apply (subst last_conv_nth)
using 1 2 5 nat_less_lesseq_pred by auto
hence "(mone ⊕ ?s ⊙ ?s⇧⊙) (last ?e,i1) ≠ bot"
by (metis matrix_kleene_algebra.star_left_unfold_equal)
hence "mone (last ?e,i1) ⊔ (?s ⊙ ?s⇧⊙) (last ?e,i1) ≠ bot"
hence "(?s ⊙ ?s⇧⊙) (last ?e,i1) ≠ bot"
using 6 by simp
hence "(⨆⇩k ?s (last ?e,k) * (?s⇧⊙) (k,i1)) ≠ bot"
by (smt (verit, best) times_matrix_def case_prod_conv sup_monoid.sum.cong)
from this obtain i5 where "?s (last ?e,i5) * (?s⇧⊙) (i5,i1) ≠ bot"
by force
hence "?s (last ?e,i5) ≠ bot"
by force
hence "(if ∃j6 . Suc j6<?l ∧ last ?e = ?e ! j6 ∧ i5 = ?e ! Suc j6 then top else bot :: 'b) ≠ bot"
from this obtain j6 where 12: "Suc j6<?l ∧ last ?e = ?e ! j6 ∧ i5 = ?e ! Suc j6"
by force
hence "?e ! ?l1 = ?e ! j6"
using 1 5 by (metis last_conv_nth)
hence "?l1 = j6"
apply (subst nth_eq_iff_index_eq[of ?e, THEN sym])
using 2 12 enum_distinct by auto
thus False
using 12 by auto
qed

lemma N_matrix_point:
assumes "n < length (enum_class.enum :: 'a list)"
shows "matrix_stone_relation_algebra.point (mnat n :: ('a::enum,'b::linorder_stone_kleene_relation_algebra_tarski_consistent_expansion) square)"
proof -
let ?e = "enum_class.enum :: 'a list"
let ?n = "mnat n :: ('a,'b) square"
let ?s = "msucc :: ('a,'b) square"
let ?z = "mZero :: ('a,'b) square"
have 1: "?n = matrix_monoid.power (?s⇧t) n ⊙ ?z"
using assms N_matrix_power_S' by blast
have "?s = matrix_skra_peano_1.S'"
by (simp add: S'_matrix_S_matrix inf_matrix_def minus_matrix_def uminus_matrix_def)
hence 2: "matrix_p_algebra.regular ?s"
by (metis matrix_skra_peano_2.S'_regular)
have "?n ≠ mbot"
proof
assume "?n = mbot"
hence "?n (?e ! n,?e ! n) = mbot (?e ! n,?e ! n)"
by simp
hence "top = (bot :: 'b)"
thus False
by (metis bot_not_top)
qed
thus "matrix_stone_relation_algebra.point ?n"
using 1 2 by (metis (no_types, lifting) matrix'_skra_peano_1.S_univalent matrix'_skra_peano_1.Z_point matrix_stone_relation_algebra.injective_power_closed matrix_stone_relation_algebra_tarski_consistent.regular_injective_vector_point_xor_bot matrix_stone_relation_algebra.regular_power_closed matrix_stone_relation_algebra.bijective_regular matrix_stone_relation_algebra.comp_associative matrix_stone_relation_algebra.injective_mult_closed matrix_stone_relation_algebra.regular_conv_closed matrix_stone_relation_algebra.regular_mult_closed matrix_stone_relation_algebra.univalent_conv_injective)
qed

lemma N_matrix_power_S'_hom_lesseq:
assumes "m < length (enum_class.enum :: 'a list)"
and "n < length (enum_class.enum :: 'a list)"
shows "m < n ⟷ mnat m ≼ msucc ⊙ msucc⇧⊙ ⊙ (mnat n :: ('a::enum,'b::linorder_stone_kleene_relation_algebra_tarski_consistent_expansion) square)"
proof -
let ?m = "mnat m :: ('a,'b) square"
let ?n = "mnat n :: ('a,'b) square"
let ?s = "msucc :: ('a,'b) square"
let ?z = "mZero :: ('a,'b) square"
have 1: "?m = matrix_monoid.power (?s⇧t) m ⊙ ?z"
using assms(1) N_matrix_power_S' by blast
have 2: "?n = matrix_monoid.power (?s⇧t) n ⊙ ?z"
using assms(2) N_matrix_power_S' by blast
have 3: "matrix_stone_relation_algebra.point ?m"
have 4: "matrix_stone_relation_algebra.point ?n"
show "m < n ⟷ ?m ≼ ?s ⊙ ?s⇧⊙ ⊙ ?n"
proof
assume "m < n"
from this obtain k where "n = Suc k + m"
hence "?n = matrix_monoid.power (?s⇧t) (Suc k) ⊙ matrix_monoid.power (?s⇧t) m ⊙ ?z"
also have "... = matrix_monoid.power (?s⇧t) (Suc k) ⊙ ?m"
using 1 by (simp add: matrix_monoid.mult_assoc)
also have "... = (matrix_monoid.power ?s (Suc k))⇧t ⊙ ?m"
by (metis matrix_stone_relation_algebra.power_conv_commute)
finally have "?m ≼ matrix_monoid.power ?s (Suc k) ⊙ ?n"
using 3 4 by (simp add: matrix_stone_relation_algebra.bijective_reverse)
also have "... = ?s ⊙ matrix_monoid.power ?s k ⊙ ?n"
by simp
also have "... ≼ ?s ⊙ ?s⇧⊙ ⊙ ?n"
using matrix_idempotent_semiring.mult_left_isotone matrix_idempotent_semiring.mult_right_isotone matrix_kleene_algebra.star.power_below_circ by blast
finally show "?m ≼ ?s ⊙ ?s⇧⊙ ⊙ ?n"
.
next
assume 5: "?m ≼ ?s ⊙ ?s⇧⊙ ⊙ ?n"
show "m < n"
proof (rule ccontr)
assume "¬ m < n"
from this obtain k where "m = k + n"
hence "?m = matrix_monoid.power (?s⇧t) k ⊙ matrix_monoid.power (?s⇧t) n ⊙ ?z"
also have "... = matrix_monoid.power (?s⇧t) k ⊙ ?n"
using 2 by (simp add: matrix_monoid.mult_assoc)
also have "... = (matrix_monoid.power ?s k)⇧t ⊙ ?n"
by (metis matrix_stone_relation_algebra.power_conv_commute)
finally have "?n ≼ matrix_monoid.power ?s k ⊙ ?m"
using 3 4 by (simp add: matrix_stone_relation_algebra.bijective_reverse)
also have "... ≼ ?s⇧⊙ ⊙ ?m"
using matrix_kleene_algebra.star.power_below_circ matrix_stone_relation_algebra.comp_left_isotone by blast
finally have "?n ≼ ?s⇧⊙ ⊙ ?m"
.
hence "?m ≼ ?s ⊙ ?s⇧⊙ ⊙ ?s⇧⊙ ⊙ ?m"
using 5 by (metis (no_types, opaque_lifting) matrix_monoid.mult_assoc matrix_order.dual_order.trans matrix_stone_relation_algebra.comp_right_isotone)
hence "?m ≼ ?s ⊙ ?s⇧⊙ ⊙ ?m"
by (metis matrix_kleene_algebra.star.circ_transitive_equal matrix_monoid.mult_assoc)
thus False
using 3 S'_matrix_acyclic matrix_stone_kleene_relation_algebra_consistent.acyclic_reachable_different by blast
qed
qed
qed

end

```