(* Title:      Matrix Model of Kleene Algebra
   Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Matrices›

theory Matrix
imports "HOL-Library.Word" Dioid
begin

text ‹In this section we formalise a perhaps more natural version of
  of fixed dimension ($m \times n$-matrices). It is well known
  such matrices over a Kleene algebra form a Kleene
 ~cite‹"conway71regular"›.›

subsection ‹Type Definition›

typedef (overloaded) 'a atMost = "{..<LENGTH('a::len)}"
by auto

declare Rep_atMost_inject [simp]

lemma UNIV_atMost:
  "(UNIV::'a atMost set) = Abs_atMost ` {..<LENGTH('a::len)}"
 apply auto
 apply (rule Abs_atMost_induct)
 apply auto
done

lemma finite_UNIV_atMost [simp]: "finite (UNIV::('a::len) atMost set)"
  by (simp add: UNIV_atMost)

text ‹Our matrix type is similar to \mbox{‹'a^'n^'m›} from
 \em HOL/Multivariate\_Analysis/Finite\_Cartesian\_Product.thy}, but
 i)~we explicitly define a type constructor for matrices and square
 , and (ii)~in the definition of operations, e.g., matrix
 , we impose weaker sort requirements on the element
 .›

context notes [[typedef_overloaded]]
begin

