Theory Matrix_Kleene_Algebras
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.
›