Theory Jordan_Normal_Form.Matrix

(*
    Author:      René Thiemann
                 Akihisa Yamada
    License:     BSD
*)
(* with contributions from Alexander Bentkamp, Universität des Saarlandes *)

section‹Vectors and Matrices›

text ‹We define vectors as pairs of dimension and a characteristic function from natural numbers
to elements.
Similarly, matrices are defined as triples of two dimensions and one
characteristic function from pairs of natural numbers to elements.
Via a subtype we ensure that the characteristic function always behaves the same
on indices outside the intended one. Hence, every matrix has a unique representation.

In this part we define basic operations like matrix-addition, -multiplication, scalar-product,
etc. We connect these operations to HOL-Algebra with its explicit carrier sets.›

theory Matrix
imports
  Polynomial_Interpolation.Ring_Hom
  Missing_Ring
  Conjugate
  "HOL-Algebra.Module"
begin

subsection‹Vectors›

text ‹Here we specify which value should be returned in case
  an index is out of bounds. The current solution has the advantage
  that in the implementation later on, no index comparison has to be performed.›

definition undef_vec :: "nat ⇒ 'a" where
  "undef_vec i ≡ [] ! i"

definition mk_vec :: "nat ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)" where
  "mk_vec n f ≡ λ i. if i < n then f i else undef_vec (i - n)"

typedef 'a vec = "{(n, mk_vec n f) | n f :: nat ⇒ 'a. True}"
  by auto

setup_lifting type_definition_vec

lift_definition dim_vec :: "'a vec ⇒ nat" is fst .
lift_definition vec_index :: "'a vec ⇒ (nat ⇒ 'a)" (infixl "$" 100) is snd .
lift_definition vec :: "nat ⇒ (nat ⇒ 'a) ⇒ 'a vec"
  is "λ n f. (n, mk_vec n f)" by auto

lift_definition vec_of_list :: "'a list ⇒ 'a vec" is
  "λ v. (length v, mk_vec (length v) (nth v))" by auto

lift_definition list_of_vec :: "'a vec ⇒ 'a list" is
  "λ (n,v). map v [0 ..< n]" .

definition carrier_vec :: "nat ⇒ 'a vec set" where
  "carrier_vec n = { v . dim_vec v = n}"

lemma carrier_vec_dim_vec[simp]: "v ∈ carrier_vec (dim_vec v)" unfolding carrier_vec_def by auto

lemma dim_vec[simp]: "dim_vec (vec n f) = n" by transfer simp
lemma vec_carrier[simp]: "vec n f ∈ carrier_vec n" unfolding carrier_vec_def by auto
lemma index_vec[simp]: "i < n ⟹ vec n f $ i = f i" by transfer (simp add: mk_vec_def)
lemma eq_vecI[intro]: "(⋀ i. i < dim_vec w ⟹ v $ i = w $ i) ⟹ dim_vec v = dim_vec w
  ⟹ v = w"
  by (transfer, auto simp: mk_vec_def)

lemma carrier_dim_vec: "v ∈ carrier_vec n ⟷ dim_vec v = n"
  unfolding carrier_vec_def by auto

lemma carrier_vecD[simp]: "v ∈ carrier_vec n ⟹ dim_vec v = n" using carrier_dim_vec by auto

lemma carrier_vecI: "dim_vec v = n ⟹ v ∈ carrier_vec n" using carrier_dim_vec by auto

instantiation vec :: (plus) plus
begin
definition plus_vec :: "'a vec ⇒ 'a vec ⇒ 'a :: plus vec" where
  "v⇩1 + v⇩2 ≡ vec (dim_vec v⇩2) (λ i. v⇩1 $ i + v⇩2 $ i)"
instance ..
end

instantiation vec :: (minus) minus
begin
definition minus_vec :: "'a vec ⇒ 'a vec ⇒ 'a :: minus vec" where
  "v⇩1 - v⇩2 ≡ vec (dim_vec v⇩2) (λ i. v⇩1 $ i - v⇩2 $ i)"
instance ..
end

definition
  zero_vec :: "nat ⇒ 'a :: zero vec" ("0⇩v")
  where "0⇩v n ≡ vec n (λ i. 0)"

lemma zero_carrier_vec[simp]: "0⇩v n ∈ carrier_vec n"
  unfolding zero_vec_def carrier_vec_def by auto

lemma index_zero_vec[simp]: "i < n ⟹ 0⇩v n $ i = 0" "dim_vec (0⇩v n) = n"
  unfolding zero_vec_def by auto

lemma vec_of_dim_0[simp]: "dim_vec v = 0 ⟷ v = 0⇩v 0" by auto

definition
  unit_vec :: "nat ⇒ nat ⇒ ('a :: zero_neq_one) vec"
  where "unit_vec n i = vec n (λ j. if j = i then 1 else 0)"

lemma index_unit_vec[simp]:
  "i < n ⟹ j < n ⟹ unit_vec n i $ j = (if j = i then 1 else 0)"
  "i < n ⟹ unit_vec n i $ i = 1"
  "dim_vec (unit_vec n i) = n"
  unfolding unit_vec_def by auto

lemma unit_vec_eq[simp]:
  assumes i: "i < n"
  shows "(unit_vec n i = unit_vec n j) = (i = j)"
proof -
  have "i ≠ j ⟹ unit_vec n i $ i ≠ unit_vec n j $ i"
    unfolding unit_vec_def using i by simp
  then show ?thesis by metis
qed

lemma unit_vec_nonzero[simp]:
  assumes i_n: "i < n" shows "unit_vec n i ≠ zero_vec n" (is "?l ≠ ?r")
proof -
  have "?l $ i = 1" "?r $ i = 0" using i_n by auto
  thus "?l ≠ ?r" by auto
qed

lemma unit_vec_carrier[simp]: "unit_vec n i ∈ carrier_vec n"
  unfolding unit_vec_def carrier_vec_def by auto

definition unit_vecs:: "nat ⇒ 'a :: zero_neq_one vec list"
  where "unit_vecs n = map (unit_vec n) [0..<n]"

text "List of first i units"

fun unit_vecs_first:: "nat ⇒ nat ⇒ 'a::zero_neq_one vec list"
  where "unit_vecs_first n 0 = []"
    |   "unit_vecs_first n (Suc i) = unit_vecs_first n i @ [unit_vec n i]"

lemma unit_vecs_first: "unit_vecs n = unit_vecs_first n n"
  unfolding unit_vecs_def set_map set_upt
proof -
  {fix m
    have "m ≤ n ⟹ map (unit_vec n) [0..<m] = unit_vecs_first n m"
    proof (induct m)
      case (Suc m) then have mn:"m≤n" by auto
        show ?case unfolding upt_Suc using Suc(1)[OF mn] by auto
    qed auto
  }
  thus "map (unit_vec n) [0..<n] = unit_vecs_first n n" by auto
qed

text "list of last i units"

fun unit_vecs_last:: "nat ⇒ nat ⇒ 'a :: zero_neq_one vec list"
  where "unit_vecs_last n 0 = []"
    |   "unit_vecs_last n (Suc i) = unit_vec n (n - Suc i) # unit_vecs_last n i"

lemma unit_vecs_last_carrier: "set (unit_vecs_last n i) ⊆ carrier_vec n"
  by (induct i;auto)

lemma unit_vecs_last[code]: "unit_vecs n = unit_vecs_last n n"
proof -
  { fix m assume "m = n"
    have "m ≤ n ⟹ map (unit_vec n) [n-m..<n] = unit_vecs_last n m"
      proof (induction m)
      case (Suc m)
        then have nm:"n - Suc m < n" by auto
        have ins: "[n - Suc m ..< n] = (n - Suc m) # [n - m ..< n]"
          unfolding upt_conv_Cons[OF nm]
          by (auto simp: Suc.prems Suc_diff_Suc Suc_le_lessD)
        show ?case
          unfolding ins
          unfolding unit_vecs_last.simps
          unfolding list.map
          using Suc
          unfolding Suc by auto
      qed simp
  }
  thus "unit_vecs n = unit_vecs_last n n"
    unfolding unit_vecs_def by auto
qed

lemma unit_vecs_carrier: "set (unit_vecs n) ⊆ carrier_vec n"
proof
  fix u :: "'a vec"  assume u: "u ∈ set (unit_vecs n)"
  then obtain i where "u = unit_vec n i" unfolding unit_vecs_def by auto
  then show "u ∈ carrier_vec n"
    using unit_vec_carrier by auto
qed

lemma unit_vecs_last_distinct:
  "j ≤ n ⟹ i < n - j ⟹ unit_vec n i ∉ set (unit_vecs_last n j)"
  by (induction j arbitrary:i, auto)

lemma unit_vecs_first_distinct:
  "i ≤ j ⟹ j < n ⟹ unit_vec n j ∉ set (unit_vecs_first n i)"
  by (induction i arbitrary:j, auto)

definition map_vec where "map_vec f v ≡ vec (dim_vec v) (λi. f (v $ i))"

instantiation vec :: (uminus) uminus
begin
definition uminus_vec :: "'a :: uminus vec ⇒ 'a vec" where
  "- v ≡ vec (dim_vec v) (λ i. - (v $ i))"
instance ..
end

definition smult_vec :: "'a :: times ⇒ 'a vec ⇒ 'a vec" (infixl "⋅⇩v" 70)
  where "a ⋅⇩v v ≡ vec (dim_vec v) (λ i. a * v $ i)"

definition scalar_prod :: "'a vec ⇒ 'a vec ⇒ 'a :: semiring_0" (infix "∙" 70)
  where "v ∙ w ≡ ∑ i ∈ {0 ..< dim_vec w}. v $ i * w $ i"

definition monoid_vec :: "'a itself ⇒ nat ⇒ ('a :: monoid_add vec) monoid" where
  "monoid_vec ty n ≡ ⦇
    carrier = carrier_vec n,
    mult = (+),
    one = 0⇩v n⦈"

definition module_vec ::
  "'a :: semiring_1 itself ⇒ nat ⇒ ('a,'a vec) module" where
  "module_vec ty n ≡ ⦇
    carrier = carrier_vec n,
    mult = undefined,
    one = undefined,
    zero = 0⇩v n,
    add = (+),
    smult = (⋅⇩v)⦈"

lemma monoid_vec_simps:
  "mult (monoid_vec ty n) = (+)"
  "carrier (monoid_vec ty n) = carrier_vec n"
  "one (monoid_vec ty n) = 0⇩v n"
  unfolding monoid_vec_def by auto

lemma module_vec_simps:
  "add (module_vec ty n) = (+)"
  "zero (module_vec ty n) = 0⇩v n"
  "carrier (module_vec ty n) = carrier_vec n"
  "smult (module_vec ty n) = (⋅⇩v)"
  unfolding module_vec_def by auto

definition finsum_vec :: "'a :: monoid_add itself ⇒ nat ⇒ ('c ⇒ 'a vec) ⇒ 'c set ⇒ 'a vec" where
  "finsum_vec ty n = finprod (monoid_vec ty n)"

lemma index_add_vec[simp]:
  "i < dim_vec v⇩2 ⟹ (v⇩1 + v⇩2) $ i = v⇩1 $ i + v⇩2 $ i" "dim_vec (v⇩1 + v⇩2) = dim_vec v⇩2"
  unfolding plus_vec_def by auto

lemma index_minus_vec[simp]:
  "i < dim_vec v⇩2 ⟹ (v⇩1 - v⇩2) $ i = v⇩1 $ i - v⇩2 $ i" "dim_vec (v⇩1 - v⇩2) = dim_vec v⇩2"
  unfolding minus_vec_def by auto

lemma index_map_vec[simp]:
  "i < dim_vec v ⟹ map_vec f v $ i = f (v $ i)"
  "dim_vec (map_vec f v) = dim_vec v"
  unfolding map_vec_def by auto

lemma map_carrier_vec[simp]: "map_vec h v ∈ carrier_vec n = (v ∈ carrier_vec n)"
  unfolding map_vec_def carrier_vec_def by auto

lemma index_uminus_vec[simp]:
  "i < dim_vec v ⟹ (- v) $ i = - (v $ i)"
  "dim_vec (- v) = dim_vec v"
  unfolding uminus_vec_def by auto

lemma index_smult_vec[simp]:
  "i < dim_vec v ⟹ (a ⋅⇩v v) $ i = a * v $ i" "dim_vec (a ⋅⇩v v) = dim_vec v"
  unfolding smult_vec_def by auto

lemma add_carrier_vec[simp]:
  "v⇩1 ∈ carrier_vec n ⟹ v⇩2 ∈ carrier_vec n ⟹ v⇩1 + v⇩2 ∈ carrier_vec n"
  unfolding carrier_vec_def by auto

lemma minus_carrier_vec[simp]:
  "v⇩1 ∈ carrier_vec n ⟹ v⇩2 ∈ carrier_vec n ⟹ v⇩1 - v⇩2 ∈ carrier_vec n"
  unfolding carrier_vec_def by auto

lemma comm_add_vec[ac_simps]:
  "(v⇩1 :: 'a :: ab_semigroup_add vec) ∈ carrier_vec n ⟹ v⇩2 ∈ carrier_vec n ⟹ v⇩1 + v⇩2 = v⇩2 + v⇩1"
  by (intro eq_vecI, auto simp: ac_simps)

lemma assoc_add_vec[simp]:
  "(v⇩1 :: 'a :: semigroup_add vec) ∈ carrier_vec n ⟹ v⇩2 ∈ carrier_vec n ⟹ v⇩3 ∈ carrier_vec n
  ⟹ (v⇩1 + v⇩2) + v⇩3 = v⇩1 + (v⇩2 + v⇩3)"
  by (intro eq_vecI, auto simp: ac_simps)

lemma zero_minus_vec[simp]: "(v :: 'a :: group_add vec) ∈ carrier_vec n ⟹ 0⇩v n - v = - v"
  by (intro eq_vecI, auto)

lemma minus_zero_vec[simp]: "(v :: 'a :: group_add vec) ∈ carrier_vec n ⟹ v - 0⇩v n = v"
  by (intro eq_vecI, auto)

lemma minus_cancel_vec[simp]: "(v :: 'a :: group_add vec) ∈ carrier_vec n ⟹ v - v = 0⇩v n"
  by (intro eq_vecI, auto)

lemma minus_add_uminus_vec: "(v :: 'a :: group_add vec) ∈ carrier_vec n ⟹
  w ∈ carrier_vec n ⟹ v - w = v + (- w)"
  by (intro eq_vecI, auto)

lemma comm_monoid_vec: "comm_monoid (monoid_vec TYPE ('a :: comm_monoid_add) n)"
  by (unfold_locales, auto simp: monoid_vec_def ac_simps)

lemma left_zero_vec[simp]: "(v :: 'a :: monoid_add vec) ∈ carrier_vec n  ⟹ 0⇩v n + v = v" by auto

lemma right_zero_vec[simp]: "(v :: 'a :: monoid_add vec) ∈ carrier_vec n  ⟹ v + 0⇩v n = v" by auto


lemma uminus_carrier_vec[simp]:
  "(- v ∈ carrier_vec n) = (v ∈ carrier_vec n)"
  unfolding carrier_vec_def by auto

lemma uminus_r_inv_vec[simp]:
  "(v :: 'a :: group_add vec) ∈ carrier_vec n ⟹ (v + - v) = 0⇩v n"
  by (intro eq_vecI, auto)

lemma uminus_l_inv_vec[simp]:
  "(v :: 'a :: group_add vec) ∈ carrier_vec n ⟹ (- v + v) = 0⇩v n"
  by (intro eq_vecI, auto)

lemma add_inv_exists_vec:
  "(v :: 'a :: group_add vec) ∈ carrier_vec n ⟹ ∃ w ∈ carrier_vec n. w + v = 0⇩v n ∧ v + w = 0⇩v n"
  by (intro bexI[of _ "- v"], auto)

lemma comm_group_vec: "comm_group (monoid_vec TYPE ('a :: ab_group_add) n)"
  by (unfold_locales, insert add_inv_exists_vec, auto simp: monoid_vec_def ac_simps Units_def)

lemmas finsum_vec_insert =
  comm_monoid.finprod_insert[OF comm_monoid_vec, folded finsum_vec_def, unfolded monoid_vec_simps]

lemmas finsum_vec_closed =
  comm_monoid.finprod_closed[OF comm_monoid_vec, folded finsum_vec_def, unfolded monoid_vec_simps]

lemmas finsum_vec_empty =
  comm_monoid.finprod_empty[OF comm_monoid_vec, folded finsum_vec_def, unfolded monoid_vec_simps]

lemma smult_carrier_vec[simp]: "(a ⋅⇩v v ∈ carrier_vec n) = (v ∈ carrier_vec n)"
  unfolding carrier_vec_def by auto

lemma scalar_prod_left_zero[simp]: "v ∈ carrier_vec n ⟹ 0⇩v n ∙ v = 0"
  unfolding scalar_prod_def
  by (rule sum.neutral, auto)

lemma scalar_prod_right_zero[simp]: "v ∈ carrier_vec n ⟹ v ∙ 0⇩v n = 0"
  unfolding scalar_prod_def
  by (rule sum.neutral, auto)

lemma scalar_prod_left_unit[simp]: assumes v: "(v :: 'a :: semiring_1 vec) ∈ carrier_vec n" and i: "i < n"
  shows "unit_vec n i ∙ v = v $ i"
proof -
  let ?f = "λ k. unit_vec n i $ k * v $ k"
  have id: "(∑k∈{0..<n}. ?f k) = unit_vec n i $ i * v $ i + (∑k∈{0..<n} - {i}. ?f k)"
    by (rule sum.remove, insert i, auto)
  also have "(∑ k∈{0..<n} - {i}. ?f k) = 0"
    by (rule sum.neutral, insert i, auto)
  finally
  show ?thesis unfolding scalar_prod_def using i v by simp
qed

lemma scalar_prod_right_unit[simp]: assumes i: "i < n"
  shows "(v :: 'a :: semiring_1 vec) ∙ unit_vec n i = v $ i"
proof -
  let ?f = "λ k. v $ k * unit_vec n i $ k"
  have id: "(∑k∈{0..<n}. ?f k) = v $ i * unit_vec n i $ i + (∑k∈{0..<n} - {i}. ?f k)"
    by (rule sum.remove, insert i, auto)
  also have "(∑k∈{0..<n} - {i}. ?f k) = 0"
    by (rule sum.neutral, insert i, auto)
  finally
  show ?thesis unfolding scalar_prod_def using i by simp
qed

lemma add_scalar_prod_distrib: assumes v: "v⇩1 ∈ carrier_vec n" "v⇩2 ∈ carrier_vec n" "v⇩3 ∈ carrier_vec n"
  shows "(v⇩1 + v⇩2) ∙ v⇩3 = v⇩1 ∙ v⇩3 + v⇩2 ∙ v⇩3"
proof -
  have "(∑i∈{0..<dim_vec v⇩3}. (v⇩1 + v⇩2) $ i * v⇩3 $ i) = (∑i∈{0..<dim_vec v⇩3}. v⇩1 $ i * v⇩3 $ i + v⇩2 $ i * v⇩3 $ i)"
    by (rule sum.cong, insert v, auto simp: algebra_simps)
  thus ?thesis unfolding scalar_prod_def using v by (auto simp: sum.distrib)
qed

lemma scalar_prod_add_distrib: assumes v: "v⇩1 ∈ carrier_vec n" "v⇩2 ∈ carrier_vec n" "v⇩3 ∈ carrier_vec n"
  shows "v⇩1 ∙ (v⇩2 + v⇩3) = v⇩1 ∙ v⇩2 + v⇩1 ∙ v⇩3"
proof -
  have "(∑i∈{0..<dim_vec v⇩3}. v⇩1 $ i * (v⇩2 + v⇩3) $ i) = (∑i∈{0..<dim_vec v⇩3}. v⇩1 $ i * v⇩2 $ i + v⇩1 $ i * v⇩3 $ i)"
    by (rule sum.cong, insert v, auto simp: algebra_simps)
  thus ?thesis unfolding scalar_prod_def using v by (auto intro: sum.distrib)
qed

lemma smult_scalar_prod_distrib[simp]: assumes v: "v⇩1 ∈ carrier_vec n" "v⇩2 ∈ carrier_vec n"
  shows "(a ⋅⇩v v⇩1) ∙ v⇩2 = a * (v⇩1 ∙ v⇩2)"
  unfolding scalar_prod_def sum_distrib_left
  by (rule sum.cong, insert v, auto simp: ac_simps)

lemma scalar_prod_smult_distrib[simp]: assumes v: "v⇩1 ∈ carrier_vec n" "v⇩2 ∈ carrier_vec n"
  shows "v⇩1 ∙ (a ⋅⇩v v⇩2) = (a :: 'a :: comm_ring) * (v⇩1 ∙ v⇩2)"
  unfolding scalar_prod_def sum_distrib_left
  by (rule sum.cong, insert v, auto simp: ac_simps)

