author paulson Fri Apr 27 12:38:30 2018 +0100 (16 months ago) changeset 68050 7eacc812ad1c parent 68045 ce8ad77cd3fa child 68051 68def9274939
minor typeclass generalisations and junk removal
```     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Apr 26 16:14:35 2018 +0100
1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Apr 27 12:38:30 2018 +0100
1.3 @@ -300,8 +300,6 @@
1.4          "box (vec a) (vec b) = {} \<longleftrightarrow> box a b = {}"
1.5    by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis)
1.6
1.7 -lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
1.8 -
1.9  lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
1.10    by (simp add: inner_axis' norm_eq_1)
1.11
1.12 @@ -314,12 +312,6 @@
1.13  lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
1.14    by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
1.15
1.16 -lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"
1.17 -  by (metis vector_mul_lcancel)
1.18 -
1.19 -lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
1.20 -  by (metis vector_mul_rcancel)
1.21 -
1.22  lemma component_le_norm_cart: "\<bar>x\$i\<bar> \<le> norm x"
1.24    apply (rule member_le_L2_set, simp_all)
1.25 @@ -604,7 +596,7 @@
1.26      sum.delta[OF finite] cong del: if_weak_cong)
1.27    done
1.28
1.29 -lemma matrix_vector_mul_component: "((A::real^_^_) *v x)\$k = (A\$k) \<bullet> x"
1.30 +lemma matrix_vector_mul_component: "(A *v x)\$k = (A\$k) \<bullet> x"
1.31    by (simp add: matrix_vector_mult_def inner_vec_def)
1.32
1.33  lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
1.34 @@ -643,12 +635,10 @@
1.35    by (metis transpose_transpose)
1.36
1.37  lemma matrix_mult_transpose_dot_column:
1.38 -  fixes A :: "real^'n^'n"
1.39    shows "transpose A ** A = (\<chi> i j. (column i A) \<bullet> (column j A))"
1.40    by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
1.41
1.42  lemma matrix_mult_transpose_dot_row:
1.43 -  fixes A :: "real^'n^'n"
1.44    shows "A ** transpose A = (\<chi> i j. (row i A) \<bullet> (row j A))"
1.45    by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
1.46
1.47 @@ -704,12 +694,11 @@
1.48  lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
1.49    by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
1.50
1.51 -lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
1.52 -  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
1.53 -      field_simps sum_distrib_left sum.distrib)
1.54 +lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::('a::real_algebra_1) ^ _))"
1.55 +  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum.distrib scaleR_right.sum)
1.56
1.57  lemma
1.58 -  fixes A :: "real^'n^'m"
1.59 +  fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
1.60    shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
1.61      and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
1.62    by (simp_all add: linear_linear linear_continuous_at linear_continuous_on matrix_vector_mul_linear)
1.63 @@ -795,7 +784,7 @@
1.64    by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
1.65
1.66  lemma scalar_invertible:
1.67 -  fixes A :: "real^'m^'n"
1.68 +  fixes A :: "('a::real_algebra_1)^'m^'n"
1.69    assumes "k \<noteq> 0" and "invertible A"
1.70    shows "invertible (k *\<^sub>R A)"
1.71  proof -
1.72 @@ -809,7 +798,7 @@
1.73  qed
1.74
1.75  lemma scalar_invertible_iff:
1.76 -  fixes A :: "real^'m^'n"
1.77 +  fixes A :: "('a::real_algebra_1)^'m^'n"
1.78    assumes "k \<noteq> 0" and "invertible A"
1.79    shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
1.80    by (simp add: assms scalar_invertible)
```
```     2.1 --- a/src/HOL/Analysis/Determinants.thy	Thu Apr 26 16:14:35 2018 +0100
2.2 +++ b/src/HOL/Analysis/Determinants.thy	Fri Apr 27 12:38:30 2018 +0100
2.3 @@ -804,21 +804,15 @@
2.4        unfolding invertible_right_inverse
2.5        unfolding matrix_right_invertible_independent_rows
2.6        by blast
2.7 -    have *: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b"
2.8 -      apply (drule_tac f="(+) (- a)" in cong[OF refl])
2.9 -      apply (simp only: ab_left_minus add.assoc[symmetric])
2.10 -      apply simp
2.11 -      done
2.12      have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
2.13 -      apply (rule vector_mul_lcancel_imp[OF ci])
2.14 -      using c ci  unfolding sum.remove[OF fU iU] sum_cmul
2.15 -      apply (auto simp add: field_simps *)
2.16 -      done
2.17 +      unfolding sum_cmul
2.18 +      using c ci