# HG changeset patch
# User immler
# Date 1519829585 -3600
# Node ID 346cb74e79f637e241dcd690915890e8a40cbabe
# Parent  f91c437f6f6893ea911a4fde572cbf94524b7f64
generalized lemmas about orthogonal transformation

diff -r f91c437f6f68 -r 346cb74e79f6 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Mon Feb 26 11:52:53 2018 +0000
+++ b/src/HOL/Analysis/Determinants.thy	Wed Feb 28 15:53:05 2018 +0100
@@ -934,7 +934,7 @@
 definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
 
 lemma orthogonal_transformation:
-  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>(v::real ^_). norm (f v) = norm v)"
+  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"
   unfolding orthogonal_transformation_def
   apply auto
   apply (erule_tac x=v in allE)+
@@ -957,8 +957,7 @@
   by (simp add: orthogonal_transformation_def linear_compose)
 
 lemma orthogonal_transformation_neg:
-  fixes f :: "real^'n \<Rightarrow> real^'n"
-  shows "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
+  "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
   by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
 
 lemma orthogonal_transformation_linear:
@@ -966,28 +965,27 @@
   by (simp add: orthogonal_transformation_def)
 
 lemma orthogonal_transformation_inj:
-  fixes f :: "real^'n \<Rightarrow> real^'n"
-  shows "orthogonal_transformation f \<Longrightarrow> inj f"
-  unfolding orthogonal_transformation_def inj_on_def by (metis euclidean_eqI)
+  "orthogonal_transformation f \<Longrightarrow> inj f"
+  unfolding orthogonal_transformation_def inj_on_def
+  by (metis vector_eq)
 
 lemma orthogonal_transformation_surj:
-  fixes f :: "real^'n \<Rightarrow> real^'n"
-  shows "orthogonal_transformation f \<Longrightarrow> surj f"
+  "orthogonal_transformation f \<Longrightarrow> surj f"
+  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
 
 lemma orthogonal_transformation_bij:
-  fixes f :: "real^'n \<Rightarrow> real^'n"
-  shows "orthogonal_transformation f \<Longrightarrow> bij f"
+  "orthogonal_transformation f \<Longrightarrow> bij f"
+  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
 
 lemma orthogonal_transformation_inv:
-  fixes f :: "real^'n \<Rightarrow> real^'n"
-  shows "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
+  "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
+  for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
 
 lemma orthogonal_transformation_norm:
-  fixes f :: "real^'n \<Rightarrow> real^'n"
-  shows "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
+  "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
   by (metis orthogonal_transformation)
 
 lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
@@ -1092,7 +1090,7 @@
 subsection \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
 
 lemma scaling_linear:
-  fixes f :: "real ^'n \<Rightarrow> real ^'n"
+  fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
   assumes f0: "f 0 = 0"
     and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
   shows "linear f"
@@ -1109,18 +1107,18 @@
       unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
   note fc = this
   show ?thesis
-    unfolding linear_iff vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR
+    unfolding linear_iff vector_eq[where 'a="'a"] scalar_mult_eq_scaleR
     by (simp add: inner_add fc field_simps)
 qed
 
 lemma isometry_linear:
-  "f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
+  "f (0::'a::real_inner) = (0::'a) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
   by (rule scaling_linear[where c=1]) simp_all
 
 text \<open>Hence another formulation of orthogonal transformation.\<close>
 
 lemma orthogonal_transformation_isometry:
-  "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
+  "orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
   unfolding orthogonal_transformation
   apply (auto simp: linear_0 isometry_linear)
    apply (metis (no_types, hide_lams) dist_norm linear_diff)
@@ -1128,7 +1126,7 @@
 
 
 lemma image_orthogonal_transformation_ball:
-  fixes f :: "real^'n \<Rightarrow> real^'n"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   assumes "orthogonal_transformation f"
   shows "f ` ball x r = ball (f x) r"
 proof (intro equalityI subsetI)
@@ -1144,7 +1142,7 @@
 qed
 
 lemma image_orthogonal_transformation_cball:
-  fixes f :: "real^'n \<Rightarrow> real^'n"
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   assumes "orthogonal_transformation f"
   shows "f ` cball x r = cball (f x) r"
 proof (intro equalityI subsetI)
@@ -1234,7 +1232,7 @@
 proof (cases "a = 0 \<or> b = 0")
   case True
   with assms show ?thesis
-    using orthogonal_transformation_isometry that by fastforce
+    using that by force
 next
   case False
   then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
@@ -1256,13 +1254,13 @@
 subsection \<open>Can extend an isometry from unit sphere.\<close>
 
 lemma isometry_sphere_extend:
-  fixes f:: "real ^'n \<Rightarrow> real ^'n"
+  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"
   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' :: "real ^'n"
+    fix x y x' y' x0 y0 x0' y0' :: "'a"
     assume H:
       "x = norm x *\<^sub>R x0"
       "y = norm y *\<^sub>R y0"
@@ -1286,7 +1284,7 @@
   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:: "real ^'n"
+    fix x:: "'a"
     assume nx: "norm x = 1"
     have "?g x = f x"
       using nx by auto
@@ -1296,7 +1294,7 @@
   have g0: "?g 0 = 0"
     by simp
   {
-    fix x y :: "real ^'n"
+    fix x y :: "'a"
     {
       assume "x = 0" "y = 0"
       then have "dist (?g x) (?g y) = dist x y"