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
```