author paulson Fri, 27 Apr 2018 12:43:05 +0100 changeset 68051 68def9274939 parent 68049 1df89db6f162 (current diff) parent 68050 7eacc812ad1c (diff) child 68052 e98988801fa9 child 68064 b249fab48c76
merged
```--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Apr 26 22:47:22 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Apr 27 12:43:05 2018 +0100
@@ -300,8 +300,6 @@
"box (vec a) (vec b) = {} \<longleftrightarrow> box a b = {}"
by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis)

-lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
-
lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"

@@ -314,12 +312,6 @@
lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)

-lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"
-  by (metis vector_mul_lcancel)
-
-lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
-  by (metis vector_mul_rcancel)
-
lemma component_le_norm_cart: "\<bar>x\$i\<bar> \<le> norm x"
apply (rule member_le_L2_set, simp_all)
@@ -604,7 +596,7 @@
sum.delta[OF finite] cong del: if_weak_cong)
done

-lemma matrix_vector_mul_component: "((A::real^_^_) *v x)\$k = (A\$k) \<bullet> x"
+lemma matrix_vector_mul_component: "(A *v x)\$k = (A\$k) \<bullet> x"

lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
@@ -643,12 +635,10 @@
by (metis transpose_transpose)

lemma matrix_mult_transpose_dot_column:
-  fixes A :: "real^'n^'n"
shows "transpose A ** A = (\<chi> i j. (column i A) \<bullet> (column j A))"
by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)

lemma matrix_mult_transpose_dot_row:
-  fixes A :: "real^'n^'n"
shows "A ** transpose A = (\<chi> i j. (row i A) \<bullet> (row j A))"
by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)

@@ -704,12 +694,11 @@
lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)

-lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
-  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
-      field_simps sum_distrib_left sum.distrib)
+lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::('a::real_algebra_1) ^ _))"
+  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum.distrib scaleR_right.sum)

lemma
-  fixes A :: "real^'n^'m"
+  fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
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)
@@ -795,7 +784,7 @@
by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)

lemma scalar_invertible:
-  fixes A :: "real^'m^'n"
+  fixes A :: "('a::real_algebra_1)^'m^'n"
assumes "k \<noteq> 0" and "invertible A"
shows "invertible (k *\<^sub>R A)"
proof -
@@ -809,7 +798,7 @@
qed

lemma scalar_invertible_iff:
-  fixes A :: "real^'m^'n"
+  fixes A :: "('a::real_algebra_1)^'m^'n"
assumes "k \<noteq> 0" and "invertible A"
shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
```--- a/src/HOL/Analysis/Determinants.thy	Thu Apr 26 22:47:22 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy	Fri Apr 27 12:43:05 2018 +0100
@@ -804,21 +804,15 @@
unfolding invertible_right_inverse
unfolding matrix_right_invertible_independent_rows
by blast
-    have *: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b"
-      apply (drule_tac f="(+) (- a)" in cong[OF refl])
-      apply (simp only: ab_left_minus add.assoc[symmetric])
-      apply simp
-      done
have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
-      apply (rule vector_mul_lcancel_imp[OF ci])
-      using c ci  unfolding sum.remove[OF fU iU] sum_cmul
-      apply (auto simp add: field_simps *)
-      done
+      unfolding sum_cmul
+      using c ci