921 fixes f :: "real ^'n \<Rightarrow> real ^'n::finite" |
921 fixes f :: "real ^'n \<Rightarrow> real ^'n::finite" |
922 assumes f0: "f 0 = 0" and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y" |
922 assumes f0: "f 0 = 0" and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y" |
923 shows "linear f" |
923 shows "linear f" |
924 proof- |
924 proof- |
925 {fix v w |
925 {fix v w |
926 {fix x note fd[rule_format, of x 0, unfolded dist_def f0 diff_0_right] } |
926 {fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] } |
927 note th0 = this |
927 note th0 = this |
928 have "f v \<bullet> f w = c^2 * (v \<bullet> w)" |
928 have "f v \<bullet> f w = c^2 * (v \<bullet> w)" |
929 unfolding dot_norm_neg dist_def[symmetric] |
929 unfolding dot_norm_neg dist_norm[symmetric] |
930 unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} |
930 unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} |
931 note fc = this |
931 note fc = this |
932 show ?thesis unfolding linear_def vector_eq |
932 show ?thesis unfolding linear_def vector_eq |
933 by (simp add: dot_lmult dot_ladd dot_rmult dot_radd fc ring_simps) |
933 by (simp add: dot_lmult dot_ladd dot_rmult dot_radd fc ring_simps) |
934 qed |
934 qed |
945 lemma orthogonal_transformation_isometry: |
945 lemma orthogonal_transformation_isometry: |
946 "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n::finite) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)" |
946 "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n::finite) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)" |
947 unfolding orthogonal_transformation |
947 unfolding orthogonal_transformation |
948 apply (rule iffI) |
948 apply (rule iffI) |
949 apply clarify |
949 apply clarify |
950 apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_def) |
950 apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_norm) |
951 apply (rule conjI) |
951 apply (rule conjI) |
952 apply (rule isometry_linear) |
952 apply (rule isometry_linear) |
953 apply simp |
953 apply simp |
954 apply simp |
954 apply simp |
955 apply clarify |
955 apply clarify |
956 apply (erule_tac x=v in allE) |
956 apply (erule_tac x=v in allE) |
957 apply (erule_tac x=0 in allE) |
957 apply (erule_tac x=0 in allE) |
958 by (simp add: dist_def) |
958 by (simp add: dist_norm) |
959 |
959 |
960 (* ------------------------------------------------------------------------- *) |
960 (* ------------------------------------------------------------------------- *) |
961 (* Can extend an isometry from unit sphere. *) |
961 (* Can extend an isometry from unit sphere. *) |
962 (* ------------------------------------------------------------------------- *) |
962 (* ------------------------------------------------------------------------- *) |
963 |
963 |
993 {assume "x = 0" "y = 0" |
993 {assume "x = 0" "y = 0" |
994 then have "dist (?g x) (?g y) = dist x y" by simp } |
994 then have "dist (?g x) (?g y) = dist x y" by simp } |
995 moreover |
995 moreover |
996 {assume "x = 0" "y \<noteq> 0" |
996 {assume "x = 0" "y \<noteq> 0" |
997 then have "dist (?g x) (?g y) = dist x y" |
997 then have "dist (?g x) (?g y) = dist x y" |
998 apply (simp add: dist_def norm_mul) |
998 apply (simp add: dist_norm norm_mul) |
999 apply (rule f1[rule_format]) |
999 apply (rule f1[rule_format]) |
1000 by(simp add: norm_mul field_simps)} |
1000 by(simp add: norm_mul field_simps)} |
1001 moreover |
1001 moreover |
1002 {assume "x \<noteq> 0" "y = 0" |
1002 {assume "x \<noteq> 0" "y = 0" |
1003 then have "dist (?g x) (?g y) = dist x y" |
1003 then have "dist (?g x) (?g y) = dist x y" |
1004 apply (simp add: dist_def norm_mul) |
1004 apply (simp add: dist_norm norm_mul) |
1005 apply (rule f1[rule_format]) |
1005 apply (rule f1[rule_format]) |
1006 by(simp add: norm_mul field_simps)} |
1006 by(simp add: norm_mul field_simps)} |
1007 moreover |
1007 moreover |
1008 {assume z: "x \<noteq> 0" "y \<noteq> 0" |
1008 {assume z: "x \<noteq> 0" "y \<noteq> 0" |
1009 have th00: "x = norm x *s (inverse (norm x) *s x)" "y = norm y *s (inverse (norm y) *s y)" "norm x *s f ((inverse (norm x) *s x)) = norm x *s f (inverse (norm x) *s x)" |
1009 have th00: "x = norm x *s (inverse (norm x) *s x)" "y = norm y *s (inverse (norm y) *s y)" "norm x *s f ((inverse (norm x) *s x)) = norm x *s f (inverse (norm x) *s x)" |
1013 "norm (inverse (norm y) *s y) = 1" |
1013 "norm (inverse (norm y) *s y) = 1" |
1014 "norm (f (inverse (norm y) *s y)) = 1" |
1014 "norm (f (inverse (norm y) *s y)) = 1" |
1015 "norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) = |
1015 "norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) = |
1016 norm (inverse (norm x) *s x - inverse (norm y) *s y)" |
1016 norm (inverse (norm x) *s x - inverse (norm y) *s y)" |
1017 using z |
1017 using z |
1018 by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def]) |
1018 by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_norm]) |
1019 from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" |
1019 from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" |
1020 by (simp add: dist_def)} |
1020 by (simp add: dist_norm)} |
1021 ultimately have "dist (?g x) (?g y) = dist x y" by blast} |
1021 ultimately have "dist (?g x) (?g y) = dist x y" by blast} |
1022 note thd = this |
1022 note thd = this |
1023 show ?thesis |
1023 show ?thesis |
1024 apply (rule exI[where x= ?g]) |
1024 apply (rule exI[where x= ?g]) |
1025 unfolding orthogonal_transformation_isometry |
1025 unfolding orthogonal_transformation_isometry |