lemma comm_scalar_prod: assumes "(v⇩1 :: 'a :: comm_semiring_0 vec) ∈ carrier_vec n" "v⇩2 ∈ carrier_vec n"
  shows "v⇩1 ∙ v⇩2 = v⇩2 ∙ v⇩1"
  unfolding scalar_prod_def
  by (rule sum.cong, insert assms, auto simp: ac_simps)

lemma add_smult_distrib_vec:
  "((a::'a::ring) + b) ⋅⇩v v = a ⋅⇩v v + b ⋅⇩v v"
  unfolding smult_vec_def plus_vec_def
  by (rule eq_vecI, auto simp: distrib_right)

lemma smult_add_distrib_vec:
  assumes "v ∈ carrier_vec n" "w ∈ carrier_vec n"
  shows "(a::'a::ring) ⋅⇩v (v + w) = a ⋅⇩v v + a ⋅⇩v w"
  apply (rule eq_vecI)
  unfolding smult_vec_def plus_vec_def
  using assms distrib_left by auto

lemma smult_smult_assoc:
  "a ⋅⇩v (b ⋅⇩v v) = (a * b::'a::ring) ⋅⇩v v"
  apply (rule sym, rule eq_vecI)
  unfolding smult_vec_def plus_vec_def using mult.assoc by auto

lemma one_smult_vec [simp]:
  "(1::'a::ring_1) ⋅⇩v v = v" unfolding smult_vec_def
  by (rule eq_vecI,auto)

lemma uminus_zero_vec[simp]: "- (0⇩v n) = (0⇩v n :: 'a :: group_add vec)" 
  by (intro eq_vecI, auto)

lemma index_finsum_vec: assumes "finite F" and i: "i < n"
  and vs: "vs ∈ F → carrier_vec n"
  shows "finsum_vec TYPE('a :: comm_monoid_add) n vs F $ i = sum (λ f. vs f $ i) F"
  using ‹finite F› vs
proof (induct F)
  case (insert f F)
  hence IH: "finsum_vec TYPE('a) n vs F $ i = (∑f∈F. vs f $ i)"
    and vs: "vs ∈ F → carrier_vec n" "vs f ∈ carrier_vec n" by auto
  show ?case unfolding finsum_vec_insert[OF insert(1-2) vs]
    unfolding sum.insert[OF insert(1-2)]
    unfolding IH[symmetric]
    by (rule index_add_vec, insert i, insert finsum_vec_closed[OF vs(1)], auto)
qed (insert i, auto simp: finsum_vec_empty)

text ‹Definition of pointwise ordering on vectors for non-strict part, and
  strict version is defined in a way such that the @{class order} constraints are satisfied.›

instantiation vec :: (ord) ord
begin

definition less_eq_vec :: "'a vec ⇒ 'a vec ⇒ bool" where
  "less_eq_vec v w = (dim_vec v = dim_vec w ∧ (∀ i < dim_vec w. v $ i ≤ w $ i))" 

definition less_vec :: "'a vec ⇒ 'a vec ⇒ bool" where
  "less_vec v w = (v ≤ w ∧ ¬ (w ≤ v))"
instance ..
end

instantiation vec :: (preorder) preorder
begin
instance
  by (standard, auto simp: less_vec_def less_eq_vec_def order_trans)
end

instantiation vec :: (order) order
begin
instance
  by (standard, intro eq_vecI, auto simp: less_eq_vec_def order.antisym)
end


subsection‹Matrices›

text ‹Similarly as for vectors, we specify which value should be returned in case
  an index is out of bounds. It is defined in a way that only few
  index comparisons have to be performed in the implementation.›

definition undef_mat :: "nat ⇒ nat ⇒ (nat × nat ⇒ 'a) ⇒ nat × nat ⇒ 'a" where
  "undef_mat nr nc f ≡ λ (i,j). [[f (i,j). j <- [0 ..< nc]] . i <- [0 ..< nr]] ! i ! j"

lemma undef_cong_mat: assumes "⋀ i j. i < nr ⟹ j < nc ⟹ f (i,j) = f' (i,j)"
  shows "undef_mat nr nc f x = undef_mat nr nc f' x"
proof (cases x)
  case (Pair i j)
  have nth_map_ge: "⋀ i xs. ¬ i < length xs ⟹ xs ! i = [] ! (i - length xs)"
    by (metis append_Nil2 nth_append)
  note [simp] = Pair undef_mat_def nth_map_ge[of i] nth_map_ge[of j]
  show ?thesis
    by (cases "i < nr", simp, cases "j < nc", insert assms, auto)
qed

definition mk_mat :: "nat ⇒ nat ⇒ (nat × nat ⇒ 'a) ⇒ (nat × nat ⇒ 'a)" where
  "mk_mat nr nc f ≡ λ (i,j). if i < nr ∧ j < nc then f (i,j) else undef_mat nr nc f (i,j)"

lemma cong_mk_mat: assumes "⋀ i j. i < nr ⟹ j < nc ⟹ f (i,j) = f' (i,j)"
  shows "mk_mat nr nc f = mk_mat nr nc f'"
  using undef_cong_mat[of nr nc f f', OF assms]
  using assms unfolding mk_mat_def
  by auto

typedef 'a mat = "{(nr, nc, mk_mat nr nc f) | nr nc f :: nat × nat ⇒ 'a. True}"
  by auto

setup_lifting type_definition_mat

lift_definition dim_row :: "'a mat ⇒ nat" is fst .
lift_definition dim_col :: "'a mat ⇒ nat" is "fst o snd" .
lift_definition index_mat :: "'a mat ⇒ (nat × nat ⇒ 'a)" (infixl "$$" 100) is "snd o snd" .
lift_definition mat :: "nat ⇒ nat ⇒ (nat × nat ⇒ 'a) ⇒ 'a mat"
  is "λ nr nc f. (nr, nc, mk_mat nr nc f)" by auto
lift_definition mat_of_row_fun :: "nat ⇒ nat ⇒ (nat ⇒ 'a vec) ⇒ 'a mat" ("mat⇩r")
  is "λ nr nc f. (nr, nc, mk_mat nr nc (λ (i,j). f i $ j))" by auto

definition mat_to_list :: "'a mat ⇒ 'a list list" where
  "mat_to_list A = [ [A $$ (i,j) . j <- [0 ..< dim_col A]] . i <- [0 ..< dim_row A]]"

fun square_mat :: "'a mat ⇒ bool" where "square_mat A = (dim_col A = dim_row A)"

definition upper_triangular :: "'a::zero mat ⇒ bool"
  where "upper_triangular A ≡
    ∀i < dim_row A. ∀ j < i. A $$ (i,j) = 0"

lemma upper_triangularD[elim] :
  "upper_triangular A ⟹ j < i ⟹ i < dim_row A ⟹ A $$ (i,j) = 0"
unfolding upper_triangular_def by auto

lemma upper_triangularI[intro] :
  "(⋀i j. j < i ⟹ i < dim_row A ⟹ A $$ (i,j) = 0) ⟹ upper_triangular A"
unfolding upper_triangular_def by auto

lemma dim_row_mat[simp]: "dim_row (mat nr nc f) = nr" "dim_row (mat⇩r nr nc g) = nr"
  by (transfer, simp)+

lemma dim_col_mat[simp]: "dim_col (mat nr nc f) = nc" "dim_col (mat⇩r nr nc g) = nc"
  by (transfer, simp)+

definition carrier_mat :: "nat ⇒ nat ⇒ 'a mat set"
  where "carrier_mat nr nc = { m . dim_row m = nr ∧ dim_col m = nc}"

lemma carrier_mat_triv[simp]: "m ∈ carrier_mat (dim_row m) (dim_col m)"
  unfolding carrier_mat_def by auto

lemma mat_carrier[simp]: "mat nr nc f ∈ carrier_mat nr nc"
  unfolding carrier_mat_def by auto

definition elements_mat :: "'a mat ⇒ 'a set"
  where "elements_mat A = set [A $$ (i,j). i <- [0 ..< dim_row A], j <- [0 ..< dim_col A]]"

lemma elements_matD [dest]:
  "a ∈ elements_mat A ⟹ ∃i j. i < dim_row A ∧ j < dim_col A ∧ a = A $$ (i,j)"
  unfolding elements_mat_def by force

lemma elements_matI [intro]:
  "A ∈ carrier_mat nr nc ⟹ i < nr ⟹ j < nc ⟹ a = A $$ (i,j) ⟹ a ∈ elements_mat A"
  unfolding elements_mat_def carrier_mat_def by force

lemma index_mat[simp]:  "i < nr ⟹ j < nc ⟹ mat nr nc f $$ (i,j) = f (i,j)"
  "i < nr ⟹ j < nc ⟹ mat⇩r nr nc g $$ (i,j) = g i $ j"
  by (transfer', simp add: mk_mat_def)+

lemma eq_matI[intro]: "(⋀ i j . i < dim_row B ⟹ j < dim_col B ⟹ A $$ (i,j) = B $$ (i,j))
  ⟹ dim_row A = dim_row B
  ⟹ dim_col A = dim_col B
  ⟹ A = B"
  by (transfer, auto intro!: cong_mk_mat, auto simp: mk_mat_def)

lemma carrier_matI[intro]:
  assumes "dim_row A = nr" "dim_col A = nc" shows  "A ∈ carrier_mat nr nc"
  using assms unfolding carrier_mat_def by auto

lemma carrier_matD[dest,simp]: assumes "A ∈ carrier_mat nr nc"
  shows "dim_row A = nr" "dim_col A = nc" using assms
  unfolding carrier_mat_def by auto

lemma cong_mat: assumes "nr = nr'" "nc = nc'" "⋀ i j. i < nr ⟹ j < nc ⟹
  f (i,j) = f' (i,j)" shows "mat nr nc f = mat nr' nc' f'"
  by (rule eq_matI, insert assms, auto)

definition row :: "'a mat ⇒ nat ⇒ 'a vec" where
  "row A i = vec (dim_col A) (λ j. A $$ (i,j))"

definition rows :: "'a mat ⇒ 'a vec list" where
  "rows A = map (row A) [0..<dim_row A]"

lemma row_carrier[simp]: "row A i ∈ carrier_vec (dim_col A)" unfolding row_def by auto

lemma rows_carrier[simp]: "set (rows A) ⊆ carrier_vec (dim_col A)" unfolding rows_def by auto

lemma length_rows[simp]: "length (rows A) = dim_row A" unfolding rows_def by auto

lemma nth_rows[simp]: "i < dim_row A ⟹ rows A ! i = row A i"
  unfolding rows_def by auto

lemma row_mat_of_row_fun[simp]: "i < nr ⟹ dim_vec (f i) = nc ⟹ row (mat⇩r nr nc f) i = f i"
  by (rule eq_vecI, auto simp: row_def)

lemma set_rows_carrier:
  assumes "A ∈ carrier_mat m n" and "v ∈ set (rows A)" shows "v ∈ carrier_vec n"
  using assms by (auto simp: rows_def row_def)

definition mat_of_rows :: "nat ⇒ 'a vec list ⇒ 'a mat"
  where "mat_of_rows n rs = mat (length rs) n (λ(i,j). rs ! i $ j)"

definition mat_of_rows_list :: "nat ⇒ 'a list list ⇒ 'a mat" where
  "mat_of_rows_list nc rs = mat (length rs) nc (λ (i,j). rs ! i ! j)"

lemma mat_of_rows_carrier[simp]:
  "mat_of_rows n vs ∈ carrier_mat (length vs) n"
  "dim_row (mat_of_rows n vs) = length vs"
  "dim_col (mat_of_rows n vs) = n"
  unfolding mat_of_rows_def by auto

lemma mat_of_rows_row[simp]:
  assumes i:"i < length vs" and n: "vs ! i ∈ carrier_vec n"
  shows "row (mat_of_rows n vs) i = vs ! i"
  unfolding mat_of_rows_def row_def using n i by auto

lemma rows_mat_of_rows[simp]:
  assumes "set vs ⊆ carrier_vec n" shows "rows (mat_of_rows n vs) = vs"
  unfolding rows_def apply (rule nth_equalityI)
  using assms unfolding subset_code(1) by auto

lemma mat_of_rows_rows[simp]:
  "mat_of_rows (dim_col A) (rows A) = A"
  unfolding mat_of_rows_def by (rule, auto simp: row_def)


definition col :: "'a mat ⇒ nat ⇒ 'a vec" where
  "col A j = vec (dim_row A) (λ i. A $$ (i,j))"

definition cols :: "'a mat ⇒ 'a vec list" where
  "cols A = map (col A) [0..<dim_col A]"

definition mat_of_cols :: "nat ⇒ 'a vec list ⇒ 'a mat"
  where "mat_of_cols n cs = mat n (length cs) (λ(i,j). cs ! j $ i)"

definition mat_of_cols_list :: "nat ⇒ 'a list list ⇒ 'a mat" where
  "mat_of_cols_list nr cs = mat nr (length cs) (λ (i,j). cs ! j ! i)"

lemma col_dim[simp]: "col A i ∈ carrier_vec (dim_row A)" unfolding col_def by auto

lemma dim_col[simp]: "dim_vec (col A i) = dim_row A" by auto

lemma cols_dim[simp]: "set (cols A) ⊆ carrier_vec (dim_row A)" unfolding cols_def by auto

lemma cols_length[simp]: "length (cols A) = dim_col A" unfolding cols_def by auto

lemma cols_nth[simp]: "i < dim_col A ⟹ cols A ! i = col A i"
  unfolding cols_def by auto

lemma mat_of_cols_carrier[simp]:
  "mat_of_cols n vs ∈ carrier_mat n (length vs)"
  "dim_row (mat_of_cols n vs) = n"
  "dim_col (mat_of_cols n vs) = length vs"
  unfolding mat_of_cols_def by auto

lemma col_mat_of_cols[simp]:
  assumes j:"j < length vs" and n: "vs ! j ∈ carrier_vec n"
  shows "col (mat_of_cols n vs) j = vs ! j"
  unfolding mat_of_cols_def col_def using j n by auto

lemma cols_mat_of_cols[simp]:
  assumes "set vs ⊆ carrier_vec n" shows "cols (mat_of_cols n vs) = vs"
  unfolding cols_def apply(rule nth_equalityI)
  using assms unfolding subset_code(1) by auto

lemma mat_of_cols_cols[simp]:
  "mat_of_cols (dim_row A) (cols A) = A"
  unfolding mat_of_cols_def by (rule, auto simp: col_def)


instantiation mat :: (ord) ord
begin

definition less_eq_mat :: "'a mat ⇒ 'a mat ⇒ bool" where
  "less_eq_mat A B = (dim_row A = dim_row B ∧ dim_col A = dim_col B ∧ 
      (∀ i < dim_row B. ∀ j < dim_col B. A $$ (i,j) ≤ B $$ (i,j)))" 

definition less_mat :: "'a mat ⇒ 'a mat ⇒ bool" where
  "less_mat A B = (A ≤ B ∧ ¬ (B ≤ A))"
instance ..
end

instantiation mat :: (preorder) preorder
begin
instance
proof (standard, auto simp: less_mat_def less_eq_mat_def, goal_cases)
  case (1 A B C i j)
  thus ?case using order_trans[of "A $$ (i,j)" "B $$ (i,j)" "C $$ (i,j)"] by auto
qed
end

instantiation mat :: (order) order
begin
instance
  by (standard, intro eq_matI, auto simp: less_eq_mat_def order.antisym)
end

instantiation mat :: (plus) plus
begin
definition plus_mat :: "('a :: plus) mat ⇒ 'a mat ⇒ 'a mat" where
  "A + B ≡ mat (dim_row B) (dim_col B) (λ ij. A $$ ij + B $$ ij)"
instance ..
end

definition map_mat :: "('a ⇒ 'b) ⇒ 'a mat ⇒ 'b mat" where
  "map_mat f A ≡ mat (dim_row A) (dim_col A) (λ ij. f (A $$ ij))"

definition smult_mat :: "'a :: times ⇒ 'a mat ⇒ 'a mat" (infixl "⋅⇩m" 70)
  where "a ⋅⇩m A ≡ map_mat (λ b. a * b) A"

definition zero_mat :: "nat ⇒ nat ⇒ 'a :: zero mat" ("0⇩m") where
  "0⇩m nr nc ≡ mat nr nc (λ ij. 0)"

lemma elements_0_mat [simp]: "elements_mat (0⇩m nr nc) ⊆ {0}"
  unfolding elements_mat_def zero_mat_def by auto

definition transpose_mat :: "'a mat ⇒ 'a mat" where
  "transpose_mat A ≡ mat (dim_col A) (dim_row A) (λ (i,j). A $$ (j,i))"

definition one_mat :: "nat ⇒ 'a :: {zero,one} mat" ("1⇩m") where
  "1⇩m n ≡ mat n n (λ (i,j). if i = j then 1 else 0)"

instantiation mat :: (uminus) uminus
begin
definition uminus_mat :: "'a :: uminus mat ⇒ 'a mat" where
  "- A ≡ mat (dim_row A) (dim_col A) (λ ij. - (A $$ ij))"
instance ..
end

instantiation mat :: (minus) minus
begin
definition minus_mat :: "('a :: minus) mat ⇒ 'a mat ⇒ 'a mat" where
  "A - B ≡ mat (dim_row B) (dim_col B) (λ ij. A $$ ij - B $$ ij)"
instance ..
end

instantiation mat :: (semiring_0) times
begin
definition times_mat :: "'a :: semiring_0 mat ⇒ 'a mat ⇒ 'a mat"
  where "A * B ≡ mat (dim_row A) (dim_col B) (λ (i,j). row A i ∙ col B j)"
instance ..
end

definition mult_mat_vec :: "'a :: semiring_0 mat ⇒ 'a vec ⇒ 'a vec" (infixl "*⇩v" 70)
  where "A *⇩v v ≡ vec (dim_row A) (λ i. row A i ∙ v)"

definition inverts_mat :: "'a :: semiring_1 mat ⇒ 'a mat ⇒ bool" where
  "inverts_mat A B ≡ A * B = 1⇩m (dim_row A)"

definition invertible_mat :: "'a :: semiring_1 mat ⇒ bool"
  where "invertible_mat A ≡ square_mat A ∧ (∃B. inverts_mat A B ∧ inverts_mat B A)"

definition monoid_mat :: "'a :: monoid_add itself ⇒ nat ⇒ nat ⇒ 'a mat monoid" where
  "monoid_mat ty nr nc ≡ ⦇
    carrier = carrier_mat nr nc,
    mult = (+),
    one = 0⇩m nr nc⦈"

definition ring_mat :: "'a :: semiring_1 itself ⇒ nat ⇒ 'b ⇒ ('a mat,'b) ring_scheme" where
  "ring_mat ty n b ≡ ⦇
    carrier = carrier_mat n n,
    mult = (*),
    one = 1⇩m n,
    zero = 0⇩m n n,
    add = (+),
    … = b⦈"

definition module_mat :: "'a :: semiring_1 itself ⇒ nat ⇒ nat ⇒ ('a,'a mat)module" where
  "module_mat ty nr nc ≡ ⦇
    carrier = carrier_mat nr nc,
    mult = (*),
    one = 1⇩m nr,
    zero = 0⇩m nr nc,
    add = (+),
    smult = (⋅⇩m)⦈"

lemma ring_mat_simps:
  "mult (ring_mat ty n b) = (*)"
  "add (ring_mat ty n b) = (+)"
  "one (ring_mat ty n b) = 1⇩m n"
  "zero (ring_mat ty n b) = 0⇩m n n"
  "carrier (ring_mat ty n b) = carrier_mat n n"
  unfolding ring_mat_def by auto

lemma module_mat_simps:
  "mult (module_mat ty nr nc) = (*)"
  "add (module_mat ty nr nc) = (+)"
  "one (module_mat ty nr nc) = 1⇩m nr"
  "zero (module_mat ty nr nc) = 0⇩m nr nc"
  "carrier (module_mat ty nr nc) = carrier_mat nr nc"
  "smult (module_mat ty nr nc) = (⋅⇩m)"
  unfolding module_mat_def by auto

lemma index_zero_mat[simp]: "i < nr ⟹ j < nc ⟹ 0⇩m nr nc $$ (i,j) = 0"
  "dim_row (0⇩m nr nc) = nr" "dim_col (0⇩m nr nc) = nc"
  unfolding zero_mat_def by auto

lemma index_one_mat[simp]: "i < n ⟹ j < n ⟹ 1⇩m n $$ (i,j) = (if i = j then 1 else 0)"
  "dim_row (1⇩m n) = n" "dim_col (1⇩m n) = n"
  unfolding one_mat_def by auto

lemma index_add_mat[simp]:
  "i < dim_row B ⟹ j < dim_col B ⟹ (A + B) $$ (i,j) = A $$ (i,j) + B $$ (i,j)"
  "dim_row (A + B) = dim_row B" "dim_col (A + B) = dim_col B"
  unfolding plus_mat_def by auto

