Theory Inf_Matrix
section ‹Infinite Matrices›
theory Inf_Matrix
imports Finite_Suprema
begin
text ‹Matrices are functions from two index sets into some suitable
algebra. We consider arbitrary index sets, not necessarily the
positive natural numbers up to some bounds; our coefficient algebra is
a dioid. Our only restriction is that summation in the product of
matrices is over a finite index set. This follows essentially Droste
and Kuich's introductory article in the Handbook of Weighted Automata~\<^cite>‹"weightedautomata09"›.
Under these assumptions we show that dioids are closed under matrix
formation. Our proofs are similar to those for formal power series,
but simpler.›
type_synonym ('a, 'b, 'c) matrix = "'a ⇒ 'b ⇒ 'c"
definition mat_one :: "('a, 'a, 'c::dioid_one_zero) matrix" ("ε") where
"ε i j ≡ (if (i = j) then 1 else 0)"
definition mat_zero :: "('a, 'b, 'c::dioid_one_zero) matrix" ("δ") where
"δ ≡ λj i. 0"
definition mat_add :: "('a, 'b, 'c::dioid_one_zero) matrix ⇒ ('a, 'b, 'c) matrix ⇒ ('a, 'b, 'c) matrix" (infixl "⊕" 70) where
"(f ⊕ g) ≡ λi j. (f i j) + (g i j)"
lemma mat_add_assoc: "(f ⊕ g) ⊕ h = f ⊕ (g ⊕ h)"
by (auto simp add: mat_add_def join.sup_assoc)
lemma mat_add_comm: "f ⊕ g = g ⊕ f"
by (auto simp add: mat_add_def join.sup_commute)
lemma mat_add_idem[simp]: "f ⊕ f = f"
by (auto simp add: mat_add_def)
lemma mat_zerol[simp]: "f ⊕ δ = f"
by (auto simp add: mat_add_def mat_zero_def)
lemma mat_zeror[simp]: "δ ⊕ f = f"
by (auto simp add: mat_add_def mat_zero_def)
definition mat_mult :: "('a, 'k::finite, 'c::dioid_one_zero) matrix ⇒ ('k, 'b, 'c) matrix ⇒ ('a, 'b, 'c) matrix" (infixl "⊗" 60) where
"(f ⊗ g) i j ≡ ∑ {(f i k) ⋅ (g k j) | k. k ∈ UNIV}"
lemma mat_annil[simp]: "δ ⊗ f = δ"
by (rule ext, auto simp add: mat_mult_def mat_zero_def)
lemma mat_annir[simp]: "f ⊗ δ = δ"
by (rule ext, auto simp add: mat_mult_def mat_zero_def)
lemma mat_distl: "f ⊗ (g ⊕ h) = (f ⊗ g) ⊕ (f ⊗ h)"
proof -
{
fix i j
have "(f ⊗ (g ⊕ h)) i j = ∑{f i k ⋅ (g k j + h k j) |k. k ∈ UNIV}"
by (simp only: mat_mult_def mat_add_def)
also have "... = ∑{f i k ⋅ g k j + f i k ⋅ h k j |k. k ∈ UNIV}"
by (simp only: distrib_left)
also have "... = ∑{f i k ⋅ g k j |k. k ∈ UNIV} + ∑{f i k ⋅ h k j |k. k ∈ UNIV}"
by (simp only: fset_to_im sum_fun_sum finite_UNIV)
finally have "(f ⊗ (g ⊕ h)) i j = ((f ⊗ g) ⊕ (f ⊗ h)) i j"
by (simp only: mat_mult_def mat_add_def)
}
thus ?thesis
by auto
qed
lemma mat_distr: "(f ⊕ g) ⊗ h = (f ⊗ h) ⊕ (g ⊗ h)"
proof -
{
fix i j
have "((f ⊕ g) ⊗ h) i j = ∑{(f i k + g i k) ⋅ h k j |k. k ∈ UNIV}"
by (simp only: mat_mult_def mat_add_def)
also have "... = ∑{f i k ⋅ h k j + g i k ⋅ h k j |k. k ∈ UNIV}"
by (simp only: distrib_right)
also have "... = ∑{f i k ⋅ h k j |k. k ∈ UNIV} + ∑{g i k ⋅ h k j |k. k ∈ UNIV}"
by (simp only: fset_to_im sum_fun_sum finite_UNIV)
finally have "((f ⊕ g) ⊗ h) i j = ((f ⊗ h) ⊕ (g ⊗ h)) i j"
by (simp only: mat_mult_def mat_add_def)
}
thus ?thesis
by auto
qed
lemma logic_aux1: "(∃k. (i = k ⟶ x = f i j) ∧ (i ≠ k ⟶ x = 0)) ⟷ (∃k. i = k ∧ x = f i j) ∨ (∃k. i ≠ k ∧ x = 0)"
by blast
lemma logic_aux2: "(∃k. (k = j ⟶ x = f i j) ∧ (k ≠ j ⟶ x = 0)) ⟷ (∃k. k = j ∧ x = f i j) ∨ (∃k. k ≠ j ∧ x = 0)"
by blast
lemma mat_onel[simp]: "ε ⊗ f = f"
proof -
{
fix i j
have "(ε ⊗ f) i j = ∑{x. (∃k. (i = k ⟶ x = f i j) ∧ (i ≠ k ⟶ x = 0))}"
by (auto simp add: mat_mult_def mat_one_def)
also have "... = ∑({x. ∃k. (i = k ∧ x = f i j)} ∪ {x. ∃k. (i ≠ k ∧ x = 0)})"
by (simp only: Collect_disj_eq logic_aux1)
also have "... = ∑{x. ∃k. (i = k ∧ x = f i j)} + ∑{x. ∃k. (i ≠ k ∧ x = 0)}"
by (rule sum_union, auto)
finally have "(ε ⊗ f) i j = f i j"
by (auto simp add: sum.neutral)
}
thus ?thesis
by auto
qed
lemma mat_oner[simp]: "f ⊗ ε = f"
proof -
{
fix i j
have "(f ⊗ ε) i j = ∑{x. (∃k. (k = j ⟶ x = f i j) ∧ (k ≠ j ⟶ x = 0))}"
by (auto simp add: mat_mult_def mat_one_def)
also have "... = ∑({x. ∃k. (k = j ∧ x = f i j)} ∪ {x. ∃k. (k ≠ j ∧ x = 0)})"
by (simp only: Collect_disj_eq logic_aux2)
also have "... = ∑{x. ∃k. (k = j ∧ x = f i j)} + ∑{x. ∃k. (k ≠ j ∧ x = 0)}"
by (rule sum_union, auto)
finally have "(f ⊗ ε) i j = f i j"
by (auto simp add: sum.neutral)
}
thus ?thesis
by auto
qed
lemma mat_rearrange:
fixes F :: "'a ⇒ 'k1 ⇒ 'k2 ⇒ 'b ⇒ 'c::dioid_one_zero"
assumes fUNk1: "finite (UNIV::'k1 set)"
assumes fUNk2: "finite (UNIV::'k2 set)"
shows "∑{∑{F i k1 k2 j |k2. k2 ∈ (UNIV::'k2 set)} |k1. k1 ∈ (UNIV::'k1 set)} = ∑{∑{F i k1 k2 j |k1. k1 ∈ UNIV} |k2. k2 ∈ UNIV}"
proof -
{
fix z :: 'c
let ?lhs = "∑{∑{F i k1 k2 j |k2. k2 ∈ UNIV} |k1. k1 ∈ UNIV}"
let ?rhs = "∑{∑{F i k1 k2 j |k1. k1 ∈ UNIV} |k2. k2 ∈ UNIV}"
have "?lhs ≤ z ⟷ (∀k1 k2. F i k1 k2 j ≤ z)"
by (simp only: fset_to_im sum_fun_image_sup fUNk1 fUNk2, auto)
hence "?lhs ≤ z ⟷ ?rhs ≤ z"
by (simp only: fset_to_im sum_fun_image_sup fUNk1 fUNk2, auto)
}
thus ?thesis
by (simp add: eq_iff)
qed
lemma mat_mult_assoc: "f ⊗ (g ⊗ h) = (f ⊗ g) ⊗ h"
proof -
{
fix i j
have "(f ⊗ (g ⊗ h)) i j = ∑{f i k1 ⋅ ∑{g k1 k2 ⋅ h k2 j |k2. k2 ∈ UNIV} |k1. k1 ∈ UNIV}"
by (simp only: mat_mult_def)
also have "... = ∑{∑{f i k1 ⋅ g k1 k2 ⋅ h k2 j |k2. k2 ∈ UNIV} |k1. k1 ∈ UNIV}"
by (simp only: fset_to_im sum_fun_distl finite_UNIV mult.assoc)
also have "... = ∑{∑{(f i k1 ⋅ g k1 k2) ⋅ h k2 j|k1. k1 ∈ UNIV} |k2. k2 ∈ UNIV}"
by (rule mat_rearrange, auto simp add: finite_UNIV)
also have "... = ∑{∑{f i k1 ⋅ g k1 k2 |k1. k1 ∈ UNIV} ⋅ h k2 j |k2. k2 ∈ UNIV}"
by (simp only: fset_to_im sum_fun_distr finite_UNIV)
finally have "(f ⊗ (g ⊗ h)) i j = ((f ⊗ g) ⊗ h) i j "
by (simp only: mat_mult_def)
}
thus ?thesis
by auto
qed
definition mat_less_eq :: "('a, 'b, 'c::dioid_one_zero) matrix ⇒ ('a, 'b, 'c) matrix ⇒ bool" where
"mat_less_eq f g = (f ⊕ g = g)"
definition mat_less :: "('a, 'b, 'c::dioid_one_zero) matrix ⇒ ('a, 'b, 'c) matrix ⇒ bool" where
"mat_less f g = (mat_less_eq f g ∧ f ≠ g)"