src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 66804 3f9bb52082c4
parent 66447 a1f5c5c26fa6
child 67155 9e5b05d54f9d
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -518,14 +518,14 @@
     1.4  
     1.5  lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
     1.6    apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
     1.7 -  apply (subst sum.commute)
     1.8 +  apply (subst sum.swap)
     1.9    apply simp
    1.10    done
    1.11  
    1.12  lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
    1.13    apply (vector matrix_matrix_mult_def matrix_vector_mult_def
    1.14      sum_distrib_left sum_distrib_right mult.assoc)
    1.15 -  apply (subst sum.commute)
    1.16 +  apply (subst sum.swap)
    1.17    apply simp
    1.18    done
    1.19  
    1.20 @@ -556,7 +556,7 @@
    1.21  
    1.22  lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
    1.23    apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
    1.24 -  apply (subst sum.commute)
    1.25 +  apply (subst sum.swap)
    1.26    apply simp
    1.27    done
    1.28  
    1.29 @@ -659,7 +659,7 @@
    1.30    apply (rule adjoint_unique)
    1.31    apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
    1.32      sum_distrib_right sum_distrib_left)
    1.33 -  apply (subst sum.commute)
    1.34 +  apply (subst sum.swap)
    1.35    apply (auto simp add: ac_simps)
    1.36    done
    1.37