lemma index_minus_mat[simp]:
  "i < dim_row B ⟹ j < dim_col B ⟹ (A - B) $$ (i,j) = A $$ (i,j) - B $$ (i,j)"
  "dim_row (A - B) = dim_row B" "dim_col (A - B) = dim_col B"
  unfolding minus_mat_def by auto

lemma index_map_mat[simp]:
  "i < dim_row A ⟹ j < dim_col A ⟹ map_mat f A $$ (i,j) = f (A $$ (i,j))"
  "dim_row (map_mat f A) = dim_row A" "dim_col (map_mat f A) = dim_col A"
  unfolding map_mat_def by auto

lemma index_smult_mat[simp]:
  "i < dim_row A ⟹ j < dim_col A ⟹ (a ⋅⇩m A) $$ (i,j) = a * A $$ (i,j)"
  "dim_row (a ⋅⇩m A) = dim_row A" "dim_col (a ⋅⇩m A) = dim_col A"
  unfolding smult_mat_def by auto

lemma index_uminus_mat[simp]:
  "i < dim_row A ⟹ j < dim_col A ⟹ (- A) $$ (i,j) = - (A $$ (i,j))"
  "dim_row (- A) = dim_row A" "dim_col (- A) = dim_col A"
  unfolding uminus_mat_def by auto

lemma index_transpose_mat[simp]:
  "i < dim_col A ⟹ j < dim_row A ⟹ transpose_mat A $$ (i,j) = A $$ (j,i)"
  "dim_row (transpose_mat A) = dim_col A" "dim_col (transpose_mat A) = dim_row A"
  unfolding transpose_mat_def by auto

lemma index_mult_mat[simp]:
  "i < dim_row A ⟹ j < dim_col B ⟹ (A * B) $$ (i,j) = row A i ∙ col B j"
  "dim_row (A * B) = dim_row A" "dim_col (A * B) = dim_col B"
  by (auto simp: times_mat_def)

lemma dim_mult_mat_vec[simp]: "dim_vec (A *⇩v v) = dim_row A"
  by (auto simp: mult_mat_vec_def)

lemma index_mult_mat_vec[simp]: "i < dim_row A ⟹ (A *⇩v v) $ i = row A i ∙ v"
  by (auto simp: mult_mat_vec_def)

lemma index_row[simp]:
  "i < dim_row A ⟹ j < dim_col A ⟹ row A i $ j = A $$ (i,j)"
  "dim_vec (row A i) = dim_col A"
  by (auto simp: row_def)

lemma index_col[simp]: "i < dim_row A ⟹ j < dim_col A ⟹ col A j $ i = A $$ (i,j)"
  by (auto simp: col_def)

lemma upper_triangular_one[simp]: "upper_triangular (1⇩m n)"
  by (rule, auto)

lemma upper_triangular_zero[simp]: "upper_triangular (0⇩m n n)"
  by (rule, auto)

lemma mat_row_carrierI[intro,simp]: "mat⇩r nr nc r ∈ carrier_mat nr nc"
  by (unfold carrier_mat_def carrier_vec_def, auto)

lemma eq_rowI: assumes rows: "⋀ i. i < dim_row B ⟹ row A i = row B i"
  and dims: "dim_row A = dim_row B" "dim_col A = dim_col B"
  shows "A = B"
proof (rule eq_matI[OF _ dims])
  fix i j
  assume i: "i < dim_row B" and j: "j < dim_col B"
  from rows[OF i] have id: "row A i $ j = row B i $ j" by simp
  show "A $$ (i, j) = B $$ (i, j)"
    using index_row(1)[OF i j, folded id] index_row(1)[of i A j] i j dims
    by auto
qed

lemma elements_mat_map[simp]: "elements_mat (map_mat f A) = f ` elements_mat A" 
  by fastforce

lemma row_mat[simp]: "i < nr ⟹ row (mat nr nc f) i = vec nc (λ j. f (i,j))"
  by auto

lemma col_mat[simp]: "j < nc ⟹ col (mat nr nc f) j = vec nr (λ i. f (i,j))"
  by auto

lemma zero_carrier_mat[simp]: "0⇩m nr nc ∈ carrier_mat nr nc"
  unfolding carrier_mat_def by auto

lemma smult_carrier_mat[simp]:
  "A ∈ carrier_mat nr nc ⟹ k ⋅⇩m A ∈ carrier_mat nr nc"
  unfolding carrier_mat_def by auto

lemma add_carrier_mat[simp]:
  "B ∈ carrier_mat nr nc ⟹ A + B ∈ carrier_mat nr nc"
  unfolding carrier_mat_def by force

lemma one_carrier_mat[simp]: "1⇩m n ∈ carrier_mat n n"
  unfolding carrier_mat_def by auto

lemma uminus_carrier_mat:
  "A ∈ carrier_mat nr nc ⟹ (- A ∈ carrier_mat nr nc)"
  unfolding carrier_mat_def by auto

lemma uminus_carrier_iff_mat[simp]:
  "(- A ∈ carrier_mat nr nc) = (A ∈ carrier_mat nr nc)"
  unfolding carrier_mat_def by auto

lemma minus_carrier_mat:
  "B ∈ carrier_mat nr nc ⟹ (A - B ∈ carrier_mat nr nc)"
  unfolding carrier_mat_def by auto

lemma transpose_carrier_mat[simp]: "(transpose_mat A ∈ carrier_mat nc nr) = (A ∈ carrier_mat nr nc)"
  unfolding carrier_mat_def by auto

lemma row_carrier_vec[simp]: "i < nr ⟹ A ∈ carrier_mat nr nc ⟹ row A i ∈ carrier_vec nc"
  unfolding carrier_vec_def by auto

lemma col_carrier_vec[simp]: "j < nc ⟹ A ∈ carrier_mat nr nc ⟹ col A j ∈ carrier_vec nr"
  unfolding carrier_vec_def by auto

lemma mult_carrier_mat[simp]:
  "A ∈ carrier_mat nr n ⟹ B ∈ carrier_mat n nc ⟹ A * B ∈ carrier_mat nr nc"
  unfolding carrier_mat_def by auto

lemma mult_mat_vec_carrier[simp]:
  "A ∈ carrier_mat nr n ⟹ v ∈ carrier_vec n ⟹ A *⇩v v ∈ carrier_vec nr"
  unfolding carrier_mat_def carrier_vec_def by auto


lemma comm_add_mat[ac_simps]:
  "(A :: 'a :: comm_monoid_add mat) ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ A + B = B + A"
  by (intro eq_matI, auto simp: ac_simps)


lemma minus_r_inv_mat[simp]:
  "(A :: 'a :: group_add mat) ∈ carrier_mat nr nc ⟹ (A - A) = 0⇩m nr nc"
  by (intro eq_matI, auto)

lemma uminus_l_inv_mat[simp]:
  "(A :: 'a :: group_add mat) ∈ carrier_mat nr nc ⟹ (- A + A) = 0⇩m nr nc"
  by (intro eq_matI, auto)

lemma add_inv_exists_mat:
  "(A :: 'a :: group_add mat) ∈ carrier_mat nr nc ⟹ ∃ B ∈ carrier_mat nr nc. B + A = 0⇩m nr nc ∧ A + B = 0⇩m nr nc"
  by (intro bexI[of _ "- A"], auto)

lemma assoc_add_mat[simp]:
  "(A :: 'a :: monoid_add mat) ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ C ∈ carrier_mat nr nc
  ⟹ (A + B) + C = A + (B + C)"
  by (intro eq_matI, auto simp: ac_simps)

lemma uminus_add_mat: fixes A :: "'a :: group_add mat"
  assumes "A ∈ carrier_mat nr nc"
  and "B ∈ carrier_mat nr nc"
  shows "- (A + B) = - B + - A"
  by (intro eq_matI, insert assms, auto simp: minus_add)

lemma transpose_transpose[simp]:
  "transpose_mat (transpose_mat A) = A"
  by (intro eq_matI, auto)

lemma transpose_one[simp]: "transpose_mat (1⇩m n) = (1⇩m n)"
  by auto

lemma row_transpose[simp]:
  "j < dim_col A ⟹ row (transpose_mat A) j = col A j"
  unfolding row_def col_def
  by (intro eq_vecI, auto)

lemma col_transpose[simp]:
  "i < dim_row A ⟹ col (transpose_mat A) i = row A i"
  unfolding row_def col_def
  by (intro eq_vecI, auto)

lemma row_zero[simp]:
  "i < nr ⟹ row (0⇩m nr nc) i = 0⇩v nc"
   by (intro eq_vecI, auto)

lemma col_zero[simp]:
  "j < nc ⟹ col (0⇩m nr nc) j = 0⇩v nr"
   by (intro eq_vecI, auto)

lemma row_one[simp]:
  "i < n ⟹ row (1⇩m n) i = unit_vec n i"
  by (intro eq_vecI, auto)

lemma col_one[simp]:
  "j < n ⟹ col (1⇩m n) j = unit_vec n j"
  by (intro eq_vecI, auto)

lemma transpose_add: "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc
  ⟹ transpose_mat (A + B) = transpose_mat A + transpose_mat B"
  by (intro eq_matI, auto)

lemma transpose_minus: "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc
  ⟹ transpose_mat (A - B) = transpose_mat A - transpose_mat B"
  by (intro eq_matI, auto)

lemma transpose_uminus: "transpose_mat (- A) = - (transpose_mat A)"
  by (intro eq_matI, auto)

lemma row_add[simp]:
  "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ i < nr
  ⟹ row (A + B) i = row A i + row B i"
  "i < dim_row A ⟹ dim_row B = dim_row A ⟹ dim_col B = dim_col A ⟹ row (A + B) i = row A i + row B i"
  by (rule eq_vecI, auto)

lemma col_add[simp]:
  "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ j < nc
  ⟹ col (A + B) j = col A j + col B j"
  by (rule eq_vecI, auto)

lemma row_mult[simp]: assumes m: "A ∈ carrier_mat nr n" "B ∈ carrier_mat n nc"
  and i: "i < nr"
  shows "row (A * B) i = vec nc (λ j. row A i ∙ col B j)"
  by (rule eq_vecI, insert m i, auto)

lemma col_mult[simp]: assumes m: "A ∈ carrier_mat nr n" "B ∈ carrier_mat n nc"
  and j: "j < nc"
  shows "col (A * B) j = vec nr (λ i. row A i ∙ col B j)"
  by (rule eq_vecI, insert m j, auto)

lemma transpose_mult:
  "(A :: 'a :: comm_semiring_0 mat) ∈ carrier_mat nr n ⟹ B ∈ carrier_mat n nc
  ⟹ transpose_mat (A * B) = transpose_mat B * transpose_mat A"
  by (intro eq_matI, auto simp: comm_scalar_prod[of _ n])

lemma left_add_zero_mat[simp]:
  "(A :: 'a :: monoid_add mat) ∈ carrier_mat nr nc  ⟹ 0⇩m nr nc + A = A"
  by (intro eq_matI, auto)

lemma add_uminus_minus_mat: "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹ 
  A + (- B) = A - (B :: 'a :: group_add mat)" 
  by (intro eq_matI, auto)

lemma right_add_zero_mat[simp]: "A ∈ carrier_mat nr nc ⟹ 
  A + 0⇩m nr nc = (A :: 'a :: monoid_add mat)" 
  by (intro eq_matI, auto)

lemma left_mult_zero_mat:
  "A ∈ carrier_mat n nc ⟹ 0⇩m nr n * A = 0⇩m nr nc"
  by (intro eq_matI, auto)

lemma left_mult_zero_mat'[simp]: "dim_row A = n ⟹ 0⇩m nr n * A = 0⇩m nr (dim_col A)"
  by (rule left_mult_zero_mat, unfold carrier_mat_def, simp)

lemma right_mult_zero_mat:
  "A ∈ carrier_mat nr n ⟹ A * 0⇩m n nc = 0⇩m nr nc"
  by (intro eq_matI, auto)

lemma right_mult_zero_mat'[simp]: "dim_col A = n ⟹ A * 0⇩m n nc = 0⇩m (dim_row A) nc"
  by (rule right_mult_zero_mat, unfold carrier_mat_def, simp)

lemma left_mult_one_mat:
  "(A :: 'a :: semiring_1 mat) ∈ carrier_mat nr nc ⟹ 1⇩m nr * A = A"
  by (intro eq_matI, auto)

lemma left_mult_one_mat'[simp]: "dim_row (A :: 'a :: semiring_1 mat) = n ⟹ 1⇩m n * A = A"
  by (rule left_mult_one_mat, unfold carrier_mat_def, simp)

lemma right_mult_one_mat:
  "(A :: 'a :: semiring_1 mat) ∈ carrier_mat nr nc ⟹ A * 1⇩m nc = A"
  by (intro eq_matI, auto)

lemma right_mult_one_mat'[simp]: "dim_col (A :: 'a :: semiring_1 mat) = n ⟹ A * 1⇩m n = A"
  by (rule right_mult_one_mat, unfold carrier_mat_def, simp)

lemma one_mult_mat_vec[simp]:
  "(v :: 'a :: semiring_1 vec) ∈ carrier_vec n ⟹ 1⇩m n *⇩v v = v"
  by (intro eq_vecI, auto)

lemma minus_add_uminus_mat: fixes A :: "'a :: group_add mat"
  shows "A ∈ carrier_mat nr nc ⟹ B ∈ carrier_mat nr nc ⟹
  A - B = A + (- B)"
  by (intro eq_matI, auto)

lemma add_mult_distrib_mat[algebra_simps]: assumes m: "A ∈ carrier_mat nr n"
  "B ∈ carrier_mat nr n" "C ∈ carrier_mat n nc"
  shows "(A + B) * C = A * C + B * C"
  using m by (intro eq_matI, auto simp: add_scalar_prod_distrib[of _ n])

lemma mult_add_distrib_mat[algebra_simps]: assumes m: "A ∈ carrier_mat nr n"
  "B ∈ carrier_mat n nc" "C ∈ carrier_mat n nc"
  shows "A * (B + C) = A * B + A * C"
  using m by (intro eq_matI, auto simp: scalar_prod_add_distrib[of _ n])

lemma add_mult_distrib_mat_vec[algebra_simps]: assumes m: "A ∈ carrier_mat nr nc"
  "B ∈ carrier_mat nr nc" "v ∈ carrier_vec nc"
  shows "(A + B) *⇩v v = A *⇩v v + B *⇩v v"
  using m by (intro eq_vecI, auto intro!: add_scalar_prod_distrib)

lemma mult_add_distrib_mat_vec[algebra_simps]: assumes m: "A ∈ carrier_mat nr nc"
  "v⇩1 ∈ carrier_vec nc" "v⇩2 ∈ carrier_vec nc"
  shows "A *⇩v (v⇩1 + v⇩2) = A *⇩v v⇩1 + A *⇩v v⇩2"
  using m by (intro eq_vecI, auto simp: scalar_prod_add_distrib[of _ nc])

lemma mult_mat_vec:
  assumes m: "(A::'a::field mat) ∈ carrier_mat nr nc" and v: "v ∈ carrier_vec nc"
  shows "A *⇩v (k ⋅⇩v v) = k ⋅⇩v (A *⇩v v)" (is "?l = ?r")
proof
  have nr: "dim_vec ?l = nr" using m v by auto
  also have "... = dim_vec ?r" using m v by auto
  finally show "dim_vec ?l = dim_vec ?r".

  show "⋀i. i < dim_vec ?r ⟹ ?l $ i = ?r $ i"
  proof -
    fix i assume "i < dim_vec ?r"
    hence i: "i < dim_row A" using nr m by auto
    hence i2: "i < dim_vec (A *⇩v v)" using m by auto
    show "?l $ i = ?r $ i"
    apply (subst (1) mult_mat_vec_def)
    apply (subst (2) smult_vec_def)
    unfolding index_vec[OF i] index_vec[OF i2]
    unfolding mult_mat_vec_def smult_vec_def
    unfolding scalar_prod_def index_vec[OF i]
    by (simp add: mult.left_commute sum_distrib_left)
  qed
qed

lemma assoc_scalar_prod: assumes *: "v⇩1 ∈ carrier_vec nr" "A ∈ carrier_mat nr nc" "v⇩2 ∈ carrier_vec nc"
  shows "vec nc (λj. v⇩1 ∙ col A j) ∙ v⇩2 = v⇩1 ∙ vec nr (λi. row A i ∙ v⇩2)"
proof -
  have "vec nc (λj. v⇩1 ∙ col A j) ∙ v⇩2 = (∑i∈{0..<nc}. vec nc (λj. ∑k∈{0..<nr}. v⇩1 $ k * col A j $ k) $ i * v⇩2 $ i)"
    unfolding scalar_prod_def using * by auto
  also have "… = (∑i∈{0..<nc}. (∑k∈{0..<nr}. v⇩1 $ k * col A i $ k) * v⇩2 $ i)"
    by (rule sum.cong, auto)
  also have "… = (∑i∈{0..<nc}. (∑k∈{0..<nr}. v⇩1 $ k * col A i $ k * v⇩2 $ i))"
    unfolding sum_distrib_right ..
  also have "… = (∑k∈{0..<nr}. (∑i∈{0..<nc}. v⇩1 $ k * col A i $ k * v⇩2 $ i))"
    by (rule sum.swap)
  also have "… = (∑k∈{0..<nr}. (∑i∈{0..<nc}. v⇩1 $ k * (col A i $ k * v⇩2 $ i)))"
    by (simp add: ac_simps)
  also have "… = (∑k∈{0..<nr}. v⇩1 $ k * (∑i∈{0..<nc}. col A i $ k * v⇩2 $ i))"
    unfolding sum_distrib_left ..
  also have "… = (∑k∈{0..<nr}. v⇩1 $ k * vec nr (λk. ∑i∈{0..<nc}. row A k $ i * v⇩2 $ i) $ k)"
    using * by auto
  also have "… = v⇩1 ∙ vec nr (λi. row A i ∙ v⇩2)" unfolding scalar_prod_def using * by simp
  finally show ?thesis .
qed

lemma transpose_vec_mult_scalar:
  fixes A :: "'a :: comm_semiring_0 mat"
  assumes A: "A ∈ carrier_mat nr nc"
    and x: "x ∈ carrier_vec nc"
    and y: "y ∈ carrier_vec nr"
  shows "(transpose_mat A *⇩v y) ∙ x = y ∙ (A *⇩v x)"
proof -
  have "(transpose_mat A *⇩v y) = vec nc (λi. col A i ∙ y)"
    unfolding mult_mat_vec_def using A by auto
  also have "… = vec nc (λi. y ∙ col A i)"
    by (intro eq_vecI, simp, rule comm_scalar_prod[OF _ y], insert A, auto)
  also have "… ∙ x = y ∙ vec nr (λi. row A i ∙ x)"
    by (rule assoc_scalar_prod[OF y A x])
  also have "vec nr (λi. row A i ∙ x) = A *⇩v x"
    unfolding mult_mat_vec_def using A by auto
  finally show ?thesis .
qed

lemma assoc_mult_mat[simp]:
  "A ∈ carrier_mat n⇩1 n⇩2 ⟹ B ∈ carrier_mat n⇩2 n⇩3 ⟹ C ∈ carrier_mat n⇩3 n⇩4
  ⟹ (A * B) * C = A * (B * C)"
  by (intro eq_matI, auto simp: assoc_scalar_prod)

lemma assoc_mult_mat_vec[simp]:
  "A ∈ carrier_mat n⇩1 n⇩2 ⟹ B ∈ carrier_mat n⇩2 n⇩3 ⟹ v ∈ carrier_vec n⇩3
  ⟹ (A * B) *⇩v v = A *⇩v (B *⇩v v)"
  by (intro eq_vecI, auto simp add: mult_mat_vec_def assoc_scalar_prod)

lemma comm_monoid_mat: "comm_monoid (monoid_mat TYPE('a :: comm_monoid_add) nr nc)"
  by (unfold_locales, auto simp: monoid_mat_def ac_simps)

lemma comm_group_mat: "comm_group (monoid_mat TYPE('a :: ab_group_add) nr nc)"
  by (unfold_locales, insert add_inv_exists_mat, auto simp: monoid_mat_def ac_simps Units_def)

lemma semiring_mat: "semiring (ring_mat TYPE('a :: semiring_1) n b)"
  by (unfold_locales, auto simp: ring_mat_def algebra_simps)

lemma ring_mat: "ring (ring_mat TYPE('a :: comm_ring_1) n b)"
  by (unfold_locales, insert add_inv_exists_mat, auto simp: ring_mat_def algebra_simps Units_def)

lemma abelian_group_mat: "abelian_group (module_mat TYPE('a :: comm_ring_1) nr nc)"
  by (unfold_locales, insert add_inv_exists_mat, auto simp: module_mat_def Units_def)

lemma row_smult[simp]: assumes i: "i < dim_row A"
  shows "row (k ⋅⇩m A) i = k ⋅⇩v (row A i)"
  by (rule eq_vecI, insert i, auto)

