src/HOL/ex/Pythagoras.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 62390 842917225d56
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/ex/Pythagoras.thy
     2     Author:     Amine Chaieb
     3 *)
     4 
     5 section "The Pythagorean Theorem"
     6 
     7 theory Pythagoras
     8 imports Complex_Main
     9 begin
    10 
    11 text \<open>Expressed in real numbers:\<close>
    12 
    13 lemma pythagoras_verbose:
    14   "((A1::real) - B1) * (C1 - B1) + (A2 - B2) * (C2 - B2) = 0 \<Longrightarrow> 
    15   (C1 - A1) * (C1 - A1) + (C2 - A2) * (C2 - A2) =
    16   ((B1 - A1) * (B1 - A1) + (B2 - A2) * (B2 - A2)) + (C1 - B1) * (C1 - B1) + (C2 - B2) * (C2 - B2)"
    17   by algebra
    18 
    19 
    20 text \<open>Expressed in vectors:\<close>
    21 
    22 type_synonym point = "real \<times> real"
    23 
    24 lemma pythagoras: 
    25   defines ort:"orthogonal \<equiv> (\<lambda>(A::point) B. fst A * fst B + snd A * snd B = 0)"
    26        and vc:"vector \<equiv> (\<lambda>(A::point) B. (fst A  - fst B, snd A - snd B))"
    27       and vcn:"vecsqnorm \<equiv> (\<lambda>A::point. fst A ^ 2 + snd A ^2)"
    28  assumes o: "orthogonal (vector A B) (vector C B)"
    29  shows "vecsqnorm(vector C A) = vecsqnorm(vector B  A) + vecsqnorm(vector C B)"
    30    using o unfolding ort vc vcn by (algebra add: fst_conv snd_conv)
    31  
    32  end