isabelle: src/HOL/ex/Pythagoras.thy@8f0ff2847ba8 (annotated)

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
62225 c8c48906b858 updated header; wenzelm parents: 61343 diff changeset	5	section "The Pythagorean Theorem"
59190 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
61343 5b5656a63bd6 isabelle update_cartouches; wenzelm parents: 59190 diff changeset	11	text \<open>Expressed in real numbers:\<close>
59190 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
61343 5b5656a63bd6 isabelle update_cartouches; wenzelm parents: 59190 diff changeset	20	text \<open>Expressed in vectors:\<close>
59190 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
62390 842917225d56 more canonical names nipkow parents: 62225 diff changeset	32	end

author	Simon Wimmer <wimmers@in.tum.de>
	Mon, 11 Mar 2024 21:31:18 +0100
changeset 79900	8f0ff2847ba8
parent 62390	842917225d56
permissions	-rw-r--r--