lemma col_smult[simp]: assumes i: "i < dim_col A"
  shows "col (k ⋅⇩m A) i = k ⋅⇩v (col A i)"
  by (rule eq_vecI, insert i, auto)

lemma row_uminus[simp]: assumes i: "i < dim_row A"
  shows "row (- A) i = - (row A i)"
  by (rule eq_vecI, insert i, auto)

lemma scalar_prod_uminus_left[simp]: assumes dim: "dim_vec v = dim_vec (w :: 'a :: ring vec)"
  shows "- v ∙ w = - (v ∙ w)"
  unfolding scalar_prod_def dim[symmetric]
  by (subst sum_negf[symmetric], rule sum.cong, auto)

lemma col_uminus[simp]: assumes i: "i < dim_col A"
  shows "col (- A) i = - (col A i)"
  by (rule eq_vecI, insert i, auto)

lemma scalar_prod_uminus_right[simp]: assumes dim: "dim_vec v = dim_vec (w :: 'a :: ring vec)"
  shows "v ∙ - w = - (v ∙ w)"
  unfolding scalar_prod_def dim
  by (subst sum_negf[symmetric], rule sum.cong, auto)

context fixes A B :: "'a :: ring mat"
  assumes dim: "dim_col A = dim_row B"
begin
lemma uminus_mult_left_mat[simp]: "(- A * B) = - (A * B)"
  by (intro eq_matI, insert dim, auto)

lemma uminus_mult_right_mat[simp]: "(A * - B) = - (A * B)"
  by (intro eq_matI, insert dim, auto)
end

lemma minus_mult_distrib_mat[algebra_simps]: fixes A :: "'a :: ring mat"
  assumes m: "A ∈ carrier_mat nr n" "B ∈ carrier_mat nr n" "C ∈ carrier_mat n nc"
  shows "(A - B) * C = A * C - B * C"
  unfolding minus_add_uminus_mat[OF m(1,2)]
    add_mult_distrib_mat[OF m(1) uminus_carrier_mat[OF m(2)] m(3)]
  by (subst uminus_mult_left_mat, insert m, auto)

lemma minus_mult_distrib_mat_vec[algebra_simps]: assumes A: "(A :: 'a :: ring mat) ∈ carrier_mat nr nc"
  and B: "B ∈ carrier_mat nr nc"
  and v: "v ∈ carrier_vec nc"
shows "(A - B) *⇩v v = A *⇩v v - B *⇩v v"
  unfolding minus_add_uminus_mat[OF A B]
  by (subst add_mult_distrib_mat_vec[OF A _ v], insert A B v, auto)

lemma mult_minus_distrib_mat_vec[algebra_simps]: assumes A: "(A :: 'a :: ring mat) ∈ carrier_mat nr nc"
  and v: "v ∈ carrier_vec nc"
  and w: "w ∈ carrier_vec nc"
shows "A *⇩v (v - w) = A *⇩v v - A *⇩v w"
  unfolding minus_add_uminus_vec[OF v w]
  by (subst mult_add_distrib_mat_vec[OF A], insert A v w, auto)

lemma mult_minus_distrib_mat[algebra_simps]: fixes A :: "'a :: ring mat"
  assumes m: "A ∈ carrier_mat nr n" "B ∈ carrier_mat n nc" "C ∈ carrier_mat n nc"
  shows "A * (B - C) = A * B - A * C"
  unfolding minus_add_uminus_mat[OF m(2,3)]
    mult_add_distrib_mat[OF m(1) m(2) uminus_carrier_mat[OF m(3)]]
  by (subst uminus_mult_right_mat, insert m, auto)

lemma uminus_mult_mat_vec[simp]: assumes v: "dim_vec v = dim_col (A :: 'a :: ring mat)"
  shows "- A *⇩v v = - (A *⇩v v)"
  using v by (intro eq_vecI, auto)

lemma uminus_zero_vec_eq: assumes v: "(v :: 'a :: group_add vec) ∈ carrier_vec n"
  shows "(- v = 0⇩v n) = (v = 0⇩v n)"
proof
  assume z: "- v = 0⇩v n"
  {
    fix i
    assume i: "i < n"
    have "v $ i = - (- (v $ i))" by simp
    also have "- (v $ i) = 0" using arg_cong[OF z, of "λ v. v $ i"] i v by auto
    also have "- 0 = (0 :: 'a)" by simp
    finally have "v $ i = 0" .
  }
  thus "v = 0⇩v n" using v
    by (intro eq_vecI, auto)
qed auto

lemma map_carrier_mat[simp]:
  "(map_mat f A ∈ carrier_mat nr nc) = (A ∈ carrier_mat nr nc)"
  unfolding carrier_mat_def by auto

lemma col_map_mat[simp]:
  assumes "j < dim_col A" shows "col (map_mat f A) j = map_vec f (col A j)"
  unfolding map_mat_def map_vec_def using assms by auto

lemma scalar_vec_one[simp]: "1 ⋅⇩v (v :: 'a :: semiring_1 vec) = v"
  by (rule eq_vecI, auto)

lemma scalar_prod_smult_right[simp]:
  "dim_vec w = dim_vec v ⟹ w ∙ (k ⋅⇩v v) = (k :: 'a :: comm_semiring_0) * (w ∙ v)"
  unfolding scalar_prod_def sum_distrib_left
  by (auto intro: sum.cong simp: ac_simps)

lemma scalar_prod_smult_left[simp]:
  "dim_vec w = dim_vec v ⟹ (k ⋅⇩v w) ∙ v = (k :: 'a :: comm_semiring_0) * (w ∙ v)"
  unfolding scalar_prod_def sum_distrib_left
  by (auto intro: sum.cong simp: ac_simps)

lemma mult_smult_distrib: assumes A: "A ∈ carrier_mat nr n" and B: "B ∈ carrier_mat n nc"
  shows "A * (k ⋅⇩m B) = (k :: 'a :: comm_semiring_0) ⋅⇩m (A * B)"
  by (rule eq_matI, insert A B, auto)

lemma add_smult_distrib_left_mat: assumes "A ∈ carrier_mat nr nc" "B ∈ carrier_mat nr nc"
  shows "k ⋅⇩m (A + B) = (k :: 'a :: semiring) ⋅⇩m A + k ⋅⇩m B"
  by (rule eq_matI, insert assms, auto simp: field_simps)

lemma add_smult_distrib_right_mat: assumes "A ∈ carrier_mat nr nc"
  shows "(k + l) ⋅⇩m A = (k :: 'a :: semiring) ⋅⇩m A + l ⋅⇩m A"
  by (rule eq_matI, insert assms, auto simp: field_simps)

lemma mult_smult_assoc_mat: assumes A: "A ∈ carrier_mat nr n" and B: "B ∈ carrier_mat n nc"
  shows "(k ⋅⇩m A) * B = (k :: 'a :: comm_semiring_0) ⋅⇩m (A * B)"
  by (rule eq_matI, insert A B, auto)

definition similar_mat_wit :: "'a :: semiring_1 mat ⇒ 'a mat ⇒ 'a mat ⇒ 'a mat ⇒ bool" where
  "similar_mat_wit A B P Q = (let n = dim_row A in {A,B,P,Q} ⊆ carrier_mat n n ∧ P * Q = 1⇩m n ∧ Q * P = 1⇩m n ∧
    A = P * B * Q)"

definition similar_mat :: "'a :: semiring_1 mat ⇒ 'a mat ⇒ bool" where
  "similar_mat A B = (∃ P Q. similar_mat_wit A B P Q)"

lemma similar_matD: assumes "similar_mat A B"
  shows "∃ n P Q. {A,B,P,Q} ⊆ carrier_mat n n ∧ P * Q = 1⇩m n ∧ Q * P = 1⇩m n ∧ A = P * B * Q"
  using assms unfolding similar_mat_def similar_mat_wit_def[abs_def] Let_def by blast

lemma similar_matI: assumes "{A,B,P,Q} ⊆ carrier_mat n n" "P * Q = 1⇩m n" "Q * P = 1⇩m n" "A = P * B * Q"
  shows "similar_mat A B" unfolding similar_mat_def
  by (rule exI[of _ P], rule exI[of _ Q], unfold similar_mat_wit_def Let_def, insert assms, auto)

fun pow_mat :: "'a :: semiring_1 mat ⇒ nat ⇒ 'a mat" (infixr "^⇩m" 75) where
  "A ^⇩m 0 = 1⇩m (dim_row A)"
| "A ^⇩m (Suc k) = A ^⇩m k * A"

lemma pow_mat_dim[simp]:
  "dim_row (A ^⇩m k) = dim_row A"
  "dim_col (A ^⇩m k) = (if k = 0 then dim_row A else dim_col A)"
  by (induct k, auto)

lemma pow_mat_dim_square[simp]:
  "A ∈ carrier_mat n n ⟹ dim_row (A ^⇩m k) = n"
  "A ∈ carrier_mat n n ⟹ dim_col (A ^⇩m k) = n"
  by auto

lemma pow_carrier_mat[simp]: "A ∈ carrier_mat n n ⟹ A ^⇩m k ∈ carrier_mat n n"
  unfolding carrier_mat_def by auto

definition diag_mat :: "'a mat ⇒ 'a list" where
  "diag_mat A = map (λ i. A $$ (i,i)) [0 ..< dim_row A]"

lemma prod_list_diag_prod: "prod_list (diag_mat A) = (∏ i = 0 ..< dim_row A. A $$ (i,i))"
  unfolding diag_mat_def
  by (subst prod.distinct_set_conv_list[symmetric], auto)

lemma diag_mat_transpose[simp]: "dim_row A = dim_col A ⟹
  diag_mat (transpose_mat A) = diag_mat A" unfolding diag_mat_def by auto

lemma diag_mat_zero[simp]: "diag_mat (0⇩m n n) = replicate n 0"
  unfolding diag_mat_def
  by (rule nth_equalityI, auto)

lemma diag_mat_one[simp]: "diag_mat (1⇩m n) = replicate n 1"
  unfolding diag_mat_def
  by (rule nth_equalityI, auto)

lemma pow_mat_ring_pow: assumes A: "(A :: ('a :: semiring_1)mat) ∈ carrier_mat n n"
  shows "A ^⇩m k = A [^]⇘ring_mat TYPE('a) n b⇙ k"
  (is "_ = A [^]⇘?C⇙ k")
proof -
  interpret semiring ?C by (rule semiring_mat)
  show ?thesis
    by (induct k, insert A, auto simp: ring_mat_def nat_pow_def)
qed

definition diagonal_mat :: "'a::zero mat ⇒ bool" where
  "diagonal_mat A ≡ ∀i<dim_row A. ∀j<dim_col A. i ≠ j ⟶ A $$ (i,j) = 0"

definition (in comm_monoid_add) sum_mat :: "'a mat ⇒ 'a" where
  "sum_mat A = sum (λ ij. A $$ ij) ({0 ..< dim_row A} × {0 ..< dim_col A})"

lemma sum_mat_0[simp]: "sum_mat (0⇩m nr nc) = (0 :: 'a :: comm_monoid_add)"
  unfolding sum_mat_def
  by (rule sum.neutral, auto)

lemma sum_mat_add: assumes A: "(A :: 'a :: comm_monoid_add mat) ∈ carrier_mat nr nc" and B: "B ∈ carrier_mat nr nc"
  shows "sum_mat (A + B) = sum_mat A + sum_mat B"
proof -
  from A B have id: "dim_row A = nr" "dim_row B = nr" "dim_col A = nc" "dim_col B = nc"
    by auto
  show ?thesis unfolding sum_mat_def id
    by (subst sum.distrib[symmetric], rule sum.cong, insert A B, auto)
qed

subsection ‹Update Operators›

definition update_vec :: "'a vec ⇒ nat ⇒ 'a ⇒ 'a vec" ("_ |⇩v _ ↦ _" [60,61,62] 60)
  where "v |⇩v i ↦ a = vec (dim_vec v) (λi'. if i' = i then a else v $ i')"

definition update_mat :: "'a mat ⇒ nat × nat ⇒ 'a ⇒ 'a mat" ("_ |⇩m _ ↦ _" [60,61,62] 60)
  where "A |⇩m ij ↦ a = mat (dim_row A) (dim_col A) (λij'. if ij' = ij then a else A $$ ij')"

lemma dim_update_vec[simp]:
  "dim_vec (v |⇩v i ↦ a) = dim_vec v" unfolding update_vec_def by simp

lemma index_update_vec1[simp]:
  assumes "i < dim_vec v" shows "(v |⇩v i ↦ a) $ i = a"
  unfolding update_vec_def using assms by simp

lemma index_update_vec2[simp]:
  assumes "i' ≠ i" shows "(v |⇩v i ↦ a) $ i' = v $ i'"
  unfolding update_vec_def
  using assms apply transfer unfolding mk_vec_def by auto

lemma dim_update_mat[simp]:
  "dim_row (A |⇩m ij ↦ a) = dim_row A"
  "dim_col (A |⇩m ij ↦ a) = dim_col A" unfolding update_mat_def by simp+

lemma index_update_mat1[simp]:
  assumes "i < dim_row A" "j < dim_col A" shows "(A |⇩m (i,j) ↦ a) $$ (i,j) = a"
  unfolding update_mat_def using assms by simp

lemma index_update_mat2[simp]:
  assumes i': "i' < dim_row A" and j': "j' < dim_col A" and neq: "(i',j') ≠ ij"
  shows "(A |⇩m ij ↦ a) $$ (i',j') = A $$ (i',j')"
  unfolding update_mat_def using assms by auto

subsection ‹Block Vectors and Matrices›

definition append_vec :: "'a vec ⇒ 'a vec ⇒ 'a vec" (infixr "@⇩v" 65) where
  "v @⇩v w ≡ let n = dim_vec v; m = dim_vec w in
    vec (n + m) (λ i. if i < n then v $ i else w $ (i - n))"

lemma index_append_vec[simp]: "i < dim_vec v + dim_vec w
  ⟹ (v @⇩v w) $ i = (if i < dim_vec v then v $ i else w $ (i - dim_vec v))"
  "dim_vec (v @⇩v w) = dim_vec v + dim_vec w"
  unfolding append_vec_def Let_def by auto

lemma append_carrier_vec[simp,intro]:
  "v ∈ carrier_vec n1 ⟹ w ∈ carrier_vec n2 ⟹ v @⇩v w ∈ carrier_vec (n1 + n2)"
  unfolding carrier_vec_def by auto

lemma scalar_prod_append: assumes "v1 ∈ carrier_vec n1" "v2 ∈ carrier_vec n2"
  "w1 ∈ carrier_vec n1" "w2 ∈ carrier_vec n2"
  shows "(v1 @⇩v v2) ∙ (w1 @⇩v w2) = v1 ∙ w1 + v2 ∙ w2"
proof -
  from assms have dim: "dim_vec v1 = n1" "dim_vec v2 = n2" "dim_vec w1 = n1" "dim_vec w2 = n2" by auto
  have id: "{0 ..< n1 + n2} = {0 ..< n1} ∪ {n1 ..< n1 + n2}" by auto
  have id2: "{n1 ..< n1 + n2} = (plus n1) ` {0 ..< n2}"
    by (simp add: ac_simps)
  have "(v1 @⇩v v2) ∙ (w1 @⇩v w2) = (∑i = 0..<n1. v1 $ i * w1 $ i) +
    (∑i = n1..<n1 + n2. v2 $ (i - n1) * w2 $ (i - n1))"
  unfolding scalar_prod_def
    by (auto simp: dim id, subst sum.union_disjoint, insert assms, force+)
  also have "(∑i = n1..<n1 + n2. v2 $ (i - n1) * w2 $ (i - n1))
    = (∑i = 0..< n2. v2 $ i * w2 $ i)"
    by (rule sum.reindex_cong [OF _ id2]) simp_all
  finally show ?thesis by (simp, insert assms, auto simp: scalar_prod_def)
qed

definition "vec_first v n ≡ vec n (λi. v $ i)"
definition "vec_last v n ≡ vec n (λi. v $ (dim_vec v - n + i))"

lemma dim_vec_first[simp]: "dim_vec (vec_first v n) = n" unfolding vec_first_def by auto
lemma dim_vec_last[simp]: "dim_vec (vec_last v n) = n" unfolding vec_last_def by auto

lemma vec_first_carrier[simp]: "vec_first v n ∈ carrier_vec n" by (rule carrier_vecI, auto)
lemma vec_last_carrier[simp]: "vec_last v n ∈ carrier_vec n" by (rule carrier_vecI, auto)

lemma vec_first_last_append[simp]:
  assumes "v ∈ carrier_vec (n+m)" shows "vec_first v n @⇩v vec_last v m = v"
  apply(rule) unfolding vec_first_def vec_last_def using assms by auto

lemma append_vec_le: assumes "v ∈ carrier_vec n" and w: "w ∈ carrier_vec n" 
  shows "v @⇩v v' ≤ w @⇩v w' ⟷ v ≤ w ∧ v' ≤ w'" 
proof -
  {
    fix i
    assume *: "∀i. (¬ i < n ⟶ i < n + dim_vec w' ⟶ v' $ (i - n) ≤ w' $ (i - n))"
      and i: "i < dim_vec w'" 
    have "v' $ i ≤ w' $ i" using *[rule_format, of "n + i"] i by auto
  }
  thus ?thesis using assms unfolding less_eq_vec_def by auto
qed

lemma all_vec_append: "(∀ x ∈ carrier_vec (n + m). P x) ⟷ (∀ x1 ∈ carrier_vec n. ∀ x2 ∈ carrier_vec m. P (x1 @⇩v x2))" 
proof (standard, force, intro ballI, goal_cases)
  case (1 x)
  have "x = vec n (λ i. x $ i) @⇩v vec m (λ i. x $ (n + i))" 
    by (rule eq_vecI, insert 1(2), auto)
  hence "P x = P (vec n (λ i. x $ i) @⇩v vec m (λ i. x $ (n + i)))" by simp
  also have "…" using 1 by auto
  finally show ?case .
qed


(* A B
   C D *)
definition four_block_mat :: "'a mat ⇒ 'a mat ⇒ 'a mat ⇒ 'a mat ⇒ 'a mat" where
  "four_block_mat A B C D =
    (let nra = dim_row A; nrd = dim_row D;
         nca = dim_col A; ncd = dim_col D
       in
    mat (nra + nrd) (nca + ncd) (λ (i,j). if i < nra then
      if j < nca then A $$ (i,j) else B $$ (i,j - nca)
      else if j < nca then C $$ (i - nra, j) else D $$ (i - nra, j - nca)))"

lemma index_mat_four_block[simp]:
  "i < dim_row A + dim_row D ⟹ j < dim_col A + dim_col D ⟹ four_block_mat A B C D $$ (i,j)
  = (if i < dim_row A then
      if j < dim_col A then A $$ (i,j) else B $$ (i,j - dim_col A)
      else if j < dim_col A then C $$ (i - dim_row A, j) else D $$ (i - dim_row A, j - dim_col A))"
  "dim_row (four_block_mat A B C D) = dim_row A + dim_row D"
  "dim_col (four_block_mat A B C D) = dim_col A + dim_col D"
  unfolding four_block_mat_def Let_def by auto

lemma four_block_carrier_mat[simp]:
  "A ∈ carrier_mat nr1 nc1 ⟹ D ∈ carrier_mat nr2 nc2 ⟹
  four_block_mat A B C D ∈ carrier_mat (nr1 + nr2) (nc1 + nc2)"
  unfolding carrier_mat_def by auto

lemma cong_four_block_mat: "A1 = B1 ⟹ A2 = B2 ⟹ A3 = B3 ⟹ A4 = B4 ⟹
  four_block_mat A1 A2 A3 A4 = four_block_mat B1 B2 B3 B4" by auto

lemma four_block_one_mat[simp]:
  "four_block_mat (1⇩m n1) (0⇩m n1 n2) (0⇩m n2 n1) (1⇩m n2) = 1⇩m (n1 + n2)"
  by (rule eq_matI, auto)

lemma four_block_zero_mat[simp]:
  "four_block_mat (0⇩m nr1 nc1) (0⇩m nr1 nc2) (0⇩m nr2 nc1) (0⇩m nr2 nc2) = 0⇩m (nr1 + nr2) (nc1 + nc2)"
  by (rule eq_matI, auto)

lemma row_four_block_mat:
  assumes c: "A ∈ carrier_mat nr1 nc1" "B ∈ carrier_mat nr1 nc2"
  "C ∈ carrier_mat nr2 nc1" "D ∈ carrier_mat nr2 nc2"
  shows
  "i < nr1 ⟹ row (four_block_mat A B C D) i = row A i @⇩v row B i" (is "_ ⟹ ?AB")
  "¬ i < nr1 ⟹ i < nr1 + nr2 ⟹ row (four_block_mat A B C D) i = row C (i - nr1) @⇩v row D (i - nr1)"
  (is "_ ⟹ _ ⟹ ?CD")