datatype ('a,'m,'n) matrix = Matrix "'m atMost → 'n atMost → 'a"

datatype ('a,'m) sqmatrix = SqMatrix "'m atMost → 'm atMost → 'a"

end

fun sqmatrix_of_matrix where
  "sqmatrix_of_matrix (Matrix A) = SqMatrix A"

fun matrix_of_sqmatrix where
  "matrix_of_sqmatrix (SqMatrix A) = Matrix A"


subsection ‹0 and 1›

instantiation matrix :: (zero,type,type) zero
begin
  definition zero_matrix_def: "0 ≡ Matrix (λi j. 0)"
  instance ..
end

instantiation sqmatrix :: (zero,type) zero
begin
  definition zero_sqmatrix_def: "0 ≡ SqMatrix (λi j. 0)"
  instance ..
end

text ‹Tricky sort issues: compare @{term one_matrix} with @{term
 } \dots›

instantiation matrix :: ("{zero,one}",len,len) one
begin
  definition one_matrix_def:
    "1 ≡ Matrix (λi j. if Rep_atMost i = Rep_atMost j then 1 else 0)"
  instance ..
end

instantiation sqmatrix :: ("{zero,one}",type) one
begin
  definition one_sqmatrix_def:
    "1 ≡ SqMatrix (λi j. if i = j then 1 else 0)"
  instance ..
end


subsection ‹Matrix Addition›

fun matrix_plus where
  "matrix_plus (Matrix A) (Matrix B) = Matrix (λi j. A i j + B i j)"

instantiation matrix :: (plus,type,type) plus
begin
  definition plus_matrix_def: "A + B ≡ matrix_plus A B"
  instance ..
end

lemma plus_matrix_def' [simp]:
  "Matrix A + Matrix B = Matrix (λi j. A i j + B i j)"
  by (simp add: plus_matrix_def)

instantiation sqmatrix :: (plus,type) plus
begin
  definition plus_sqmatrix_def:
    "A + B ≡ sqmatrix_of_matrix (matrix_of_sqmatrix A + matrix_of_sqmatrix B)"
  instance ..
end

lemma plus_sqmatrix_def' [simp]:
  "SqMatrix A + SqMatrix B = SqMatrix (λi j. A i j + B i j)"
  by (simp add: plus_sqmatrix_def)

lemma matrix_add_0_right [simp]:
  "A + 0 = (A::('a::monoid_add,'m,'n) matrix)"
  by (cases A, simp add: zero_matrix_def)

lemma matrix_add_0_left [simp]:
  "0 + A = (A::('a::monoid_add,'m,'n) matrix)"
  by (cases A, simp add: zero_matrix_def)

lemma matrix_add_commute [simp]:
  "(A::('a::ab_semigroup_add,'m,'n) matrix) + B = B + A"
  by (cases A, cases B, simp add: add.commute)

lemma matrix_add_assoc:
  "(A::('a::semigroup_add,'m,'n) matrix) + B + C = A + (B + C)"
  by (cases A, cases B, cases C, simp add: add.assoc)

lemma matrix_add_left_commute [simp]:
  "(A::('a::ab_semigroup_add,'m,'n) matrix) + (B + C) = B + (A + C)"
  by (metis matrix_add_assoc matrix_add_commute)

lemma sqmatrix_add_0_right [simp]:
  "A + 0 = (A::('a::monoid_add,'m) sqmatrix)"
  by (cases A, simp add: zero_sqmatrix_def)

lemma sqmatrix_add_0_left [simp]:
  "0 + A = (A::('a::monoid_add,'m) sqmatrix)"
  by (cases A, simp add: zero_sqmatrix_def)

lemma sqmatrix_add_commute [simp]:
  "(A::('a::ab_semigroup_add,'m) sqmatrix) + B = B + A"
  by (cases A, cases B, simp add: add.commute)

lemma sqmatrix_add_assoc:
  "(A::('a::semigroup_add,'m) sqmatrix) + B + C = A + (B + C)"
  by (cases A, cases B, cases C, simp add: add.assoc)

lemma sqmatrix_add_left_commute [simp]:
  "(A::('a::ab_semigroup_add,'m) sqmatrix) + (B + C) = B + (A + C)"
  by (metis sqmatrix_add_commute sqmatrix_add_assoc)


subsection ‹Order (via Addition)›

instantiation matrix :: (plus,type,type) plus_ord
begin
  definition less_eq_matrix_def:
    "(A::('a, 'b, 'c) matrix) ≤ B ≡ A + B = B"
  definition less_matrix_def:
    "(A::('a, 'b, 'c) matrix) < B ≡ A ≤ B ∧ A ≠ B"

  instance
  proof
    fix A B :: "('a, 'b, 'c) matrix"
    show "A ≤ B ⟷ A + B = B"
      by (metis less_eq_matrix_def)
    show "A < B ⟷ A ≤ B ∧ A ≠ B"
      by (metis less_matrix_def)
  qed
end

instantiation sqmatrix :: (plus,type) plus_ord
begin
  definition less_eq_sqmatrix_def:
    "(A::('a, 'b) sqmatrix) ≤ B ≡ A + B = B"
  definition less_sqmatrix_def:
    "(A::('a, 'b) sqmatrix) < B ≡ A ≤ B ∧ A ≠ B"

  instance
  proof
    fix A B :: "('a, 'b) sqmatrix"
    show "A ≤ B ⟷ A + B = B"
      by (metis less_eq_sqmatrix_def)
    show "A < B ⟷ A ≤ B ∧ A ≠ B"
      by (metis less_sqmatrix_def)
  qed
end


subsection ‹Matrix Multiplication›

fun matrix_times :: "('a::{comm_monoid_add,times},'m,'k) matrix → ('a,'k,'n) matrix → ('a,'m,'n) matrix" where
  "matrix_times (Matrix A) (Matrix B) = Matrix (λi j. sum (λk. A i k * B k j) (UNIV::'k atMost set))"

notation matrix_times (infixl ‹*_M› 70)

instantiation sqmatrix :: ("{comm_monoid_add,times}",type) times
begin
  definition times_sqmatrix_def:
    "A * B = sqmatrix_of_matrix (matrix_of_sqmatrix A *_M matrix_of_sqmatrix B)"
  instance ..
end

lemma times_sqmatrix_def' [simp]:
  "SqMatrix A * SqMatrix B = SqMatrix (λi j. sum (λk. A i k * B k j) (UNIV::'k atMost set))"
  by (simp add: times_sqmatrix_def)

lemma matrix_mult_0_right [simp]:
  "(A::('a::{comm_monoid_add,mult_zero},'m,'n) matrix) *_M 0 = 0"
  by (cases A, simp add: zero_matrix_def)

lemma matrix_mult_0_left [simp]:
  "0 *_M (A::('a::{comm_monoid_add,mult_zero},'m,'n) matrix) = 0"
  by (cases A, simp add: zero_matrix_def)

lemma sum_delta_r_0 [simp]:
  "[ finite S; j ∉ S ] ==> (∑k∈S. f k * (if k = j then 1 else (0::'b::{semiring_0,monoid_mult}))) = 0"
  by (induct S rule: finite_induct, auto)

lemma sum_delta_r_1 [simp]:
  "[ finite S; j ∈ S ] ==> (∑k∈S. f k * (if k = j then 1 else (0::'b::{semiring_0,monoid_mult}))) = f j"
  by (induct S rule: finite_induct, auto)

lemma matrix_mult_1_right [simp]:
  "(A::('a::{semiring_0,monoid_mult},'m::len,'n::len) matrix) *_M 1 = A"
  by (cases A, simp add: one_matrix_def)

lemma sum_delta_l_0 [simp]:
  "[ finite S; i ∉ S ] ==> (∑k∈S. (if i = k then 1 else (0::'b::{semiring_0,monoid_mult})) * f k j) = 0"
  by (induct S rule: finite_induct, auto)

lemma sum_delta_l_1 [simp]:
  "[ finite S; i ∈ S ] ==> (∑k∈S. (if i = k then 1 else (0::'b::{semiring_0,monoid_mult})) * f k j) = f i j"
  by (induct S rule: finite_induct, auto)

lemma matrix_mult_1_left [simp]:
  "1 *_M (A::('a::{semiring_0,monoid_mult},'m::len,'n::len) matrix) = A"
  by (cases A, simp add: one_matrix_def)

lemma matrix_mult_assoc:
  "(A::('a::semiring_0,'m,'n) matrix) *_M B *_M C = A *_M (B *_M C)"
 apply (cases A)
 apply (cases B)
 apply (cases C)
 apply (simp add: sum_distrib_right sum_distrib_left mult.assoc)
 apply (subst sum.swap)
 apply (rule refl)
done

lemma matrix_mult_distrib_left:
  "(A::('a::{comm_monoid_add,semiring},'m,'n::len) matrix) *_M (B + C) = A *_M B + A *_M C"
  by (cases A, cases B, cases C, simp add: distrib_left sum.distrib)

lemma matrix_mult_distrib_right:
  "((A::('a::{comm_monoid_add,semiring},'m,'n::len) matrix) + B) *_M C = A *_M C + B *_M C"
  by (cases A, cases B, cases C, simp add: distrib_right sum.distrib)

lemma sqmatrix_mult_0_right [simp]:
  "(A::('a::{comm_monoid_add,mult_zero},'m) sqmatrix) * 0 = 0"
  by (cases A, simp add: zero_sqmatrix_def)

lemma sqmatrix_mult_0_left [simp]:
  "0 * (A::('a::{comm_monoid_add,mult_zero},'m) sqmatrix) = 0"
  by (cases A, simp add: zero_sqmatrix_def)

lemma sqmatrix_mult_1_right [simp]:
  "(A::('a::{semiring_0,monoid_mult},'m::len) sqmatrix) * 1 = A"
  by (cases A, simp add: one_sqmatrix_def)

lemma sqmatrix_mult_1_left [simp]:
  "1 * (A::('a::{semiring_0,monoid_mult},'m::len) sqmatrix) = A"
  by (cases A, simp add: one_sqmatrix_def)

lemma sqmatrix_mult_assoc:
  "(A::('a::{semiring_0,monoid_mult},'m) sqmatrix) * B * C = A * (B * C)"
 apply (cases A)
 apply (cases B)
 apply (cases C)
 apply (simp add: sum_distrib_right sum_distrib_left mult.assoc)
 apply (subst sum.swap)
 apply (rule refl)
done

lemma sqmatrix_mult_distrib_left:
  "(A::('a::{comm_monoid_add,semiring},'m::len) sqmatrix) * (B + C) = A * B + A * C"
  by (cases A, cases B, cases C, simp add: distrib_left sum.distrib)

lemma sqmatrix_mult_distrib_right:
  "((A::('a::{comm_monoid_add,semiring},'m::len) sqmatrix) + B) * C = A * C + B * C"
  by (cases A, cases B, cases C, simp add: distrib_right sum.distrib)


subsection ‹Square-Matrix Model of Dioids›

text ‹The following subclass proofs are necessary to connect parts
  our algebraic hierarchy to the hierarchy found in the Isabelle/HOL
 .›

subclass (in ab_near_semiring_one_zerol) comm_monoid_add
proof
  fix a :: 'a
  show "0 + a = a"
    by (fact add_zerol)
qed

subclass (in semiring_one_zero) semiring_0
proof
  fix a :: 'a
  show "0 * a = 0"
    by (fact annil)
  show "a * 0 = 0"
    by (fact annir)
qed

subclass (in ab_near_semiring_one) monoid_mult ..

instantiation sqmatrix :: (dioid_one_zero,len) dioid_one_zero
begin
  instance
  proof
    fix A B C :: "('a, 'b) sqmatrix"
    show "A + B + C = A + (B + C)"
      by (fact sqmatrix_add_assoc)
    show "A + B = B + A"
      by (fact sqmatrix_add_commute)
    show "A * B * C = A * (B * C)"
      by (fact sqmatrix_mult_assoc)
    show "(A + B) * C = A * C + B * C"
      by (fact sqmatrix_mult_distrib_right)
    show "1 * A = A"
      by (fact sqmatrix_mult_1_left)
    show "A * 1 = A"
      by (fact sqmatrix_mult_1_right)
    show "0 + A = A"
      by (fact sqmatrix_add_0_left)
    show "0 * A = 0"
      by (fact sqmatrix_mult_0_left)
    show "A * 0 = 0"
      by (fact sqmatrix_mult_0_right)
    show "A + A = A"
      by (cases A, simp)
    show "A * (B + C) = A * B + A * C"
      by (fact sqmatrix_mult_distrib_left)
  qed
end

subsection ‹Kleene Star for Matrices›

text ‹We currently do not implement the Kleene star of matrices,
  this is complicated.›

end