# Theory More_Jordan_Normal_Forms

theory More_Jordan_Normal_Forms
imports Matrix_Impl
```theory More_Jordan_Normal_Forms
imports
Jordan_Normal_Form.Matrix_Impl
begin

lemma set_comprehension_list_comprehension:
"set [f i . i <- [x..<a]] = {f i |i. i ∈ {x..<a}}"
by (simp) (fastforce)

lemma in_second_append_list: "i≥ length a ⟹ i < length (a@b) ⟹ (a@b)!i ∈ set b"
by (metis diff_add_inverse diff_less_mono in_set_conv_nth leD length_append nth_append)

section ‹ General Theorems used later, that could be moved ›

lemma split_four_block_dual_fst_lst:
assumes "split_block (four_block_mat A B C D) (dim_row A) (dim_col A) = (U, X, Y, V)"
shows "U = A" "V = D"
proof -
define nr where nr: "nr = dim_row (four_block_mat A B C D)"
define nc where nc: "nc = dim_col (four_block_mat A B C D)"
define nr2 where nr2: "nr2 = nr - dim_row A"
define nc2 where nc2: "nc2 = nc - dim_col A"
define A1 where A1: "A1 = mat (dim_row A) (dim_col A) ((\$\$) (four_block_mat A B C D))"
define A2 where A2: "A2 = mat (dim_row A) nc2 (λ(i, j). (four_block_mat A B C D) \$\$ (i, j + dim_col A))"
define A3 where A3: "A3 = mat nr2 (dim_col A) (λ(i, j). (four_block_mat A B C D) \$\$ (i + dim_row A, j))"
define A4 where A4: "A4 = mat nr2 nc2 (λ(i, j). (four_block_mat A B C D) \$\$ (i + dim_row A, j + dim_col A))"
have g: "split_block (four_block_mat A B C D) (dim_row A) (dim_col A) = (A1, A2, A3, A4)"
using split_block_def[of "(four_block_mat A B C D)" "(dim_row A)" "(dim_col A)"]
by (metis A1 A2 A3 A4 nc nc2 nr nr2)
have D: "D = A4"
using A4 by (auto) (standard, (simp add:  nr nr2 nc nc2)+)
have "A = A1"
using A1 by auto
then have "split_block (four_block_mat A B C D) (dim_row A) (dim_col A) = (A, A2, A3, D)"
using D g by blast
also show "U = A"
using assms calculation by auto
ultimately show "V = D"
using assms by auto
qed

lemma append_split_vec_distrib_scalar_prod:
assumes "dim_vec (u @⇩v w) = dim_vec x"
shows "(u @⇩v w) ∙ x = u ∙ (vec_first x (dim_vec u)) + w ∙ (vec_last x (dim_vec w))"
proof -
have "(u @⇩v w) ∙ (vec_first x (dim_vec u) @⇩v vec_last x (dim_vec w)) =
u ∙ vec_first x (dim_vec u) + w ∙ vec_last x (dim_vec w)"
by (meson carrier_vec_dim_vec scalar_prod_append vec_first_carrier vec_last_carrier)
then show ?thesis
by (metis assms carrier_vec_dim_vec index_append_vec(2) vec_first_last_append)
qed

lemma append_dot_product_split:
assumes "dim_vec (u @⇩v w) = dim_vec x"
shows "(u @⇩v w) ∙ x = (∑i∈{0..< dim_vec u}. u\$i * x\$i) + (∑i∈{0..< dim_vec w}. w\$i * x\$(i + dim_vec u))"
proof -
define ix where "ix = vec_first x (dim_vec u)"
define lx where lx: "lx = vec_last x (dim_vec w)"
have *: "(u @⇩v w) ∙ x = u ∙ ix + w ∙ lx"
using append_split_vec_distrib_scalar_prod ix_def lx assms by blast
have "(u @⇩v w) ∙ x = (∑ i ∈ {0 ..< dim_vec x}. (u @⇩v w) \$ i * x \$ i)"
using scalar_prod_def[of "(u @⇩v w)" x] by simp
also have "... = (∑ i ∈ {0 ..< dim_vec u}. (u @⇩v w) \$ i * x \$ i) +
(∑ i ∈ {dim_vec u ..< dim_vec (u @⇩v w)}. (u @⇩v w) \$ i * x \$ i)"
using assms sum.atLeastLessThan_concat[of "0" "dim_vec u" "dim_vec (u @⇩v w)"
"(λi. (u @⇩v w) \$ i * x \$ i)", OF le0[of "dim_vec u"]]
le_add1[of  "dim_vec u" "dim_vec w"] index_append_vec(2)[of u w] by simp
also have *: "... =(∑i∈{0..<dim_vec u}. u\$i * x\$i) + w ∙ lx"
using * calculation by (auto simp: ix_def scalar_prod_def vec_first_def)
have "w ∙ lx = (∑i∈{0..< dim_vec w}. w\$i * x\$(i + dim_vec u))" unfolding lx vec_last_def
unfolding scalar_prod_def using add_diff_cancel_right' index_append_vec(2)[of u w] by (auto)
(metis ‹dim_vec (u @⇩v w) = dim_vec u + dim_vec w› add.commute add_diff_cancel_right' assms)
then show ?thesis
using * calculation by auto
qed

lemma assoc_scalar_prod_mult_mat_vec:
fixes A :: "'a::comm_semiring_1 mat"
assumes "y ∈ carrier_vec n"
assumes "x ∈ carrier_vec m"
assumes "A ∈ carrier_mat n m"
shows "(A *⇩v x) ∙ y = (A⇧T *⇩v y) ∙ x"
proof -
have "(A *⇩v x) ∙ y = (∑ i ∈ {0 ..< n}. (A *⇩v x) \$ i * y \$ i)"
unfolding scalar_prod_def using assms(1) carrier_vecD by blast
also have "... = (∑ i ∈ {0 ..< n}. (vec (dim_row A) (λ i. row A i ∙ x)) \$ i * y \$ i)"
unfolding mult_mat_vec_def by blast
also have "... = (∑ i ∈ {0 ..< n}. (λ i. row A i ∙ x)  i * y \$ i)"
using assms(3) by auto
also have "... = (∑ i ∈ {0 ..< n}. (∑ j ∈ {0 ..< m}. (row A i) \$ j * x \$ j) * y \$ i)"
unfolding scalar_prod_def using assms(2) carrier_vecD by blast
also have "... = (∑ j ∈ {0 ..< n}. (∑ i ∈ {0 ..< m}. (row A j) \$ i * x \$ i * y \$ j))"
also have "... = (∑ j ∈ {0 ..< n}. (∑ i ∈ {0 ..< m}.  A \$\$ (j,i) * x \$ i * y \$ j))"
unfolding row_def using assms(3) by auto
also have "... = (∑ j ∈ {0 ..< n}. (∑ i ∈ {0 ..< m}.  A \$\$ (j,i) * y \$ j * x \$ i))"
by (meson semiring_normalization_rules(16) sum.cong)
also have "... = (∑ j ∈ {0 ..< n}. (∑ i ∈ {0 ..< m}. (col A i) \$ j * y \$ j * x \$ i))"
using assms(3) by auto
also have "... = (∑ i ∈ {0 ..< m}. (∑ j ∈ {0 ..< n}. (col A i) \$ j * y \$ j * x \$ i))"
"(λi j. (col A i) \$ j * y \$ j * x \$ i)" "{0..<n}" "{0 ..< m}", symmetric]
by simp
also have "... = (∑ i ∈ {0 ..< m}. (∑ j ∈ {0 ..< n}. (col A i) \$ j * y \$ j) * x \$ i)"
also have "... = (∑ i ∈ {0 ..< m}. (λ i. col A i ∙ y) i * x \$ i)"
unfolding scalar_prod_def using assms(1) carrier_vecD by blast
also have "... = (∑ i ∈ {0 ..< m}. (λ i. row A⇧T i ∙ y) i * x \$ i)"
using assms(3) by auto
also have "... = (∑ i ∈ {0 ..< m}. (vec (dim_row A⇧T) (λ i. row A⇧T i ∙ y)) \$ i * x \$ i)"
using assms by auto
also have "... = (∑ i ∈ {0 ..< m}. (A⇧T *⇩v y) \$ i * x \$ i)"
using assms by auto
also have "... = (A⇧T *⇩v y) ∙ x"
using scalar_prod_def[of "(A⇧T *⇩v y)" x,symmetric] using assms(2) carrier_vecD by blast
finally show ?thesis .
qed

section ‹ Vectors ›

abbreviation singletonV ("[_]⇩v" ) where "singletonV e ≡ (vec 1 (λi. e))"

lemma elem_in_singleton [simp]: "[a]⇩v \$ 0 = a"
by simp

lemma elem_in_singleton_append [simp]: "(x @⇩v [a]⇩v) \$ dim_vec x = a"
by simp

lemma vector_cases_append:
fixes x :: "'a vec"
shows "x = vNil ∨ (∃v a. x = v @⇩v [a]⇩v)"
proof -
have "x ≠ vNil ⟹ (∃v a. x = v @⇩v [a]⇩v)"
proof (rule ccontr)
assume a1: "x ≠ vNil"
assume na: "¬ (∃v a. x = v @⇩v [a]⇩v)"
have "dim_vec x ≥ 1"
using a1 eq_vecI by auto
define v where v: "v = vec (dim_vec x - 1) (λi. x \$ i)"
have v': "∀i < dim_vec v. v \$ i = x \$ i"
using v by auto
define a where a: "a = x \$ (dim_vec x - 1)"
have a': "[a]⇩v \$ 0 = a" by simp
have ff1: "1 + dim_vec v = dim_vec x"
by (metis (no_types) ‹1 ≤ dim_vec x› add_diff_cancel_left' dim_vec le_Suc_ex v)
have "∀i < dim_vec x. x\$i = (v @⇩v [a]⇩v)\$i"
proof (standard,standard)
fix i :: nat
assume as: "i < dim_vec x"
have "x \$ dim_vec v = a"
then have "x \$ i = (v @⇩v [a]⇩v) \$ i"
using ff1 as by (metis (no_types) One_nat_def a' add.left_neutral
dim_vec index_append_vec(1) less_Suc_eq v')
then show "x\$i = (v @⇩v [a]⇩v)\$i"
by blast
qed
then have "x = v @⇩v [a]⇩v"
using a a' v v'
by (metis dim_vec eq_vecI ff1 index_append_vec(2) semiring_normalization_rules(24))
then show False using na by auto
qed
then show ?thesis
by blast
qed

lemma vec_rev_induct [case_names vNil append, induct type: vec]:
assumes "P vNil" and "⋀a v. P v ⟹ P (v @⇩v [a]⇩v)"
shows "P v"
proof (induction "dim_vec v" arbitrary: v)
case 0
then have "v = vNil"
by auto
then show ?case
using assms(1) by auto
next
case (Suc l)
obtain xs x where xs_x: "v = xs @⇩v [x]⇩v"
using vector_cases_append[of v] Suc.hyps(2) dim_vec by (auto)
have "l = dim_vec xs"
using Suc.hyps(2) xs_x by auto
then have "P xs"
using Suc.hyps(1)[of xs] by auto
then have "P (xs @⇩v [x]⇩v)"
using assms(2)[of xs x] by auto
then show ?case
qed

lemma singleton_append_dotP:
assumes "dim_vec z = dim_vec y + 1"
shows "(y @⇩v [x]⇩v) ∙ z = (∑i∈{0..<dim_vec y}. y \$ i * z \$ i) + x * z \$ dim_vec y"
proof -
have "(y @⇩v [x]⇩v) ∙ z = (∑i∈{0..<dim_vec z}. (y @⇩v [x]⇩v) \$ i * z \$ i)"
unfolding scalar_prod_def by blast
also have "... = (∑i∈{0..<dim_vec z-1}. (y @⇩v [x]⇩v) \$ i * z \$ i) +
(y @⇩v [x]⇩v)\$(dim_vec z-1) * z\$(dim_vec z-1)"
also have "... = (∑i∈{0..<dim_vec y}. (y @⇩v [x]⇩v) \$ i * z \$ i) +
(y @⇩v [x]⇩v)\$(dim_vec y)* z\$(dim_vec y)"
using assms by auto
also have "... = (∑i∈{0..<dim_vec y}. y \$ i * z \$ i) +
x * z\$(dim_vec y)"
by simp
finally show ?thesis .
qed

lemma map_vec_append: "map_vec f (a @⇩v b) = map_vec f a @⇩v map_vec f b"
by (induction a arbitrary: b) (auto)

lemma map_mat_map_vec:
assumes "i < dim_row P"
shows "row (map_mat f P) i = map_vec f (row P i)"
using assms by auto

lemma append_rows_access1 [simp]:
assumes "i < dim_row A"
assumes "dim_col A = dim_col B"
shows "row (A @⇩r B) i = row A i"
proof
show "dim_vec (Matrix.row (A @⇩r B) i) = dim_vec (Matrix.row A i)"
fix ia
assume "ia < dim_vec (row A i)"
have "row (A @⇩r B) i = (row A i @⇩v row (0⇩m (dim_row A) 0) i)"
unfolding append_rows_def using
carrier_mat_triv[of A] row_four_block_mat(1)[of A "dim_row A"
_ "0⇩m (dim_row A) 0" 0 B "dim_row B" "0⇩m (dim_row B) 0" i, OF _ _ _ _ assms(1)]
by (metis assms(2) carrier_mat_triv zero_carrier_mat)
also have "... = row A i @⇩v vNil"
also have "... = row A i"
by auto
finally show "row (A @⇩r B) i \$ ia = row A i \$ ia"
by auto
qed

lemma append_rows_access2 [simp]:
assumes "i ≥ dim_row A"
assumes "i < dim_row A + dim_row B"
assumes "dim_col A = dim_col B"
shows "row (A @⇩r B) i = row B (i - dim_row A)"
proof
show "dim_vec (row (A @⇩r B) i) = dim_vec (row B (i - dim_row A))"
fix ia
assume "ia < dim_vec (row B (i - dim_row A))"
have "row (A @⇩r B) i = (row B (i - dim_row A) @⇩v row (0⇩m (dim_row B) 0) (i - dim_row A))"
unfolding append_rows_def using carrier_mat_triv[of A] row_four_block_mat(2)[of A "dim_row A"
_ "0⇩m (dim_row A) 0" 0 B "dim_row B" "0⇩m (dim_row B) 0" i, OF _ _ _ _ _ assms(2)]
by (metis assms(1) assms(3) carrier_mat_triv le_antisym less_imp_le_nat nat_less_le zero_carrier_mat)
also have "... = row B (i - dim_row A) @⇩v vNil"
by fastforce
also have "... = row B (i - dim_row A)"
by auto
finally show "row (A @⇩r B) i \$ ia = row B (i - dim_row A) \$ ia"
by auto
qed

lemma append_singleton_access [simp]: "(Matrix.vec n f @⇩v [r]⇩v) \$ n = r"
by simp

text ‹ Move to right place ›

fun mat_append_col where
"mat_append_col A b = mat_of_cols (dim_row A) (cols A @ [b])"

fun mat_append_row where
"mat_append_row A c = mat_of_rows (dim_col A) (rows A @ [c])"

lemma mat_append_col_dims:
shows "mat_append_col A b ∈ carrier_mat (dim_row A) (dim_col A + 1)"
by auto

lemma mat_append_row_dims:
shows "mat_append_row A c ∈ carrier_mat (dim_row A + 1) (dim_col A)"
by auto

lemma mat_append_col_col:
assumes "dim_row A = dim_vec b"
shows "col (mat_append_col A b) (dim_col A) = b"
proof (standard)
let ?nA = "(mat_of_cols (dim_row A) (cols A @ [b]))"
show "dim_vec (col (mat_append_col A b) (dim_col A)) = dim_vec b"
fix i
assume "i < dim_vec b"
have "col (mat_append_col A b) (dim_col A) \$ i = vec_index (vec (dim_row ?nA) (λ i. ?nA \$\$ (i, (dim_col A)))) i"
also have "... = vec_index (vec (dim_row A) (λ i. ?nA \$\$ (i, (dim_col A)))) i"
by auto
also have "... = vec_index ((cols A @ [b]) ! dim_col A) i"
by (simp add: ‹i < dim_vec b› assms mat_of_cols_index)
also have "... = vec_index b i"
by (metis cols_length nth_append_length)
finally show "col (mat_append_col A b) (dim_col A) \$ i = b \$ i" .
qed

lemma mat_append_col_vec_index:
assumes "i < dim_row A"
and "dim_row A = dim_vec b"
shows "(row (mat_append_col A b) i) \$ (dim_col A) = b \$ i"
using mat_append_col_col
by (metis (no_types, lifting) One_nat_def add_Suc_right assms(1) assms(2) carrier_matD(2)
col_def dim_row_mat(1) index_row(1) index_vec lessI mat_append_col.simps
mat_append_col_dims mat_of_cols_def semiring_norm(51))

lemma mat_append_row_row:
assumes "dim_col A = dim_vec c"
shows "row (mat_append_row A c) (dim_row A) = c"
proof
let ?nA = "(mat_of_rows (dim_col A) (Matrix.rows A @ [c]))"
show "dim_vec (Matrix.row (mat_append_row A c) (dim_row A)) = dim_vec c"
using assms by simp
fix i assume "i < dim_vec c"
from mat_append_row.simps[of A c]
have "row (mat_append_row A c) (dim_row A) \$ i = vec_index (row ?nA (dim_row A)) i"
by auto
also have "... = vec_index (vec (dim_col ?nA) (λ j. ?nA \$\$ (dim_row A,j))) i"
also have "... =  vec_index ((rows A @ [c]) ! dim_row A) i"
by (metis (mono_tags, lifting) ‹mat_append_row A c = mat_of_rows (dim_col A) (Matrix.rows A @ [c])›
add_Suc_right append_Nil2 assms calculation carrier_matD(1) col_transpose cols_transpose
index_transpose_mat(2) index_transpose_mat(3) length_append length_rows lessI list.size(3)
mat_append_col.elims mat_append_col_col mat_append_row_dims nth_append_length
transpose_mat_of_rows One_nat_def)
also have "... = vec_index c i"
by (metis length_rows nth_append_length)
finally show "Matrix.row (mat_append_row A c) (dim_row A) \$ i = c \$ i" .
qed

lemma mat_append_row_in_mat:
assumes "i < dim_row A"
shows "row (mat_append_row A r) i = row A i"
by (auto) (metis assms le_imp_less_Suc length_append_singleton
length_rows mat_of_rows_row nat_less_le nth_append nth_rows row_carrier)

lemma mat_append_row_vec_index:
assumes "i < dim_col A"
and "dim_col A = dim_vec b"
shows "vec_index (col (mat_append_row A b) i) (dim_row A) = vec_index b i"
carrier_matD(2) index_col index_row(1) lessI mat_append_row_dims mat_append_row_row)

lemma mat_append_col_access_in_mat:
assumes "dim_row A = dim_vec b"
and "i < dim_row A"
and "j < dim_col A"
shows "(row (mat_append_col A b) i) \$ j = (row A i) \$ j"
using Matrix.row_transpose[of j A, OF assms(3)]
Matrix.transpose_transpose[of "(mat_append_col A b)"] assms carrier_matD(1)
carrier_matD(2) cols_length cols_transpose index_col index_row(1)[of i "mat_append_col A b" j] index_transpose_mat(2)
mat_append_col.simps mat_append_col_dims
mat_of_cols_carrier(3) mat_of_rows_row
mat_of_cols_index
by (smt cols_nth index_row(1))

lemma constructing_append_col_row:
assumes "i < dim_row A"
and "dim_row A = dim_vec b"
shows "row (mat_append_col A b) i = row A i @⇩v [vec_index b i]⇩v"
proof
show 1: "dim_vec (Matrix.row (mat_append_col A b) i) = dim_vec (Matrix.row A i @⇩v [b \$ i]⇩v)"
by simp
fix ia
assume a: "ia < dim_vec (Matrix.row A i @⇩v [b \$ i]⇩v)"
consider "ia = dim_col A" | "ia < dim_col A"
using a less_SucE by auto
then show "row (mat_append_col A b) i \$ ia = (Matrix.row A i @⇩v [b \$ i]⇩v) \$ ia "
proof (cases)
case 1
then show ?thesis
using mat_append_col_vec_index[of i A b, OF assms] by auto
next
case 2
have "row (mat_append_col A b) i \$ ia = (mat_append_col A b) \$\$ (i, ia)"
using a assms(1) by auto
then show ?thesis using mat_append_col_access_in_mat[of A b i ia, OF assms(2) assms(1) 2]
using "2" by auto
qed
qed

definition one_element_vec where "one_element_vec n e = vec n (λi. e)"

lemma one_element_vec_carrier: "one_element_vec n e ∈ carrier_vec n"
unfolding one_element_vec_def by auto

lemma one_element_vec_dim [simp]: "dim_vec (one_element_vec n (r::rat)) = n"

lemma one_element_vec_access [simp]: "⋀i. i < n ⟹ vec_index (one_element_vec n e) i = e"
unfolding one_element_vec_def by (auto)

fun single_nz_val where "single_nz_val n i v = vec n (λj. (if i = j then v else 0))"

lemma single_nz_val_carrier: "single_nz_val n i v ∈ carrier_vec n"
by auto

lemma single_nz_val_access1 [simp]: "i < n ⟹ single_nz_val n i v \$ i = v"
by auto

lemma single_nz_val_access2 [simp]: "i < n ⟹ j < n ⟹ i ≠ j⟹ single_nz_val n i v \$ j = 0"
by (auto)

lemma "i < n ⟹ (v ⋅⇩v unit_vec n i) \$ i = (v::'a::{monoid_mult,times,zero_neq_one})"
by(auto)

lemma single_nz_val_unit_vec:
fixes v::"'a::{monoid_mult,times,zero_neq_one,mult_zero}"
shows "v ⋅⇩v (unit_vec n i) = single_nz_val n i v"
proof
show *: "dim_vec (v ⋅⇩v unit_vec n i) = dim_vec (single_nz_val n i v)"
by (simp)
fix ia
assume "ia < dim_vec (single_nz_val n i v)"
then show "(v ⋅⇩v unit_vec n i) \$ ia = single_nz_val n i v \$ ia"
using * by (simp add: unit_vec_def)
qed

lemma single_nz_valI [intro]:
fixes v i val
assumes "⋀j. j < dim_vec v ⟹ j ≠ i ⟹ v\$j = 0"
assumes "v\$i = val"
shows "v = single_nz_val (dim_vec v) i val"
using assms(1) assms(2) by auto

lemma single_nz_val_dotP:
assumes "i < n"
assumes "dim_vec x = n"
shows "single_nz_val n i v ∙ x = v * x \$ i"
proof -
let ?y = "single_nz_val n i v"
have "single_nz_val n i v ∙ x = (∑i∈{0 ..< dim_vec x}. ?y \$ i * x \$ i)"
unfolding scalar_prod_def by auto
also have "... = (∑i∈{0 ..< dim_vec x}-{i}. ?y \$ i * x \$ i) + ?y \$ i * x \$ i"
by (metis (no_types, lifting) add.commute assms(1) assms(2) atLeast0LessThan
finite_atLeastLessThan lessThan_iff sum.remove)
also have "... = (∑i∈{0 ..< dim_vec x}-{i}. ?y \$ i * x \$ i) + v * x \$ i"
also have "... = v * x \$ i"
proof -
have "⋀j. j ∈ {0 ..< dim_vec x}-{i} ⟹ ?y \$ j * x \$ j = 0"
then have "(∑i∈{0 ..< dim_vec x}-{i}. ?y \$ i * x \$ i) = 0" by auto
then show ?thesis by auto
qed
finally show ?thesis .
qed

lemma single_nz_zero_singleton: "single_nz_val 1 0 v = [v]⇩v"
by (auto)

lemma append_one_elem_zero_dotP:
assumes "dim_vec u = m"
and "dim_vec x = n"
shows "(one_element_vec n e @⇩v (0⇩v m)) ∙ (x @⇩v u) = (∑i∈{0 ..< dim_vec x}. e * x \$ i)"
proof -
let ?OEV = "one_element_vec n e"
have "dim_vec (?OEV @⇩v (0⇩v m)) = dim_vec (x @⇩v u)"
by (simp add: assms(1) assms(2) one_element_vec_carrier)
have "(one_element_vec n e @⇩v 0⇩v m) ∙ (x @⇩v u) = one_element_vec n e ∙ x + 0⇩v m ∙ u"
using scalar_prod_append[of ?OEV _ "0⇩v m" _ x u] assms
by (meson carrier_vec_dim_vec one_element_vec_carrier zero_carrier_vec)
also have "... = (∑i∈{0..<dim_vec x}. ?OEV \$ i * x \$ i) + (∑i∈{0..<dim_vec u}. (0⇩v m)\$i * u\$i)"
unfolding scalar_prod_def by blast
also have "... = (∑i∈{0..<dim_vec x}. ?OEV \$ i * x \$ i)"
using assms(1) by auto
also have "... = (∑i∈{0..<dim_vec x}. e * x \$ i)"
using assms(2) by auto
finally show ?thesis .
qed

lemma one_element_vec_dotP:
assumes "dim_vec x = n"
shows "(one_element_vec n e) ∙ x = (∑i∈{0 ..< dim_vec x}. e * x \$ i)"
by (metis (no_types, lifting) assms one_element_vec_access scalar_prod_def sum.ivl_cong)

lemma singleton_dotP [simp]: "dim_vec x = 1 ⟹ [v]⇩v ∙ x = v * x\$0"
by (metis dim_vec index_vec less_one single_nz_valI single_nz_val_dotP)

lemma singletons_dotP [simp]: "[v]⇩v ∙ [w]⇩v = v * w"
by (metis dim_vec index_vec less_one singleton_dotP)

lemma singleton_appends_dotP [simp]: "dim_vec x = dim_vec y ⟹ (x @⇩v [v]⇩v) ∙ (y @⇩v [w]⇩v) = x ∙ y + v * w"
using scalar_prod_append[of x "dim_vec x" "[v]⇩v" 1 y "[w]⇩v"]
by (metis carrier_dim_vec singletons_dotP vec_carrier)

end```