proof -
  assume i: "i < nr1"
  show ?AB by (rule eq_vecI, insert i c, auto)
next
  assume i: "¬ i < nr1" "i < nr1 + nr2"
  show ?CD by (rule eq_vecI, insert i c, auto)
qed

lemma col_four_block_mat:
  assumes c: "A ∈ carrier_mat nr1 nc1" "B ∈ carrier_mat nr1 nc2"
  "C ∈ carrier_mat nr2 nc1" "D ∈ carrier_mat nr2 nc2"
  shows
  "j < nc1 ⟹ col (four_block_mat A B C D) j = col A j @⇩v col C j" (is "_ ⟹ ?AC")
  "¬ j < nc1 ⟹ j < nc1 + nc2 ⟹ col (four_block_mat A B C D) j = col B (j - nc1) @⇩v col D (j - nc1)"
  (is "_ ⟹ _ ⟹ ?BD")
proof -
  assume j: "j < nc1"
  show ?AC by (rule eq_vecI, insert j c, auto)
next
  assume j: "¬ j < nc1" "j < nc1 + nc2"
  show ?BD by (rule eq_vecI, insert j c, auto)
qed

lemma mult_four_block_mat: assumes
  c1: "A1 ∈ carrier_mat nr1 n1" "B1 ∈ carrier_mat nr1 n2" "C1 ∈ carrier_mat nr2 n1" "D1 ∈ carrier_mat nr2 n2" and
  c2: "A2 ∈ carrier_mat n1 nc1" "B2 ∈ carrier_mat n1 nc2" "C2 ∈ carrier_mat n2 nc1" "D2 ∈ carrier_mat n2 nc2"
  shows "four_block_mat A1 B1 C1 D1 * four_block_mat A2 B2 C2 D2
  = four_block_mat (A1 * A2 + B1 * C2) (A1 * B2 + B1 * D2)
    (C1 * A2 + D1 * C2) (C1 * B2 + D1 * D2)" (is "?M1 * ?M2 = _")
proof -
  note row = row_four_block_mat[OF c1]
  note col = col_four_block_mat[OF c2]
  {
    fix i j
    assume i: "i < nr1" and j: "j < nc1"
    have "row ?M1 i ∙ col ?M2 j = row A1 i ∙ col A2 j + row B1 i ∙ col C2 j"
      unfolding row(1)[OF i] col(1)[OF j]
      by (rule scalar_prod_append[of _ n1 _ n2], insert c1 c2 i j, auto)
  }
  moreover
  {
    fix i j
    assume i: "¬ i < nr1" "i < nr1 + nr2" and j: "j < nc1"
    hence i': "i - nr1 < nr2" by auto
    have "row ?M1 i ∙ col ?M2 j = row C1 (i - nr1) ∙ col A2 j + row D1 (i - nr1) ∙ col C2 j"
      unfolding row(2)[OF i] col(1)[OF j]
      by (rule scalar_prod_append[of _ n1 _ n2], insert c1 c2 i i' j, auto)
  }
  moreover
  {
    fix i j
    assume i: "i < nr1" and j: "¬ j < nc1" "j < nc1 + nc2"
    hence j': "j - nc1 < nc2" by auto
    have "row ?M1 i ∙ col ?M2 j = row A1 i ∙ col B2 (j - nc1) + row B1 i ∙ col D2 (j - nc1)"
      unfolding row(1)[OF i] col(2)[OF j]
      by (rule scalar_prod_append[of _ n1 _ n2], insert c1 c2 i j' j, auto)
  }
  moreover
  {
    fix i j
    assume i: "¬ i < nr1" "i < nr1 + nr2" and j: "¬ j < nc1" "j < nc1 + nc2"
    hence i': "i - nr1 < nr2" and j': "j - nc1 < nc2" by auto
    have "row ?M1 i ∙ col ?M2 j = row C1 (i - nr1) ∙ col B2 (j - nc1) + row D1 (i - nr1) ∙ col D2 (j - nc1)"
      unfolding row(2)[OF i] col(2)[OF j]
      by (rule scalar_prod_append[of _ n1 _ n2], insert c1 c2 i i' j' j, auto)
  }
  ultimately show ?thesis
    by (intro eq_matI, insert c1 c2, auto)
qed

definition append_rows :: "'a :: zero mat ⇒ 'a mat ⇒ 'a mat" (infixr "@⇩r" 65)where
  "A @⇩r B = four_block_mat A (0⇩m (dim_row A) 0) B (0⇩m (dim_row B) 0)" 

lemma carrier_append_rows[simp,intro]: "A ∈ carrier_mat nr1 nc ⟹ B ∈ carrier_mat nr2 nc ⟹
  A @⇩r B ∈ carrier_mat (nr1 + nr2) nc" 
  unfolding append_rows_def by auto

lemma col_mult2[simp]:
  assumes A: "A : carrier_mat nr n"
      and B: "B : carrier_mat n nc"
      and j: "j < nc"
  shows "col (A * B) j = A *⇩v col B j"
proof
  have AB: "A * B : carrier_mat nr nc" using A B by auto
  fix i assume i: "i < dim_vec (A *⇩v col B j)"
  show "col (A * B) j $ i = (A *⇩v col B j) $ i"
    using A B AB j i by simp
qed auto

lemma mat_vec_as_mat_mat_mult: assumes A: "A ∈ carrier_mat nr nc" 
  and v: "v ∈ carrier_vec nc" 
shows "A *⇩v v = col (A * mat_of_cols nc [v]) 0"  
  by (subst col_mult2[OF A], insert v, auto)

lemma mat_mult_append: assumes A: "A ∈ carrier_mat nr1 nc" 
  and B: "B ∈ carrier_mat nr2 nc" 
  and v: "v ∈ carrier_vec nc" 
shows "(A @⇩r B) *⇩v v = (A *⇩v v) @⇩v (B *⇩v v)" 
proof -
  let ?Fb1 = "four_block_mat A (0⇩m nr1 0) B (0⇩m nr2 0)" 
  let ?Fb2 = "four_block_mat (mat_of_cols nc [v]) (0⇩m nc 0) (0⇩m 0 1) (0⇩m 0 0)" 
  have id: "?Fb2 = mat_of_cols nc [v]" 
    using v by auto
  have "(A @⇩r B) *⇩v v = col (?Fb1 * ?Fb2) 0" unfolding id
    by (subst mat_vec_as_mat_mat_mult[OF _ v], insert A B, auto simp: append_rows_def)
  also have "?Fb1 * ?Fb2 = four_block_mat (A * mat_of_cols nc [v] + 0⇩m nr1 0 * 0⇩m 0 1) (A * 0⇩m nc 0 + 0⇩m nr1 0 * 0⇩m 0 0)
     (B * mat_of_cols nc [v] + 0⇩m nr2 0 * 0⇩m 0 1) (B * 0⇩m nc 0 + 0⇩m nr2 0 * 0⇩m 0 0)" 
    by (rule mult_four_block_mat[OF A _ B], auto)
  also have "(A * mat_of_cols nc [v] + 0⇩m nr1 0 * 0⇩m 0 1) = A * mat_of_cols nc [v]" 
    using A v by auto
  also have "(B * mat_of_cols nc [v] + 0⇩m nr2 0 * 0⇩m 0 1) = B * mat_of_cols nc [v]" 
    using B v by auto
  also have "(A * 0⇩m nc 0 + 0⇩m nr1 0 * 0⇩m 0 0) = 0⇩m nr1 0" using A by auto 
  also have "(B * 0⇩m nc 0 + 0⇩m nr2 0 * 0⇩m 0 0) = 0⇩m nr2 0" using B by auto
  finally have "(A @⇩r B) *⇩v v = col (four_block_mat (A * mat_of_cols nc [v]) (0⇩m nr1 0) (B * mat_of_cols nc [v]) (0⇩m nr2 0)) 0" .
  also have "… = col (A * mat_of_cols nc [v]) 0 @⇩v col (B * mat_of_cols nc [v]) 0" 
    by (rule col_four_block_mat, insert A B v, auto)
  also have "col (A * mat_of_cols nc [v]) 0 = A *⇩v v" 
    by (rule mat_vec_as_mat_mat_mult[symmetric, OF A v])
  also have "col (B * mat_of_cols nc [v]) 0 = B *⇩v v" 
    by (rule mat_vec_as_mat_mat_mult[symmetric, OF B v])
  finally show ?thesis .
qed
 
lemma append_rows_le: assumes A: "A ∈ carrier_mat nr1 nc" 
  and B: "B ∈ carrier_mat nr2 nc" 
  and a: "a ∈ carrier_vec nr1" 
  and v: "v ∈ carrier_vec nc"
shows "(A @⇩r B) *⇩v v ≤ (a @⇩v b) ⟷ A *⇩v v ≤ a ∧ B *⇩v v ≤ b" 
  unfolding mat_mult_append[OF A B v]
  by (rule append_vec_le[OF _ a], insert A v, auto)


lemma elements_four_block_mat:
  assumes c: "A ∈ carrier_mat nr1 nc1" "B ∈ carrier_mat nr1 nc2"
  "C ∈ carrier_mat nr2 nc1" "D ∈ carrier_mat nr2 nc2"
  shows
  "elements_mat (four_block_mat A B C D) ⊆
   elements_mat A ∪ elements_mat B ∪ elements_mat C ∪ elements_mat D"
   (is "elements_mat ?four ⊆ _")
proof rule
  fix a assume "a ∈ elements_mat ?four"
  then obtain i j
    where i4: "i < dim_row ?four" and j4: "j < dim_col ?four" and a: "a = ?four $$ (i, j)"
    by auto
  show "a ∈ elements_mat A ∪ elements_mat B ∪ elements_mat C ∪ elements_mat D"
  proof (cases "i < nr1")
    case True note i1 = this
    show ?thesis
    proof (cases "j < nc1")
      case True
      then have "a = A $$ (i,j)" using c i1 a by simp
      thus ?thesis using c i1 True by auto next
      case False
      then have "a = B $$ (i,j-nc1)" using c i1 a j4 by simp
      moreover have "j - nc1 < nc2" using c j4 False by auto
      ultimately show ?thesis using c i1 by auto
    qed next
    case False note i1 = this
    have i2: "i - nr1 < nr2" using c i1 i4 by auto
    show ?thesis
    proof (cases "j < nc1")
      case True
      then have "a = C $$ (i-nr1,j)" using c i2 a i1 by simp
      thus ?thesis using c i2 True by auto next
      case False
      then have "a = D $$ (i-nr1,j-nc1)" using c i2 a i1 j4 by simp
      moreover have "j - nc1 < nc2" using c j4 False by auto
      ultimately show ?thesis using c i2 by auto
    qed
  qed
qed

lemma assoc_four_block_mat: fixes FB :: "'a mat ⇒ 'a mat ⇒ 'a :: zero mat"
  defines FB: "FB ≡ λ Bb Cc. four_block_mat Bb (0⇩m (dim_row Bb) (dim_col Cc)) (0⇩m (dim_row Cc) (dim_col Bb)) Cc"
  shows "FB A (FB B C) = FB (FB A B) C" (is "?L = ?R")
proof -
  let ?ar = "dim_row A" let ?ac = "dim_col A"
  let ?br = "dim_row B" let ?bc = "dim_col B"
  let ?cr = "dim_row C" let ?cc = "dim_col C"
  let ?r = "?ar + ?br + ?cr" let ?c = "?ac + ?bc + ?cc"
  let ?BC = "FB B C" let ?AB = "FB A B"
  have dL: "dim_row ?L = ?r" "dim_col ?L = ?c" unfolding FB by auto
  have dR: "dim_row ?R = ?ar + ?br + ?cr" "dim_col ?R = ?ac + ?bc + ?cc" unfolding FB by auto
  have dBC: "dim_row ?BC = ?br + ?cr" "dim_col ?BC = ?bc + ?cc" unfolding FB by auto
  have dAB: "dim_row ?AB = ?ar + ?br" "dim_col ?AB = ?ac + ?bc" unfolding FB by auto
  show ?thesis
  proof (intro eq_matI[of ?R ?L, unfolded dL dR, OF _ refl refl])
    fix i j
    assume i: "i < ?r" and j: "j < ?c"
    show "?L $$ (i,j) = ?R $$ (i,j)"
    proof (cases "i < ?ar")
      case True note i = this
      thus ?thesis using j
        by (cases "j < ?ac", auto simp: FB)
    next
      case False note ii = this
      show ?thesis
      proof (cases "j < ?ac")
        case True
        with i ii show ?thesis unfolding FB by auto
      next
        case False note jj = this
        from j jj i ii have L: "?L $$ (i,j) = ?BC $$ (i - ?ar, j - ?ac)" unfolding FB by auto
        have R: "?R $$ (i,j) = ?BC $$ (i - ?ar, j - ?ac)" using ii jj i j
          by (cases "i < ?ar + ?br"; cases "j < ?ac + ?bc", auto simp: FB)
        show ?thesis unfolding L R ..
      qed
    qed
  qed
qed

definition split_block :: "'a mat ⇒ nat ⇒ nat ⇒ ('a mat × 'a mat × 'a mat × 'a mat)"
  where "split_block A sr sc = (let
    nr = dim_row A; nc = dim_col A;
    nr2 = nr - sr; nc2 = nc - sc;
    A1 = mat sr sc (λ ij. A $$ ij);
    A2 = mat sr nc2 (λ (i,j). A $$ (i,j+sc));
    A3 = mat nr2 sc (λ (i,j). A $$ (i+sr,j));
    A4 = mat nr2 nc2 (λ (i,j). A $$ (i+sr,j+sc))
  in (A1,A2,A3,A4))"

lemma split_block: assumes res: "split_block A sr1 sc1 = (A1,A2,A3,A4)"
  and dims: "dim_row A = sr1 + sr2" "dim_col A = sc1 + sc2"
  shows "A1 ∈ carrier_mat sr1 sc1" "A2 ∈ carrier_mat sr1 sc2"
    "A3 ∈ carrier_mat sr2 sc1" "A4 ∈ carrier_mat sr2 sc2"
    "A = four_block_mat A1 A2 A3 A4"
  using res unfolding split_block_def Let_def
  by (auto simp: dims)

text ‹Using @{const four_block_mat} we define block-diagonal matrices.›

fun diag_block_mat :: "'a :: zero mat list ⇒ 'a mat" where
  "diag_block_mat [] = 0⇩m 0 0"
| "diag_block_mat (A # As) = (let
     B = diag_block_mat As
     in four_block_mat A (0⇩m (dim_row A) (dim_col B)) (0⇩m (dim_row B) (dim_col A)) B)"

lemma dim_diag_block_mat:
  "dim_row (diag_block_mat As) = sum_list (map dim_row As)" (is "?row")
  "dim_col (diag_block_mat As) = sum_list (map dim_col As)" (is "?col")
proof -
  have "?row ∧ ?col"
    by (induct As, auto simp: Let_def)
  thus ?row and ?col by auto
qed

lemma diag_block_mat_singleton[simp]: "diag_block_mat [A] = A"
  by auto

lemma diag_block_mat_append: "diag_block_mat (As @ Bs) =
  (let A = diag_block_mat As; B = diag_block_mat Bs
  in four_block_mat A (0⇩m (dim_row A) (dim_col B)) (0⇩m (dim_row B) (dim_col A)) B)"
  unfolding Let_def
proof (induct As)
  case (Cons A As)
  show ?case
    unfolding append.simps
    unfolding diag_block_mat.simps Let_def
    unfolding Cons
    by (rule assoc_four_block_mat)
qed auto

lemma diag_block_mat_last: "diag_block_mat (As @ [B]) =
  (let A = diag_block_mat As
  in four_block_mat A (0⇩m (dim_row A) (dim_col B)) (0⇩m (dim_row B) (dim_col A)) B)"
  unfolding diag_block_mat_append diag_block_mat_singleton by auto


lemma diag_block_mat_square:
  "Ball (set As) square_mat ⟹ square_mat (diag_block_mat As)"
by (induct As, auto simp:Let_def)

lemma diag_block_one_mat[simp]:
  "diag_block_mat (map (λA. 1⇩m (dim_row A)) As) = (1⇩m (sum_list (map dim_row As)))"
  by (induct As, auto simp: Let_def)

lemma elements_diag_block_mat:
  "elements_mat (diag_block_mat As) ⊆ {0} ∪ ⋃ (set (map elements_mat As))"
proof (induct As)
  case Nil then show ?case using dim_diag_block_mat[of Nil] by auto next
  case (Cons A As)
    let ?D = "diag_block_mat As"
    let ?B = "0⇩m (dim_row A) (dim_col ?D)"
    let ?C = "0⇩m (dim_row ?D) (dim_col A)"
    have A: "A ∈ carrier_mat (dim_row A) (dim_col A)" by auto
    have B: "?B ∈ carrier_mat (dim_row A) (dim_col ?D)" by auto
    have C: "?C ∈ carrier_mat (dim_row ?D) (dim_col A)" by auto
    have D: "?D ∈ carrier_mat (dim_row ?D) (dim_col ?D)" by auto
    have
      "elements_mat (diag_block_mat (A#As)) ⊆
       elements_mat A ∪ elements_mat ?B ∪ elements_mat ?C ∪ elements_mat ?D"
      unfolding diag_block_mat.simps Let_def
      using elements_four_block_mat[OF A B C D] elements_0_mat
      by auto
    also have "... ⊆ {0} ∪ elements_mat A ∪ elements_mat ?D"
      using elements_0_mat by auto
    finally show ?case using Cons by auto
qed

lemma diag_block_pow_mat: assumes sq: "Ball (set As) square_mat"
  shows "diag_block_mat As ^⇩m n = diag_block_mat (map (λ A. A ^⇩m n) As)" (is "?As ^⇩m _ = _")
proof (induct n)
  case 0
  have "?As ^⇩m 0 = 1⇩m (dim_row ?As)" by simp
  also have "dim_row ?As = sum_list (map dim_row As)"
    using diag_block_mat_square[OF sq] unfolding dim_diag_block_mat by auto
  also have "1⇩m … = diag_block_mat (map (λA. 1⇩m (dim_row A)) As)" by simp
  also have "… = diag_block_mat (map (λ A. A ^⇩m 0) As)" by simp
  finally show ?case .
next
  case (Suc n)
  let ?An = "λ As. diag_block_mat (map (λA. A ^⇩m n) As)"
  let ?Asn = "λ As. diag_block_mat (map (λA. A ^⇩m n * A) As)"
  from Suc have "?case = (?An As * diag_block_mat As = ?Asn As)" by simp
  also have "…" using sq
  proof (induct As)
    case (Cons A As)
    hence IH: "?An As * diag_block_mat As = ?Asn As"
      and sq: "Ball (set As) square_mat" and A: "dim_col A = dim_row A" by auto
    have sq2: "Ball (set (List.map (λA. A ^⇩m n) As)) square_mat"
      and sq3: "Ball (set (List.map (λA. A ^⇩m n * A) As)) square_mat"
      using sq by auto
    define n1 where "n1 = dim_row A"
    define n2 where "n2 = sum_list (map dim_row As)"
    from A have A: "A ∈ carrier_mat n1 n1" unfolding n1_def carrier_mat_def by simp
    have [simp]: "dim_col (?An As) = n2" "dim_row (?An As) = n2"
      unfolding n2_def
      using diag_block_mat_square[OF sq2,unfolded square_mat.simps]
      unfolding dim_diag_block_mat map_map by (auto simp:o_def)
    have [simp]: "dim_col (?Asn As) = n2" "dim_row (?Asn As) = n2"
      unfolding n2_def
      using diag_block_mat_square[OF sq3,unfolded square_mat.simps]
      unfolding dim_diag_block_mat map_map by (auto simp:o_def)
    have [simp]:
      "dim_row (diag_block_mat As) = n2"
      "dim_col (diag_block_mat As) = n2"
      unfolding n2_def
      using diag_block_mat_square[OF sq,unfolded square_mat.simps]
      unfolding dim_diag_block_mat by auto

    have [simp]: "diag_block_mat As ∈ carrier_mat n2 n2" unfolding carrier_mat_def by simp
    have [simp]: "?An As ∈ carrier_mat n2 n2" unfolding carrier_mat_def by simp
    show ?case unfolding diag_block_mat.simps Let_def list.simps
      by (subst mult_four_block_mat[of _ n1 n1 _ n2 _ n2 _ _ n1 _ n2],
      insert A, auto simp: IH)
  qed auto
  finally show ?case by simp
qed

lemma diag_block_upper_triangular: assumes
    "⋀ A i j. A ∈ set As ⟹ j < i ⟹ i < dim_row A ⟹ A $$ (i,j) = 0"
  and "Ball (set As) square_mat"
  and "j < i" "i < dim_row (diag_block_mat As)"
  shows "diag_block_mat As $$ (i,j) = 0"
  using assms
