Theory GeneralTriangle

Up to index of Isabelle/HOL/General-Triangle

theory GeneralTriangle
imports Complex_Main
`theory GeneralTriangleimports Complex_Mainbeginsection {* Type definitions *}text {* Since we are only considering acute-angled triangles, we define @{textangles} as numbers from the real interval \$[0\ldots 90]\$. *}abbreviation "angles ≡ { x::real . 0 ≤ x ∧ x ≤ 90 }"text {* Triangles are represented as lists consisting of exactly three angleswhich add up to 180\textdegree. As we consider triangles up to similarity, weassume the angles to be given in ascending order.Isabelle expects us to prove that the type is not empty, which we do by an example.*}definition  "triangle =    { l . l ∈ lists angles ∧                     length l = 3 ∧                    listsum l = 180 ∧                    sorted l                    }"typedef triangle = triangle  unfolding triangle_def  apply (rule_tac x = "[45,45,90]" in exI)  apply auto  donetext {* For convenience, the following lemma gives us easy access to the three anglesof a triangle and their properties. *}lemma unfold_triangle:  obtains a b c   where "Rep_triangle t = [a,b,c]"    and "a ∈ angles"    and "b ∈ angles"    and "c ∈ angles"    and "a + b + c = 180"    and "a ≤ b"    and "b ≤ c"proof-  obtain a b c where  "a = Rep_triangle t ! 0" and "b = Rep_triangle t ! 1" and "c = Rep_triangle t ! 2"    using Rep_triangle[of t]    by (auto simp add:triangle_def)  hence "Rep_triangle t = [a,b,c]"    using Rep_triangle[of t]    apply (auto simp add:triangle_def)    apply (cases "Rep_triangle t", auto)    apply (case_tac "list", auto)    apply (case_tac "lista", auto)    done  with that show thesis    using Rep_triangle[of t]    by (auto simp add:triangle_def)qedsection {* Property definitions *}text {* Two angles can be considered too similar if they differ by less than15\textdegree. This number is obtained heuristically by a field experiment withan 11th grade class and was chosen that statistically, 99\% will consider theangles as different. *}definition similar_angle :: "real => real => bool"  (infix "∼" 50)  where "similar_angle x y = (abs (x - y) < 15)"text {* The usual definitions of right-angled and isosceles, using the justintroduced similarity for comparison of angles. *}definition right_angled  where "right_angled l = (∃ x ∈ set (Rep_triangle l). x ∼ 90)"definition isosceles  where "isosceles l = ((Rep_triangle l) ! 0 ∼ (Rep_triangle l) ! 1 ∨                        (Rep_triangle l) ! 1 ∼ (Rep_triangle l) ! (Suc 1))"text {* A triangle is special if it is isosceles or right-angled, and generalif not. Equilateral triangle are isosceles and thus not mentioned on their ownhere. *}definition special  where "special t = (isosceles t ∨ right_angled t)"definition general  where "general t = (¬ special t)"section {* The Theorem *}theorem "∃! t. general t"txt {* The proof proceeds in two steps: There is a general triangle, and it is       unique. For the first step we give the triangle (angles 45\textdegree,       60\textdegree and 75\textdegree), show that it is a triangle and that it       is general. *}proof  have is_t [simp]: "[45, 60, 75] ∈ triangle" by (auto simp add: triangle_def)  show "general (Abs_triangle [45,60,75])" (is "general ?t")  by (auto simp add:general_def special_def isosceles_def right_angled_def                    Abs_triangle_inverse similar_angle_def)next  txt {* For the second step, we give names to the three angles and         successively find upper bounds to them. *}  fix t  obtain a b c where     abc: "Rep_triangle t = [a,b,c]"    and "a ∈ angles" and "b ∈ angles" and "c ∈ angles"    and "a ≤ b" and "b ≤ c"    and "a + b + c = 180"  by (rule unfold_triangle)  assume "general t"  hence ni: "¬ isosceles t" and nra: "¬ right_angled t"    by (auto simp add: general_def special_def)  have "¬ c ∼ 90" using nra abc     by (auto simp add:right_angled_def)  hence "c ≤ 75" using `c ∈ angles`    by (auto simp add:similar_angle_def)  have "¬ b ∼ c" using ni abc    by (auto simp add:isosceles_def)  hence "b ≤ 60" using `b ≤ c` and `c ≤ 75`    by (auto simp add:similar_angle_def)    have "¬ a ∼ b" using ni abc    by (auto simp add:isosceles_def)  hence "a ≤ 45" using `a ≤ b` and `b ≤ 60`    by (auto simp add:similar_angle_def)    txt {* The upper bound is actually the value, or we would not have a triangle *}  have "¬ (c < 75 ∨ b < 60 ∨ a < 45)"  proof    assume "c < 75 ∨ b < 60 ∨ a < 45"    hence "a + b + c < 180" using `c ≤ 75` `b ≤ 60` `a ≤ 45`                            and `a ∈ angles` `b ∈ angles` `c ∈ angles`      by auto    thus False using `a + b + c = 180` by auto  qed  hence "c = 75" and "b = 60" and "a = 45"    using `c ≤ 75` `b ≤ 60` `a ≤ 45`    by auto  txt {* And this concludes the proof. *}  hence "Abs_triangle (Rep_triangle t) = Abs_triangle [45, 60, 75]"    using abc by simp  thus "t = Abs_triangle [45, 60, 75]" by (simp add: Rep_triangle_inverse)qedend`