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 ---------------------------------------------------------------------------*)
9
10open HolKernel Parse boolLib bossLib
11open numRingLib;
12
13val _ = new_theory "ringExamples"
14
15val num_norm_conv = NUM_NORM_CONV o Parse.Term
16val num_ring_conv = NUM_RING_CONV o Parse.Term;
17
18val res1 = num_norm_conv ` 3*(9+7) : num `;             (* normalization *)
19val res2 = num_norm_conv `x+y+x : num`;
20val res3 = num_norm_conv `(a+b)*(a+b) : num`;
21val res4 = num_norm_conv `(b+a)*(b+a) : num`;
22val res5 = num_norm_conv `(a+b)*(a+b)*(a+b) : num`;
23
24val res6 = num_ring_conv `(a+b)*(a+b) = (b+a)*(b+a) : num`;  (* equality *)
25val _ = if rhs (concl res6) !~ boolSyntax.T then raise Fail "res6 test failed"
26        else ()
27
28(*---------------------------------------------------------------------------
29      An example: sum of squares
30 ---------------------------------------------------------------------------*)
31
32open arithmeticTheory;
33
34val sum_def =
35 Define `(sum f 0 = 0n) /\ (sum f (SUC n) = sum f n + f (SUC n))`;
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
55open integerRingLib;
56
57val int_norm_conv = INT_NORM_CONV o Parse.Term
58val int_ring_conv = INT_RING_CONV o Parse.Term;
59
60val _ = int_norm_conv `~(3 * (9 - 7)) : int`;        (* normalization *)
61val _ = int_norm_conv `x+y+x:int`;
62val _ = int_norm_conv `(a+b)*(a+b) : int`;
63val _ = int_norm_conv `(b+a)*(b+a) : int`;
64val _ = int_norm_conv `(a+b)*(a+b)*(a+b) : int`;
65val _ = int_norm_conv `(a-b)*(a+b) : int`;
66
67val res7 = int_ring_conv `(a+b)*(a+b) = (b+a)*(b+a) :int`;   (* equality *)
68val _ = if rhs (concl res7) !~ boolSyntax.T then raise Fail "res7 test failed"
69        else ()
70
71
72(*---------------------------------------------------------------------------
73       Bigger test: 8 squares
74 ---------------------------------------------------------------------------*)
75
76val _ = Q.store_thm(
77  "big_int_ring_example",
78   `(p1*p1+q1*q1+r1*r1+s1*s1+t1*t1+u1*u1+v1*v1+w1*w1)
79  * (p2*p2+q2*q2+r2*r2+s2*s2+t2*t2+u2*u2+v2*v2+w2*w2)
80
81         =
82
83    (p1*p2-q1*q2-r1*r2-s1*s2-t1*t2-u1*u2-v1*v2-w1*w2)*
84    (p1*p2-q1*q2-r1*r2-s1*s2-t1*t2-u1*u2-v1*v2-w1*w2)
85    +
86    (p1*q2+q1*p2+r1*s2-s1*r2+t1*u2-u1*t2-v1*w2+w1*v2)*
87    (p1*q2+q1*p2+r1*s2-s1*r2+t1*u2-u1*t2-v1*w2+w1*v2)
88    +
89    (p1*r2-q1*s2+r1*p2+s1*q2+t1*v2+u1*w2-v1*t2-w1*u2)*
90    (p1*r2-q1*s2+r1*p2+s1*q2+t1*v2+u1*w2-v1*t2-w1*u2)
91    +
92    (p1*s2+q1*r2-r1*q2+s1*p2+t1*w2-u1*v2+v1*u2-w1*t2)*
93    (p1*s2+q1*r2-r1*q2+s1*p2+t1*w2-u1*v2+v1*u2-w1*t2)
94    +
95    (p1*t2-q1*u2-r1*v2-s1*w2+t1*p2+u1*q2+v1*r2+w1*s2)*
96    (p1*t2-q1*u2-r1*v2-s1*w2+t1*p2+u1*q2+v1*r2+w1*s2)
97    +
98    (p1*u2+q1*t2-r1*w2+s1*v2-t1*q2+u1*p2-v1*s2+w1*r2)*
99    (p1*u2+q1*t2-r1*w2+s1*v2-t1*q2+u1*p2-v1*s2+w1*r2)
100    +
101    (p1*v2+q1*w2+r1*t2-s1*u2-t1*r2+u1*s2+v1*p2-w1*q2)*
102    (p1*v2+q1*w2+r1*t2-s1*u2-t1*r2+u1*s2+v1*p2-w1*q2)
103    +
104    (p1*w2-q1*v2+r1*u2+s1*t2-t1*s2-u1*r2+v1*q2+w1*p2)*
105    (p1*w2-q1*v2+r1*u2+s1*t2-t1*s2-u1*r2+v1*q2+w1*p2)
106    : int`,
107  CONV_TAC (Count.apply INT_RING_CONV))
108
109val _ = export_theory()
110