Theory Cayley_Hamilton.Square_Matrix
theory Square_Matrix
imports
"HOL-Analysis.Determinants"
"HOL-Analysis.Cartesian_Euclidean_Space"
begin
lemma smult_axis: "x *s axis i y = axis i (x * y::_::mult_zero)"
by (simp add: axis_def vec_eq_iff)
typedef ('a, 'n) sq_matrix = "UNIV :: ('n ⇒ 'n ⇒ 'a) set"
morphisms to_fun of_fun
by (rule UNIV_witness)
syntax "_sq_matrix" :: "type ⇒ type ⇒ type" ("(_ ^^/ _)" [15, 16] 15)
parse_translation ‹
let
fun vec t u = Syntax.const @{type_syntax sq_matrix} $ t $ u;
fun sq_matrix_tr [t, u] =
(case Term_Position.strip_positions u of
v as Free (x, _) =>
if Lexicon.is_tid x then
vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
Syntax.const @{class_syntax finite})
else vec t u
| _ => vec t u)
in
[(@{syntax_const "_sq_matrix"}, K sq_matrix_tr)]
end
›
setup_lifting type_definition_sq_matrix
lift_definition map_sq_matrix :: "('a ⇒ 'c) ⇒ 'a^^'b ⇒ 'c^^'b" is
"λf M i j. f (M i j)" .
lift_definition from_vec :: "'a^'n^'n ⇒ 'a^^'n" is
"λM i j. M $ i $ j" .
lift_definition to_vec :: "'a^^'n ⇒ 'a^'n^'n" is
"λM. χ i j. M i j" .
lemma from_vec_eq_iff: "from_vec M = from_vec N ⟷ M = N"
by transfer (auto simp: vec_eq_iff fun_eq_iff)
lemma to_vec_from_vec[simp]: "to_vec (from_vec M) = M"
by transfer (simp add: vec_eq_iff)
lemma from_vec_to_vec[simp]: "from_vec (to_vec M) = M"
by transfer (simp add: vec_eq_iff fun_eq_iff)
lemma map_sq_matrix_compose[simp]: "map_sq_matrix f (map_sq_matrix g M) = map_sq_matrix (λx. f (g x)) M"
by transfer simp
lemma map_sq_matrix_ident[simp]: "map_sq_matrix (λx. x) M = M"
by transfer (simp add: vec_eq_iff)
lemma map_sq_matrix_cong:
"M = N ⟹ (⋀i j. f (to_fun N i j) = g (to_fun N i j)) ⟹ map_sq_matrix f M = map_sq_matrix g N"
by transfer simp
lift_definition diag :: "'a::zero ⇒ 'a^^'n" is
"λk i j. if i = j then k else 0" .
lemma diag_eq_iff: "diag x = diag y ⟷ x = y"
by transfer (simp add: fun_eq_iff)
lemma map_sq_matrix_diag[simp]: "f 0 = 0 ⟹ map_sq_matrix f (diag c) = diag (f c)"
by transfer (simp add: fun_eq_iff)
lift_definition smult_sq_matrix :: "'a::times ⇒ 'a^^'n ⇒ 'a^^'n" (infixr "*⇩S" 75) is
"λc M i j. c * M i j" .
lemma smult_map_sq_matrix:
"(⋀y. f (x * y) = z * f y) ⟹ map_sq_matrix f (x *⇩S A) = z *⇩S map_sq_matrix f A"
by transfer simp
lemma map_sq_matrix_smult: "c *⇩S map_sq_matrix f A = map_sq_matrix (λx. c * f x) A"
by transfer simp
lemma one_smult[simp]: "(1::_::monoid_mult) *⇩S x = x"
by transfer simp
lemma smult_diag: "x *⇩S diag y = diag (x * y::_::mult_zero)"
by transfer (simp add: fun_eq_iff)
instantiation sq_matrix :: (semigroup_add, finite) semigroup_add
begin
lift_definition plus_sq_matrix :: "'a^^'b ⇒ 'a^^'b ⇒ 'a^^'b" is
"λA B i j. A i j + B i j" .
instance
by standard (transfer, simp add: field_simps)
end
lemma map_sq_matrix_add:
"(⋀a b. f (a + b) = f a + f b) ⟹ map_sq_matrix f (A + B) = map_sq_matrix f A + map_sq_matrix f B"
by transfer simp
lemma add_map_sq_matrix: "map_sq_matrix f A + map_sq_matrix g A = map_sq_matrix (λx. f x + g x) A"
by transfer simp
instantiation sq_matrix :: (monoid_add, finite) monoid_add
begin
lift_definition zero_sq_matrix :: "'a^^'b" is "λi j. 0" .
instance
by standard (transfer, simp)+
end
lemma diag_0: "diag 0 = 0"
by transfer simp
lemma diag_0_eq: "diag x = 0 ⟷ x = 0"
by transfer (simp add: fun_eq_iff)
lemma zero_map_sq_matrix: "f 0 = 0 ⟹ map_sq_matrix f 0 = 0"
by transfer simp
lemma map_sq_matrix_0[simp]: "map_sq_matrix (λx. 0) A = 0"
by transfer simp
instance sq_matrix :: (ab_semigroup_add, finite) ab_semigroup_add
by standard (transfer, simp add: field_simps)+
instantiation sq_matrix :: (minus, finite) minus
begin
lift_definition minus_sq_matrix :: "'a^^'b ⇒ 'a^^'b ⇒ 'a^^'b" is
"λA B i j. A i j - B i j" .
instance ..
end
instantiation sq_matrix :: (group_add, finite) group_add
begin
lift_definition uminus_sq_matrix :: "'a^^'b ⇒ 'a^^'b" is
"uminus" .
instance
by standard (transfer, simp)+
end
lemma map_sq_matrix_diff:
"(⋀a b. f (a - b) = f a - f b) ⟹ map_sq_matrix f (A - B) = map_sq_matrix f A - map_sq_matrix f B"
by transfer (simp add: vec_eq_iff)
lemma smult_diff: fixes a :: "'a::comm_ring_1" shows "a *⇩S (A - B) = a *⇩S A - a *⇩S B"
by transfer (simp add: field_simps)
instance sq_matrix :: (cancel_semigroup_add, finite) cancel_semigroup_add
by (standard; transfer, simp add: field_simps fun_eq_iff)
instance sq_matrix :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add
by (standard; transfer, simp add: field_simps)
instance sq_matrix :: (comm_monoid_add, finite) comm_monoid_add
by (standard; transfer, simp add: field_simps)
lemma map_sq_matrix_sum:
"f 0 = 0 ⟹ (⋀a b. f (a + b) = f a + f b) ⟹
map_sq_matrix f (∑i∈I. A i) = (∑i∈I. map_sq_matrix f (A i))"
by (induction I rule: infinite_finite_induct)
(auto simp: zero_map_sq_matrix map_sq_matrix_add)
lemma sum_map_sq_matrix: "(∑i∈I. map_sq_matrix (f i) A) = map_sq_matrix (λx. ∑i∈I. f i x) A"
by (induction I rule: infinite_finite_induct) (simp_all add: add_map_sq_matrix)
lemma smult_zero[simp]: fixes a :: "'a::ring_1" shows "a *⇩S 0 = 0"
by transfer (simp add: vec_eq_iff)
lemma smult_right_add: fixes a :: "'a::ring_1" shows "a *⇩S (x + y) = a *⇩S x + a *⇩S y"
by transfer (simp add: vec_eq_iff field_simps)
lemma smult_sum: fixes a :: "'a::ring_1" shows "(∑i∈I. a *⇩S f i) = a *⇩S (sum f I)"
by (induction I rule: infinite_finite_induct)
(simp_all add: smult_right_add vec_eq_iff)
instance sq_matrix :: (ab_group_add, finite) ab_group_add
by standard (transfer, simp add: field_simps)+
instantiation sq_matrix :: ("semiring_0", finite) semiring_0
begin
lift_definition times_sq_matrix :: "'a^^'b ⇒ 'a^^'b ⇒ 'a^^'b" is
"λM N i j. ∑k∈UNIV. M i k * N k j" .
instance
proof
fix a b c :: "'a^^'b" show "a * b * c = a * (b * c)"
by transfer
(auto simp: fun_eq_iff sum_distrib_left sum_distrib_right field_simps intro: sum.swap)
qed (transfer, simp add: vec_eq_iff sum.distrib field_simps)+
end
lemma diag_mult: "diag x * A = x *⇩S A"
by transfer (simp add: if_distrib[where f="λx. x * a" for a] sum.If_cases)
lemma mult_diag:
fixes x :: "'a::comm_ring_1"
shows "A * diag x = x *⇩S A"
by transfer (simp add: if_distrib[where f="λx. a * x" for a] mult.commute sum.If_cases)
lemma smult_mult1: fixes a :: "'a::comm_ring_1" shows "a *⇩S (A * B) = (a *⇩S A) * B"
by transfer (simp add: sum_distrib_left field_simps)
lemma smult_mult2: fixes a :: "'a::comm_ring_1" shows "a *⇩S (A * B) = A * (a *⇩S B)"
by transfer (simp add: sum_distrib_left field_simps)
lemma map_sq_matrix_mult:
fixes f :: "'a::semiring_1 ⇒ 'b::semiring_1"
assumes f: "⋀a b. f (a + b) = f a + f b" "⋀a b. f (a * b) = f a * f b" "f 0 = 0"
shows "map_sq_matrix f (A * B) = map_sq_matrix f A * map_sq_matrix f B"
proof (transfer fixing: f)
fix A B :: "'c ⇒ 'c ⇒ 'a"
{ fix I i j have "f (∑k∈I. A i k * B k j) = (∑k∈I. f (A i k) * f (B k j))"
by (induction I rule: infinite_finite_induct) (auto simp add: f) }
then show "(λi j. f (∑k∈UNIV. A i k * B k j)) = (λi j. ∑k∈UNIV. f (A i k) * f (B k j))"
by simp
qed
lemma from_vec_mult[simp]: "from_vec (M ** N) = from_vec M * from_vec N"
by transfer (simp add: matrix_matrix_mult_def fun_eq_iff vec_eq_iff)
instantiation sq_matrix :: ("semiring_1", finite) semiring_1
begin
lift_definition one_sq_matrix :: "'a^^'b" is
"λi j. if i = j then 1 else 0" .
instance
by standard (transfer, simp add: fun_eq_iff sum.If_cases
if_distrib[where f="λx. x * b" for b] if_distrib[where f="λx. b * x" for b])+
end
instance sq_matrix :: ("semiring_1", finite) numeral ..
lemma diag_1: "diag 1 = 1"
by transfer simp
lemma diag_1_eq: "diag x = 1 ⟷ x = 1"
by transfer (simp add: fun_eq_iff)
instance sq_matrix :: ("ring_1", finite) ring_1
by standard simp_all