src/HOL/Analysis/Determinants.thy
 changeset 68143 58c9231c2937 parent 68138 c738f40e88d4 child 68263 e4e536a71e3d
```--- 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 \<open>Traces, Determinant of square matrices and some properties\<close>
@@ -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"
@@ -734,7 +734,7 @@
unfolding invertible_right_inverse matrix_right_invertible_independent_rows
by blast
have thr0: "- row i A = sum (\<lambda>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 \<in> vec.span {row j A| j. j \<noteq> 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 \<Rightarrow> 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 \<or> det Q = - 1"
proof -
-  have th: "\<And>x::'a. x = 1 \<or> x = - 1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x")
-  proof -
-    fix x:: 'a
-    have th0: "x * x - 1 = (x - 1) * (x + 1)"
-    have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0"
-      apply (subst eq_iff_diff_eq_0, simp)
-      done
-    have "x * x = 1 \<longleftrightarrow> x * x - 1 = 0"
-      by simp
-    also have "\<dots> \<longleftrightarrow> x = 1 \<or> 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"
-  then show ?thesis unfolding th .
+  then show ?thesis
qed

lemma orthogonal_transformation_det [simp]:
@@ -1268,98 +1250,40 @@

lemma isometry_sphere_extend:
fixes f:: "'a::real_inner \<Rightarrow> 'a"
-  assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1"
-    and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y"
+  assumes f1: "\<And>x. norm x = 1 \<Longrightarrow> norm (f x) = 1"
+    and fd1: "\<And>x y. \<lbrakk>norm x = 1; norm y = 1\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y"
shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> 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 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> 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 \<bullet> v = u' \<bullet> v' + v' \<bullet> u' - v \<bullet> u "
-    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 *
-      done
-  }
-  note th0 = this
-  let ?g = "\<lambda>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: "\<forall>x. norm x = 1 \<longrightarrow> ?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 \<noteq> 0"
-      then have "dist (?g x) (?g y) = dist x y"
-        apply (rule f1[rule_format])
-        done
-    }
-    moreover
-    {
-      assume "x \<noteq> 0" "y = 0"
-      then have "dist (?g x) (?g y) = dist x y"
-        apply (rule f1[rule_format])
-        done
-    }
-    moreover
-    {
-      assume z: "x \<noteq> 0" "y \<noteq> 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"
-    }
-    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 = "\<lambda>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 \<or> 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 \<open>auto simp: field_simps intro: f1 fd1[unfolded dist_norm]\<close>)
+  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 \<open>Rotation, reflection, rotoinversion\<close>```