ringExamplesScript.sml
1(*---------------------------------------------------------------------------
2 Normalizers and equality provers for rings. These are applications
3 of general support available in ringLib for normalizing ring terms,
4 and proving equality of ring terms. The library ringLib is Coq
5 technology transported to HOL by Bruno Barras.
6
7 First, we try some examples on natural numbers
8 ---------------------------------------------------------------------------*)
9Theory ringExamples
10Ancestors
11 arithmetic EVAL_numRing integerRing
12Libs
13 EVAL_numRingLib integerRingLib
14
15
16val num_norm_conv = NUM_NORM_CONV o Parse.Term
17val num_ring_conv = NUM_RING_CONV o Parse.Term;
18
19val res1 = num_norm_conv ` 3*(9+7) : num `; (* normalization *)
20val res2 = num_norm_conv `x+y+x : num`;
21val res3 = num_norm_conv `(a+b)*(a+b) : num`;
22val res4 = num_norm_conv `(b+a)*(b+a) : num`;
23val res5 = num_norm_conv `(a+b)*(a+b)*(a+b) : num`;
24
25val res6 = num_ring_conv `(a+b)*(a+b) = (b+a)*(b+a) : num`; (* equality *)
26val _ = if rhs (concl res6) !~ boolSyntax.T then raise Fail "res6 test failed"
27 else ()
28
29(*---------------------------------------------------------------------------
30 An example: sum of squares
31 ---------------------------------------------------------------------------*)
32
33Definition sum_def:
34 (sum f 0 = 0n) /\ (sum f (SUC n) = sum f n + f (SUC n))
35End
36
37val lemma = Q.prove
38(`!n:num. sum (\m. m * m) n * 6 = n * (n+1) * (2 * n + 1)`,
39 Induct
40 THEN RW_TAC std_ss [sum_def,RIGHT_ADD_DISTRIB]
41 THEN NUM_RING_TAC);
42
43val sum_squares = Q.prove
44(`!n:num. sum (\m. m * m) n = (n*(n+1) * (2*n + 1)) DIV 6`,
45 GEN_TAC
46 THEN MATCH_MP_TAC (GSYM DIV_UNIQUE)
47 THEN Q.EXISTS_TAC `0`
48 THEN RW_TAC arith_ss [lemma]);
49
50
51(*---------------------------------------------------------------------------
52 Now the integers
53 ---------------------------------------------------------------------------*)
54
55val int_norm_conv = INT_NORM_CONV o Parse.Term
56val int_ring_conv = INT_RING_CONV o Parse.Term;
57
58val _ = int_norm_conv `~(3 * (9 - 7)) : int`; (* normalization *)
59val _ = int_norm_conv `x+y+x:int`;
60val _ = int_norm_conv `(a+b)*(a+b) : int`;
61val _ = int_norm_conv `(b+a)*(b+a) : int`;
62val _ = int_norm_conv `(a+b)*(a+b)*(a+b) : int`;
63val _ = int_norm_conv `(a-b)*(a+b) : int`;
64
65val res7 = int_ring_conv `(a+b)*(a+b) = (b+a)*(b+a) :int`; (* equality *)
66val _ = if rhs (concl res7) !~ boolSyntax.T then raise Fail "res7 test failed"
67 else ()
68
69
70(*---------------------------------------------------------------------------
71 Bigger test: 8 squares
72 ---------------------------------------------------------------------------*)
73
74val _ = Q.store_thm(
75 "big_int_ring_example",
76 `(p1*p1+q1*q1+r1*r1+s1*s1+t1*t1+u1*u1+v1*v1+w1*w1)
77 * (p2*p2+q2*q2+r2*r2+s2*s2+t2*t2+u2*u2+v2*v2+w2*w2)
78
79 =
80
81 (p1*p2-q1*q2-r1*r2-s1*s2-t1*t2-u1*u2-v1*v2-w1*w2)*
82 (p1*p2-q1*q2-r1*r2-s1*s2-t1*t2-u1*u2-v1*v2-w1*w2)
83 +
84 (p1*q2+q1*p2+r1*s2-s1*r2+t1*u2-u1*t2-v1*w2+w1*v2)*
85 (p1*q2+q1*p2+r1*s2-s1*r2+t1*u2-u1*t2-v1*w2+w1*v2)
86 +
87 (p1*r2-q1*s2+r1*p2+s1*q2+t1*v2+u1*w2-v1*t2-w1*u2)*
88 (p1*r2-q1*s2+r1*p2+s1*q2+t1*v2+u1*w2-v1*t2-w1*u2)
89 +
90 (p1*s2+q1*r2-r1*q2+s1*p2+t1*w2-u1*v2+v1*u2-w1*t2)*
91 (p1*s2+q1*r2-r1*q2+s1*p2+t1*w2-u1*v2+v1*u2-w1*t2)
92 +
93 (p1*t2-q1*u2-r1*v2-s1*w2+t1*p2+u1*q2+v1*r2+w1*s2)*
94 (p1*t2-q1*u2-r1*v2-s1*w2+t1*p2+u1*q2+v1*r2+w1*s2)
95 +
96 (p1*u2+q1*t2-r1*w2+s1*v2-t1*q2+u1*p2-v1*s2+w1*r2)*
97 (p1*u2+q1*t2-r1*w2+s1*v2-t1*q2+u1*p2-v1*s2+w1*r2)
98 +
99 (p1*v2+q1*w2+r1*t2-s1*u2-t1*r2+u1*s2+v1*p2-w1*q2)*
100 (p1*v2+q1*w2+r1*t2-s1*u2-t1*r2+u1*s2+v1*p2-w1*q2)
101 +
102 (p1*w2-q1*v2+r1*u2+s1*t2-t1*s2-u1*r2+v1*q2+w1*p2)*
103 (p1*w2-q1*v2+r1*u2+s1*t2-t1*s2-u1*r2+v1*q2+w1*p2)
104 : int`,
105 CONV_TAC (Count.apply INT_RING_CONV))