proof (induct As arbitrary: i j)
  case (Cons A As i j)
  let ?n1 = "dim_row A"
  let ?n2 = "sum_list (map dim_row As)"
  from Cons have [simp]: "dim_col A = ?n1" by simp
  from Cons have "Ball (set As) square_mat" by auto
  note [simp] = diag_block_mat_square[OF this,unfolded square_mat.simps]
  note [simp] = dim_diag_block_mat(1)
  from Cons(5) have i: "i < ?n1 + ?n2" by simp
  show ?case
  proof (cases "i < ?n1")
    case True
    with Cons(4) have j: "j < ?n1" by auto
    with True Cons(2)[of A, OF _ Cons(4)] show ?thesis
      by (simp add: Let_def)
  next
    case False note iAs = this
    show ?thesis
    proof (cases "j < ?n1")
      case True
      with i iAs show ?thesis by (simp add: Let_def)
    next
      case False note jAs = this
      from Cons(4) i have j: "j < ?n1 + ?n2" by auto
      show ?thesis using iAs jAs i j
        by (simp add: Let_def, subst Cons(1), insert Cons(2-4), auto)
    qed
  qed
qed simp

lemma smult_four_block_mat: assumes c: "A ∈ carrier_mat nr1 nc1" "B ∈ carrier_mat nr1 nc2"
  "C ∈ carrier_mat nr2 nc1" "D ∈ carrier_mat nr2 nc2"
  shows "a ⋅⇩m four_block_mat A B C D = four_block_mat (a ⋅⇩m A) (a ⋅⇩m B) (a ⋅⇩m C) (a ⋅⇩m D)"
  by (rule eq_matI, insert c, auto)

lemma map_four_block_mat: assumes c: "A ∈ carrier_mat nr1 nc1" "B ∈ carrier_mat nr1 nc2"
  "C ∈ carrier_mat nr2 nc1" "D ∈ carrier_mat nr2 nc2"
  shows "map_mat f (four_block_mat A B C D) = four_block_mat (map_mat f A) (map_mat f B) (map_mat f C) (map_mat f D)"
  by (rule eq_matI, insert c, auto)

lemma add_four_block_mat: assumes
  c1: "A1 ∈ carrier_mat nr1 nc1" "B1 ∈ carrier_mat nr1 nc2" "C1 ∈ carrier_mat nr2 nc1" "D1 ∈ carrier_mat nr2 nc2" and
  c2: "A2 ∈ carrier_mat nr1 nc1" "B2 ∈ carrier_mat nr1 nc2" "C2 ∈ carrier_mat nr2 nc1" "D2 ∈ carrier_mat nr2 nc2"
  shows "four_block_mat A1 B1 C1 D1 + four_block_mat A2 B2 C2 D2
  = four_block_mat (A1 + A2) (B1 + B2) (C1 + C2) (D1 + D2)"
  by (rule eq_matI, insert assms, auto)


lemma diag_four_block_mat: assumes c: "A ∈ carrier_mat n1 n1"
   "D ∈ carrier_mat n2 n2"
  shows "diag_mat (four_block_mat A B C D) = diag_mat A @ diag_mat D"
  by (rule nth_equalityI, insert c, auto simp: diag_mat_def nth_append)

definition mk_diagonal :: "'a::zero list ⇒ 'a mat"
  where "mk_diagonal as = diag_block_mat (map (λa. mat (Suc 0) (Suc 0) (λ_. a)) as)"

lemma mk_diagonal_dim:
  "dim_row (mk_diagonal as) = length as" "dim_col (mk_diagonal as) = length as"
  unfolding mk_diagonal_def by(induct as, auto simp: Let_def)

lemma mk_diagonal_diagonal: "diagonal_mat (mk_diagonal as)"
  unfolding mk_diagonal_def
proof (induct as)
  case Nil show ?case unfolding mk_diagonal_def diagonal_mat_def by simp next
  case (Cons a as)
    let ?n = "length (a#as)"
    let ?A = "mat (Suc 0) (Suc 0) (λ_. a)"
    let ?f = "map (λa. mat (Suc 0) (Suc 0) (λ_. a))"
    let ?AS = "diag_block_mat (?f as)"
    let ?AAS = "diag_block_mat (?f (a#as))"
    show ?case
      unfolding diagonal_mat_def
    proof(intro allI impI)
      fix i j assume ir: "i < dim_row ?AAS" and jc: "j < dim_col ?AAS" and ij: "i ≠ j"
      hence ir2: "i < 1 + dim_row ?AS" and jc2: "j < 1 + dim_col ?AS"
        unfolding dim_row_mat list.map diag_block_mat.simps Let_def
        by auto
      show "?AAS $$ (i,j) = 0"
      proof (cases "i = 0")
        case True
          then show ?thesis using jc ij by (auto simp: Let_def) next
        case False note i0 = this
          show ?thesis
          proof (cases "j = 0")
            case True
              then show ?thesis using ir ij by (auto simp: Let_def) next
            case False
              have ir3: "i-1 < dim_row ?AS" and jc3: "j-1 < dim_col ?AS"
                using ir2 jc2 i0 False by auto
              have IH: "⋀i j. i < dim_row ?AS ⟹ j < dim_col ?AS ⟹ i ≠ j ⟹
                ?AS $$ (i,j) = 0"
                using Cons unfolding diagonal_mat_def by auto
              have "?AS $$ (i-1,j-1) = 0"
                using IH[OF ir3 jc3] i0 False ij by auto
              thus ?thesis using ir jc ij by (simp add: Let_def)
          qed
      qed
    qed
qed

definition orthogonal_mat :: "'a::semiring_0 mat ⇒ bool"
  where "orthogonal_mat A ≡
    let B = transpose_mat A * A in
    diagonal_mat B ∧ (∀i<dim_col A. B $$ (i,i) ≠ 0)"

lemma orthogonal_matD[elim]:
  "orthogonal_mat A ⟹
   i < dim_col A ⟹ j < dim_col A ⟹ (col A i ∙ col A j = 0) = (i ≠ j)"
  unfolding orthogonal_mat_def diagonal_mat_def by auto

lemma orthogonal_matI[intro]:
  "(⋀i j. i < dim_col A ⟹ j < dim_col A ⟹ (col A i ∙ col A j = 0) = (i ≠ j)) ⟹
   orthogonal_mat A"
  unfolding orthogonal_mat_def diagonal_mat_def by auto

definition orthogonal :: "'a::semiring_0 vec list ⇒ bool"
  where "orthogonal vs ≡
    ∀i j. i < length vs ⟶ j < length vs ⟶
      (vs ! i ∙ vs ! j = 0) = (i ≠ j)"

lemma orthogonalD[elim]:
  "orthogonal vs ⟹ i < length vs ⟹ j < length vs ⟹
  (nth vs i ∙ nth vs j = 0) = (i ≠ j)"
  unfolding orthogonal_def by auto

lemma orthogonalI[intro]:
  "(⋀i j. i < length vs ⟹ j < length vs ⟹ (nth vs i ∙ nth vs j = 0) = (i ≠ j)) ⟹
   orthogonal vs"
  unfolding orthogonal_def by auto


lemma transpose_four_block_mat: assumes *: "A ∈ carrier_mat nr1 nc1" "B ∈ carrier_mat nr1 nc2"
  "C ∈ carrier_mat nr2 nc1" "D ∈ carrier_mat nr2 nc2"
  shows "transpose_mat (four_block_mat A B C D) =
    four_block_mat (transpose_mat A) (transpose_mat C) (transpose_mat B) (transpose_mat D)"
  by (rule eq_matI, insert *, auto)

lemma zero_transpose_mat[simp]: "transpose_mat (0⇩m n m) = (0⇩m m n)"
  by (rule eq_matI, auto)

lemma upper_triangular_four_block: assumes AD: "A ∈ carrier_mat n n" "D ∈ carrier_mat m m"
  and ut: "upper_triangular A" "upper_triangular D"
  shows "upper_triangular (four_block_mat A B (0⇩m m n) D)"
proof -
  let ?C = "four_block_mat A B (0⇩m m n) D"
  from AD have dim: "dim_row ?C = n + m" "dim_col ?C = n + m" "dim_row A = n" by auto
  show ?thesis
  proof (rule upper_triangularI, unfold dim)
    fix i j
    assume *: "j < i" "i < n + m"
    show "?C $$ (i,j) = 0"
    proof (cases "i < n")
      case True
      with upper_triangularD[OF ut(1) *(1)] * AD show ?thesis by auto
    next
      case False note i = this
      show ?thesis by (cases "j < n", insert upper_triangularD[OF ut(2)] * i AD, auto)
    qed
  qed
qed

lemma pow_four_block_mat: assumes A: "A ∈ carrier_mat n n"
  and B: "B ∈ carrier_mat m m"
  shows "(four_block_mat A (0⇩m n m) (0⇩m m n) B) ^⇩m k =
    four_block_mat (A ^⇩m k) (0⇩m n m) (0⇩m m n) (B ^⇩m k)"
proof (induct k)
  case (Suc k)
  let ?FB = "λ A B. four_block_mat A (0⇩m n m) (0⇩m m n) B"
  let ?A = "?FB A B"
  let ?B = "?FB (A ^⇩m k) (B ^⇩m k)"
  from A B have Ak: "A ^⇩m k ∈ carrier_mat n n" and Bk: "B ^⇩m k ∈ carrier_mat m m" by auto
  have "?A ^⇩m Suc k = ?A ^⇩m k * ?A" by simp
  also have "?A ^⇩m k = ?B " by (rule Suc)
  also have "?B * ?A = ?FB (A ^⇩m Suc k) (B ^⇩m Suc k)"
    by (subst mult_four_block_mat[OF Ak _ _ Bk A _ _ B], insert A B, auto)
  finally show ?case .
qed (insert A B, auto)


lemma uminus_scalar_prod:
  assumes [simp]: "v : carrier_vec n" "w : carrier_vec n"
  shows "- ((v::'a::field vec) ∙ w) = (- v) ∙ w"
  unfolding scalar_prod_def uminus_vec_def
  apply (subst sum_negf[symmetric])
proof (rule sum.cong[OF refl])
  fix i assume i: "i : {0 ..<dim_vec w}"
  have [simp]: "dim_vec v = n" "dim_vec w = n" by auto
  show "- (v $ i * w $ i) = vec (dim_vec v) (λi. - v $ i) $ i * w $ i"
    unfolding minus_mult_left using i by auto
qed


lemma append_vec_eq:
  assumes [simp]: "v : carrier_vec n" "v' : carrier_vec n"
  shows [simp]: "v @⇩v w = v' @⇩v w' ⟷ v = v' ∧ w = w'" (is "?L ⟷ ?R")
