| author | Rene Thiemann <rene.thiemann@uibk.ac.at> |
| Fri, 17 Apr 2015 11:52:36 +0200 | |
| changeset 60112 | 3eab4acaa035 |
| parent 59190 | 3a594fd13ca4 |
| child 61343 | 5b5656a63bd6 |
| permissions | -rw-r--r-- |
|
59190
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/Pythagoras.thy |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
2 |
Author: Amine Chaieb |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
3 |
*) |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
4 |
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
5 |
header "The Pythagorean Theorem" |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
6 |
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
7 |
theory Pythagoras |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
8 |
imports Complex_Main |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
9 |
begin |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
10 |
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
11 |
text {* Expressed in real numbers: *}
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
12 |
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
13 |
lemma pythagoras_verbose: |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
14 |
"((A1::real) - B1) * (C1 - B1) + (A2 - B2) * (C2 - B2) = 0 \<Longrightarrow> |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
15 |
(C1 - A1) * (C1 - A1) + (C2 - A2) * (C2 - A2) = |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
16 |
((B1 - A1) * (B1 - A1) + (B2 - A2) * (B2 - A2)) + (C1 - B1) * (C1 - B1) + (C2 - B2) * (C2 - B2)" |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
17 |
by algebra |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
18 |
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
19 |
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
20 |
text {* Expressed in vectors: *}
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
21 |
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
22 |
type_synonym point = "real \<times> real" |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
23 |
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
24 |
lemma pythagoras: |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
25 |
defines ort:"orthogonal \<equiv> (\<lambda>(A::point) B. fst A * fst B + snd A * snd B = 0)" |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
26 |
and vc:"vector \<equiv> (\<lambda>(A::point) B. (fst A - fst B, snd A - snd B))" |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
27 |
and vcn:"vecsqnorm \<equiv> (\<lambda>A::point. fst A ^ 2 + snd A ^2)" |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
28 |
assumes o: "orthogonal (vector A B) (vector C B)" |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
29 |
shows "vecsqnorm(vector C A) = vecsqnorm(vector B A) + vecsqnorm(vector C B)" |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
30 |
using o unfolding ort vc vcn by (algebra add: fst_conv snd_conv) |
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
31 |
|
|
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
diff
changeset
|
32 |
end |