|
(* Title: HOL/ex/Pythagoras.thy
Author: Amine Chaieb
*)
section "The Pythagorean Theorem"
theory Pythagoras
imports Complex_Main
begin
text \<open>Expressed in real numbers:\<close>
lemma pythagoras_verbose:
"((A1::real) - B1) * (C1 - B1) + (A2 - B2) * (C2 - B2) = 0 \
(C1 - A1) * (C1 - A1) + (C2 - A2) * (C2 - A2) =
((B1 - A1) * (B1 - A1) + (B2 - A2) * (B2 - A2)) + (C1 - B1) * (C1 - B1) + (C2 - B2) * (C2 - B2)"
by algebra
text \<open>Expressed in vectors:\<close>
type_synonym point = "real \ real"
lemma pythagoras:
defines ort:"orthogonal \ (\(A::point) B. fst A * fst B + snd A * snd B = 0)"
and vc:"vector \ (\(A::point) B. (fst A - fst B, snd A - snd B))"
and vcn:"vecsqnorm \ (\A::point. fst A ^ 2 + snd A ^2)"
assumes o: "orthogonal (vector A B) (vector C B)"
shows "vecsqnorm(vector C A) = vecsqnorm(vector B A) + vecsqnorm(vector C B)"
using o unfolding ort vc vcn by (algebra add: fst_conv snd_conv)
end
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
