# HG changeset patch # User paulson # Date 1525986231 -3600 # Node ID 58c9231c293754572151adca8225d56c554625d5 # Parent 53b4e204755e22ce367db1326beaefeebfefea4b tidied some messy proofs diff -r 53b4e204755e -r 58c9231c2937 src/HOL/Analysis/Determinants.thy --- a/src/HOL/Analysis/Determinants.thy Thu May 10 18:17:55 2018 +0200 +++ b/src/HOL/Analysis/Determinants.thy Thu May 10 22:03:51 2018 +0100 @@ -1,5 +1,5 @@ (* Title: HOL/Analysis/Determinants.thy - Author: Amine Chaieb, University of Cambridge + Author: Amine Chaieb, University of Cambridge; proofs reworked by LCP *) section \Traces, Determinant of square matrices and some properties\ @@ -202,7 +202,7 @@ apply (subst sum_permutations_compose_right[OF p]) apply (rule *) done -qed +qed lemma det_permute_columns: fixes A :: "'a::comm_ring_1^'n^'n" @@ -447,7 +447,7 @@ unfolding thz step.IH det_row_mul[of i] det_row_add[of i] by simp then show ?case unfolding scalar_mult_eq_scaleR . -qed +qed lemma matrix_id [simp]: "det (matrix id) = 1" by (simp add: matrix_id_mat_1) @@ -734,7 +734,7 @@ unfolding invertible_right_inverse matrix_right_invertible_independent_rows by blast have thr0: "- row i A = sum (\j. (1/ c i) *s (c j *s row j A)) (?U - {i})" - unfolding sum_cmul using c ci + unfolding sum_cmul using c ci by (auto simp: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff) have thr: "- row i A \ vec.span {row j A| j. j \ i}" unfolding thr0 by (auto intro: vec.span_base vec.span_scale vec.span_sum) @@ -1011,14 +1011,10 @@ lemma orthogonal_matrix_mul: fixes A :: "real ^'n^'n" - assumes oA : "orthogonal_matrix A" - and oB: "orthogonal_matrix B" + assumes "orthogonal_matrix A" "orthogonal_matrix B" shows "orthogonal_matrix(A ** B)" - using oA oB - unfolding orthogonal_matrix matrix_transpose_mul - apply (subst matrix_mul_assoc) - apply (subst matrix_mul_assoc[symmetric], simp) - done + using assms + by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc) lemma orthogonal_transformation_matrix: fixes f:: "real^'n \ real^'n" @@ -1058,9 +1054,8 @@ { assume lf: "Vector_Spaces.linear ( *s) ( *s) f" and om: "orthogonal_matrix ?mf" from lf om have ?lhs - apply (simp only: orthogonal_matrix_def norm_eq orthogonal_transformation) - apply (simp only: matrix_works[OF lf, symmetric]) - apply (subst dot_matrix_vector_mul) + unfolding orthogonal_matrix_def norm_eq orthogonal_transformation + apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul) apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR) done } @@ -1073,27 +1068,14 @@ assumes oQ: "orthogonal_matrix Q" shows "det Q = 1 \ det Q = - 1" proof - - have th: "\x::'a. x = 1 \ x = - 1 \ x*x = 1" (is "\x::'a. ?ths x") - proof - - fix x:: 'a - have th0: "x * x - 1 = (x - 1) * (x + 1)" - by (simp add: field_simps) - have th1: "\(x::'a) y. x = - y \ x + y = 0" - apply (subst eq_iff_diff_eq_0, simp) - done - have "x * x = 1 \ x * x - 1 = 0" - by simp - also have "\ \ x = 1 \ x = - 1" - unfolding th0 th1 by simp - finally show "?ths x" .. - qed - from oQ have "Q ** transpose Q = mat 1" - by (metis orthogonal_matrix_def) + have "Q ** transpose Q = mat 1" + by (metis oQ orthogonal_matrix_def) then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" by simp then have "det Q * det Q = 1" by (simp add: det_mul) - then show ?thesis unfolding th . + then show ?thesis + by (simp add: square_eq_1_iff) qed lemma orthogonal_transformation_det [simp]: @@ -1268,98 +1250,40 @@ lemma isometry_sphere_extend: fixes f:: "'a::real_inner \ 'a" - assumes f1: "\x. norm x = 1 \ norm (f x) = 1" - and fd1: "\ x y. norm x = 1 \ norm y = 1 \ dist (f x) (f y) = dist x y" + assumes f1: "\x. norm x = 1 \ norm (f x) = 1" + and fd1: "\x y. \norm x = 1; norm y = 1\ \ dist (f x) (f y) = dist x y" shows "\g. orthogonal_transformation g \ (\x. norm x = 1 \ g x = f x)" proof - { - fix x y x' y' x0 y0 x0' y0' :: "'a" - assume H: - "x = norm x *\<^sub>R x0" - "y = norm y *\<^sub>R y0" - "x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'" - "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1" - "norm(x0' - y0') = norm(x0 - y0)" - then have *: "x0 \ y0 = x0' \ y0' + y0' \ x0' - y0 \ x0 " + fix x y x' y' u v u' v' :: "'a" + assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v" + "x' = norm x *\<^sub>R u'" "y' = norm y *\<^sub>R v'" + and J: "norm u = 1" "norm u' = 1" "norm v = 1" "norm v' = 1" "norm(u' - v') = norm(u - v)" + then have *: "u \ v = u' \ v' + v' \ u' - v \ u " by (simp add: norm_eq norm_eq_1 inner_add inner_diff) - have "norm(x' - y') = norm(x - y)" - apply (subst H(1)) - apply (subst H(2)) - apply (subst H(3)) - apply (subst H(4)) - using H(5-9) - apply (simp add: norm_eq norm_eq_1) - apply (simp add: inner_diff scalar_mult_eq_scaleR) - unfolding * - apply (simp add: field_simps) - done - } - note th0 = this - let ?g = "\x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" - { - fix x:: "'a" - assume nx: "norm x = 1" - have "?g x = f x" - using nx by auto + have "norm (norm x *\<^sub>R u' - norm y *\<^sub>R v') = norm (norm x *\<^sub>R u - norm y *\<^sub>R v)" + using J by (simp add: norm_eq norm_eq_1 inner_diff * field_simps) + then have "norm(x' - y') = norm(x - y)" + using H by metis } - then have thfg: "\x. norm x = 1 \ ?g x = f x" - by blast - have g0: "?g 0 = 0" - by simp - { - fix x y :: "'a" - { - assume "x = 0" "y = 0" - then have "dist (?g x) (?g y) = dist x y" - by simp - } - moreover - { - assume "x = 0" "y \ 0" - then have "dist (?g x) (?g y) = dist x y" - apply (simp add: dist_norm) - apply (rule f1[rule_format]) - apply (simp add: field_simps) - done - } - moreover - { - assume "x \ 0" "y = 0" - then have "dist (?g x) (?g y) = dist x y" - apply (simp add: dist_norm) - apply (rule f1[rule_format]) - apply (simp add: field_simps) - done - } - moreover - { - assume z: "x \ 0" "y \ 0" - have th00: - "x = norm x *\<^sub>R (inverse (norm x) *\<^sub>R x)" - "y = norm y *\<^sub>R (inverse (norm y) *\<^sub>R y)" - "norm x *\<^sub>R f ((inverse (norm x) *\<^sub>R x)) = norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" - "norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y) = norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y)" - "norm (inverse (norm x) *\<^sub>R x) = 1" - "norm (f (inverse (norm x) *\<^sub>R x)) = 1" - "norm (inverse (norm y) *\<^sub>R y) = 1" - "norm (f (inverse (norm y) *\<^sub>R y)) = 1" - "norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) = - norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)" - using z - by (auto simp: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm]) - from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" - by (simp add: dist_norm) - } - ultimately have "dist (?g x) (?g y) = dist x y" - by blast - } - note thd = this - show ?thesis - apply (rule exI[where x= ?g]) + note norm_eq = this + let ?g = "\x. if x = 0 then 0 else norm x *\<^sub>R f (x /\<^sub>R norm x)" + have thfg: "?g x = f x" if "norm x = 1" for x + using that by auto + have thd: "dist (?g x) (?g y) = dist x y" for x y + proof (cases "x=0 \ y=0") + case False + show "dist (?g x) (?g y) = dist x y" + unfolding dist_norm + proof (rule norm_eq) + show "x = norm x *\<^sub>R (x /\<^sub>R norm x)" "y = norm y *\<^sub>R (y /\<^sub>R norm y)" + "norm (f (x /\<^sub>R norm x)) = 1" "norm (f (y /\<^sub>R norm y)) = 1" + using False f1 by auto + qed (use False in \auto simp: field_simps intro: f1 fd1[unfolded dist_norm]\) + qed (auto simp: f1) + show ?thesis unfolding orthogonal_transformation_isometry - using g0 thfg thd - apply metis - done + by (rule exI[where x= ?g]) (metis thfg thd) qed subsection \Rotation, reflection, rotoinversion\