Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Fri, 22 Jan 1993 10:48:04 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA21665; Fri, 22 Jan 93 02:30:34 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA21660; Fri, 22 Jan 93 02:30:07 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Fri, 22 Jan 93 10:29:28 GMT From: David Shepherd Message-Id: <2609.9301221029@frogland.inmos.co.uk> Subject: Benchmarks, again! To: info-hol@edu.uidaho.cs.ted (info-hol mailing list) Date: Fri, 22 Jan 1993 10:29:54 +0000 (GMT) X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 23753 Ok, given that I seem to have caused general confusion with some comments on benchmarking that I made only to find that all my data was hopelessly out of date, I have rejigged the benchmark program. Below is a Shar file of a new contrib entry "newbench". There is a shell (sh) script in it called "benchmark" which should run the benchmark, pipe the output through a simple awk script to get the info needed and leave the results in a file "benchmark.log". All you need to do is to run this script, edit the info requested into the top of "benchmark.log" and mail the result to me and I will then try to build up a new table. The process should only take about 5 minutes. Thanks -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq Life doesn't imitate art, it imitates bad television - Husbands and Wives -------------------------------------------------------------------------- #!/bin/sh # This is a shell archive (shar 3.24) # made 01/22/1993 09:58 UTC by des@inmos.co.uk # Source directory /tmp_mnt/import/inmos/sun4/hol/contrib # # existing files WILL be overwritten # # This shar contains: # length mode name # ------ ---------- ------------------------------------------ # 1623 -rw-r--r-- newbench/READ-ME # 610 -rwxr-xr-x newbench/benchmark # 2086 -rw-r--r-- newbench/benchmark.ml # 15369 -rw-r--r-- newbench/do_benchmark.ml # if touch 2>&1 | fgrep '[-amc]' > /dev/null then TOUCH=touch else TOUCH=true fi # ============= newbench/READ-ME ============== if test ! -d 'newbench'; then echo "x - creating directory newbench" mkdir 'newbench' fi echo "x - extracting newbench/READ-ME (Text)" sed 's/^X//' << 'SHAR_EOF' > newbench/READ-ME && X% --------------------------------------------------------------------- % X% DIRECTORY: newbench % X% % X% DESCRIPTION: The HOL "multiplier" benchmark (for version 2..). % X% % X% AUTHOR: Mike Gordon % X% % X% ADDRESS: University of Cambridge % X% Computer Laboratory % X% New Museums Site % X% Pembroke Street % X% Cambridge, CB2 3QG % X% England % X% % X% email: mjcg@cl.cam.ac.uk % X% % X% DATE: 91.01.28 % X% % X% adapted by David Shepherd, INMOS ltd - des@inmos.co.uk % X% january 1993 % X% % X% --------------------------------------------------------------------- % X XThis directory contains the proof of the multiplier example, which is often Xused as a HOL benchmark, from the LCF_LSM paper done in HOL. X XIt has been modified to run in HOL version 2. X XAll the files from the previous benchmark have been combined into a single Xfile which does all the proof work. The benchmark time is the time taken Xto process this. Various bits and pieces have been added to automatically Xextract the relevant info. X XThe unix shell script (sh) X X % benchmark X Xwill automatically run the benchmark and give info on where to send them Xto get included in the "league table". Eventually a copy of a recent table Xwill exist here so you can tell if your machine has been done already. X XFinally, this is probably not a very scientific benchmark, so it Xshould only be used to give very broad comparisons of different Xsystems. X XN.b. you *may* need to edit in the path to your hol implementation in Xthe benchmark script. SHAR_EOF $TOUCH -am 0121172693 newbench/READ-ME && chmod 0644 newbench/READ-ME || echo "restore of newbench/READ-ME failed" set `wc -c newbench/READ-ME`;Wc_c=$1 if test "$Wc_c" != "1623"; then echo original size 1623, current size $Wc_c fi # ============= newbench/benchmark ============== echo "x - extracting newbench/benchmark (Text)" sed 's/^X//' << 'SHAR_EOF' > newbench/benchmark && X#! /bin/sh X Xecho 'running HOL multiplier benchmark' X Xrm -f benchmark.th X Xecho 'PLEASE COMPLETE THE FOLLOWING INFORMATION THEN MAIL FILE TO des@inmos.co.uk. X XMeasured by: XHol Version: XLisp/SML type: XMachine type: X Xan example is X XMeasured by: des@inmos.co.uk XHol Version: HOL88 v2.00 XLisp/SML type: Allegro CL v3 XMachine type: Sun 4.65 SparcStation 1+ X' > benchmark.log X Xecho 'loadt `benchmark`;; Xquit();; X' | hol | awk '/<<>>/' >> benchmark.log X Xecho ' XPlease fill in information requested at start of file benchmark.log Xand email results to des@inmos.co.uk X XThanks for your help.' X SHAR_EOF $TOUCH -am 0121171393 newbench/benchmark && chmod 0755 newbench/benchmark || echo "restore of newbench/benchmark failed" set `wc -c newbench/benchmark`;Wc_c=$1 if test "$Wc_c" != "610"; then echo original size 610, current size $Wc_c fi # ============= newbench/benchmark.ml ============== echo "x - extracting newbench/benchmark.ml (Text)" sed 's/^X//' << 'SHAR_EOF' > newbench/benchmark.ml && X% ---------------------------------------- X X run the benchmark X X---------------------------------------- % X X Xload_library `unwind`;; X X Xlet LESS_SUC_REFL = theorem `prim_rec` `LESS_SUC_REFL`;; Xlet LESS_LESS_SUC = theorem `arithmetic` `LESS_LESS_SUC`;; Xlet LESS_SUC_EQ_COR = theorem `arithmetic` `LESS_SUC_EQ_COR`;; Xlet SUC_LESS = theorem `prim_rec` `SUC_LESS`;; Xlet FUN_EQ_LEMMA = theorem `arithmetic` `FUN_EQ_LEMMA`;; Xlet LESS_TRANS = theorem `arithmetic` `LESS_TRANS`;; Xlet LESS_OR_EQ = definition `arithmetic` `LESS_OR_EQ`;; Xlet LESS_ADD_NONZERO = theorem `arithmetic` `LESS_ADD_NONZERO`;; Xlet LESS_SUC_REFL = theorem `prim_rec` `LESS_SUC_REFL`;; Xlet LESS_EQ_SUC_REFL = theorem `arithmetic` `LESS_EQ_SUC_REFL`;; Xlet LESS_CASES_IMP = theorem `arithmetic` `LESS_CASES_IMP`;; X Xlet ADD_INV_0 = theorem `arithmetic` `ADD_INV_0`;; Xlet ADD1 = theorem `arithmetic` `ADD1`;; Xlet LESS_REFL = theorem `prim_rec` `LESS_REFL`;; X Xlet ADD_CLAUSES = theorem `arithmetic` `ADD_CLAUSES`;; X Xlet num_Axiom = theorem `prim_rec` `num_Axiom`;; Xlet num_CASES = theorem `arithmetic` `num_CASES`;; Xlet SUC_SUB1 = theorem `arithmetic` `SUC_SUB1`;; Xlet SUB = definition `arithmetic` `SUB`;; X Xlet LESS_0 = theorem `prim_rec` `LESS_0`;; Xlet LESS_MONO_EQ = theorem `arithmetic` `LESS_MONO_EQ`;; Xlet ADD_EQ_SUB = theorem `arithmetic` `ADD_EQ_SUB`;; Xlet SUB_0 = theorem `arithmetic` `SUB_0`;; Xlet MULT_CLAUSES = theorem `arithmetic` `MULT_CLAUSES`;; Xlet ADD_SYM = theorem `arithmetic` `ADD_SYM`;; Xlet ADD_ASSOC = theorem `arithmetic` `ADD_ASSOC`;; Xlet LESS_EQ_ADD = theorem `arithmetic` `LESS_EQ_ADD`;; Xlet RIGHT_SUB_DISTRIB = theorem `arithmetic` `RIGHT_SUB_DISTRIB`;; Xlet SUB_ADD = theorem `arithmetic` `SUB_ADD`;; Xlet INDUCTION = theorem `num` `INDUCTION`;; Xlet INDUCT_TAC = INDUCT_THEN INDUCTION ASSUME_TAC;; X Xtimer true;; X Xnew_theory `benchmark`;; X X(print_newline();print_string `<<<`;print_newline());; Xsystem `date`;; X(print_newline();print_string `>>>`;print_newline());; X Xloadt `do_benchmark`;; X Xsystem `date`;; X(print_newline();print_string `>>>`;print_newline());; X Xclose_theory();; X Xquit();; X SHAR_EOF $TOUCH -am 0121164093 newbench/benchmark.ml && chmod 0644 newbench/benchmark.ml || echo "restore of newbench/benchmark.ml failed" set `wc -c newbench/benchmark.ml`;Wc_c=$1 if test "$Wc_c" != "2086"; then echo original size 2086, current size $Wc_c fi # ============= newbench/do_benchmark.ml ============== echo "x - extracting newbench/do_benchmark.ml (Text)" sed 's/^X//' << 'SHAR_EOF' > newbench/do_benchmark.ml && X% X Theorem for projection of a sequence of microcycles into a single macrocycle. X% X Xnew_theory `benchmark`;; X Xlet NEXT = X new_definition X (`NEXT`, X "!done x1 x2. X NEXT (x1,x2) done = X (x1 < x2) /\ (done x2) /\ (!x. (x1 < x) /\ (x < x2) ==> ~done x)");; X Xlet STABLE = X new_definition X (`STABLE`, X "!i:num->*. !x1 x2. X STABLE (x1,x2) i = !x. (x1 <= x) /\ (x < x2) ==> (i x = i x1)");; X Xlet NEXT_SUC1 = X prove_thm X (`NEXT_SUC1`, X "!done x. done(SUC x) ==> NEXT (x,SUC x) done", X REPEAT STRIP_TAC X THEN REWRITE_TAC[NEXT] X THEN REPEAT STRIP_TAC X THEN ASM_REWRITE_TAC[LESS_SUC_REFL] X THEN IMP_RES_TAC LESS_LESS_SUC X THEN ASM_REWRITE_TAC[]);; X X% LESS_SUC_EQ_LEMMA = |- ~(n = SUC m) ==> m < n ==> (SUC m) < n % X Xlet LESS_SUC_EQ_LEMMA = X (DISCH_ALL X (MP (SPEC_ALL LESS_SUC_EQ_COR) X (CONJ (ASSUME "m < n") (NOT_EQ_SYM(ASSUME "~(n = SUC m)")))));; X Xlet NEXT_SUC2 = X prove_thm X (`NEXT_SUC2`, X "!done x1 x2. X NEXT (x1,x2) done /\ ~done(SUC x1) ==> NEXT (SUC x1,x2) done", X REPEAT GEN_TAC X THEN REWRITE_TAC[NEXT] X THEN REPEAT STRIP_TAC X THEN IMP_RES_TAC SUC_LESS X THEN RES_TAC X THEN ASM_REWRITE_TAC[] X THEN IMP_RES_TAC X (SPECL["done:num->bool";"x2:num";"SUC x1"] X (INST_TYPE[":num",":*"]FUN_EQ_LEMMA)) X THEN IMP_RES_TAC LESS_SUC_EQ_LEMMA X THEN ASM_REWRITE_TAC[]);; X Xlet STABLE_SUC = X prove_thm X (`STABLE_SUC`, X "!x1 x2. !i:num->*. STABLE (x1,x2) i ==> STABLE (SUC x1,x2) i", X REPEAT GEN_TAC X THEN REWRITE_TAC[STABLE;LESS_OR_EQ] X THEN REPEAT STRIP_TAC X THEN ASM_REWRITE_TAC[] X THEN IMP_RES_TAC SUC_LESS X THEN IMP_RES_TAC LESS_TRANS X THEN ASSUME_TAC(SPEC "x1:num" LESS_SUC_REFL) X THEN RES_TAC X THEN ASM_REWRITE_TAC[]);; X Xlet SUC_LEMMA = X let [th1;th2;th3;th4] = CONJUNCTS ADD_CLAUSES X in X save_thm(`SUC_LEMMA`,LIST_CONJ[th1;th2;SYM th3;th4]);; X Xlet stb_SUC = X SPEC X "SUC x" X (ASSUME "!x'. x <= x' /\ x' < ((SUC x) + d) ==> ((i:num->*) x' = i x)");; X X X% Proof modified for HOL version 1.12 [TFM 91.01.28] % Xlet STABLE_LEMMA = X prove_thm X (`STABLE_LEMMA`, X "!x d. !i:num->*. X STABLE (x,(SUC x)+d) i /\ ~(d = 0) ==> (i x = i(SUC x))", X REWRITE_TAC[STABLE] X THEN REPEAT STRIP_TAC X THEN ASSUME_TAC stb_SUC X THEN IMP_RES_TAC(SPECL["SUC x";"d:num"]LESS_ADD_NONZERO) X THEN CONV_TAC SYM_CONV X THEN FIRST_ASSUM MATCH_MP_TAC X THEN ASSUME_TAC(SPEC "x:num" LESS_EQ_SUC_REFL) X THEN ASM_REWRITE_TAC[]);; X Xlet NEXT_LEMMA1 = X prove_thm X (`NEXT_LEMMA1`, X "!done x1 x2. X NEXT (x1,x2) done /\ NEXT (x1,x3) done ==> (x2 = x3)", X REPEAT GEN_TAC X THEN REWRITE_TAC[NEXT] X THEN STRIP_TAC X THEN ASM_CASES_TAC "x2:num = x3" X THEN ASM_CASES_TAC "x2 < x3" X THEN ASM_REWRITE_TAC[] X THEN IMP_RES_TAC LESS_CASES_IMP X THEN RES_TAC);; X Xlet next_SUC = X DISCH_ALL X (REWRITE_RULE X [ADD_CLAUSES] X (SUBS[ASSUME "d = 0"](ASSUME "(done:num->bool)((SUC x) + d)")));; X Xlet NEXT_LEMMA2 = X prove_thm X (`NEXT_LEMMA2`, X "!x d done. X NEXT (x,(SUC x)+d) done /\ ~done(SUC x) ==> ~(d = 0)", X REWRITE_TAC[NEXT] X THEN REPEAT STRIP_TAC X THEN IMP_RES_TAC next_SUC X THEN RES_TAC);; X Xlet assm = X ASSUME "(!x. (done x = f(s x)) /\ (s(SUC x) = g(i x,s x))) /\ X (!a b. (FUN:*#**->**)(a,b) = (f b => b | FUN(a,g(a,b))))" ;; X Xlet [done_s;FUN] = CONJUNCTS assm;; X Xlet ind_hyp = X ASSUME "!x. NEXT(x,x + d)done /\ STABLE(x,x + d)i ==> X (s(x + d) = (FUN:*#**->**)(i x,g(i x,s x)))";; X Xlet s_tm = X ASSUME "s((SUC x) + d) = (FUN:*#**->**)(i(SUC x),g(i(SUC x),s(SUC x)))";; X Xlet NEXT_THM = X prove_thm X (`NEXT_THM`, X "!FUN:*#**->**. X !f:**->bool. !g:*#**->**. !done:num->bool. !i:num->*. !s:num->**. X (!x. (done x = f(s x)) /\ (s(x+1) = g(i x,s x))) /\ X (!a b. FUN(a,b) = (f b => b | FUN(a,g(a,b)))) ==> X (!d x. X NEXT(x,x+d)done /\ STABLE(x,x+d)i ==> X (s(x+d) = FUN(i x,g(i x,s x))))", X REPEAT GEN_TAC X THEN REWRITE_TAC[SYM(SPEC_ALL ADD1)] X THEN REPEAT DISCH_TAC X THEN INDUCT_TAC X THENL [REWRITE_TAC[NEXT;LESS_REFL;ADD_CLAUSES];ALL_TAC] X THEN REWRITE_TAC[SUC_LEMMA] X THEN REPEAT STRIP_TAC X THEN ASM_CASES_TAC "done(SUC x):bool" X THENL X [IMP_RES_TAC NEXT_SUC1 X THEN IMP_RES_TAC NEXT_LEMMA1 X THEN IMP_RES_TAC ADD_INV_0 X THEN REWRITE_TAC[ASSUME "d=0";ADD_CLAUSES] X THEN REWRITE_TAC X ([SPECL["(i:num->*)x";"(g:*#**->**)(i(x:num),s x)"]FUN; X ASSUME "done(SUC x):bool"]@ X (map SYM (CONJUNCTS(SPEC_ALL done_s)))); X ALL_TAC] X THEN ASSUME_TAC(SPEC "SUC x" ind_hyp) X THEN IMP_RES_TAC STABLE_SUC X THEN IMP_RES_TAC NEXT_SUC2 X THEN RES_TAC X THEN REWRITE_TAC[s_tm] X THEN SUBST_TAC[SPECL["(i:num->*)x";"(g:*#**->**)(i(x:num),s x)"]FUN] X THEN REWRITE_TAC X (ASSUME "~done(SUC x)" .(map SYM (CONJUNCTS(SPEC_ALL done_s)))) X THEN IMP_RES_TAC NEXT_LEMMA2 X THEN IMP_RES_TAC STABLE_LEMMA X THEN REWRITE_TAC[ASSUME "(i:num->*) x = i(SUC x)";done_s]);; X Xlet MULT_FUN_CURRY = X new_prim_rec_definition X (`MULT_FUN_CURRY`, X "(MULT_FUN_CURRY 0 i1 i2 m t = X (t => (m,0,t) | ((i1=0)=>m|i2+m),0,T)) /\ X (MULT_FUN_CURRY (SUC n) i1 i2 m t = X (t => (m,SUC n,t) | X MULT_FUN_CURRY n i1 i2 ((i1=0)=>m|i2+m) (((n-1)=0) \/ (i2=0))))");; X Xlet MULT_FUN_CURRY_THM = X prove_thm X (`MULT_FUN_CURRY_THM`, X "!i1 i2 m n t. X MULT_FUN_CURRY n i1 i2 m t = X (t => X (m,n,t) | X MULT_FUN_CURRY (n-1) i1 i2 ((i1=0)=>m|i2+m) ((((n-1)-1)=0)\/(i2=0)))", X REPEAT GEN_TAC X THEN STRUCT_CASES_TAC(SPEC "n:num" num_CASES) X THEN ASM_CASES_TAC "t:bool" X THEN ASM_REWRITE_TAC[MULT_FUN_CURRY;SUB;SUC_SUB1]);; X X Xlet MULT_FUN = X new_definition X (`MULT_FUN`, "MULT_FUN((i1,i2),m,n,t) = MULT_FUN_CURRY n i1 i2 m t");; X Xlet MULT_FUN_DEF = X prove_thm X (`MULT_FUN_DEF`, X "!i1 i2 m n t. X MULT_FUN((i1,i2),m,n,t) = X (t => X (m,n,t) | X MULT_FUN((i1,i2),((i1=0)=>m|i2+m),n-1,((((n-1)-1)=0) \/ (i2=0))))", X REPEAT GEN_TAC X THEN REWRITE_TAC[MULT_FUN] X THEN ACCEPT_TAC(SPEC_ALL MULT_FUN_CURRY_THM));; X X% X |- !i1 i2 m n t. X MULT_FUN((i1,i2),m,n,t) = X (t => X (m,n,t) | X MULT_FUN((i1,i2),((i1=0)=>m|i2+m),n-1,((((n-1)-1)=0) \/ (i2=0)))) X% X Xlet MULT_FUN_T = X prove_thm X (`MULT_FUN_T`, X "!i1 i2 m n. X MULT_FUN((i1,i2),m,n,T) = (m,n,T)", X REPEAT GEN_TAC X THEN ASM_CASES_TAC "t:bool" X THEN REWRITE_TAC[INST["T","t:bool"](SPEC_ALL MULT_FUN_DEF)]);; X Xlet MULT_FUN_F = X prove_thm X (`MULT_FUN_F`, X "!i1 i2 m n. X MULT_FUN((i1,i2),m,n,F) = X MULT_FUN((i1,i2),((i1=0)=>m|i2+m),n-1,((((n-1)-1)=0) \/ (i2=0)))", X REPEAT GEN_TAC X THEN ASM_CASES_TAC "t:bool" X THEN REWRITE_TAC[INST["F","t:bool"](SPEC_ALL MULT_FUN_DEF)]);; X Xlet LESS_EQ_0 = X prove_thm X (`LESS_EQ_0`, X "!m. 0 <= m", X INDUCT_TAC X THEN ASM_REWRITE_TAC[LESS_OR_EQ;LESS_0]);; X Xlet LESS_EQ_SUC_1 = X prove_thm X (`LESS_EQ_SUC_1`, X "!m. 1 <= SUC m", X INDUCT_TAC X THEN ASM_REWRITE_TAC[num_CONV "1";LESS_OR_EQ;LESS_MONO_EQ;LESS_0]);; X Xlet SUB_LEMMA1 = X prove_thm X (`SUB_LEMMA1`, X "!m.~(m=0) ==> (m-1=0) ==> (m=1)", X INDUCT_TAC X THEN REWRITE_TAC X [SYM X (SUBS X [SPECL["0";"(SUC m)-1"](INST_TYPE[":num",":*"]EQ_SYM_EQ)] X (MP X (SPECL X ["0";"1";"SUC m"]ADD_EQ_SUB)(SPEC "m:num" LESS_EQ_SUC_1))); X ADD_CLAUSES] X THEN REPEAT STRIP_TAC X THEN ASM_REWRITE_TAC[]);; X Xlet SUB_LEMMA2 = X prove_thm X (`SUB_LEMMA2`, X "!m.(m=0) ==> ~(m-1=0) ==> F", X GEN_TAC X THEN DISCH_TAC X THEN ASM_REWRITE_TAC[SUB_0]);; X Xlet MULT_NOT_0_LESS = X prove_thm X (`MULT_NOT_0_LESS`, X "!m n. ~(m = 0) ==> n <= (m * n)", X INDUCT_TAC X THEN GEN_TAC X THEN REWRITE_TAC X [MULT_CLAUSES;SUBS[SPEC_ALL ADD_SYM](SPEC_ALL LESS_EQ_ADD)]);; X X% Proof modified for HOL version 1.12 [TFM 91.01.29] % Xlet MULT_ADD_LEMMA1 = X prove_thm X (`MULT_ADD_LEMMA1`, X "!m. ~(m=0) ==> !n p. (((m-1)*n)+(n+p) = (m*n)+p)", X REPEAT STRIP_TAC X THEN REWRITE_TAC[ADD_ASSOC;RIGHT_SUB_DISTRIB;MULT_CLAUSES] X THEN IMP_RES_THEN (ASSUME_TAC o SPEC "n:num") MULT_NOT_0_LESS X THEN IMP_RES_TAC SUB_ADD X THEN ASM_REWRITE_TAC[]);; X Xlet MULT_FUN_THM = X prove_thm X (`MULT_FUN_THM`, X "!n i1 i2 m t. X MULT_FUN((i1,i2),m,n,t) = X (t => X (m,n,t) | X (((n-1)=0)\/(i2=0)) => X (((i1=0)=>m|i2+m),n-1,T) | X (((i1=0)=>m|((n-1)*i2)+m),1,T))", X INDUCT_TAC X THEN REPEAT GEN_TAC X THEN ASM_CASES_TAC "t:bool" X THEN ASM_REWRITE_TAC[MULT_FUN_T;MULT_FUN_F;SUC_SUB1;SUB_0] X THEN ASM_CASES_TAC "i1=0" X THEN ASM_CASES_TAC "i2=0" X THEN ASM_CASES_TAC "n=0" X THEN ASM_CASES_TAC "(n-1)=0" X THEN ASM_REWRITE_TAC[MULT_FUN_T;MULT_FUN_F;SUC_SUB1;SUB_0] X THEN IMP_RES_TAC SUB_LEMMA1 X THEN IMP_RES_TAC SUB_LEMMA2 X THEN IMP_RES_TAC MULT_ADD_LEMMA1 X THEN ASM_REWRITE_TAC[MULT_CLAUSES]);; X X% Proof modified for HOL version 1.12 [TFM 91.01.29] % Xlet MULT_ADD_LEMMA2 = X prove_thm X (`MULT_ADD_LEMMA2`, X "!m. ~(m=0) ==> !n. ((m-1)*n)+n = m*n", X REPEAT STRIP_TAC X THEN REWRITE_TAC[RIGHT_SUB_DISTRIB;MULT_CLAUSES] X THEN IMP_RES_THEN (ASSUME_TAC o SPEC "n:num") MULT_NOT_0_LESS X THEN IMP_RES_TAC SUB_ADD X THEN ASM_REWRITE_TAC[]);; X Xlet MULT_FUN_LEMMA = X prove_thm X (`MULT_FUN_LEMMA`, X "!i1 i2. X MULT_FUN((i1,i2),((i1=0)=>0|i2),i1,(((i1-1)=0)\/(i2=0))) = X (i1*i2, ((((i1-1)=0)\/(i2=0))=>i1|1), T)", X REPEAT GEN_TAC X THEN ASM_CASES_TAC "i1=0" X THEN ASM_CASES_TAC "i2=0" X THEN ASM_REWRITE_TAC[MULT_FUN_THM;MULT_CLAUSES;SUB_0] X THEN ASM_CASES_TAC "i1-1=0" X THEN IMP_RES_TAC SUB_LEMMA1 X THEN IMP_RES_TAC MULT_ADD_LEMMA2 X THEN ASM_REWRITE_TAC[MULT_CLAUSES]);; X Xlet time = ":num";; X Xlet sig = ":^time -> bool" Xand bus = ":^time -> num";; X Xlet prims = Xmap X new_definition X [`MUX` , "MUX(switch,i1:^bus,i2:^bus,out) = X !x:^time. out x = (switch x => i1 x | i2 x)"; X `REG` , "REG(i:^bus,out) = X !x:^time. out(x+1) = i x"; X `FLIPFLOP` , "FLIPFLOP(i:^sig,out) = X !x:^time. out(x+1) = i x"; X `DEC` , "DEC(i,out) = X !x:^time. out x = (i x - 1)"; X `ADDER` , "ADDER(i1,i2,out) = X !x:^time. out x = (i1 x + i2 x)"; X `ZERO_TEST`, "ZERO_TEST(i,out) = X !x:^time. out x = (i x = 0)"; X `OR_GATE` , "OR_GATE(i1,i2,out) = X !x:^time. out x = (i1 x \/ i2 x)"; X `ZERO` , "ZERO(out) = X !x:^time. out x = 0"];; X Xlet MULT_IMP = Xnew_definition X (`MULT_IMP`, X "MULT_IMP(i1,i2,o1,o2,done) = X ?b1 b2 b3 b4 l1 l2 l3 l4 l5 l6 l7 l8 l9. X MUX(done,l8,l7,l6) /\ X REG(l6,o2) /\ X ADDER(l8,o2,l7) /\ X DEC(i1,l5) /\ X MUX(done,l5,l3,l4) /\ X MUX(done,i1,l2,l1) /\ X REG(l1,o1) /\ X DEC(o1,l2) /\ X DEC(l2,l3) /\ X ZERO(l9) /\ X MUX(b4,l9,i2,l8) /\ X ZERO_TEST(i1,b4) /\ X ZERO_TEST(l4,b1) /\ X ZERO_TEST(i2,b2) /\ X OR_GATE(b1,b2,b3) /\ X FLIPFLOP(b3,done)");; X X%< OLD Xlet MULT_IMP_UNFOLD = X save_thm(`MULT_IMP_UNFOLD`, UNFOLD_RULE prims MULT_IMP);; Xlet MULT_IMP_UNWIND = X save_thm(`MULT_IMP_UNWIND`, UNWINDF_RULE MULT_IMP_UNFOLD);; Xlet MULT_IMP_PRUNE = X save_thm(`MULT_IMP_PRUNE`, PRUNEF_RULE MULT_IMP_UNWIND);; Xlet MULT_IMP_EXPAND = save_thm(`MULT_IMP_EXPAND`, EXPANDF prims MULT_IMP);; X>% X Xlet MULT_IMP_UNFOLD = save_thm(`MULT_IMP_UNFOLD`, X UNFOLD_RIGHT_RULE prims MULT_IMP);; Xlet MULT_IMP_UNWIND = save_thm(`MULT_IMP_UNWIND`, X UNWIND_AUTO_RIGHT_RULE MULT_IMP_UNFOLD);; Xlet MULT_IMP_PRUNE = save_thm(`MULT_IMP_PRUNE`, X PRUNE_RIGHT_RULE MULT_IMP_UNWIND);; Xlet MULT_IMP_EXPAND = save_thm(`MULT_IMP_EXPAND`, X EXPAND_AUTO_RIGHT_RULE prims MULT_IMP);; X Xlet COND_ADD_LEMMA = X prove_thm X (`COND_ADD_LEMMA`, X "(b => m | n) + p = (b => m + p | n + p)", X COND_CASES_TAC X THEN ASM_REWRITE_TAC[]);; X Xlet MULT_FUN_EXPANDED_DEF = X prove_thm X (`MULT_FUN_EXPANDED_DEF`, X "!i1 i2 m n t. X MULT_FUN((i1,i2),m,n,t) = X (t => X (m,n,t) | X MULT_FUN X ((i1, i2), X (t => ((i1 = 0) => 0 | i2) | ((i1 = 0) => 0 | i2) + m), X (t => i1 | n - 1), X (((t => i1 - 1 | (n - 1) - 1) = 0) \/ (i2 = 0))))", X REPEAT GEN_TAC X THEN ASM_CASES_TAC "t:bool" X THEN ASM_REWRITE_TAC X [MULT_FUN_T;MULT_FUN_F;COND_ADD_LEMMA;ADD_CLAUSES]);; X Xlet G_FUN = X new_definition X (`G_FUN`, X "!i1 i2 m n t. X G_FUN((i1,i2),(m,n,t)) = X ((t => ((i1 = 0) => 0 | i2) | ((i1 = 0) => 0 | i2) + m), X (t => i1 | n - 1), X (((t => i1 - 1 | (n - 1) - 1) = 0) \/ (i2 = 0)))");; X Xlet NEXT_MULT_LEMMA1 = X save_thm X (`NEXT_MULT_LEMMA1`, X REWRITE_RULE X [] X (CONV_RULE X (DEPTH_CONV BETA_CONV) X (SPECL X ["MULT_FUN"; X "\x:num#num#bool.SND(SND x)"; X "G_FUN"; X "done:num->bool"; X "\x. ((i1:num->num) x, (i2:num->num) x)"; X "\x. ((o2:num->num) x, (o1:num->num) x, (done:num->bool) x)"] X (INST_TYPE[":num#num",":*";":num#num#bool",":**"]NEXT_THM))));; X Xlet NEXT_MULT_LEMMA2 = X prove_thm X (`NEXT_MULT_LEMMA2`, X "MULT_IMP(i1,i2,o1,o2,done) ==> X (!x. X o2(x + 1),o1(x + 1),done(x + 1) = X G_FUN((i1 x,i2 x),o2 x,o1 x,done x))", X REWRITE_TAC[MULT_IMP_EXPAND] X THEN REPEAT STRIP_TAC X THEN ASM_REWRITE_TAC[G_FUN]);; X Xlet G_FUN_LEMMA = X save_thm X (`G_FUN_LEMMA`, X PURE_REWRITE_RULE X [PAIR] X (SPECL X ["FST(a:num#num)"; X "SND(a:num#num)"; X "FST(b:num#num#bool)"; X "FST(SND(b:num#num#bool))"; X "SND(SND(b:num#num#bool))"] X G_FUN));; X Xlet NEXT_MULT_LEMMA3 = X save_thm X (`NEXT_MULT_LEMMA3`, X PURE_REWRITE_RULE X [PAIR;SYM G_FUN_LEMMA] X (SPECL X ["FST(a:num#num)"; X "SND(a:num#num)"; X "FST(b:num#num#bool)"; X "FST(SND(b:num#num#bool))"; X "SND(SND(b:num#num#bool))"] X MULT_FUN_EXPANDED_DEF));; X Xlet NEXT_MULT_LEMMA4 = X save_thm X (`NEXT_MULT_LEMMA4`, X DISCH_ALL X (REWRITE_RULE X [UNDISCH NEXT_MULT_LEMMA2;SYM NEXT_MULT_LEMMA3] X NEXT_MULT_LEMMA1));; X Xlet MULT_FUN_LEMMA2 = X prove_thm X (`MULT_FUN_LEMMA2`, X "(done:^sig) x ==> X (MULT_FUN((i1 x,i2 x),G_FUN((i1 x,i2 x),o2 x,o1 x,done x)) = X (i1 x * i2 x, ((((i1 x - 1) = 0) \/ (i2 x = 0)) => i1 x | 1), T))", X DISCH_TAC X THEN ASM_REWRITE_TAC[MULT_FUN_LEMMA;G_FUN]);; X Xlet PAIR_SPLIT = X prove_thm X (`PAIR_SPLIT`, X "!x1:*.!y1:**.!x2 y2. X ((x1,y1) = (x2,y2)) = (x1 = x2) /\ (y1 = y2)", X REPEAT GEN_TAC X THEN EQ_TAC X THEN REPEAT STRIP_TAC X THEN ASM_REWRITE_TAC[] X THEN ASSUME_TAC X (REWRITE_RULE X [] X (AP_TERM "FST:*#**->*" (ASSUME "(x1:*,y1:**) = (x2,y2)"))) X THEN ASSUME_TAC X (REWRITE_RULE X [] X (AP_TERM "SND:*#**->**" (ASSUME "(x1:*,y1:**) = (x2,y2)"))) X THEN ASM_REWRITE_TAC[]);; X Xlet MULT_CORRECTNESS = X prove_thm X (`MULT_CORRECTNESS`, X "MULT_IMP(i1,i2,o1,o2,done) /\ X NEXT(x,x + d)done /\ X STABLE(x,x + d)(\x'. i1 x',i2 x') /\ X done x ==> X (o2(x + d) = (i1 x) * (i2 x))", X REPEAT STRIP_TAC X THEN IMP_RES_TAC NEXT_MULT_LEMMA4 X THEN ASSUME_TAC (UNDISCH MULT_FUN_LEMMA2) X THEN IMP_RES_TAC EQ_TRANS X THEN IMP_RES_TAC(fst(EQ_IMP_RULE(SPEC_ALL PAIR_SPLIT))));; X X(print_newline();print_string `<<<`;print_newline());; X SHAR_EOF $TOUCH -am 0122095893 newbench/do_benchmark.ml && chmod 0644 newbench/do_benchmark.ml || echo "restore of newbench/do_benchmark.ml failed" set `wc -c newbench/do_benchmark.ml`;Wc_c=$1 if test "$Wc_c" != "15369"; then echo original size 15369, current size $Wc_c fi exit 0