Commit 0c4de5fe authored by Rene Thiemann's avatar Rene Thiemann
Browse files

consolidate vec_conjugate and conjugate

parent 44d196e58f3d
......@@ -18,118 +18,6 @@ imports
Conjugate
begin
subsection \<open>Conjugates of Vectors\<close>
definition vec_conjugate::"'a :: conjugate vec \<Rightarrow> 'a vec" ("conjugate\<^sub>v")
where "conjugate\<^sub>v v = vec (dim_vec v) (\<lambda>i. conjugate (v $ i))"
lemma vec_conjugate_index[simp]:
shows "i < dim_vec v \<Longrightarrow> conjugate\<^sub>v v $ i = conjugate (v $ i)"
and "dim_vec (conjugate\<^sub>v v) = dim_vec v"
unfolding vec_conjugate_def by auto
lemma vec_conjugate_closed[simp]: "v : carrier_vec n \<Longrightarrow> conjugate\<^sub>v v : carrier_vec n"
unfolding vec_conjugate_def by auto
lemma vec_conjugate_dist_add:
fixes v w :: "'a :: conjugatable_ring vec"
assumes dim: "v : carrier_vec n" "w : carrier_vec n"
shows "conjugate\<^sub>v (v + w) = conjugate\<^sub>v v + conjugate\<^sub>v w"
by (rule, insert dim, auto simp: conjugate_dist_add)
lemma vec_conjugate_uminus:
fixes v w :: "'a :: conjugatable_ring vec"
shows "- (conjugate\<^sub>v v) = conjugate\<^sub>v (- v)"
by (rule, auto simp:conjugate_neg)
lemma vec_conjugate_zero[simp]:
"conjugate\<^sub>v (0\<^sub>v n :: 'a :: conjugatable_ring vec) = 0\<^sub>v n" by auto
lemma vec_conjugate_id[simp]: "conjugate\<^sub>v (conjugate\<^sub>v v) = v"
unfolding vec_conjugate_def by auto
lemma vec_conjugate_cancel_iff[simp]: "conjugate\<^sub>v v = conjugate\<^sub>v w \<longleftrightarrow> v = w"
(is "?v = ?w \<longleftrightarrow> _")
proof(rule iffI)
assume cvw: "?v = ?w" show "v = w"
proof(rule)
have "dim_vec ?v = dim_vec ?w" using cvw by auto
thus dim: "dim_vec v = dim_vec w" by simp
fix i assume i: "i < dim_vec w"
hence "conjugate\<^sub>v v $ i = conjugate\<^sub>v w $ i" using cvw by auto
hence "conjugate (v$i) = conjugate (w $ i)" using i dim by auto
thus "v $ i = w $ i" by auto
qed
qed auto
lemma vec_conjugate_zero_iff[simp]:
fixes v :: "'a :: conjugatable_ring vec"
shows "conjugate\<^sub>v v = 0\<^sub>v n \<longleftrightarrow> v = 0\<^sub>v n"
using vec_conjugate_cancel_iff[of _ "0\<^sub>v n :: 'a vec"] by auto
lemma vec_conjugate_dist_smult:
fixes k :: "'a :: conjugatable_ring"
shows "conjugate\<^sub>v (k \<cdot>\<^sub>v v) = conjugate k \<cdot>\<^sub>v conjugate\<^sub>v v"
unfolding vec_conjugate_def
apply(rule) using conjugate_dist_mul by auto
lemma vec_conjugate_dist_sprod:
fixes v w :: "'a :: conjugatable_ring vec"
assumes v[simp]: "v : carrier_vec n" and w[simp]: "w : carrier_vec n"
shows "conjugate (v \<bullet> w) = conjugate\<^sub>v v \<bullet> conjugate\<^sub>v w"
unfolding scalar_prod_def
apply (subst sum_conjugate[OF finite_atLeastLessThan])
unfolding vec_conjugate_index
proof (rule sum.cong[OF refl])
fix i assume "i : {0..<dim_vec w}"
hence [simp]:"i < dim_vec v" "i < dim_vec w"
unfolding carrier_vecD[OF v] carrier_vecD[OF w]
using atLeastLessThan_iff by auto
show "conjugate (v $ i * w $ i) = conjugate\<^sub>v v $ i * conjugate\<^sub>v w $ i"
using conjugate_dist_mul vec_conjugate_index by auto
qed
abbreviation cscalar_prod :: "'a vec \<Rightarrow> 'a vec \<Rightarrow> 'a :: conjugatable_ring" (infix "\<bullet>c" 70)
where "(\<bullet>c) == \<lambda>v w. v \<bullet> conjugate\<^sub>v w"
lemma vec_conjugate_conjugate_sprod[simp]:
assumes v[simp]: "v : carrier_vec n" and w[simp]: "w : carrier_vec n"
shows "conjugate (conjugate\<^sub>v v \<bullet> w) = v \<bullet>c w"
apply (subst vec_conjugate_dist_sprod[of _ n]) by auto
lemma vec_conjugate_sprod_comm:
fixes v w :: "'a :: {conjugatable_ring, comm_ring} vec"
assumes "v : carrier_vec n" and "w : carrier_vec n"
shows "v \<bullet>c w = (conjugate\<^sub>v w \<bullet> v)"
unfolding scalar_prod_def using assms by(subst sum.ivl_cong, auto simp: ac_simps)
lemma vec_conjugate_square_zero:
fixes v :: "'a :: {conjugatable_ordered_ring,semiring_no_zero_divisors} vec"
assumes v[simp]: "v : carrier_vec n"
shows "v \<bullet>c v = 0 \<longleftrightarrow> v = 0\<^sub>v n"
proof
have dim: "dim_vec v = dim_vec (0\<^sub>v n)" by auto
let ?f = "\<lambda>i. v$i * conjugate (v$i)"
let ?I = "{0..<dim_vec v}"
have f: "?f : ?I \<rightarrow> { y. y \<ge> 0 }" using conjugate_square_positive by auto
assume vv0: "v \<bullet>c v = 0"
hence fI0: "?f ` ?I \<subseteq> {0}"
unfolding scalar_prod_def
using positive_sum[OF _ f] by auto
{ fix i assume i: "i < dim_vec v"
hence "?f i = 0" using fI0 by fastforce
hence "v $ i = 0" using conjugate_square_0 by auto
hence "v $ i = 0\<^sub>v n $ i" using i v by auto
}
from eq_vecI[OF this] show "v = 0\<^sub>v n" by auto
next assume "v = 0\<^sub>v n" thus "v \<bullet>c v = 0"
unfolding scalar_prod_def by auto
qed
lemma vec_conjugate_rat[simp]: "(conjugate\<^sub>v :: rat vec \<Rightarrow> rat vec) = (\<lambda>x. x)" by force
lemma vec_conjugate_real[simp]: "(conjugate\<^sub>v :: real vec \<Rightarrow> real vec) = (\<lambda>x. x)" by force
subsection \<open>Orthogonality with Conjugates\<close>
definition "corthogonal vs \<equiv>
......@@ -381,7 +269,7 @@ lemma adjust_zero:
proof -
define u where "u = us!i"
have u[simp]: "u : carrier_vec n" using i U u_def by auto
hence cu[simp]: "conjugate\<^sub>v u : carrier_vec n" by auto
hence cu[simp]: "conjugate u : carrier_vec n" by auto
have uU: "u : set us" using i u_def by auto
let ?g = "\<lambda>u'::'a vec. (-(w \<bullet>c u')/(u' \<bullet>c u') \<cdot>\<^sub>v u')"
have g: "?g : set us \<rightarrow> carrier_vec n" using w U by auto
......@@ -391,7 +279,7 @@ proof -
{ fix u' assume u': "(u'::'a vec) : carrier_vec n"
have [simp]: "dim_vec u = n" by auto
have "?f u' = (- (w \<bullet>c u') / (u' \<bullet>c u')) * (u' \<bullet>c u)"
using scalar_prod_smult_left[of "u'" "conjugate\<^sub>v u"]
using scalar_prod_smult_left[of "u'" "conjugate u"]
unfolding carrier_vecD[OF u] carrier_vecD[OF u'] by auto
} note conv = this
have "?f : ?U \<rightarrow> {0}"
......@@ -463,7 +351,7 @@ proof
have dist: "distinct us" using corthogonal_distinct orth by auto
have aw[simp]: "?aw : carrier_vec n" using U dist by auto
note adjust_nonzero[OF U dist w] wsU
hence aw0: "?aw \<bullet>c ?aw \<noteq> 0" using vec_conjugate_square_zero[OF aw] by auto
hence aw0: "?aw \<bullet>c ?aw \<noteq> 0" using conjugate_square_eq_0_vec[OF aw] by auto
fix i j assume i: "i < length (?aw # us)" and j: "j < length (?aw # us)"
show "((?aw # us) ! i \<bullet>c (?aw # us) ! j = 0) = (i \<noteq> j)"
proof (cases "i = 0")
......@@ -483,14 +371,14 @@ proof
hence ifold: "i = i'+1" using False by auto
hence i': "i' < length us" using i by auto
have [simp]: "us ! i' : carrier_vec n" using U i' by auto
hence cu': "conjugate\<^sub>v (us ! i') : carrier_vec n" by auto
hence cu': "conjugate (us ! i') : carrier_vec n" by auto
show ?thesis
proof (cases "j = 0")
case True
{ assume "?aw \<bullet>c us ! i' = 0"
hence "conjugate (?aw \<bullet>c us ! i') = 0" using conjugate_zero by auto
hence "conjugate\<^sub>v ?aw \<bullet> us ! i' = 0"
using vec_conjugate_dist_sprod[OF aw cu'] by auto
hence "conjugate ?aw \<bullet> us ! i' = 0"
using conjugate_sprod_vec[OF aw cu'] by auto
}
thus ?thesis unfolding True ifold
using adjust_zero[OF U orth w i']
......
......@@ -22,6 +22,7 @@ imports
Missing_Ring
"HOL-Algebra.Module"
Polynomial_Interpolation.Ring_Hom
Conjugate
begin
subsection\<open>Vectors\<close>
......@@ -2864,5 +2865,136 @@ shows "a \<in> set\<^sub>v v" using assms unfolding vec_set_def using image_eqI
lemma set_list_of_vec: "set (list_of_vec v) = set\<^sub>v v" unfolding vec_set_def by transfer auto
instantiation vec :: (conjugate) conjugate
begin
definition conjugate_vec :: "'a :: conjugate vec \<Rightarrow> 'a vec"
where "conjugate v = vec (dim_vec v) (\<lambda>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 \<in> carrier_vec n \<Longrightarrow> conjugate v \<in> carrier_vec n"
by (auto intro!: carrier_vecI)
lemma vec_index_conjugate[simp]:
shows "i < dim_vec v \<Longrightarrow> 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 \<longleftrightarrow> 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\<^sub>v n :: 'a :: conjugatable_ring vec) = 0\<^sub>v n" by auto
lemma conjugate_vec_0[simp]:
"conjugate (vec 0 f) = vec 0 f" by auto
lemma sprod_vec_0[simp]: "v \<bullet> 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\<^sub>v n \<longleftrightarrow> v = 0\<^sub>v n"
using conjugate_cancel_iff[of _ "0\<^sub>v n :: 'a vec"] by auto
lemma conjugate_smult_vec:
fixes k :: "'a :: conjugatable_ring"
shows "conjugate (k \<cdot>\<^sub>v v) = conjugate k \<cdot>\<^sub>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 \<bullet> w) = conjugate v \<bullet> 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 \<Rightarrow> 'a vec \<Rightarrow> 'a :: conjugatable_ring" (infix "\<bullet>c" 70)
where "(\<bullet>c) \<equiv> \<lambda>v w. v \<bullet> 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 \<bullet> w) = v \<bullet>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 \<bullet>c w = (conjugate w \<bullet> 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 \<bullet>c v \<ge> 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 \<in> carrier_vec n"
shows "v \<bullet>c v = 0 \<longleftrightarrow> v = 0\<^sub>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 \<in> carrier_vec n"
shows "v \<bullet>c v > 0 \<longleftrightarrow> v \<noteq> 0\<^sub>v n"
using assms by (auto simp: less_le)
lemma vec_conjugate_rat[simp]: "(conjugate :: rat vec \<Rightarrow> rat vec) = (\<lambda>x. x)" by force
lemma vec_conjugate_real[simp]: "(conjugate :: real vec \<Rightarrow> real vec) = (\<lambda>x. x)" by force
end
......@@ -26,7 +26,7 @@ imports
begin
definition vec_inv :: "'a::conjugatable_field vec \<Rightarrow> 'a vec"
where "vec_inv v = 1 / (v \<bullet>c v) \<cdot>\<^sub>v conjugate\<^sub>v v"
where "vec_inv v = 1 / (v \<bullet>c v) \<cdot>\<^sub>v conjugate v"
lemma vec_inv_closed[simp]: "v \<in> carrier_vec n \<Longrightarrow> vec_inv v \<in> carrier_vec n"
unfolding vec_inv_def by auto
......@@ -40,10 +40,10 @@ lemma vec_inv[simp]:
shows "vec_inv v \<bullet> v = 1"
proof -
{ assume "v \<bullet>c v = 0"
hence "v = 0\<^sub>v n" using vec_conjugate_square_zero[OF v] by auto
hence "v = 0\<^sub>v n" using conjugate_square_eq_0_vec[OF v] by auto
hence False using v0 by auto
}
moreover have "conjugate\<^sub>v v \<bullet> v = v \<bullet>c v"
moreover have "conjugate v \<bullet> v = v \<bullet>c v"
apply (rule comm_scalar_prod) using v by auto
ultimately show ?thesis
unfolding vec_inv_def
......@@ -75,7 +75,7 @@ proof -
and j2: "j<length vs" using l_def by auto
hence id2: "vs ! i \<in> carrier_vec n"
and id3: "map vec_inv vs ! i \<in> carrier_vec n"
and id4: "conjugate\<^sub>v (vs ! i) \<in> carrier_vec n"
and id4: "conjugate (vs ! i) \<in> carrier_vec n"
and jd2: "vs ! j \<in> carrier_vec n" using dim by auto
show "(?W * ?V) $$ (i,j) = (if i = j then 1 else 0)"
unfolding times_mat_def rW cV
......@@ -94,7 +94,7 @@ definition corthogonal_inv :: "'a::conjugatable_field mat \<Rightarrow> 'a mat"
where "corthogonal_inv A = mat_of_rows (dim_row A) (map vec_inv (cols A))"
definition mat_adjoint :: "'a :: conjugatable_field mat \<Rightarrow> 'a mat"
where "mat_adjoint A \<equiv> mat_of_rows (dim_row A) (map conjugate\<^sub>v (cols A))"
where "mat_adjoint A \<equiv> mat_of_rows (dim_row A) (map conjugate (cols A))"
definition corthogonal_mat :: "'a::conjugatable_field mat \<Rightarrow> bool"
where "corthogonal_mat A \<equiv>
......@@ -109,25 +109,25 @@ lemma corthogonal_matD[elim]:
proof
have ci: "col A i : carrier_vec (dim_row A)"
and cj: "col A j : carrier_vec (dim_row A)" by auto
note [simp] = vec_conjugate_conjugate_sprod[OF ci cj]
note [simp] = conjugate_conjugate_sprod[OF ci cj]
let ?B = "mat_adjoint A * A"
have diag: "diagonal_mat ?B" and zero: "\<And>i. i<dim_col A \<Longrightarrow> ?B $$ (i,i) \<noteq> 0"
using orth unfolding corthogonal_mat_def Let_def by auto
{ assume "i = j"
hence "conjugate\<^sub>v (col A i) \<bullet> col A j \<noteq> 0"
hence "conjugate (col A i) \<bullet> col A j \<noteq> 0"
using zero[OF i] unfolding mat_adjoint_def using i by simp
hence "conjugate (conjugate\<^sub>v (col A i) \<bullet> col A j) \<noteq> 0"
hence "conjugate (conjugate (col A i) \<bullet> col A j) \<noteq> 0"
unfolding conjugate_zero_iff.
hence "col A i \<bullet>c col A j \<noteq> 0" by simp
}
thus "col A i \<bullet>c col A j = 0 \<Longrightarrow> i \<noteq> j" by auto
{ assume "i \<noteq> j"
hence "conjugate\<^sub>v (col A i) \<bullet> col A j = 0"
hence "conjugate (col A i) \<bullet> col A j = 0"
using diag
unfolding diagonal_mat_def
unfolding mat_adjoint_def using i j by simp
hence "conjugate (conjugate\<^sub>v (col A i) \<bullet> col A j) = 0" by simp
hence "conjugate (conjugate (col A i) \<bullet> col A j) = 0" by simp
thus "col A i \<bullet>c col A j = 0" by simp
}
qed
......@@ -137,13 +137,13 @@ lemma corthogonal_matI[intro]:
shows "corthogonal_mat A"
proof -
{ fix i j assume i: "i < dim_col A" and j: "j < dim_col A" and ij: "i \<noteq> j"
have "conjugate\<^sub>v (col A i) \<bullet> col A j = 0"
by (metis assms col_dim i j ij vec_conjugate_sprod_comm)
have "conjugate (col A i) \<bullet> col A j = 0"
by (metis assms col_dim i j ij conjugate_vec_sprod_comm)
}
moreover
{ fix i assume "i < dim_col A"
hence "conjugate\<^sub>v (col A i) \<bullet> col A i \<noteq> 0"
by (metis assms comm_scalar_prod vec_conjugate_closed carrier_vecI)
hence "conjugate (col A i) \<bullet> col A i \<noteq> 0"
by (metis assms comm_scalar_prod carrier_vec_conjugate carrier_vecI)
}
ultimately show ?thesis
unfolding corthogonal_mat_def Let_def
......@@ -410,10 +410,10 @@ proof -
next
case False
hence z: "0 < length ws" using i ws by auto
note cwsi = vec_conjugate_closed[OF wsi]
have "vec_inv ?wsi \<bullet> v = 1 / (?wsi \<bullet>c ?wsi) * (conjugate\<^sub>v ?wsi \<bullet> v)"
note cwsi = carrier_vec_conjugate[OF wsi]
have "vec_inv ?wsi \<bullet> v = 1 / (?wsi \<bullet>c ?wsi) * (conjugate ?wsi \<bullet> v)"
unfolding vec_inv_def unfolding smult_scalar_prod_distrib[OF cwsi v]..
also have "conjugate\<^sub>v ?wsi \<bullet> v = v \<bullet>c ?wsi"
also have "conjugate ?wsi \<bullet> v = v \<bullet>c ?wsi"
using comm_scalar_prod[OF cwsi v].
also have "... = 0"
using corthogonalD[OF ws(2) z i2] False unfolding ws0 by auto
......
......@@ -50,10 +50,6 @@ lemma rev_unsimp: "rev xs @ (r # rs) = rev (r#xs) @ rs" by(induct xs,auto)
(* TODO: unify *)
no_notation Gram_Schmidt.cscalar_prod (infix "\<bullet>c" 70)
lemma vec_conjugate_connect[simp]: "Gram_Schmidt.vec_conjugate = conjugate"
by (auto simp: vec_conjugate_def conjugate_vec_def)
lemma corthogonal_is_orthogonal[simp]:
"corthogonal (xs :: 'a :: trivial_conjugatable_ordered_field vec list) = orthogonal xs"
......
......@@ -359,145 +359,6 @@ lemma coeff_mult_monom:
(**** End of the lemmas which may be part of the standard library ****)
(**** The following lemmas could be part of Jordan_Normal_Form/Conjugate.thy ****)
(**** The following lemmas could be part of Jordan_Normal_Form/Matrix.thy ****)
(* adapting from Jordan_Normal_Form/Gram_Schmidt to a class-oriented manner *)
instantiation vec :: (conjugate) conjugate
begin
definition conjugate_vec :: "'a :: conjugate vec \<Rightarrow> 'a vec"
where "conjugate v = vec (dim_vec v) (\<lambda>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 \<in> carrier_vec n \<Longrightarrow> conjugate v \<in> carrier_vec n"
by (auto intro!: carrier_vecI)
lemma vec_index_conjugate[simp]:
shows "i < dim_vec v \<Longrightarrow> 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 \<longleftrightarrow> 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\<^sub>v n :: 'a :: conjugatable_ring vec) = 0\<^sub>v n" by auto
lemma conjugate_vec_0[simp]:
"conjugate (vec 0 f) = vec 0 f" by auto
lemma sprod_vec_0[simp]: "v \<bullet> 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\<^sub>v n \<longleftrightarrow> v = 0\<^sub>v n"
using conjugate_cancel_iff[of _ "0\<^sub>v n :: 'a vec"] by auto
lemma conjugate_smult_vec:
fixes k :: "'a :: conjugatable_ring"
shows "conjugate (k \<cdot>\<^sub>v v) = conjugate k \<cdot>\<^sub>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 \<bullet> w) = conjugate v \<bullet> 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 \<Rightarrow> 'a vec \<Rightarrow> 'a :: conjugatable_ring" (infix "\<bullet>c" 70)
where "(\<bullet>c) \<equiv> \<lambda>v w. v \<bullet> 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 \<bullet> w) = v \<bullet>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 \<bullet>c w = (conjugate w \<bullet> 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 \<bullet>c v \<ge> 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 \<in> carrier_vec n"
shows "v \<bullet>c v = 0 \<longleftrightarrow> v = 0\<^sub>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 \<in> carrier_vec n"
shows "v \<bullet>c v > 0 \<longleftrightarrow> v \<noteq> 0\<^sub>v n"
using assms by (auto simp: less_le)
lemma vec_conjugate_rat[simp]: "(conjugate :: rat vec \<Rightarrow> rat vec) = (\<lambda>x. x)" by force
lemma vec_conjugate_real[simp]: "(conjugate :: real vec \<Rightarrow> real vec) = (\<lambda>x. x)" by force
(**** End of the lemmas which could be part of Jordan_Normal_Form/Matrix.thy ****)
(**** The following lemmas could be moved to Algebraic_Numbers/Resultant.thy ****)
lemma vec_of_poly_0 [simp]: "vec_of_poly 0 = 0\<^sub>v 1" by (auto simp: vec_of_poly_def)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment