src/HOL/Analysis/Cartesian_Euclidean_Space.thy
 changeset 68041 d45b78cb86cf parent 68038 20b713cff87a child 68043 d345e9c35ae1
```     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Apr 25 16:40:29 2018 +0100
1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Apr 25 21:29:02 2018 +0100
1.3 @@ -1078,23 +1078,18 @@
1.4    have fU: "finite ?U" by simp
1.5    have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). sum (\<lambda>i. (x\$i) *s column i A) ?U = y)"
1.6      unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
1.7 -    apply (subst eq_commute)
1.8 -    apply rule
1.9 -    done
1.10 +    by (simp add: eq_commute)
1.11    have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> span (columns A))" by blast
1.12    { assume h: ?lhs
1.13      { fix x:: "real ^'n"
1.14        from h[unfolded lhseq, rule_format, of x] obtain y :: "real ^'m"
1.15          where y: "sum (\<lambda>i. (y\$i) *s column i A) ?U = x" by blast
1.16        have "x \<in> span (columns A)"
1.17 -        unfolding y[symmetric]
1.18 -        apply (rule span_sum)
1.19 -        unfolding scalar_mult_eq_scaleR
1.20 -        apply (rule span_mul)
1.21 -        apply (rule span_superset)
1.22 -        unfolding columns_def
1.23 -        apply blast
1.24 -        done
1.25 +        unfolding y[symmetric] scalar_mult_eq_scaleR
1.26 +      proof (rule span_sum [OF span_mul])
1.27 +        show "column i A \<in> span (columns A)" for i
1.28 +          using columns_def span_inc by auto
1.29 +      qed
1.30      }
1.31      then have ?rhs unfolding rhseq by blast }
1.32    moreover
1.33 @@ -1121,9 +1116,7 @@
1.34              using i(1) by (simp add: field_simps)
1.35            have "sum (\<lambda>xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j)
1.36                else (x\$xa) * ((column xa A\$j))) ?U = sum (\<lambda>xa. (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))) ?U"
1.37 -            apply (rule sum.cong[OF refl])
1.38 -            using th apply blast
1.39 -            done
1.40 +            by (rule sum.cong[OF refl]) (use th in blast)
1.41            also have "\<dots> = sum (\<lambda>xa. if xa = i then c * ((column i A)\$j) else 0) ?U + sum (\<lambda>xa. ((x\$xa) * ((column xa A)\$j))) ?U"
1.43            also have "\<dots> = c * ((column i A)\$j) + sum (\<lambda>xa. ((x\$xa) * ((column xa A)\$j))) ?U"
1.44 @@ -1164,10 +1157,10 @@
1.45        where f': "linear f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
1.46      have th: "matrix f' ** A = mat 1"
1.47        by (simp add: matrix_eq matrix_works[OF f'(1)]
1.48 -          matrix_vector_mul_assoc[symmetric] matrix_vector_mul_lid f'(2)[rule_format])
1.49 +          matrix_vector_mul_assoc[symmetric] f'(2)[rule_format])
1.50      hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp
1.51      hence "matrix f' = A'"
1.52 -      by (simp add: matrix_mul_assoc[symmetric] AA' matrix_mul_rid matrix_mul_lid)
1.53 +      by (simp add: matrix_mul_assoc[symmetric] AA')
1.54      hence "matrix f' ** A = A' ** A" by simp
1.55      hence "A' ** A = mat 1" by (simp add: th)
1.56    }
1.57 @@ -1186,6 +1179,26 @@
1.58    shows "invertible (transpose A)"
1.59    by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose)
1.60
1.61 +lemma vector_matrix_mul_assoc:
1.62 +  fixes v :: "('a::comm_semiring_1)^'n"
1.63 +  shows "(v v* M) v* N = v v* (M ** N)"
1.64 +proof -
1.65 +  from matrix_vector_mul_assoc
1.66 +  have "transpose N *v (transpose M *v v) = (transpose N ** transpose M) *v v" by fast
1.67 +  thus "(v v* M) v* N = v v* (M ** N)"
1.68 +    by (simp add: matrix_transpose_mul [symmetric])
1.69 +qed
1.70 +
1.71 +lemma matrix_scalar_vector_ac:
1.72 +  fixes A :: "real^('m::finite)^'n"
1.73 +  shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v"
1.74 +  by (metis matrix_vector_mult_scaleR transpose_scalar vector_scalar_matrix_ac vector_transpose_matrix)
1.75 +
1.76 +lemma scalar_matrix_vector_assoc:
1.77 +  fixes A :: "real^('m::finite)^'n"
1.78 +  shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v"
1.79 +  by (metis matrix_scalar_vector_ac matrix_vector_mult_scaleR)
1.80 +
1.81  text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
1.82
1.83  definition "rowvector v = (\<chi> i j. (v\$j))"
```