src/HOL/ex/Pythagoras.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 59190 3a594fd13ca4
child 61343 5b5656a63bd6
permissions -rw-r--r--
prefer symbols;
kleing@59190
     1
(*  Title:      HOL/ex/Pythagoras.thy
kleing@59190
     2
    Author:     Amine Chaieb
kleing@59190
     3
*)
kleing@59190
     4
kleing@59190
     5
header "The Pythagorean Theorem"
kleing@59190
     6
kleing@59190
     7
theory Pythagoras
kleing@59190
     8
imports Complex_Main
kleing@59190
     9
begin
kleing@59190
    10
kleing@59190
    11
text {* Expressed in real numbers: *}
kleing@59190
    12
kleing@59190
    13
lemma pythagoras_verbose:
kleing@59190
    14
  "((A1::real) - B1) * (C1 - B1) + (A2 - B2) * (C2 - B2) = 0 \<Longrightarrow> 
kleing@59190
    15
  (C1 - A1) * (C1 - A1) + (C2 - A2) * (C2 - A2) =
kleing@59190
    16
  ((B1 - A1) * (B1 - A1) + (B2 - A2) * (B2 - A2)) + (C1 - B1) * (C1 - B1) + (C2 - B2) * (C2 - B2)"
kleing@59190
    17
  by algebra
kleing@59190
    18
kleing@59190
    19
kleing@59190
    20
text {* Expressed in vectors: *}
kleing@59190
    21
kleing@59190
    22
type_synonym point = "real \<times> real"
kleing@59190
    23
kleing@59190
    24
lemma pythagoras: 
kleing@59190
    25
  defines ort:"orthogonal \<equiv> (\<lambda>(A::point) B. fst A * fst B + snd A * snd B = 0)"
kleing@59190
    26
       and vc:"vector \<equiv> (\<lambda>(A::point) B. (fst A  - fst B, snd A - snd B))"
kleing@59190
    27
      and vcn:"vecsqnorm \<equiv> (\<lambda>A::point. fst A ^ 2 + snd A ^2)"
kleing@59190
    28
 assumes o: "orthogonal (vector A B) (vector C B)"
kleing@59190
    29
 shows "vecsqnorm(vector C A) = vecsqnorm(vector B  A) + vecsqnorm(vector C B)"
kleing@59190
    30
   using o unfolding ort vc vcn by (algebra add: fst_conv snd_conv)
kleing@59190
    31
 
kleing@59190
    32
 end