proof
  have [simp]: "dim_vec v = n" "dim_vec v' = n" by auto
  { assume L: ?L
    have vv': "v = v'"
    proof
      fix i assume i: "i < dim_vec v'"
      have "(v @⇩v w) $ i = (v' @⇩v w') $ i" using L by auto
      thus "v $ i = v' $ i" using i by auto
    qed auto
    moreover have "w = w'"
    proof
      show "dim_vec w = dim_vec w'" using vv' L
        by (metis add_diff_cancel_left' index_append_vec(2))
      moreover fix i assume i: "i < dim_vec w'"
      have "(v @⇩v w) $ (n + i) = (v' @⇩v w') $ (n + i)" using L by auto
      ultimately show "w $ i = w' $ i" using i by simp
    qed
    ultimately show ?R by simp
  }
qed auto

lemma append_vec_add:
  assumes [simp]: "v : carrier_vec n" "v' : carrier_vec n"
      and [simp]: "w : carrier_vec m" "w' : carrier_vec m"
  shows "(v @⇩v w) + (v' @⇩v w') = (v + v') @⇩v (w + w')" (is "?L = ?R")
proof
  have [simp]: "dim_vec v = n" "dim_vec v' = n" by auto
  have [simp]: "dim_vec w = m" "dim_vec w' = m" by auto
  fix i assume i: "i < dim_vec ?R"
  thus "?L $ i = ?R $ i" by (cases "i < n",auto)
qed auto

lemma four_block_mat_mult_vec:
  assumes A: "A : carrier_mat nr1 nc1"
      and B: "B : carrier_mat nr1 nc2" 
      and C: "C : carrier_mat nr2 nc1" 
      and D: "D : carrier_mat nr2 nc2"
      and a: "a : carrier_vec nc1"
      and d: "d : carrier_vec nc2"
  shows "four_block_mat A B C D *⇩v (a @⇩v d) = (A *⇩v a + B *⇩v d) @⇩v (C *⇩v a + D *⇩v d)"
    (is "?ABCD *⇩v _ = ?r")
proof
  have ABCD: "?ABCD : carrier_mat (nr1+nr2) (nc1+nc2)" using four_block_carrier_mat[OF A D].
  fix i assume i: "i < dim_vec ?r"
  show "(?ABCD *⇩v (a @⇩v d)) $ i = ?r $ i" (is "?li = _")
  proof (cases "i < nr1")
    case True
      have "?li = (row A i @⇩v row B i) ∙ (a @⇩v d)"
        using A row_four_block_mat[OF A B C D] True by simp
      also have "... = row A i ∙ a + row B i ∙ d"
        apply (rule scalar_prod_append) using A B D a d True by auto
      finally show ?thesis using A B True by auto
    next case False
      let ?i = "i - nr1"
      have "?li = (row C ?i @⇩v row D ?i) ∙ (a @⇩v d)"
        using i row_four_block_mat[OF A B C D] False A B C D by simp
      also have "... = row C ?i ∙ a + row D ?i ∙ d"
        apply (rule scalar_prod_append) using A B C D a d False by auto
      finally show ?thesis using A B C D False i by auto
  qed
qed (insert A B, auto)

lemma mult_mat_vec_split:
  assumes A: "A : carrier_mat n n"
      and D: "D : carrier_mat m m"
      and a: "a : carrier_vec n"
      and d: "d : carrier_vec m"
  shows "four_block_mat A (0⇩m n m) (0⇩m m n) D *⇩v (a @⇩v d) = A *⇩v a @⇩v D *⇩v d"
  by (subst four_block_mat_mult_vec[OF A _ _ D a d], insert A D a d, auto)

lemma similar_mat_witI: assumes "P * Q = 1⇩m n" "Q * P = 1⇩m n" "A = P * B * Q"
  "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "P ∈ carrier_mat n n" "Q ∈ carrier_mat n n"
  shows "similar_mat_wit A B P Q" using assms unfolding similar_mat_wit_def Let_def by auto

lemma similar_mat_witD: assumes "n = dim_row A" "similar_mat_wit A B P Q"
  shows "P * Q = 1⇩m n" "Q * P = 1⇩m n" "A = P * B * Q"
  "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "P ∈ carrier_mat n n" "Q ∈ carrier_mat n n"
  using assms(2) unfolding similar_mat_wit_def Let_def assms(1)[symmetric] by auto

lemma similar_mat_witD2: assumes "A ∈ carrier_mat n m" "similar_mat_wit A B P Q"
  shows "P * Q = 1⇩m n" "Q * P = 1⇩m n" "A = P * B * Q"
  "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" "P ∈ carrier_mat n n" "Q ∈ carrier_mat n n"
  using similar_mat_witD[OF _ assms(2), of n] assms(1)[unfolded carrier_mat_def] by auto

lemma similar_mat_wit_sym: assumes sim: "similar_mat_wit A B P Q"
  shows "similar_mat_wit B A Q P"
proof -
  from similar_mat_witD[OF refl sim] obtain n where
    AB: "{A, B, P, Q} ⊆ carrier_mat n n" "P * Q = 1⇩m n" "Q * P = 1⇩m n" and A: "A = P * B * Q" by blast
  hence *: "{B, A, Q, P} ⊆ carrier_mat n n" "Q * P = 1⇩m n" "P * Q = 1⇩m n" by auto
  let ?c = "λ A. A ∈ carrier_mat n n"
  from * have Carr: "?c B" "?c P" "?c Q" by auto
  note [simp] = assoc_mult_mat[of _ n n _ n _ n]
  show ?thesis
  proof (rule similar_mat_witI[of _ _ n])
    have "Q * A * P = (Q * P) * B * (Q * P)"
      using Carr unfolding A by simp
    also have "… = B" using Carr unfolding AB by simp
    finally show "B = Q * A * P" by simp
  qed (insert * AB, auto)
qed

lemma similar_mat_wit_refl: assumes A: "A ∈ carrier_mat n n"
  shows "similar_mat_wit A A (1⇩m n) (1⇩m n)"
  by (rule similar_mat_witI[OF _ _ _ A], insert A, auto)

lemma similar_mat_wit_trans: assumes AB: "similar_mat_wit A B P Q"
  and BC: "similar_mat_wit B C P' Q'"
  shows "similar_mat_wit A C (P * P') (Q' * Q)"
proof -
  from similar_mat_witD[OF refl AB] obtain n where
    AB: "{A, B, P, Q} ⊆ carrier_mat n n" "P * Q = 1⇩m n" "Q * P = 1⇩m n" "A = P * B * Q" by blast
  hence B: "B ∈ carrier_mat n n" by auto
  from similar_mat_witD2[OF B BC] have
    BC: "{C, P', Q'} ⊆ carrier_mat n n" "P' * Q' = 1⇩m n" "Q' * P' = 1⇩m n" "B = P' * C * Q'" by auto
  let ?c = "λ A. A ∈ carrier_mat n n"
  let ?P = "P * P'"
  let ?Q = "Q' * Q"
  from AB BC have carr: "?c A" "?c B" "?c C" "?c P" "?c P'" "?c Q" "?c Q'"
    and Carr: "{A, C, ?P, ?Q} ⊆ carrier_mat n n" by auto
  note [simp] = assoc_mult_mat[of _ n n _ n _ n]
  have id: "A = ?P * C * ?Q" unfolding AB(4)[unfolded BC(4)] using carr
    by simp
  have "?P * ?Q = P * (P' * Q') * Q" using carr by simp
  also have "… = 1⇩m n" unfolding BC using carr AB by simp
  finally have PQ: "?P * ?Q = 1⇩m n" .
  have "?Q * ?P = Q' * (Q * P) * P'" using carr by simp
  also have "… = 1⇩m n" unfolding AB using carr BC by simp
  finally have QP: "?Q * ?P = 1⇩m n" .
  show ?thesis
    by (rule similar_mat_witI[OF PQ QP id], insert Carr, auto)
qed

lemma similar_mat_refl: "A ∈ carrier_mat n n ⟹ similar_mat A A"
  using similar_mat_wit_refl unfolding similar_mat_def by blast

lemma similar_mat_trans: "similar_mat A B ⟹ similar_mat B C ⟹ similar_mat A C"
  using similar_mat_wit_trans unfolding similar_mat_def by blast

lemma similar_mat_sym: "similar_mat A B ⟹ similar_mat B A"
  using similar_mat_wit_sym unfolding similar_mat_def by blast

lemma similar_mat_wit_four_block: assumes
      1: "similar_mat_wit A1 B1 P1 Q1"
  and 2: "similar_mat_wit A2 B2 P2 Q2"
  and URA: "URA = (P1 * UR * Q2)"
  and LLA: "LLA = (P2 * LL * Q1)"
  and A1: "A1 ∈ carrier_mat n n"
  and A2: "A2 ∈ carrier_mat m m"
  and LL: "LL ∈ carrier_mat m n"
  and UR: "UR ∈ carrier_mat n m"
  shows "similar_mat_wit (four_block_mat A1 URA LLA A2) (four_block_mat B1 UR LL B2)
    (four_block_mat P1 (0⇩m n m) (0⇩m m n) P2) (four_block_mat Q1 (0⇩m n m) (0⇩m m n) Q2)"
  (is "similar_mat_wit ?A ?B ?P ?Q")
proof -
  let ?n = "n + m"
  let ?O1 = "1⇩m n"   let ?O2 = "1⇩m m"   let ?O = "1⇩m ?n"
  from similar_mat_witD2[OF A1 1] have 11: "P1 * Q1 = ?O1" "Q1 * P1 = ?O1"
    and P1: "P1 ∈ carrier_mat n n" and Q1: "Q1 ∈ carrier_mat n n"
    and B1: "B1 ∈ carrier_mat n n" and 1: "A1 = P1 * B1 * Q1" by auto
  from similar_mat_witD2[OF A2 2] have 21: "P2 * Q2 = ?O2" "Q2 * P2 = ?O2"
    and P2: "P2 ∈ carrier_mat m m" and Q2: "Q2 ∈ carrier_mat m m"
    and B2: "B2 ∈ carrier_mat m m" and 2: "A2 = P2 * B2 * Q2" by auto
  have PQ1: "?P * ?Q = ?O"
    by (subst mult_four_block_mat[OF P1 _ _ P2 Q1 _ _ Q2], unfold 11 21, insert P1 P2 Q1 Q2,
      auto intro!: eq_matI)
  have QP1: "?Q * ?P = ?O"
    by (subst mult_four_block_mat[OF Q1 _ _ Q2 P1 _ _ P2], unfold 11 21, insert P1 P2 Q1 Q2,
      auto intro!: eq_matI)
  let ?PB = "?P * ?B"
  have P: "?P ∈ carrier_mat ?n ?n" using P1 P2 by auto
  have Q: "?Q ∈ carrier_mat ?n ?n" using Q1 Q2 by auto
  have B: "?B ∈ carrier_mat ?n ?n" using B1 UR LL B2 by auto
  have PB: "?PB ∈ carrier_mat ?n ?n" using P B by auto
  have PB1: "P1 * B1 ∈ carrier_mat n n" using P1 B1 by auto
  have PB2: "P2 * B2 ∈ carrier_mat m m" using P2 B2 by auto
  have P1UR: "P1 * UR ∈ carrier_mat n m" using P1 UR by auto
  have P2LL: "P2 * LL ∈ carrier_mat m n" using P2 LL by auto
  have id: "?PB = four_block_mat (P1 * B1) (P1 * UR) (P2 * LL) (P2 * B2)"
    by (subst mult_four_block_mat[OF P1 _ _ P2 B1 UR LL B2], insert P1 P2 B1 B2 LL UR, auto)
  have id: "?PB * ?Q = four_block_mat (P1 * B1 * Q1) (P1 * UR * Q2)
    (P2 * LL * Q1) (P2 * B2 * Q2)" unfolding id
    by (subst mult_four_block_mat[OF PB1 P1UR P2LL PB2 Q1 _ _ Q2],
    insert P1 P2 B1 B2 Q1 Q2 UR LL, auto)
  have id: "?A = ?P * ?B * ?Q" unfolding id 1 2 URA LLA ..
  show ?thesis
    by (rule similar_mat_witI[OF PQ1 QP1 id], insert A1 A2 B1 B2 Q1 Q2 P1 P2, auto)
qed


lemma similar_mat_four_block_0_ex: assumes
      1: "similar_mat A1 B1"
  and 2: "similar_mat A2 B2"
  and A0: "A0 ∈ carrier_mat n m"
  and A1: "A1 ∈ carrier_mat n n"
  and A2: "A2 ∈ carrier_mat m m"
  shows "∃ B0. B0 ∈ carrier_mat n m ∧ similar_mat (four_block_mat A1 A0 (0⇩m m n) A2)
    (four_block_mat B1 B0 (0⇩m m n) B2)"
proof -
  from 1[unfolded similar_mat_def] obtain P1 Q1 where 1: "similar_mat_wit A1 B1 P1 Q1" by auto
  note w1 = similar_mat_witD2[OF A1 1]
  from 2[unfolded similar_mat_def] obtain P2 Q2 where 2: "similar_mat_wit A2 B2 P2 Q2" by auto
  note w2 = similar_mat_witD2[OF A2 2]
  from w1 w2 have C: "B1 ∈ carrier_mat n n" "B2 ∈ carrier_mat m m" by auto
  from w1 w2 have id: "0⇩m m n = Q2 * 0⇩m m n * P1" by simp
  let ?wit = "Q1 * A0 * P2"
  from w1 w2 A0 have wit: "?wit ∈ carrier_mat n m" by auto
  from similar_mat_wit_sym[OF similar_mat_wit_four_block[OF similar_mat_wit_sym[OF 1] similar_mat_wit_sym[OF 2]
    refl id C zero_carrier_mat A0]]
  have "similar_mat (four_block_mat A1 A0 (0⇩m m n) A2) (four_block_mat B1 (Q1 * A0 * P2) (0⇩m m n) B2)"
    unfolding similar_mat_def by auto
  thus ?thesis using wit by auto
qed

lemma similar_mat_four_block_0_0: assumes
      1: "similar_mat A1 B1"
  and 2: "similar_mat A2 B2"
  and A1: "A1 ∈ carrier_mat n n"
  and A2: "A2 ∈ carrier_mat m m"
  shows "similar_mat (four_block_mat A1 (0⇩m n m) (0⇩m m n) A2)
    (four_block_mat B1 (0⇩m n m) (0⇩m m n) B2)"
proof -
  from 1[unfolded similar_mat_def] obtain P1 Q1 where 1: "similar_mat_wit A1 B1 P1 Q1" by auto
  note w1 = similar_mat_witD2[OF A1 1]
  from 2[unfolded similar_mat_def] obtain P2 Q2 where 2: "similar_mat_wit A2 B2 P2 Q2" by auto
  note w2 = similar_mat_witD2[OF A2 2]
  from w1 w2 have C: "B1 ∈ carrier_mat n n" "B2 ∈ carrier_mat m m" by auto
  from w1 w2 have id: "0⇩m m n = Q2 * 0⇩m m n * P1" by simp
  from w1 w2 have id2: "0⇩m n m = Q1 * 0⇩m n m * P2" by simp
  from similar_mat_wit_sym[OF similar_mat_wit_four_block[OF similar_mat_wit_sym[OF 1] similar_mat_wit_sym[OF 2]
    id2 id C zero_carrier_mat zero_carrier_mat]]
  show ?thesis unfolding similar_mat_def by blast
qed

lemma similar_diag_mat_block_mat: assumes "⋀ A B. (A,B) ∈ set Ms ⟹ similar_mat A B"
  shows "similar_mat (diag_block_mat (map fst Ms)) (diag_block_mat (map snd Ms))"
  using assms
proof (induct Ms)
  case Nil
  show ?case by (auto intro!: similar_mat_refl[of _ 0])
next
  case (Cons AB Ms)
  obtain A B where AB: "AB = (A,B)" by force
  from Cons(2)[of A B] have simAB: "similar_mat A B" unfolding AB by auto
  from similar_matD[OF this] obtain n where A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" by auto
  hence [simp]: "dim_row A = n" "dim_col A = n" "dim_row B = n" "dim_col B = n" by auto
  let ?C = "diag_block_mat (map fst Ms)" let ?D = "diag_block_mat (map snd Ms)"
  from Cons(1)[OF Cons(2)] have simRec: "similar_mat ?C ?D" by auto
  from similar_matD[OF this] obtain m where C: "?C ∈ carrier_mat m m" and D: "?D ∈ carrier_mat m m" by auto
  hence [simp]: "dim_row ?C = m" "dim_col ?C = m" "dim_row ?D = m" "dim_col ?D = m" by auto
  have "similar_mat (diag_block_mat (map fst (AB # Ms))) (diag_block_mat (map snd (AB # Ms)))
    = similar_mat (four_block_mat A (0⇩m n m) (0⇩m m n) ?C) (four_block_mat B (0⇩m n m) (0⇩m m n) ?D)"
    unfolding AB by (simp add: Let_def)
  also have "…"
    by (rule similar_mat_four_block_0_0[OF simAB simRec A C])
  finally show ?case .
qed

lemma similar_mat_wit_pow: assumes wit: "similar_mat_wit A B P Q"
  shows "similar_mat_wit (A ^⇩m k) (B ^⇩m k) P Q"
proof -
  define n where "n = dim_row A"
  let ?C = "carrier_mat n n"
  from similar_mat_witD[OF refl wit, folded n_def] have
    A: "A ∈ ?C" and B: "B ∈ ?C" and P: "P ∈ ?C" and Q: "Q ∈ ?C"
    and PQ: "P * Q = 1⇩m n" and QP: "Q * P = 1⇩m n"
    and AB: "A = P * B * Q"
    by auto
  from A B have *: "(A ^⇩m k) ∈ carrier_mat n n" "B ^⇩m k ∈ carrier_mat n n" by auto
  note carr = A B P Q
  have id: "A ^⇩m k = P * B ^⇩m k * Q" unfolding AB
  proof (induct k)
    case 0
    thus ?case using carr by (simp add: PQ)
  next
    case (Suc k)
    define Bk where "Bk = B ^⇩m k"
    have Bk: "Bk ∈ carrier_mat n n" unfolding Bk_def using carr by simp
    have "(P * B * Q) ^⇩m Suc k = (P * Bk * Q) * (P * B * Q)" by (simp add: Suc Bk_def)
    also have "… = P * (Bk * (Q * P) * B) * Q"
      using carr Bk by (simp add: assoc_mult_mat[of _ n n _ n _ n])
    also have "Bk * (Q * P) = Bk" unfolding QP using Bk by simp
    finally show ?case unfolding Bk_def by simp
  qed
  show ?thesis
    by (rule similar_mat_witI[OF PQ QP id * P Q])
qed

lemma similar_mat_wit_pow_id: "similar_mat_wit A B P Q ⟹ A ^⇩m k = P * B ^⇩m k * Q"
  using similar_mat_wit_pow[of A B P Q k] unfolding similar_mat_wit_def Let_def by blast

subsection‹Homomorphism properties›

context semiring_hom
begin
abbreviation mat_hom :: "'a mat ⇒ 'b mat" ("mat⇩h")
  where "mat⇩h ≡ map_mat hom"

abbreviation vec_hom :: "'a vec ⇒ 'b vec" ("vec⇩h")
  where "vec⇩h ≡ map_vec hom"

lemma vec_hom_zero: "vec⇩h (0⇩v n) = 0⇩v n"
  by (rule eq_vecI, auto)

lemma mat_hom_one: "mat⇩h (1⇩m n) = 1⇩m n"
  by (rule eq_matI, auto)

lemma mat_hom_mult: assumes A: "A ∈ carrier_mat nr n" and B: "B ∈ carrier_mat n nc"
  shows "mat⇩h (A * B) = mat⇩h A * mat⇩h B"
proof -
  let ?L = "mat⇩h (A * B)"
  let ?R = "mat⇩h A * mat⇩h B"
  let ?A = "mat⇩h A"
  let ?B = "mat⇩h B"
  from A B have id:
    "dim_row ?L = nr" "dim_row ?R = nr"
    "dim_col ?L = nc" "dim_col ?R = nc"  by auto
  show ?thesis
  proof (rule eq_matI, unfold id)
    fix i j
    assume *: "i < nr" "j < nc"
    define I where "I = {0 ..< n}"
    have id: "{0 ..< dim_vec (col ?B j)} = I" "{0 ..< dim_vec (col B j)} = I"
      unfolding I_def using * B by auto
    have finite: "finite I" unfolding I_def by auto
    have I: "I ⊆ {0 ..< n}" unfolding I_def by auto
    have "?L $$ (i,j) = hom (row A i ∙ col B j)" using A B * by auto
    also have "… = row ?A i ∙ col ?B j" unfolding scalar_prod_def id using finite I
    proof (induct I)
      case (insert k I)
      show ?case unfolding sum.insert[OF insert(1-2)] hom_add hom_mult
        using insert(3-) * A B by auto
    qed simp
    also have "… = ?R $$ (i,j)" using A B * by auto
    finally
    show "?L $$ (i, j) = ?R $$ (i, j)" .
  qed auto
qed

lemma mult_mat_vec_hom: assumes A: "A ∈ carrier_mat nr n" and v: "v ∈ carrier_vec n"
  shows "vec⇩h (A *⇩v v) = mat⇩h A *⇩v vec⇩h v"
proof -
  let ?L = "vec⇩h (A *⇩v v)"
  let ?R = "mat⇩h A *⇩v vec⇩h v"
  let ?A = "mat⇩h A"
  let ?v = "vec⇩h v"
  from A v have id:
    "dim_vec ?L = nr" "dim_vec ?R = nr"
    by auto
  show ?thesis
  proof (rule eq_vecI, unfold id)
    fix i
    assume *: "i < nr"
    define I where "I = {0 ..< n}"
    have id: "{0 ..< dim_vec v} = I" "{0 ..< dim_vec (vec⇩h v)} = I"
      unfolding I_def using * v  by auto
    have finite: "finite I" unfolding I_def by auto
    have I: "I ⊆ {0 ..< n}" unfolding I_def by auto
    have "?L $ i = hom (row A i ∙ v)" using A v * by auto
    also have "… = row ?A i ∙ ?v" unfolding scalar_prod_def id using finite I
    proof (induct I)
      case (insert k I)
      show ?case unfolding sum.insert[OF insert(1-2)] hom_add hom_mult
        using insert(3-) * A v by auto
    qed simp
    also have "… = ?R $ i" using A v * by auto
    finally
    show "?L $ i = ?R $ i" .
  qed auto
qed
end

lemma vec_eq_iff: "(x = y) = (dim_vec x = dim_vec y ∧ (∀ i < dim_vec y. x $ i = y $ i))" (is "?l = ?r")
proof
  assume ?r
  show ?l
    by (rule eq_vecI, insert ‹?r›, auto)
qed simp

lemma mat_eq_iff: "(x = y) = (dim_row x = dim_row y ∧ dim_col x = dim_col y ∧
  (∀ i j. i < dim_row y ⟶ j < dim_col y ⟶ x $$ (i,j) = y $$ (i,j)))" (is "?l = ?r")
proof
  assume ?r
  show ?l
    by (rule eq_matI, insert ‹?r›, auto)
qed simp

lemma (in inj_semiring_hom) vec_hom_zero_iff[simp]: "(vec⇩h x = 0⇩v n) = (x = 0⇩v n)"
proof -
  {
    fix i
    assume i: "i < n" "dim_vec x = n"
    hence "vec⇩h x $ i = 0 ⟷ x $ i = 0"
      using index_map_vec(1)[of i x] by simp
  } note main = this
  show ?thesis unfolding vec_eq_iff by (simp, insert main, auto)
qed

lemma (in inj_semiring_hom) mat_hom_inj: "mat⇩h A = mat⇩h B ⟹ A = B"
  unfolding mat_eq_iff by auto

lemma (in inj_semiring_hom) vec_hom_inj: "vec⇩h v = vec⇩h w ⟹ v = w"
  unfolding vec_eq_iff by auto

lemma (in semiring_hom) mat_hom_pow: assumes A: "A ∈ carrier_mat n n"
  shows "mat⇩h (A ^⇩m k) = (mat⇩h A) ^⇩m k"
proof (induct k)
  case (Suc k)
  thus ?case using mat_hom_mult[OF pow_carrier_mat[OF A, of k] A] by simp
qed (simp add: mat_hom_one)

lemma (in semiring_hom) hom_sum_mat: "hom (sum_mat A) = sum_mat (mat⇩h A)"
proof -
  obtain B where id: "?thesis = (hom (sum (($$) A) B) = sum (($$) (mat⇩h A)) B)"
    and B: "B ⊆ {0..<dim_row A} × {0..<dim_col A}"
  unfolding sum_mat_def by auto
  from B have "finite B"
    using finite_subset by blast
  thus ?thesis unfolding id using B
  proof (induct B)
    case (insert x F)
    show ?case unfolding sum.insert[OF insert(1-2)] hom_add
      using insert(3-) by auto
  qed simp
qed

lemma (in semiring_hom) vec_hom_smult: "vec⇩h (ev ⋅⇩v v) = hom ev ⋅⇩v vec⇩h v"
  by (rule eq_vecI, auto simp: hom_distribs)

lemma minus_scalar_prod_distrib: fixes v⇩1 :: "'a :: ring vec"
  assumes v: "v⇩1 ∈ carrier_vec n" "v⇩2 ∈ carrier_vec n" "v⇩3 ∈ carrier_vec n"
  shows "(v⇩1 - v⇩2) ∙ v⇩3 = v⇩1 ∙ v⇩3 - v⇩2 ∙ v⇩3"
  unfolding minus_add_uminus_vec[OF v(1-2)]
  by (subst add_scalar_prod_distrib[OF v(1)], insert v, auto)

lemma scalar_prod_minus_distrib: fixes v⇩1 :: "'a :: ring vec"
  assumes v: "v⇩1 ∈ carrier_vec n" "v⇩2 ∈ carrier_vec n" "v⇩3 ∈ carrier_vec n"
  shows "v⇩1 ∙ (v⇩2 - v⇩3) = v⇩1 ∙ v⇩2 - v⇩1 ∙ v⇩3"
  unfolding minus_add_uminus_vec[OF v(2-3)]
  by (subst scalar_prod_add_distrib[OF v(1)], insert v, auto)

lemma uminus_add_minus_vec:
  assumes "l ∈ carrier_vec n" "r ∈ carrier_vec n"
  shows "- ((l::'a :: ab_group_add vec) + r) = (- l - r)"
  using assms by auto

lemma minus_add_minus_vec: fixes u :: "'a :: ab_group_add vec"
  assumes "u ∈ carrier_vec n" "v ∈ carrier_vec n" "w ∈ carrier_vec n"
  shows "u - (v + w) = u - v - w"
  using assms by auto

lemma uminus_add_minus_mat:
  assumes "l ∈ carrier_mat nr nc" "r ∈ carrier_mat nr nc"
  shows "- ((l::'a :: ab_group_add mat) + r) = (- l - r)"
  using assms by auto

lemma minus_add_minus_mat: fixes u :: "'a :: ab_group_add mat"
  assumes "u ∈ carrier_mat nr nc" "v ∈ carrier_mat nr nc" "w ∈ carrier_mat nr nc"
  shows "u - (v + w) = u - v - w"
  using assms by auto

lemma uminus_uminus_vec[simp]: "- (- (v::'a:: group_add vec)) = v"
  by auto

lemma uminus_eq_vec[simp]: "- (v::'a:: group_add vec) = - w ⟷ v = w"
  by (metis uminus_uminus_vec)

lemma uminus_uminus_mat[simp]: "- (- (A::'a:: group_add mat)) = A"
  by auto

lemma uminus_eq_mat[simp]: "- (A::'a:: group_add mat) = - B ⟷ A = B"
  by (metis uminus_uminus_mat)

lemma smult_zero_mat[simp]: "(k :: 'a :: mult_zero) ⋅⇩m 0⇩m nr nc = 0⇩m nr nc"
  by (intro eq_matI, auto)

lemma similar_mat_wit_smult: fixes A :: "'a :: comm_ring_1 mat"
  assumes "similar_mat_wit A B P Q"
  shows "similar_mat_wit (k ⋅⇩m A) (k ⋅⇩m B) P Q"
proof -
  define n where "n = dim_row A"
  note main = similar_mat_witD[OF n_def assms]
  show ?thesis
    by (rule similar_mat_witI[OF main(1-2) _ _ _ main(6-7)], insert main(3-), auto
      simp: mult_smult_distrib mult_smult_assoc_mat[of _ n n _ n])
qed

lemma similar_mat_smult: fixes A :: "'a :: comm_ring_1 mat"
  assumes "similar_mat A B"
  shows "similar_mat (k ⋅⇩m A) (k ⋅⇩m B)"
  using similar_mat_wit_smult assms unfolding similar_mat_def by blast

definition mat_diag :: "nat ⇒ (nat ⇒ 'a :: zero) ⇒ 'a mat" where
  "mat_diag n f = Matrix.mat n n (λ (i,j). if i = j then f j else 0)"

lemma mat_diag_dim[simp]: "mat_diag n f ∈ carrier_mat n n"
  unfolding mat_diag_def by auto

lemma mat_diag_mult_left: assumes A: "A ∈ carrier_mat n nr"
  shows "mat_diag n f * A = Matrix.mat n nr (λ (i,j). f i * A $$ (i,j))"
proof (rule eq_matI, insert A, auto simp: mat_diag_def scalar_prod_def, goal_cases)
  case (1 i j)
  thus ?case by (subst sum.remove[of _ i], auto)
qed

lemma mat_diag_mult_right: assumes A: "A ∈ carrier_mat nr n"
  shows "A * mat_diag n f = Matrix.mat nr n (λ (i,j). A $$ (i,j) * f j)"
proof (rule eq_matI, insert A, auto simp: mat_diag_def scalar_prod_def, goal_cases)
  case (1 i j)
  thus ?case by (subst sum.remove[of _ j], auto)
qed

lemma mat_diag_diag[simp]: "mat_diag n f * mat_diag n g = mat_diag n (λ i. f i * g i)"
  by (subst mat_diag_mult_left[of _ n n], auto simp: mat_diag_def)

lemma mat_diag_one[simp]: "mat_diag n (λ x. 1) = 1⇩m n" unfolding mat_diag_def by auto

text ‹Interpret vector as row-matrix›

definition "mat_of_row y = mat 1 (dim_vec y) (λ ij. y $ (snd ij))" 

lemma mat_of_row_carrier[simp,intro]: 
  "y ∈ carrier_vec n ⟹ mat_of_row y ∈ carrier_mat 1 n"
  "y ∈ carrier_vec n ⟹ mat_of_row y ∈ carrier_mat (Suc 0) n"
  unfolding mat_of_row_def by auto

lemma mat_of_row_dim[simp]: "dim_row (mat_of_row y) = 1" 
  "dim_col (mat_of_row y) = dim_vec y" 
  unfolding mat_of_row_def by auto

lemma mat_of_row_index[simp]: "x < dim_vec y ⟹ mat_of_row y $$ (0,x) = y $ x" 
  unfolding mat_of_row_def by auto

lemma row_mat_of_row[simp]: "row (mat_of_row y) 0 = y" 
  by auto

