I am a novice user of the geometry theory in HOL-light and have been stuck with one theorem for the last 3 weeks or so and though to seek some guidance in this regard from this forum.
I want to prove "If a point lies on the interior of an angle, that angle is the sum of two smaller angles with legs that go through the given point" .In HOL-Light geometry theory a related theorem named " ANGLES_ADD_BETWEEN" exists ANGLES_ADD_BETWEEN;; val it : thm = |- !A B C D. between C (A,B) /\ ~(D = A) /\ ~(D = B) ==> angle (A,D,C) + angle (C,D,B) = angle (A,D,B) but it is restricted by the use of between predicate. I want to verify a more general result. One of the simpler case of my desired theorem is when the sum of both the angles is less than pi/2. g`!(A:real^2) (B:real^2). angle (A,D,B) <= pi / &2 /\ angle (C,D,B) => &0 ==> angle (A,D,B) = angle (A,D,C) + angle (C,D,B)`;; If we replace A with basis 1 (x-axis) then the configuration is illustrated by the attached figure. Now if i use the above mentioned theorem then the condition "between C (A,B)" appears. How can i remove this restriction? Moreover, I have been trying to verify this result based on forming triangles and using the result that the sum of the three angles of a triangle is pi. But for that I need the classical result that "If a transversal intersects two *parallel* lines, the pairs of corresponding angles are congruent" but I have been unable to locate this result in the geometry theory of HOL0light. Please guide me about it also. Regards BINYAMEEN System Analysis and Verification (SAVE) Lab School of Electrical Engineering and Computer Science (SEECS) National University of Science and Technology (NUST) Islamabad, Pakistan.
<<attachment: fig.jpg>>
------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
