[1] | 1 | /*----------------------------------------------------------------
|
---|
| 2 | Basic function for construction of equations
|
---|
| 3 | in Geometric Theorem proving
|
---|
| 4 | ----------------------------------------------------------------*/
|
---|
| 5 | put('geometry2,1,'version);
|
---|
| 6 |
|
---|
| 7 | generate_ideal(hypotheses,conclusions):=
|
---|
| 8 | append(hypotheses,
|
---|
| 9 | makelist(1-genpar()*conclusions[i],i,1,length(conclusions)));
|
---|
| 10 |
|
---|
| 11 | /* X, Y, Z on the plane are colinear */
|
---|
| 12 | collinear(X,Y,Z):= det(matrix(cons(1,X),cons(1,Y),cons(1,Z)));
|
---|
| 13 |
|
---|
| 14 | /* Vector AB and CD are perpendicular */
|
---|
| 15 | perpendicular(A,B,C,D):= (B-A).(D-C);
|
---|
| 16 |
|
---|
| 17 | /* AB and CD have equal length */
|
---|
| 18 | equidistant(A,B,C,D):=(B-A).(B-A)-(D-C).(D-C);
|
---|
| 19 |
|
---|
| 20 | /* AB and CD are parallel */
|
---|
| 21 | parallel(A,B,C,D):=det(matrix(B-A,D-C));
|
---|
| 22 |
|
---|
| 23 | /* M is the midpoint of AB; 2 equations */
|
---|
| 24 | midpoint(M,A,B):=2*M-(A+B);
|
---|
| 25 |
|
---|
| 26 | /* Points A and B are identical */
|
---|
| 27 | identical(A,B):=B-A;
|
---|
| 28 |
|
---|
| 29 | /* D is the distance between A and B */
|
---|
| 30 | distance(A,B,D):=D^2-(B-A).(B-A);
|
---|
| 31 |
|
---|
| 32 | /* Angle P with cos COS_P and sin SIN_P is the angle ABC
|
---|
| 33 | where segments AB and BC have lengths D_AB and D_BC */
|
---|
| 34 | angle(COS_P,SIN_P,A,B,C,D_AB,D_BC):=
|
---|
| 35 | [
|
---|
| 36 | cos_p^2+sin_p^2-1,
|
---|
| 37 | distance(A,B,D_AB),
|
---|
| 38 | distance(B,C,D_BC),
|
---|
| 39 | COS_P*D_AB*D_BC-(C-B).(A-B),
|
---|
| 40 | SIN_P*D_AB*D_BC-det(matrix(C-B,A-B))
|
---|
| 41 | ];
|
---|
| 42 |
|
---|
| 43 | /* Point X is on ellipse with center at O with semi-axes a and b */
|
---|
| 44 | ellipse(X,O,a,b):= b^2*(X[1]-O[1])^2+a^2*(x[2]-o[2])^2-a^2*b^2;
|
---|