lemma mat_of_row_mult_append_rows: assumes y1: "y1 ∈ carrier_vec nr1" 
  and y2: "y2 ∈ carrier_vec nr2" 
  and A1: "A1 ∈ carrier_mat nr1 nc" 
  and A2: "A2 ∈ carrier_mat nr2 nc" 
shows "mat_of_row (y1 @⇩v y2) * (A1 @⇩r A2) = 
  mat_of_row y1 * A1 + mat_of_row y2 * A2" 
proof -
  from A1 A2 have dim: "dim_row A1 = nr1" "dim_row A2 = nr2" by auto
  let ?M1 = "mat_of_row y1" 
  have M1: "?M1 ∈ carrier_mat 1 nr1" using y1 by auto
  let ?M2 = "mat_of_row y2" 
  have M2: "?M2 ∈ carrier_mat 1 nr2" using y2 by auto
  let ?M3 = "0⇩m 0 nr1" 
  let ?M4 = "0⇩m 0 nr2" 
  note z = zero_carrier_mat
  have id: "mat_of_row (y1 @⇩v y2) = four_block_mat 
    ?M1 ?M2 ?M3 ?M4" using y1 y2 
    by (intro eq_matI, auto simp: mat_of_rows_def)
  show ?thesis
    unfolding id append_rows_def dim
    by (subst mult_four_block_mat[OF M1 M2 z z A1 z A2 z], insert A1 A2, auto)
qed

lemma mat_of_row_uminus: "mat_of_row (- v) = - mat_of_row v"
  by auto



text ‹Allowing to construct and deconstruct vectors like lists›
abbreviation vNil where "vNil ≡ vec 0 ((!) [])"
definition vCons where "vCons a v ≡ vec (Suc (dim_vec v)) (λi. case i of 0 ⇒ a | Suc i ⇒ v $ i)"

lemma vec_index_vCons_0 [simp]: "vCons a v $ 0 = a"
  by (simp add: vCons_def)

lemma vec_index_vCons_Suc [simp]:
  fixes v :: "'a vec"
  shows "vCons a v $ Suc n = v $ n"
proof-
  have 1: "vec (Suc d) f $ Suc n = vec d (f ∘ Suc) $ n" for d and f :: "nat ⇒ 'a"
    by (transfer, auto simp: mk_vec_def)
  show ?thesis
    apply (auto simp: 1 vCons_def o_def) apply transfer apply (auto simp: mk_vec_def)
    done
qed

lemma vec_index_vCons: "vCons a v $ n = (if n = 0 then a else v $ (n - 1))"
  by (cases n, auto)

lemma dim_vec_vCons [simp]: "dim_vec (vCons a v) = Suc (dim_vec v)"
  by (simp add: vCons_def)

lemma vCons_carrier_vec[simp]: "vCons a v ∈ carrier_vec (Suc n) ⟷ v ∈ carrier_vec n"
  by (auto dest!: carrier_vecD intro: carrier_vecI)

lemma vec_Suc: "vec (Suc n) f = vCons (f 0) (vec n (f ∘ Suc))" (is "?l = ?r")
proof (unfold vec_eq_iff, intro conjI allI impI)
  fix i assume "i < dim_vec ?r"
  then show "?l $ i = ?r $ i" by (cases i, auto)
qed simp

declare Abs_vec_cases[cases del]

lemma vec_cases [case_names vNil vCons, cases type: vec]:
  assumes "v = vNil ⟹ thesis" and "⋀a w. v = vCons a w ⟹ thesis"
  shows "thesis"
proof (cases "dim_vec v")
  case 0 then show thesis by (intro assms(1), auto)
next
  case (Suc n)
  show thesis
  proof (rule assms(2))
    show v: "v = vCons (v $ 0) (vec n (λi. v $ Suc i))" (is "v = ?r")
    proof (rule eq_vecI, unfold dim_vec_vCons dim_vec Suc)
      fix i
      assume "i < Suc n"
      then show "v $ i = ?r $ i" by (cases i, auto simp: vCons_def)
    qed simp
  qed
qed

lemma vec_induct [case_names vNil vCons, induct type: vec]:
  assumes "P vNil" and "⋀a v. P v ⟹ P (vCons a v)"
  shows "P v"
proof (induct "dim_vec v" arbitrary:v)
  case 0 then show ?case by (cases v, auto intro: assms(1))
next
  case (Suc n) then show ?case by (cases v, auto intro: assms(2))
qed

lemma carrier_vec_induct [consumes 1, case_names 0 Suc, induct set:carrier_vec]:
  assumes v: "v ∈ carrier_vec n"
    and 1: "P 0 vNil" and 2: "⋀n a v. v ∈ carrier_vec n ⟹ P n v ⟹ P (Suc n) (vCons a v)"
  shows "P n v"
proof (insert v, induct n arbitrary: v)
  case 0 then have "v = vec 0 ((!) [])" by auto
  with 1 show ?case by auto
next
  case (Suc n) then show ?case by (cases v, auto dest!: carrier_vecD intro:2)
qed

lemma vec_of_list_Cons[simp]: "vec_of_list (a#as) = vCons a (vec_of_list as)"
  by (unfold vCons_def, transfer, auto simp:mk_vec_def split:nat.split)

lemma vec_of_list_Nil[simp]: "vec_of_list [] = vNil"
  by (transfer', auto)

lemma scalar_prod_vCons[simp]:
  "vCons a v ∙ vCons b w = a * b + v ∙ w"
  apply (unfold scalar_prod_def atLeast0_lessThan_Suc_eq_insert_0 dim_vec_vCons)
  apply (subst sum.insert) apply (simp,simp)
  apply (subst sum.reindex) apply force
  apply simp
  done

lemma zero_vec_Suc: "0⇩v (Suc n) = vCons 0 (0⇩v n)"
  by (auto simp: zero_vec_def vec_Suc o_def)

lemma zero_vec_zero[simp]: "0⇩v 0 = vNil" by auto

lemma vCons_eq_vCons[simp]: "vCons a v = vCons b w ⟷ a = b ∧ v = w" (is "?l ⟷ ?r")
proof
  assume ?l
  note arg_cong[OF this]
  from this[of dim_vec] this[of "λx. x$0"] this[of "λx. x$Suc _"]
  show ?r by (auto simp: vec_eq_iff)
qed simp

lemma vec_carrier_vec[simp]: "vec n f ∈ carrier_vec m ⟷ n = m"
  unfolding carrier_vec_def by auto

notation transpose_mat ("(_⇧T)" [1000])

lemma map_mat_transpose: "(map_mat f A)⇧T = map_mat f A⇧T" by auto

lemma cols_transpose[simp]: "cols A⇧T = rows A" unfolding cols_def rows_def by auto
lemma rows_transpose[simp]: "rows A⇧T = cols A" unfolding cols_def rows_def by auto
lemma list_of_vec_vec [simp]: "list_of_vec (vec n f) = map f [0..<n]"
  by (transfer, auto simp: mk_vec_def)

lemma list_of_vec_0 [simp]: "list_of_vec (0⇩v n) = replicate n 0"
  by (simp add: zero_vec_def map_replicate_trivial)

lemma diag_mat_map:
  assumes M_carrier: "M ∈ carrier_mat n n"
  shows "diag_mat (map_mat f M) = map f (diag_mat M)"
proof -
  have dim_eq: "dim_row M = dim_col M" using M_carrier by auto
  have m: "map_mat f M $$ (i, i) = f (M $$ (i, i))" if i: "i < dim_row M" for i
    using dim_eq i by auto
  show ?thesis
    by (rule nth_equalityI, insert m, auto simp add: diag_mat_def M_carrier)
qed

lemma mat_of_rows_map [simp]:
  assumes x: "set vs ⊆ carrier_vec n"
  shows "mat_of_rows n (map (map_vec f) vs) = map_mat f (mat_of_rows n vs)"
proof-
  have "∀x∈set vs. dim_vec x = n" using x by auto
  then show ?thesis by (auto simp add: mat_eq_iff map_vec_def mat_of_rows_def)
qed

lemma mat_of_cols_map [simp]:
  assumes x: "set vs ⊆ carrier_vec n"
  shows "mat_of_cols n (map (map_vec f) vs) = map_mat f (mat_of_cols n vs)"
proof-
  have "∀x∈set vs. dim_vec x = n" using x by auto
  then show ?thesis by (auto simp add: mat_eq_iff map_vec_def mat_of_cols_def)
qed

lemma vec_of_list_map [simp]: "vec_of_list (map f xs) = map_vec f (vec_of_list xs)"
  unfolding map_vec_def by (transfer, auto simp add: mk_vec_def)

lemma map_vec: "map_vec f (vec n g) = vec n (f o g)" by auto

lemma mat_of_cols_Cons_index_0: "i < n ⟹ mat_of_cols n (w # ws) $$ (i, 0) = w $ i"
  by (unfold mat_of_cols_def, transfer', auto simp: mk_mat_def)

lemma nth_map_out_of_bound: "i ≥ length xs ⟹ map f xs ! i = [] ! (i - length xs)"
  by (induct xs arbitrary:i, auto)

lemma mat_of_cols_Cons_index_Suc:
  "i < n ⟹ mat_of_cols n (w # ws) $$ (i, Suc j) = mat_of_cols n ws $$ (i,j)"
  by (unfold mat_of_cols_def, transfer, auto simp: mk_mat_def undef_mat_def nth_append nth_map_out_of_bound)

lemma mat_of_cols_index: "i < n ⟹ j < length ws ⟹ mat_of_cols n ws $$ (i,j) = ws ! j $ i"
  by (unfold mat_of_cols_def, auto)

lemma mat_of_rows_index: "i < length rs ⟹ j < n ⟹ mat_of_rows n rs $$ (i,j) = rs ! i $ j"
  by (unfold mat_of_rows_def, auto)

lemma transpose_mat_of_rows: "(mat_of_rows n vs)⇧T = mat_of_cols n vs"
  by (auto intro!: eq_matI simp: mat_of_rows_index mat_of_cols_index)

lemma transpose_mat_of_cols: "(mat_of_cols n vs)⇧T = mat_of_rows n vs"
  by (auto intro!: eq_matI simp: mat_of_rows_index mat_of_cols_index)

lemma nth_list_of_vec [simp]:
  assumes "i < dim_vec v" shows "list_of_vec v ! i = v $ i"
  using assms by (transfer, auto)

lemma length_list_of_vec [simp]:
  "length (list_of_vec v) = dim_vec v" by (transfer, auto)

lemma vec_eq_0_iff:
  "v = 0⇩v n ⟷ n = dim_vec v ∧ (n = 0 ∨ set (list_of_vec v) = {0})" (is "?l ⟷ ?r")
proof
  show "?l ⟹ ?r" by auto
  show "?r ⟹ ?l" by (intro iffI eq_vecI, force simp: set_conv_nth, force)
qed

lemma list_of_vec_vCons[simp]: "list_of_vec (vCons a v) = a # list_of_vec v" (is "?l = ?r")
proof (intro nth_equalityI)
  fix i
  assume "i < length ?l"
  then show "?l ! i = ?r ! i" by (cases i, auto)
qed simp

lemma append_vec_vCons[simp]: "vCons a v @⇩v w = vCons a (v @⇩v w)" (is "?l = ?r")
proof (unfold vec_eq_iff, intro conjI allI impI)
  fix i assume "i < dim_vec ?r"
  then show "?l $ i = ?r $ i" by (cases i; subst index_append_vec, auto)
qed simp

lemma append_vec_vNil[simp]: "vNil @⇩v v = v"
  by (unfold vec_eq_iff, auto)

lemma list_of_vec_append[simp]: "list_of_vec (v @⇩v w) = list_of_vec v @ list_of_vec w"
  by (induct v, auto)

lemma transpose_mat_eq[simp]: "A⇧T = B⇧T ⟷ A = B"
  using transpose_transpose by metis

lemma mat_col_eqI: assumes cols: "⋀ i. i < dim_col B ⟹ col A i = col B i"
  and dims: "dim_row A = dim_row B" "dim_col A = dim_col B"
shows "A = B"
  by(subst transpose_mat_eq[symmetric], rule eq_rowI,insert assms,auto)

lemma upper_triangular_imp_distinct:
  assumes A: "A ∈ carrier_mat n n"
    and tri: "upper_triangular A"
    and diag: "0 ∉ set (diag_mat A)"
  shows "distinct (rows A)"
proof-
  { fix i and j
    assume eq: "rows A ! i = rows A ! j" and ij: "i < j" and jn: "j < n"
    from tri A ij jn have "rows A ! j $ i = 0" by (auto dest!:upper_triangularD)
    with eq have "rows A ! i $ i = 0" by auto
    with diag ij jn A have False by (auto simp: diag_mat_def)
  }
  with A show ?thesis by (force simp: distinct_conv_nth nat_neq_iff)
qed

lemma dim_vec_of_list[simp] :"dim_vec (vec_of_list as) = length as" by transfer auto

lemma list_vec: "list_of_vec (vec_of_list xs) = xs"
by (transfer, metis (mono_tags, lifting) atLeastLessThan_iff map_eq_conv map_nth mk_vec_def old.prod.case set_upt)

lemma vec_list: "vec_of_list (list_of_vec v) = v"
apply transfer unfolding mk_vec_def by auto

lemma index_vec_of_list: "i<length xs ⟹ (vec_of_list xs) $ i = xs ! i"
by (metis vec.abs_eq index_vec vec_of_list.abs_eq)

lemma vec_of_list_index: "vec_of_list xs $ j = xs ! j"
  apply transfer unfolding mk_vec_def unfolding undef_vec_def
  by (simp, metis append_Nil2 nth_append)

lemma list_of_vec_index: "list_of_vec v ! j = v $ j"
  by (metis vec_list vec_of_list_index)

lemma list_of_vec_map: "list_of_vec xs = map (($) xs) [0..<dim_vec xs]" by transfer auto

definition "component_mult v w = vec (min (dim_vec v) (dim_vec w)) (λi. v $ i * w $ i)"

definition vec_set::"'a vec ⇒ 'a set" ("set⇩v")
  where "vec_set v = vec_index v ` {..<dim_vec v}"

lemma vec_set_map[simp]: "set⇩v (map_vec f v) = f ` set⇩v v" 
  unfolding vec_set_def by auto

lemma index_component_mult:
assumes "i < dim_vec v" "i < dim_vec w"
shows "component_mult v w $ i = v $ i * w $ i"
  unfolding component_mult_def using assms index_vec by auto

lemma dim_component_mult:
"dim_vec (component_mult v w) = min (dim_vec v) (dim_vec w)"
  unfolding component_mult_def using index_vec by auto

lemma vec_setE:
assumes "a ∈ set⇩v v"
obtains i where "v$i = a" "i<dim_vec v" using assms unfolding vec_set_def by blast

lemma vec_setI:
assumes "v$i = a" "i<dim_vec v"
shows "a ∈ set⇩v v" using assms unfolding vec_set_def using image_eqI lessThan_iff by blast

lemma set_list_of_vec: "set (list_of_vec v) = set⇩v v" unfolding vec_set_def by transfer auto


instantiation vec :: (conjugate) conjugate
begin

definition conjugate_vec :: "'a :: conjugate vec ⇒ 'a vec"
  where "conjugate v = vec (dim_vec v) (λi. conjugate (v $ i))"

lemma conjugate_vCons [simp]:
  "conjugate (vCons a v) = vCons (conjugate a) (conjugate v)"
  by (auto simp: vec_Suc conjugate_vec_def)

lemma dim_vec_conjugate[simp]: "dim_vec (conjugate v) = dim_vec v"
  unfolding conjugate_vec_def by auto

lemma carrier_vec_conjugate[simp]: "v ∈ carrier_vec n ⟹ conjugate v ∈ carrier_vec n"
  by (auto intro!: carrier_vecI)

lemma vec_index_conjugate[simp]:
  shows "i < dim_vec v ⟹ conjugate v $ i = conjugate (v $ i)"
  unfolding conjugate_vec_def by auto

instance
proof
  fix v w :: "'a vec"
  show "conjugate (conjugate v) = v" by (induct v, auto simp: conjugate_vec_def)
  let ?v = "conjugate v"
  let ?w = "conjugate w"
  show "conjugate v = conjugate w ⟷ v = w"
  proof(rule iffI)
    assume cvw: "?v = ?w" show "v = w"
    proof(rule)
      have "dim_vec ?v = dim_vec ?w" using cvw by auto
      then show dim: "dim_vec v = dim_vec w" by simp
      fix i assume i: "i < dim_vec w"
      then have "conjugate v $ i = conjugate w $ i" using cvw by auto
      then have "conjugate (v$i) = conjugate (w $ i)" using i dim by auto
      then show "v $ i = w $ i" by auto
    qed
  qed auto
qed

end

lemma conjugate_add_vec:
  fixes v w :: "'a :: conjugatable_ring vec"
  assumes dim: "v : carrier_vec n" "w : carrier_vec n"
  shows "conjugate (v + w) = conjugate v + conjugate w"
  by (rule, insert dim, auto simp: conjugate_dist_add)

lemma uminus_conjugate_vec:
  fixes v w :: "'a :: conjugatable_ring vec"
  shows "- (conjugate v) = conjugate (- v)"
  by (rule, auto simp:conjugate_neg)

lemma conjugate_zero_vec[simp]:
  "conjugate (0⇩v n :: 'a :: conjugatable_ring vec) = 0⇩v n" by auto

lemma conjugate_vec_0[simp]:
  "conjugate (vec 0 f) = vec 0 f" by auto

lemma sprod_vec_0[simp]: "v ∙ vec 0 f = 0"
  by(auto simp: scalar_prod_def)

lemma conjugate_zero_iff_vec[simp]:
  fixes v :: "'a :: conjugatable_ring vec"
  shows "conjugate v = 0⇩v n ⟷ v = 0⇩v n"
  using conjugate_cancel_iff[of _ "0⇩v n :: 'a vec"] by auto

lemma conjugate_smult_vec:
  fixes k :: "'a :: conjugatable_ring"
  shows "conjugate (k ⋅⇩v v) = conjugate k ⋅⇩v conjugate v"
  using conjugate_dist_mul by (intro eq_vecI, auto)

lemma conjugate_sprod_vec:
  fixes v w :: "'a :: conjugatable_ring vec"
  assumes v: "v : carrier_vec n" and w: "w : carrier_vec n"
  shows "conjugate (v ∙ w) = conjugate v ∙ conjugate w"
proof (insert w v, induct w arbitrary: v rule:carrier_vec_induct)
  case 0 then show ?case by (cases v, auto)
next
  case (Suc n b w) then show ?case
    by (cases v, auto dest: carrier_vecD simp:conjugate_dist_add conjugate_dist_mul)
qed 

abbreviation cscalar_prod :: "'a vec ⇒ 'a vec ⇒ 'a :: conjugatable_ring" (infix "∙c" 70)
  where "(∙c) ≡ λv w. v ∙ conjugate w"

lemma conjugate_conjugate_sprod[simp]:
  assumes v[simp]: "v : carrier_vec n" and w[simp]: "w : carrier_vec n"
  shows "conjugate (conjugate v ∙ w) = v ∙c w"
  apply (subst conjugate_sprod_vec[of _ n]) by auto

lemma conjugate_vec_sprod_comm:
  fixes v w :: "'a :: {conjugatable_ring, comm_ring} vec"
  assumes "v : carrier_vec n" and "w : carrier_vec n"
  shows "v ∙c w = (conjugate w ∙ v)"
  unfolding scalar_prod_def using assms by(subst sum.ivl_cong, auto simp: ac_simps)

lemma conjugate_square_ge_0_vec[intro!]:
  fixes v :: "'a :: conjugatable_ordered_ring vec"
  shows "v ∙c v ≥ 0"
proof (induct v)
  case vNil
  then show ?case by auto
next
  case (vCons a v)
  then show ?case using conjugate_square_positive[of a] by auto
qed

lemma conjugate_square_eq_0_vec[simp]:
  fixes v :: "'a :: {conjugatable_ordered_ring,semiring_no_zero_divisors} vec"
  assumes "v ∈ carrier_vec n"
  shows "v ∙c v = 0 ⟷ v = 0⇩v n"
proof (insert assms, induct rule: carrier_vec_induct)
  case 0
  then show ?case by auto
next
  case (Suc n a v)
  then show ?case
    using conjugate_square_positive[of a] conjugate_square_ge_0_vec[of v]
    by (auto simp: le_less add_nonneg_eq_0_iff zero_vec_Suc)
qed

lemma conjugate_square_greater_0_vec[simp]:
  fixes v :: "'a :: {conjugatable_ordered_ring,semiring_no_zero_divisors} vec"
  assumes "v ∈ carrier_vec n"
  shows "v ∙c v > 0 ⟷ v ≠ 0⇩v n"
  using assms by (auto simp: less_le)

lemma vec_conjugate_rat[simp]: "(conjugate :: rat vec ⇒ rat vec) = (λx. x)" by force
lemma vec_conjugate_real[simp]: "(conjugate :: real vec ⇒ real vec) = (λx. x)" by force


end