minor typeclass generalisations and junk removal
authorpaulson <lp15@cam.ac.uk>
Fri Apr 27 12:38:30 2018 +0100 (16 months ago)
changeset 680507eacc812ad1c
parent 68045 ce8ad77cd3fa
child 68051 68def9274939
minor typeclass generalisations and junk removal
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Determinants.thy
     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.23    apply (simp add: norm_vec_def)
    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   
    2.19 +      by (auto simp add: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
    2.20      have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
    2.21        unfolding thr0
    2.22        apply (rule span_sum)
    2.23        apply simp
    2.24 -      apply (rule span_mul [where 'a="real^'n"])
    2.25 +      apply (rule span_mul)
    2.26        apply (rule span_superset)
    2.27        apply auto
    2.28        done