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;
 kleing@59190 ` 1` ```(* Title: HOL/ex/Pythagoras.thy ``` kleing@59190 ` 2` ``` Author: Amine Chaieb ``` kleing@59190 ` 3` ```*) ``` kleing@59190 ` 4` wenzelm@62225 ` 5` ```section "The Pythagorean Theorem" ``` kleing@59190 ` 6` kleing@59190 ` 7` ```theory Pythagoras ``` kleing@59190 ` 8` ```imports Complex_Main ``` kleing@59190 ` 9` ```begin ``` kleing@59190 ` 10` wenzelm@61343 ` 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 \ ``` 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` wenzelm@61343 ` 20` ```text \Expressed in vectors:\ ``` kleing@59190 ` 21` kleing@59190 ` 22` ```type_synonym point = "real \ real" ``` kleing@59190 ` 23` kleing@59190 ` 24` ```lemma pythagoras: ``` kleing@59190 ` 25` ``` defines ort:"orthogonal \ (\(A::point) B. fst A * fst B + snd A * snd B = 0)" ``` kleing@59190 ` 26` ``` and vc:"vector \ (\(A::point) B. (fst A - fst B, snd A - snd B))" ``` kleing@59190 ` 27` ``` and vcn:"vecsqnorm \ (\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` ``` ``` nipkow@62390 ` 32` ``` end ```