Theory Code_Cayley_Hamilton
section‹Code Cayley Hamilton›
theory Code_Cayley_Hamilton
imports
"HOL-Computational_Algebra.Polynomial"
Cayley_Hamilton_Compatible
Gauss_Jordan.Code_Matrix
begin
subsection‹Code equations for the definitions presented in the Cayley-Hamilton development›
definition "scalar_matrix_mult_row c A i = (χ j. c * (A $ i $ j))"
lemma scalar_matrix_mult_row_code [code abstract]:
"vec_nth (scalar_matrix_mult_row c A i) =(% j. c * (A $ i $ j))"
by(simp add: scalar_matrix_mult_row_def fun_eq_iff)
lemma scalar_matrix_mult_code [code abstract]: "vec_nth (c *k A) = scalar_matrix_mult_row c A"
unfolding matrix_scalar_mult_def scalar_matrix_mult_row_def[abs_def]
using vec_lambda_beta by auto
definition "minorM_row A i j k= vec_lambda (%l. if k = i ∧ l = j then 1 else
if k = i ∨ l = j then 0 else A$k$l)"
lemma minorM_row_code [code abstract]:
"vec_nth (minorM_row A i j k) =(%l. if k = i ∧ l = j then 1 else
if k = i ∨ l = j then 0 else A$k$l)"
by(simp add: minorM_row_def fun_eq_iff)
lemma minorM_code [code abstract]: "vec_nth (minorM A i j) = minorM_row A i j"
unfolding minorM_def by transfer (auto simp: vec_eq_iff fun_eq_iff minorM_row_def)
definition "cofactorM_row A i = vec_lambda (λj. cofactorM A $ i $ j)"
lemma cofactorM_row_code [code abstract]: "vec_nth (cofactorM_row A i) = cofactor A i"
by (simp add: fun_eq_iff cofactorM_row_def cofactor_def cofactorM_def)
lemma cofactorM_code [code abstract]: "vec_nth (cofactorM A) = cofactorM_row A"
by (simp add: fun_eq_iff cofactorM_row_def vec_eq_iff)
lemmas cofactor_def[code_unfold]
definition mat2matofpoly_row
where "mat2matofpoly_row A i = vec_lambda (λj. [: A $ i $ j :])"
lemma mat2matofpoly_row_code [code abstract]:
"vec_nth (mat2matofpoly_row A i) = (%j. [: A $ i $ j :])"
unfolding mat2matofpoly_row_def by auto
lemma [code abstract]: "vec_nth (mat2matofpoly k) = mat2matofpoly_row k"
unfolding mat2matofpoly_def unfolding mat2matofpoly_row_def[abs_def] by auto
primrec matpow :: "'a::semiring_1^'n^'n ⇒ nat ⇒ 'a^'n^'n" where
matpow_0: "matpow A 0 = mat 1" |
matpow_Suc: "matpow A (Suc n) = A ** (matpow A n)"
definition evalmat :: "'a::comm_ring_1 poly ⇒ 'a^'n^'n ⇒ 'a^'n^'n" where
"evalmat P A = (∑ i ∈ { n::nat . n ≤ ( degree P ) } . (coeff P i) *k (matpow A i) )"
lemma evalmat_unfold:
"evalmat P A = (∑i = 0..degree P. coeff P i *k matpow A i)"
by (simp add: evalmat_def atMost_def [symmetric] atMost_atLeast0)
lemma evalmat_code[code]:
"evalmat P A = (∑i←[0..int (degree P)]. coeff P (nat i) *k matpow A (nat i))" (is "_ = ?rhs")
proof -
let ?t = "λn. coeff P n *k matpow A n"
have "(∑i = 0..degree P. coeff P i *k matpow A i) = (∑i∈{0..int (degree P)}. coeff P (nat i) *k matpow A (nat i))"
by (rule sum.reindex_cong [of nat])
(auto simp add: eq_nat_nat_iff image_iff intro: inj_onI, presburger)
also have "… = ?rhs"
by (simp add: sum_set_upto_conv_sum_list_int [symmetric])
finally show ?thesis
by (simp add: evalmat_unfold)
qed
definition coeffM_zero :: "'a poly^'n^'n ⇒ 'a::zero^'n^'n" where
"coeffM_zero A = (χ i j. (coeff (A $ i $ j) 0))"
definition "coeffM_zero_row A i = (χ j. (coeff (A $ i $ j) 0))"
definition coeffM :: "'a poly^'n^'n ⇒ nat ⇒ 'a::zero^'n^'n" where
"coeffM A n = (χ i j. coeff (A $ i $ j) n)"
lemma coeffM_zero_row_code [code abstract]:
"vec_nth (coeffM_zero_row A i) = (% j. (coeff (A $ i $ j) 0))"
by(simp add: coeffM_zero_row_def fun_eq_iff)
lemma coeffM_zero_code [code abstract]: "vec_nth (coeffM_zero A) = coeffM_zero_row A"
unfolding coeffM_zero_def coeffM_zero_row_def[abs_def]
using vec_lambda_beta by auto
definition
"coeffM_row A n i = (χ j. coeff (A $ i $ j) n)"
lemma coeffM_row_code [code abstract]:
"vec_nth (coeffM_row A n i) = (% j. coeff (A $ i $ j) n)"
by(simp add: coeffM_row_def coeffM_def fun_eq_iff)
lemma coeffM_code [code abstract]: "vec_nth (coeffM A n) = coeffM_row A n"
unfolding coeffM_def coeffM_row_def[abs_def]
using vec_lambda_beta by auto
end