# HG changeset patch
# User nipkow
# Date 1524772643 -7200
# Node ID f76e8180c498253c3cb81836dc1c369c0ed31fa1
# Parent  ce8ad77cd3fa4a940b425343f9ab92758e91aead# Parent  6aba668aea78d69d27297b356509450dbec97bc0
merged

diff -r 6aba668aea78 -r f76e8180c498 src/Doc/JEdit/JEdit.thy
--- 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>
     ('-'?)
diff -r 6aba668aea78 -r f76e8180c498 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- 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>