Eine aufbereitete Darstellung der Quelle

 
     
 
 
Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 
Benutzer

products/Sources/formale Sprachen/C/Gnome/gtk/   (Gnome Linux Desktop Version 4.23.2©)  Datei vom 30.5.2026 mit Größe 8 kB image not shown  

Bilddatei

Angles.thy


products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Triangle/Angles.thy

(* File: Angles.thy Author: Manuel Eberl Definition of angles between vectors and between three points. *) section \Definition of angles\ theory Angles imports "HOL-Analysis.Multivariate_Analysis" begin lemma collinear_translate_iff: "collinear (((+) a) ` A) \ collinear A" by (auto simp: collinear_def) definition vangle where "vangle u v = (if u = 0 \ v = 0 then pi / 2 else arccos (u \ v / (norm u * norm v)))" definition angle where "angle a b c = vangle (a - b) (c - b)" lemma angle_altdef: "angle a b c = arccos ((a - b) \ (c - b) / (dist a b * dist c b))" by (simp add: angle_def vangle_def dist_norm) lemma vangle_0_left [simp]: "vangle 0 v = pi / 2" and vangle_0_right [simp]: "vangle u 0 = pi / 2" by (simp_all add: vangle_def) lemma vangle_refl [simp]: "u \ 0 \ vangle u u = 0" by (simp add: vangle_def dot_square_norm power2_eq_square) lemma angle_refl [simp]: "angle a a b = pi / 2" "angle a b b = pi / 2" by (simp_all add: angle_def) lemma angle_refl_mid [simp]: "a \ b \ angle a b a = 0" by (simp add: angle_def) lemma cos_vangle: "cos (vangle u v) = u \ v / (norm u * norm v)" unfolding vangle_def using Cauchy_Schwarz_ineq2[of u v] by (auto simp: field_simps) lemma cos_angle: "cos (angle a b c) = (a - b) \ (c - b) / (dist a b * dist c b)" by (simp add: angle_def cos_vangle dist_norm) lemma inner_conv_angle: "(a - b) \ (c - b) = dist a b * dist c b * cos (angle a b c)" by (simp add: cos_angle) lemma vangle_commute: "vangle u v = vangle v u" by (simp add: vangle_def inner_commute mult.commute) lemma angle_commute: "angle a b c = angle c b a" by (simp add: angle_def vangle_commute) lemma vangle_nonneg: "vangle u v \ 0" and vangle_le_pi: "vangle u v \ pi" using Cauchy_Schwarz_ineq2[of u v] by (auto simp: vangle_def field_simps intro!: arccos_lbound arccos_ubound) lemmas vangle_bounds = vangle_nonneg vangle_le_pi lemma angle_nonneg: "angle a b c \ 0" and angle_le_pi: "angle a b c \ pi" using vangle_bounds unfolding angle_def by blast+ lemmas angle_bounds = angle_nonneg angle_le_pi lemma sin_vangle_nonneg: "sin (vangle u v) \ 0" using vangle_bounds by (rule sin_ge_zero) lemma sin_angle_nonneg: "sin (angle a b c) \ 0" using angle_bounds by (rule sin_ge_zero) lemma vangle_eq_0D: assumes "vangle u v = 0" shows "norm u *\<^sub>R v = norm v *\<^sub>R u" proof - from assms have "u \ v = norm u * norm v" using arccos_eq_iff[of "(u \ v) / (norm u * norm v)" 1] Cauchy_Schwarz_ineq2[of u v] by (fastforce simp: vangle_def split: if_split_asm) thus ?thesis by (subst (asm) norm_cauchy_schwarz_eq) simp_all qed lemma vangle_eq_piD: assumes "vangle u v = pi" shows "norm u *\<^sub>R v + norm v *\<^sub>R u = 0" proof - from assms have "(-u) \ v = norm (-u) * norm v" using arccos_eq_iff[of "(u \ v) / (norm u * norm v)" "-1"] Cauchy_Schwarz_ineq2[of u v] by (simp add: field_simps vangle_def split: if_split_asm) thus ?thesis by (subst (asm) norm_cauchy_schwarz_eq) simp_all qed lemma dist_triangle_eq: fixes a b c :: "'a :: real_inner" shows "(dist a c = dist a b + dist b c) \ dist a b *\<^sub>R (c - b) + dist b c *\<^sub>R (a - b) = 0" using norm_triangle_eq[of "b - a" "c - b"] by (simp add: dist_norm norm_minus_commute algebra_simps) lemma angle_eq_pi_imp_dist_additive: assumes "angle a b c = pi" shows "dist a c = dist a b + dist b c" using vangle_eq_piD[OF assms[unfolded angle_def]] by (subst dist_triangle_eq) (simp add: dist_norm norm_minus_commute) lemma orthogonal_iff_vangle: "orthogonal u v \ vangle u v = pi / 2" using arccos_eq_iff[of "u \ v / (norm u * norm v)" 0] Cauchy_Schwarz_ineq2[of u v] by (auto simp: vangle_def orthogonal_def) lemma cos_minus1_imp_pi: assumes "cos x = -1" "x \ 0" "x < 3 * pi" shows "x = pi" proof - have "cos (x - pi) = 1" by (simp add: assms) then obtain n :: int where n: "of_int n = (x / pi - 1) / 2" by (subst (asm) cos_one_2pi_int) (auto simp: field_simps) also from assms have "\ \ {-1<..<1}" by (auto simp: field_simps) finally have "n = 0" by simp with n show ?thesis by simp qed lemma vangle_eqI: assumes "u \ 0" "v \ 0" "w \ 0" "x \ 0" assumes "(u \ v) * norm w * norm x = (w \ x) * norm u * norm v" shows "vangle u v = vangle w x" using assms Cauchy_Schwarz_ineq2[of u v] Cauchy_Schwarz_ineq2[of w x] unfolding vangle_def by (auto simp: arccos_eq_iff field_simps) lemma angle_eqI: assumes "a \ b" "a \ c" "d \ e" "d \ f" assumes "((b-a) \ (c-a)) * dist d e * dist d f = ((e-d) \ (f-d)) * dist a b * dist a c" shows "angle b a c = angle e d f" using assms unfolding angle_def by (intro vangle_eqI) (simp_all add: dist_norm norm_minus_commute) lemma cos_vangle_eqD: "cos (vangle u v) = cos (vangle w x) \ vangle u v = vangle w x" by (rule cos_inj_pi) (simp_all add: vangle_bounds) lemma cos_angle_eqD: "cos (angle a b c) = cos (angle d e f) \ angle a b c = angle d e f" unfolding angle_def by (rule cos_vangle_eqD) lemma sin_vangle_zero_iff: "sin (vangle u v) = 0 \ vangle u v \ {0, pi}" proof assume "sin (vangle u v) = 0" then obtain n :: int where n: "of_int n = vangle u v / pi" by (subst (asm) sin_zero_iff_int2) auto also have "\ \ {0..1}" using vangle_bounds by (auto simp: field_simps) finally have "n \ {0,1}" by auto thus "vangle u v \ {0,pi}" using n by (auto simp: field_simps) qed auto lemma sin_angle_zero_iff: "sin (angle a b c) = 0 \ angle a b c \ {0, pi}" unfolding angle_def by (simp only: sin_vangle_zero_iff) lemma vangle_collinear: "vangle u v \ {0, pi} \ collinear {0, u, v}" apply (subst norm_cauchy_schwarz_equal [symmetric]) apply (subst norm_cauchy_schwarz_abs_eq) apply (auto dest!: vangle_eq_0D vangle_eq_piD simp: eq_neg_iff_add_eq_0) done lemma angle_collinear: "angle a b c \ {0, pi} \ collinear {a, b, c}" apply (unfold angle_def, drule vangle_collinear) apply (subst collinear_translate_iff[symmetric, of _ "-b"]) apply (auto simp: insert_commute) done lemma not_collinear_vangle: "\collinear {0,u,v} \ vangle u v \ {0<.. vangle u v = pi") auto lemma not_collinear_angle: "\collinear {a,b,c} \ angle a b c \ {0<.. angle a b c = pi") auto subsection\Contributions from Lukas Bulwahn\ lemma vangle_scales: assumes "0 < c" shows "vangle (c *\<^sub>R v\<^sub>1) v\<^sub>2 = vangle v\<^sub>1 v\<^sub>2" using assms unfolding vangle_def by auto lemma vangle_inverse: "vangle (- v\<^sub>1) v\<^sub>2 = pi - vangle v\<^sub>1 v\<^sub>2" proof - have "\v\<^sub>1 \ v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\ \ 1" proof cases assume "v\<^sub>1 \ 0 \ v\<^sub>2 \ 0" from this show ?thesis by (simp add: Cauchy_Schwarz_ineq2) next assume "\ (v\<^sub>1 \ 0 \ v\<^sub>2 \ 0)" from this show ?thesis by auto qed from this show ?thesis unfolding vangle_def by (simp add: arccos_minus_abs) qed lemma orthogonal_iff_angle: shows "orthogonal (A - B) (C - B) \ angle A B C = pi / 2" unfolding angle_def by (auto simp only: orthogonal_iff_vangle) lemma angle_inverse: assumes "between (A, C) B" assumes "A \ B" "B \ C" shows "angle A B D = pi - angle C B D" proof - from \between (A, C) B\ obtain u where u: "u \ 0" "u \ 1" and X: "B = u *\<^sub>R A + (1 - u) *\<^sub>R C" by (metis add.commute betweenE between_commute) from \A \ B\ \B \ C\ X have "u \ 0" "u \ 1" by auto have "0 < ((1 - u) / u)" using \u \ 0\ \u \ 1\ \u \ 0\ \u \ 1\ by simp from X have "A - B = - (1 - u) *\<^sub>R (C - A)" by (simp add: real_vector.scale_right_diff_distrib real_vector.scale_left_diff_distrib) moreover from X have "C - B = u *\<^sub>R (C - A)" by (simp add: scaleR_diff_left real_vector.scale_right_diff_distrib) ultimately have "A - B = - (((1 - u) / u) *\<^sub>R (C - B))" using \u \ 0\ by simp (metis minus_diff_eq real_vector.scale_minus_left) from this have "vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)" using \0 < (1 - u) / u\ by (simp add: vangle_inverse vangle_scales) from this show ?thesis unfolding angle_def by simp qed lemma strictly_between_implies_angle_eq_pi: assumes "between (A, C) B" assumes "A \ B" "B \ C" shows "angle A B C = pi" proof - from \between (A, C) B\ obtain u where u: "u \ 0" "u \ 1" and X: "B = u *\<^sub>R A + (1 - u) *\<^sub>R C" by (metis add.commute betweenE between_commute) from \A \ B\ \B \ C\ X have "u \ 0" "u \ 1" by auto from \A \ B\ \B \ C\ \between (A, C) B\ have "A \ C" by auto from X have "A - B = - (1 - u) *\<^sub>R (C - A)" by (simp add: real_vector.scale_right_diff_distrib real_vector.scale_left_diff_distrib) moreover from this have "dist A B = norm ((1 - u) *\<^sub>R (C - A))" using \u \ 0\ \u \ 1\ by (simp add: dist_norm) moreover from X have "C - B = u *\<^sub>R (C - A)" by (simp add: scaleR_diff_left real_vector.scale_right_diff_distrib) moreover from this have "dist C B = norm (u *\<^sub>R (C - A))" by (simp add: dist_norm) ultimately have "(A - B) \ (C - B) / (dist A B * dist C B) = u * (u - 1) / (\1 - u\ * \u\)" using \A \ C\ by (simp add: dot_square_norm power2_eq_square) also have "\ = - 1" using \u \ 0\ \u \ 1\ \u \ 0\ \u \ 1\ by (simp add: divide_eq_minus_1_iff) finally show ?thesis unfolding angle_altdef by simp qed end

                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Open Source Software

     Quellcodebibliothek
     Eigene Quellcodes
     Fremde Quellcodes
     Suchen
Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik
Statistik
#Sources=1126438
#Domains=1897691