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;
|
---|