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.42              by (simp add: sum.distrib)
    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))"