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