--- a/src/Doc/JEdit/JEdit.thy Thu Apr 26 19:51:32 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Apr 26 21:57:23 2018 +0200
@@ -1154,7 +1154,7 @@
text \<open>
The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the theory
or proof context matching all of given criteria in the \<^emph>\<open>Find\<close> text field. A
- single criterium has the following syntax:
+ single criterion has the following syntax:
@{rail \<open>
('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
@@ -1171,7 +1171,7 @@
text \<open>
The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants whose type
meets all of the given criteria in the \<^emph>\<open>Find\<close> text field. A single
- criterium has the following syntax:
+ criterion has the following syntax:
@{rail \<open>
('-'?)
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Apr 26 19:51:32 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Apr 26 21:57:23 2018 +0200
@@ -1,5 +1,5 @@
(* Title: HOL/Analysis/Cartesian_Euclidean_Space.thy
- Some material by Tim Makarios and L C Paulson
+ Some material by Jose Divasón, Tim Makarios and L C Paulson
*)
section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\<close>
@@ -573,12 +573,12 @@
done
lemma scalar_matrix_assoc:
- fixes A :: "real^'m^'n"
+ fixes A :: "('a::real_algebra_1)^'m^'n"
shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B"
- by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
+ by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right)
lemma matrix_scalar_ac:
- fixes A :: "real^'m^'n"
+ fixes A :: "('a::real_algebra_1)^'m^'n"
shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B"
by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
@@ -714,7 +714,12 @@
and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
by (simp_all add: linear_linear linear_continuous_at linear_continuous_on matrix_vector_mul_linear)
-lemma matrix_vector_mult_add_distrib [algebra_simps]:
+lemma vector_matrix_left_distrib [algebra_simps]:
+ shows "(x + y) v* A = x v* A + y v* A"
+ unfolding vector_matrix_mult_def
+ by (simp add: algebra_simps sum.distrib vec_eq_iff)
+
+lemma matrix_vector_right_distrib [algebra_simps]:
"A *v (x + y) = A *v x + A *v y"
by (vector matrix_vector_mult_def sum.distrib distrib_left)
@@ -817,34 +822,44 @@
unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
by simp
-lemma vector_matrix_mul_rid:
+lemma vector_scalar_commute:
+ fixes A :: "'a::{field}^'m^'n"
+ shows "A *v (c *s x) = c *s (A *v x)"
+ by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left)
+
+lemma scalar_vector_matrix_assoc:
+ fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
+ shows "(k *s x) v* A = k *s (x v* A)"
+ by (metis transpose_matrix_vector vector_scalar_commute)
+
+lemma vector_matrix_mult_0 [simp]: "0 v* A = 0"
+ unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
+
+lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
+ unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
+
+lemma vector_matrix_mul_rid [simp]:
fixes v :: "('a::semiring_1)^'n"
shows "v v* mat 1 = v"
by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
-lemma scalar_vector_matrix_assoc:
+lemma scaleR_vector_matrix_assoc:
fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
-lemma vector_scalar_matrix_ac:
+lemma vector_scaleR_matrix_ac:
fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
proof -
have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
unfolding vector_matrix_mult_def
by (simp add: algebra_simps)
- with scalar_vector_matrix_assoc
+ with scaleR_vector_matrix_assoc
show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
by auto
qed
-lemma vector_matrix_left_distrib:
- fixes x y :: "real^'n" and A :: "real^'m^'n"
- shows "(x + y) v* A = x v* A + y v* A"
- unfolding vector_matrix_mult_def
- by (simp add: algebra_simps sum.distrib vec_eq_iff)
-
subsection\<open>Some bounds on components etc. relative to operator norm\<close>
@@ -1168,10 +1183,31 @@
qed
lemma invertible_mult:
- fixes A B :: "real^'n^'n"
- assumes "invertible A" and "invertible B"
- shows "invertible (A ** B)"
- by (metis (no_types, hide_lams) assms invertible_def matrix_left_right_inverse matrix_mul_assoc matrix_mul_lid)
+ assumes inv_A: "invertible A"
+ and inv_B: "invertible B"
+ shows "invertible (A**B)"
+proof -
+ obtain A' where AA': "A ** A' = mat 1" and A'A: "A' ** A = mat 1"
+ using inv_A unfolding invertible_def by blast
+ obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1"
+ using inv_B unfolding invertible_def by blast
+ show ?thesis
+ proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI)
+ have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))"
+ using matrix_mul_assoc[of A B "(B' ** A')", symmetric] .
+ also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] ..
+ also have "... = A ** (mat 1 ** A')" unfolding BB' ..
+ also have "... = A ** A'" unfolding matrix_mul_lid ..
+ also have "... = mat 1" unfolding AA' ..
+ finally show "A ** B ** (B' ** A') = mat (1::'a)" .
+ have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] .
+ also have "... = B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] ..
+ also have "... = B' ** (mat 1 ** B)" unfolding A'A ..
+ also have "... = B' ** B" unfolding matrix_mul_lid ..
+ also have "... = mat 1" unfolding B'B ..
+ finally show "B' ** A' ** (A ** B) = mat 1" .
+ qed
+qed
lemma transpose_invertible:
fixes A :: "real^'n^'n"
@@ -1189,15 +1225,15 @@
by (simp add: matrix_transpose_mul [symmetric])
qed
-lemma matrix_scalar_vector_ac:
+lemma matrix_scaleR_vector_ac:
fixes A :: "real^('m::finite)^'n"
shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v"
- by (metis matrix_vector_mult_scaleR transpose_scalar vector_scalar_matrix_ac vector_transpose_matrix)
+ by (metis matrix_vector_mult_scaleR transpose_scalar vector_scaleR_matrix_ac vector_transpose_matrix)
-lemma scalar_matrix_vector_assoc:
+lemma scaleR_matrix_vector_assoc:
fixes A :: "real^('m::finite)^'n"
shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v"
- by (metis matrix_scalar_vector_ac matrix_vector_mult_scaleR)
+ by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR)
text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>