1(*---------------------------------------------------------------------------* 2 * The multiplier example from the LCF_LSM paper. * 3 *---------------------------------------------------------------------------*) 4 5app load ["unwindLib", "numLib", "pairTheory"]; 6 7open Prim_rec numLib unwindLib Rsyntax; 8 9val _ = Rewrite.add_implicit_rewrites pairTheory.pair_rws; 10 11 12(*---------------------------------------------------------------------------* 13 * Do some profiling. * 14 *---------------------------------------------------------------------------*) 15 16val meter = Count.mk_meter(); 17val timer = Lib.start_time(); 18 19(*--------------------------------------------------------------------------- 20 * Theorem for projection of a sequence of microcycles into a single 21 * macrocycle. 22 *---------------------------------------------------------------------------*) 23 24val _ = new_theory "NEXT"; 25 26val INDUCTION = numTheory.INDUCTION; 27val INDUCT_TAC = INDUCT_THEN INDUCTION ASSUME_TAC; 28 29val SUC_LESS = prim_recTheory.SUC_LESS; 30val LESS_REFL = prim_recTheory.LESS_REFL; 31val LESS_SUC_REFL = prim_recTheory.LESS_SUC_REFL; 32 33val LESS_LESS_SUC = arithmeticTheory.LESS_LESS_SUC; 34val LESS_SUC_EQ_COR = arithmeticTheory.LESS_SUC_EQ_COR; 35val FUN_EQ_LEMMA = arithmeticTheory.FUN_EQ_LEMMA; 36val LESS_TRANS = arithmeticTheory.LESS_TRANS; 37val LESS_OR_EQ = arithmeticTheory.LESS_OR_EQ; 38val LESS_ADD_NONZERO = arithmeticTheory.LESS_ADD_NONZERO; 39val LESS_EQ_SUC_REFL = arithmeticTheory.LESS_EQ_SUC_REFL; 40val LESS_CASES_IMP = arithmeticTheory.LESS_CASES_IMP; 41val ADD_INV_0 = arithmeticTheory.ADD_INV_0; 42val ADD1 = arithmeticTheory.ADD1; 43val ADD_CLAUSES = arithmeticTheory.ADD_CLAUSES; 44 45 46val NEXT = 47 new_definition 48 ("NEXT", 49 --`!done x1 x2. 50 NEXT (x1,x2) done = 51 (x1 < x2 /\ done x2 /\ !x. x1 < x /\ x < x2 ==> ~done x)`--); 52 53val STABLE = 54 new_definition 55 ("STABLE", 56 --`!(i:num->'a). !x1 x2. 57 STABLE (x1,x2) i = !x. ((x1 <= x) /\ (x < x2)) ==> (i x = i x1)`--); 58 59val NEXT_SUC1 = 60 store_thm 61 ("NEXT_SUC1", 62 --`!done x. done(SUC x) ==> NEXT (x,SUC x) done`--, 63 REPEAT STRIP_TAC 64 THEN REWRITE_TAC[NEXT] 65 THEN REPEAT STRIP_TAC 66 THEN ASM_REWRITE_TAC[LESS_SUC_REFL] 67 THEN IMP_RES_TAC LESS_LESS_SUC 68 THEN ASM_REWRITE_TAC[]); 69 70(* LESS_SUC_EQ_LEMMA = |- ~(n = SUC m) ==> m < n ==> (SUC m) < n *) 71val LESS_SUC_EQ_LEMMA = 72 (DISCH_ALL 73 (MP (SPEC_ALL LESS_SUC_EQ_COR) 74 (CONJ (ASSUME (--`m < n`--)) 75 (NOT_EQ_SYM(ASSUME (--`~(n = SUC m)`--)))))); 76 77local val FUN_EQ_LEMMA' = INST_TYPE[alpha |-> Type`:num`] FUN_EQ_LEMMA 78in 79val NEXT_SUC2 = 80 store_thm 81 ("NEXT_SUC2", 82 --`!done x1 x2. 83 (NEXT (x1,x2) done /\ ~(done(SUC x1))) ==> NEXT (SUC x1,x2) done`--, 84 REPEAT GEN_TAC 85 THEN REWRITE_TAC[NEXT] 86 THEN REPEAT STRIP_TAC 87 THEN IMP_RES_TAC SUC_LESS 88 THEN RES_TAC 89 THEN ASM_REWRITE_TAC[] 90 THEN IMP_RES_TAC 91 (SPECL[--`done:num->bool`--, 92 --`x2:num`--, 93 --`SUC x1`--] FUN_EQ_LEMMA') 94 THEN IMP_RES_TAC LESS_SUC_EQ_LEMMA 95 THEN ASM_REWRITE_TAC[]) 96end; 97 98val STABLE_SUC = 99 store_thm 100 ("STABLE_SUC", 101 --`!x1 x2 (i:num->'a). (STABLE (x1,x2) i) ==> (STABLE ((SUC x1),x2) i)`--, 102 REPEAT GEN_TAC 103 THEN REWRITE_TAC[STABLE,LESS_OR_EQ] 104 THEN REPEAT STRIP_TAC 105 THEN ASM_REWRITE_TAC[] 106 THEN IMP_RES_TAC SUC_LESS 107 THEN IMP_RES_TAC LESS_TRANS 108 THEN ASSUME_TAC(SPEC (--`x1:num`--) LESS_SUC_REFL) 109 THEN RES_TAC 110 THEN ASM_REWRITE_TAC[]); 111 112val SUC_LEMMA = 113 let val [th1,th2,th3,th4] = CONJUNCTS ADD_CLAUSES 114 in save_thm("SUC_LEMMA",LIST_CONJ[th1,th2,SYM th3,th4]) 115 end; 116 117val stb_SUC = 118 SPEC (--`SUC x`--) 119 (ASSUME (--`!x'. ((x <= x') /\ (x' < ((SUC x) + d))) ==> 120 ((i:num->'a) x' = (i x))`--)); 121 122val STABLE_LEMMA = store_thm("STABLE_LEMMA", 123 --`!x d (i:num->'a). 124 ((STABLE (x,((SUC x)+d)) i) /\ ~(d = 0)) ==> (i x = i(SUC x))`--, 125 REWRITE_TAC[STABLE] 126 THEN REPEAT STRIP_TAC 127 THEN ASSUME_TAC stb_SUC 128 THEN IMP_RES_TAC(SPECL[--`SUC x`--, --`d:num`--] LESS_ADD_NONZERO) 129 THEN CONV_TAC SYM_CONV 130 THEN FIRST_ASSUM MATCH_MP_TAC 131 THEN ASSUME_TAC(SPEC (--`x:num`--) LESS_EQ_SUC_REFL) 132 THEN ASM_REWRITE_TAC[]); 133 134val NEXT_LEMMA1 = 135 store_thm 136 ("NEXT_LEMMA1", 137 --`!done x1 x2. 138 (NEXT (x1,x2) done /\ NEXT (x1,x3) done) ==> (x2 = x3)`--, 139 REPEAT GEN_TAC 140 THEN REWRITE_TAC[NEXT] 141 THEN STRIP_TAC 142 THEN ASM_CASES_TAC (--`(x2:num) = x3`--) 143 THEN ASM_CASES_TAC (--`x2 < x3`--) 144 THEN ASM_REWRITE_TAC[] 145 THEN IMP_RES_TAC LESS_CASES_IMP 146 THEN RES_TAC); 147 148val next_SUC = 149 DISCH_ALL 150 (REWRITE_RULE 151 [ADD_CLAUSES] 152 (SUBS [ASSUME (--`d = 0`--)] 153 (ASSUME (--`(done:num->bool) (SUC x + d)`--)))); 154 155val NEXT_LEMMA2 = 156 store_thm 157 ("NEXT_LEMMA2", 158 --`!x d done. 159 (NEXT (x,(SUC x)+d) done /\ ~(done(SUC x))) ==> ~(d = 0)`--, 160 REWRITE_TAC[NEXT] 161 THEN REPEAT STRIP_TAC 162 THEN IMP_RES_TAC next_SUC 163 THEN RES_TAC); 164 165val assm = 166 ASSUME (--`(!x. (done x = f(s x)) /\ (s(SUC x) = g(i x,s x))) /\ 167 (!a b. (FN:('a#'b)->'b)(a,b) = (if f b then b else FN(a,g(a,b))))`--) ; 168 169val [done_s,FN] = CONJUNCTS assm; 170 171val ind_hyp = 172 ASSUME (--`!x. (NEXT(x,x + d)done /\ STABLE(x,x + d)i) ==> 173 (s(x + d) = (FN:('a#'b)->'b)(i x,g(i x,s x)))`--); 174 175val s_tm = 176 ASSUME (--`s(SUC x + d) = (FN:('a#'b)->'b)(i(SUC x),g(i(SUC x),s(SUC x)))`--); 177 178val NEXT_THM = 179 store_thm 180 ("NEXT_THM", 181 --`!(FN : 'a#'b -> 'b). 182 !(f:'b->bool). 183 !(g: 'a#'b -> 'b). 184 !(done : num->bool). 185 !(i:num->'a). 186 !(s:num->'b). 187 ((!x. (done x = f(s x)) /\ (s(x+1) = g(i x,s x))) /\ 188 (!a b. FN(a,b) = (if f b then b else FN(a,g(a,b))))) ==> 189 (!d x. 190 (NEXT(x,x+d)done /\ STABLE(x,x+d)i) ==> 191 (s(x+d) = FN(i x,g(i x,s x))))`--, 192 REPEAT GEN_TAC 193 THEN REWRITE_TAC[SYM(SPEC_ALL ADD1)] 194 THEN REPEAT DISCH_TAC 195 THEN INDUCT_TAC 196 THENL [REWRITE_TAC[NEXT,LESS_REFL,ADD_CLAUSES],ALL_TAC] 197 THEN REWRITE_TAC[SUC_LEMMA] 198 THEN REPEAT STRIP_TAC 199 THEN ASM_CASES_TAC (--`(done(SUC x)):bool`--) 200 THENL 201 [IMP_RES_TAC NEXT_SUC1 202 THEN IMP_RES_TAC NEXT_LEMMA1 203 THEN IMP_RES_TAC ADD_INV_0 204 THEN REWRITE_TAC[ASSUME (--`d=0`--),ADD_CLAUSES] 205 THEN REWRITE_TAC 206 ([SPECL[--`(i:num->'a)x`--, 207 --`(g:('a#'b)->'b)(i(x:num),s x)`--] FN, 208 ASSUME (--`(done(SUC x)):bool`--)] @ 209 (map SYM (CONJUNCTS(SPEC_ALL done_s)))), 210 ALL_TAC] 211 THEN ASSUME_TAC(SPEC (--`SUC x`--) ind_hyp) 212 THEN IMP_RES_TAC STABLE_SUC 213 THEN IMP_RES_TAC NEXT_SUC2 214 THEN RES_TAC 215 THEN REWRITE_TAC[s_tm] 216 THEN SUBST_TAC[SPECL[--`(i:num->'a)x`--, 217 --`(g:('a#'b)->'b)(i(x:num),s x)`--]FN] 218 THEN REWRITE_TAC 219 (ASSUME (--`~done(SUC x)`--)::(map SYM (CONJUNCTS(SPEC_ALL done_s)))) 220 THEN IMP_RES_TAC NEXT_LEMMA2 221 THEN IMP_RES_TAC STABLE_LEMMA 222 THEN REWRITE_TAC[ASSUME (--`(i:num->'a) x = i(SUC x)`--),done_s]); 223 224val _ = export_theory(); 225 226 227(****************************************************************************) 228(****************************************************************************) 229(****************************************************************************) 230 231 232val _ = new_theory "MULT_FUN_CURRY"; 233 234val num_Axiom = prim_recTheory.num_Axiom; 235val num_CASES = arithmeticTheory.num_CASES; 236val SUC_SUB1 = arithmeticTheory.SUC_SUB1; 237val SUB = arithmeticTheory.SUB; 238 239val MULT_FUN_CURRY = new_recursive_definition 240 {name = "MULT_FUN_CURRY", rec_axiom = num_Axiom, 241 def = --`(MULT_FUN_CURRY 0 i1 i2 m t = 242 (if t then (m,0,t) else (if i1=0 then m else i2+m,0,T))) 243 /\ 244 (MULT_FUN_CURRY (SUC n) i1 i2 m t = 245 (if t then (m,SUC n,t) 246 else MULT_FUN_CURRY n i1 i2 (if i1=0 then m else i2+m) 247 (((n-1)=0) \/ (i2=0))))`--}; 248 249(*--------------------------------------------------------------------------- 250 * Rewriting ambiguity between SUC_SUB1 and SUB means that hol88 251 * does the following proof properly, but hol90 won't. Both will do 252 * the "non-commented-out version" 253 * 254 * val MULT_FUN_CURRY_THM = 255 * store_thm 256 * ("MULT_FUN_CURRY_THM", 257 * --`!i1 i2 m n t. 258 * MULT_FUN_CURRY n i1 i2 m t = 259 * (if t then (m,n,t) 260 * else MULT_FUN_CURRY (n-1) i1 i2 (if i1=0 then m else i2+m) 261 * ((((n-1)-1)=0) \/ (i2=0)))`--, 262 * REPEAT GEN_TAC 263 * THEN STRUCT_CASES_TAC(SPEC (--`n:num`--) num_CASES) 264 * THEN ASM_CASES_TAC (--`t:bool`--) 265 * THEN ASM_REWRITE_TAC[MULT_FUN_CURRY,SUC_SUB1,SUB]); 266 *---------------------------------------------------------------------------*) 267 268val MULT_FUN_CURRY_THM = store_thm("MULT_FUN_CURRY_THM", 269 --`!i1 i2 m n t. 270 MULT_FUN_CURRY n i1 i2 m t = 271 (if t then (m,n,t) 272 else MULT_FUN_CURRY(n-1) i1 i2 (if i1=0 then m else i2+m) (((n-1)-1=0)\/(i2=0)))`--, 273 REPEAT GEN_TAC 274 THEN STRUCT_CASES_TAC(SPEC (--`n:num`--) num_CASES) 275 THEN ASM_CASES_TAC (--`t:bool`--) 276 THEN REWRITE_TAC[SUC_SUB1] 277 THEN ASM_REWRITE_TAC[MULT_FUN_CURRY,SUB]); 278 279 280val MULT_FUN = new_definition("MULT_FUN", 281 --`MULT_FUN((i1,i2),m,n,t) = MULT_FUN_CURRY n i1 i2 m t`--); 282 283val MULT_FUN_DEF = store_thm("MULT_FUN_DEF", 284 --`!i1 i2 m n t. 285 MULT_FUN((i1,i2),m,n,t) = 286 (if t then (m,n,t) 287 else MULT_FUN ((i1,i2), (if i1=0 then m else i2+m), (n-1), 288 ((((n-1)-1)=0) \/ (i2=0))))`--, 289 REPEAT GEN_TAC 290 THEN REWRITE_TAC[MULT_FUN] 291 THEN ACCEPT_TAC(SPEC_ALL MULT_FUN_CURRY_THM)); 292 293val _ = export_theory(); 294 295 296(****************************************************************************) 297(****************************************************************************) 298(****************************************************************************) 299 300 301val _ = new_theory "MULT_FUN"; 302 303val LESS_0 = prim_recTheory.LESS_0; 304 305val LESS_OR_EQ = arithmeticTheory.LESS_OR_EQ; 306val LESS_MONO_EQ = arithmeticTheory.LESS_MONO_EQ; 307val ADD_EQ_SUB = arithmeticTheory.ADD_EQ_SUB; 308val ADD_CLAUSES = arithmeticTheory.ADD_CLAUSES; 309val SUB_0 = arithmeticTheory.SUB_0; 310val MULT_CLAUSES = arithmeticTheory.MULT_CLAUSES; 311val ADD_SYM = arithmeticTheory.ADD_SYM; 312val ADD_ASSOC = arithmeticTheory.ADD_ASSOC; 313val LESS_EQ_ADD = arithmeticTheory.LESS_EQ_ADD; 314val RIGHT_SUB_DISTRIB = arithmeticTheory.RIGHT_SUB_DISTRIB; 315val SUB_ADD = arithmeticTheory.SUB_ADD; 316val SUC_SUB1 = arithmeticTheory.SUC_SUB1; 317 318(* val MULT_FUN_DEF = MULT_FUN_CURRYTheory.MULT_FUN_DEF; *) 319 320val MULT_FUN_T = 321 store_thm 322 ("MULT_FUN_T", 323 --`!i1 i2 m n. 324 MULT_FUN((i1,i2),m,n,T) = (m,n,T)`--, 325 REPEAT GEN_TAC 326 THEN ASM_CASES_TAC (--`t:bool`--) 327 THEN REWRITE_TAC[INST [--`t:bool`-- |-> --`T`--] (SPEC_ALL MULT_FUN_DEF)]); 328 329val MULT_FUN_F = 330 store_thm 331 ("MULT_FUN_F", 332 --`!i1 i2 m n. 333 MULT_FUN((i1,i2),m,n,F) = 334 MULT_FUN((i1,i2),(if i1=0 then m else i2+m),(n-1),((((n-1)-1)=0) \/ (i2=0)))`--, 335 REPEAT GEN_TAC 336 THEN ASM_CASES_TAC (--`t:bool`--) 337 THEN REWRITE_TAC[INST[--`t:bool`-- |-> --`F`--] (SPEC_ALL MULT_FUN_DEF)]); 338 339val LESS_EQ_0 = 340 store_thm 341 ("LESS_EQ_0", 342 --`!m. 0 <= m`--, 343 INDUCT_TAC 344 THEN ASM_REWRITE_TAC[LESS_OR_EQ,LESS_0]); 345 346val LESS_EQ_SUC_1 = 347 store_thm 348 ("LESS_EQ_SUC_1", 349 --`!m. 1 <= SUC m`--, 350 INDUCT_TAC 351 THEN ASM_REWRITE_TAC[num_CONV (--`1`--),LESS_OR_EQ,LESS_MONO_EQ,LESS_0]); 352 353val EQ_SYM_EQ' = INST_TYPE[alpha |-> Type`:num`] EQ_SYM_EQ; 354 355val SUB_LEMMA1 = 356 store_thm 357 ("SUB_LEMMA1", 358 --`!m.(~(m=0)) ==> (((m-1)=0) ==> (m=1))`--, 359 INDUCT_TAC 360 THEN REWRITE_TAC 361 [SYM 362 (SUBS 363 [SPECL[--`0`--, --`(SUC m)-1`--]EQ_SYM_EQ'] 364 (MP 365 (SPECL 366 [--`0`--, --`1`--, --`SUC m`--]ADD_EQ_SUB) 367 (SPEC (--`m:num`--) LESS_EQ_SUC_1))), 368 ADD_CLAUSES] 369 THEN REPEAT STRIP_TAC 370 THEN ASM_REWRITE_TAC[]); 371 372val SUB_LEMMA2 = 373 store_thm 374 ("SUB_LEMMA2", 375 --`!m.(m=0) ==> ((~((m-1)=0)) ==> F)`--, 376 GEN_TAC 377 THEN DISCH_TAC 378 THEN ASM_REWRITE_TAC[SUB_0]); 379 380val MULT_NOT_0_LESS = 381 store_thm 382 ("MULT_NOT_0_LESS", 383 --`!m n. (~(m = 0)) ==> (n <= (m * n))`--, 384 INDUCT_TAC 385 THEN GEN_TAC 386 THEN REWRITE_TAC[MULT_CLAUSES,SUBS[SPEC_ALL ADD_SYM] 387 (SPEC_ALL LESS_EQ_ADD)]); 388 389val MULT_ADD_LEMMA1 = 390 store_thm 391 ("MULT_ADD_LEMMA1", 392 --`!m. (~(m=0)) ==> (!n p. (((m-1)*n)+(n+p)) = ((m*n)+p))`--, 393 REPEAT STRIP_TAC 394 THEN REWRITE_TAC[ADD_ASSOC,RIGHT_SUB_DISTRIB,MULT_CLAUSES] 395 THEN IMP_RES_THEN (ASSUME_TAC o SPEC (--`n:num`--)) MULT_NOT_0_LESS 396 THEN IMP_RES_TAC SUB_ADD 397 THEN ASM_REWRITE_TAC[]); 398 399val MULT_FUN_THM = 400 store_thm 401 ("MULT_FUN_THM", 402 --`!n i1 i2 m t. 403 MULT_FUN((i1,i2),m,n,t) = 404 if t then 405 (m,n,t) 406 else 407 (if ((n-1)=0)\/(i2=0) then 408 ((if i1=0 then m else i2+m),(n-1),T) 409 else 410 ((if i1=0 then m else ((n-1)*i2)+m),1,T))`--, 411 INDUCT_TAC 412 THEN REPEAT GEN_TAC 413 THEN ASM_CASES_TAC (--`t:bool`--) 414 THEN ASM_REWRITE_TAC[MULT_FUN_T,MULT_FUN_F,SUC_SUB1,SUB_0] 415 THEN ASM_CASES_TAC (--`i1=0`--) 416 THEN ASM_CASES_TAC (--`i2=0`--) 417 THEN ASM_CASES_TAC (--`n=0`--) 418 THEN ASM_CASES_TAC (--`(n-1)=0`--) 419 THEN ASM_REWRITE_TAC[MULT_FUN_T,MULT_FUN_F,SUC_SUB1,SUB_0] 420 THEN IMP_RES_TAC SUB_LEMMA1 421 THEN IMP_RES_TAC SUB_LEMMA2 422 THEN IMP_RES_TAC MULT_ADD_LEMMA1 423 THEN ASM_REWRITE_TAC[MULT_CLAUSES]); 424 425val MULT_ADD_LEMMA2 = 426 store_thm 427 ("MULT_ADD_LEMMA2", 428 --`!m. ~(m=0) ==> !n. ((m-1)*n)+n = m*n`--, 429 REPEAT STRIP_TAC 430 THEN REWRITE_TAC[RIGHT_SUB_DISTRIB,MULT_CLAUSES] 431 THEN IMP_RES_THEN (ASSUME_TAC o SPEC (--`n:num`--)) MULT_NOT_0_LESS 432 THEN IMP_RES_TAC SUB_ADD 433 THEN ASM_REWRITE_TAC[]); 434 435val MULT_FUN_LEMMA = 436 store_thm 437 ("MULT_FUN_LEMMA", 438 --`!i1 i2. 439 (MULT_FUN((i1,i2),(if i1=0 then 0 else i2),i1,(((i1-1)=0)\/(i2=0)))) = 440 ((i1*i2), (if ((i1-1)=0)\/(i2=0) then i1 else 1), T)`--, 441 REPEAT GEN_TAC 442 THEN ASM_CASES_TAC (--`i1=0`--) 443 THEN ASM_CASES_TAC (--`i2=0`--) 444 THEN ASM_REWRITE_TAC[MULT_FUN_THM,MULT_CLAUSES,SUB_0] 445 THEN ASM_CASES_TAC (--`(i1-1)=0`--) 446 THEN IMP_RES_TAC SUB_LEMMA1 447 THEN IMP_RES_TAC MULT_ADD_LEMMA2 448 THEN ASM_REWRITE_TAC[MULT_CLAUSES]); 449 450val _ = export_theory(); 451 452 453(****************************************************************************) 454(****************************************************************************) 455(****************************************************************************) 456 457(*--------------------------------------------------------------------------- 458 * Define the basic components of the circuit. 459 *---------------------------------------------------------------------------*) 460 461val _ = new_theory "prims"; 462 463val [MUX,REG,FLIPFLOP,DEC,ADDER,ZERO_TEST,OR_GATE,IS_ZERO] = 464 map new_definition 465 [("MUX" , --`MUX(switch,(i1:num->num),(i2:num->num),out) = 466 !(x:num). out x = (if switch x then i1 x else i2 x)`--), 467 468 ("REG" , --`REG((i:num->num),out) = !x. out(x+1) = i x`--), 469 470 ("FLIPFLOP" , --`FLIPFLOP((i:num->bool),out) = !x. out(x+1) = i x`--), 471 472 ("DEC" , --`DEC(i,out) = !x:num. out x = (i x - 1)`--), 473 474 ("ADDER" , --`ADDER(i1,i2,out) = !x:num. out x = i1 x + i2 x`--), 475 476 ("ZERO_TEST", --`ZERO_TEST(i,out) = !x:num. out x = (i x = 0)`--), 477 478 ("OR_GATE" , --`OR_GATE(i1,i2,out) = !x:num. out x = (i1 x \/ i2 x)`--), 479 480 ("IS_ZERO" , --`IS_ZERO(out) = !x:num. out x = 0`--)]; 481 482val _ = export_theory(); 483 484 485 486(*--------------------------------------------------------------------------- 487 * Define the implementation of the circuit. 488 *---------------------------------------------------------------------------*) 489 490val _ = new_theory "MULT_IMP"; 491 492val _ = ``prims$MUX``; 493 494val MULT_IMP = new_definition 495 ("MULT_IMP", 496 --`MULT_IMP(i1,i2,o1,o2,done) = 497 ?b1 b2 b3 b4 l1 l2 l3 l4 l5 l6 l7 l8 l9. 498 MUX(done,l8,l7,l6) /\ 499 REG(l6,o2) /\ 500 ADDER(l8,o2,l7) /\ 501 DEC(i1,l5) /\ 502 MUX(done,l5,l3,l4) /\ 503 MUX(done,i1,l2,l1) /\ 504 REG(l1,o1) /\ 505 DEC(o1,l2) /\ 506 DEC(l2,l3) /\ 507 IS_ZERO(l9) /\ 508 MUX(b4,l9,i2,l8) /\ 509 ZERO_TEST(i1,b4) /\ 510 ZERO_TEST(l4,b1) /\ 511 ZERO_TEST(i2,b2) /\ 512 OR_GATE(b1,b2,b3) /\ 513 FLIPFLOP(b3,done)`--); 514 515val _ = new_theory"MULT_VER"; 516 517 518val ADD_CLAUSES = arithmeticTheory.ADD_CLAUSES; 519val prims = [MUX,REG,FLIPFLOP,DEC,ADDER,ZERO_TEST,IS_ZERO,OR_GATE] 520 521 522(* Now use the unwinding rules. *) 523val MULT_IMP_UNFOLD = 524 save_thm("MULT_IMP_UNFOLD", 525 unwindLib.UNFOLD_RIGHT_RULE prims MULT_IMP); 526 527val MULT_IMP_UNWIND = 528 save_thm("MULT_IMP_UNWIND", 529 unwindLib.UNWIND_AUTO_RIGHT_RULE MULT_IMP_UNFOLD); 530 531val MULT_IMP_PRUNE = 532 save_thm("MULT_IMP_PRUNE", 533 unwindLib.PRUNE_RIGHT_RULE MULT_IMP_UNWIND); 534 535val MULT_IMP_EXPAND = 536 save_thm("MULT_IMP_EXPAND", 537 unwindLib.EXPAND_AUTO_RIGHT_RULE prims MULT_IMP); 538 539val COND_ADD_LEMMA = store_thm("COND_ADD_LEMMA", 540 --`((if b then m else n) + p) = (if b then m + p else n + p)`--, 541 COND_CASES_TAC 542 THEN ASM_REWRITE_TAC[]); 543 544 545val MULT_FUN_EXPANDED_DEF = store_thm("MULT_FUN_EXPANDED_DEF", 546 --`!i1 i2 m n t. 547 MULT_FUN((i1,i2),m,n,t) = 548 (if t then 549 (m,n,t) 550 else 551 MULT_FUN 552 ((i1, i2), 553 (if t then (if i1 = 0 then 0 else i2) else (if i1 = 0 then 0 else i2) + m), 554 (if t then i1 else n - 1), 555 (((if t then i1 - 1 else (n - 1) - 1) = 0) \/ (i2 = 0))))`--, 556 REPEAT GEN_TAC 557 THEN ASM_CASES_TAC (--`t:bool`--) 558 THEN ASM_REWRITE_TAC[MULT_FUN_T,MULT_FUN_F,COND_ADD_LEMMA,ADD_CLAUSES]); 559 560 561val G_FUN = new_definition("G_FUN", 562 --`!i1 i2 m n t. 563 G_FUN((i1,i2),(m,n,t)) = 564 ((if t then (if i1 = 0 then 0 else i2) else (if i1 = 0 then 0 else i2) + m), 565 (if t then i1 else n - 1), 566 (((if t then i1 - 1 else (n - 1) - 1) = 0) \/ (i2 = 0)))`--); 567 568val NEXT_THM' = 569 INST_TYPE[alpha |-> Type`:num#num`, beta |-> Type`:num#num#bool`] NEXT_THM; 570 571 572val NEXT_MULT_LEMMA1 = save_thm("NEXT_MULT_LEMMA1", 573 REWRITE_RULE [] 574 (CONV_RULE (DEPTH_CONV BETA_CONV) 575 (SPECL [--`MULT_FUN`--, 576 --`\(x:num#num#bool).SND(SND x)`--, 577 --`G_FUN`--, 578 --`done:num->bool`--, 579 --`\x. ((i1:num->num) x, (i2:num->num) x)`--, 580 --`\x. ((o2:num->num) x, 581 (o1:num->num) x, 582 (done:num->bool) x)`--] 583 NEXT_THM'))); 584 585val NEXT_MULT_LEMMA2 = store_thm("NEXT_MULT_LEMMA2", 586 --`MULT_IMP(i1,i2,o1,o2,done) 587 ==> !x. 588 (o2(x + 1),o1(x + 1),done(x + 1)) = 589 G_FUN((i1 x,i2 x),o2 x,o1 x,done x)`--, 590 REWRITE_TAC[MULT_IMP_EXPAND] 591 THEN REPEAT STRIP_TAC 592 THEN ASM_REWRITE_TAC[G_FUN]); 593 594val PAIR = pairTheory.PAIR; 595 596val G_FUN_LEMMA = save_thm("G_FUN_LEMMA", 597 PURE_REWRITE_RULE [PAIR] 598 (SPECL [--`FST(a:num#num)`--, 599 --`SND(a:num#num)`--, 600 --`FST(b:num#num#bool)`--, 601 --`FST(SND(b:num#num#bool))`--, 602 --`SND(SND(b:num#num#bool))`--] G_FUN)); 603 604val NEXT_MULT_LEMMA3 = save_thm("NEXT_MULT_LEMMA3", 605 PURE_REWRITE_RULE [PAIR,SYM G_FUN_LEMMA] 606 (SPECL [--`FST(a:num#num)`--, 607 --`SND(a:num#num)`--, 608 --`FST(b:num#num#bool)`--, 609 --`FST(SND(b:num#num#bool))`--, 610 --`SND(SND(b:num#num#bool))`--] MULT_FUN_EXPANDED_DEF)); 611 612val NEXT_MULT_LEMMA4 = save_thm("NEXT_MULT_LEMMA4", 613 DISCH_ALL (REWRITE_RULE [UNDISCH NEXT_MULT_LEMMA2,SYM NEXT_MULT_LEMMA3] 614 NEXT_MULT_LEMMA1)); 615 616val MULT_FUN_LEMMA1 = MULT_FUN_LEMMA; 617 618val MULT_FUN_LEMMA2 = store_thm("MULT_FUN_LEMMA2", 619 --`(done:num->bool) x ==> 620 (MULT_FUN((i1 x,i2 x),G_FUN((i1 x,i2 x),o2 x,o1 x,done x)) = 621 ((i1 x * i2 x), 622 (if ((i1 x - 1) = 0) \/ (i2 x = 0) 623 then i1 x 624 else 1), 625 T))`--, 626 DISCH_TAC THEN ASM_REWRITE_TAC[MULT_FUN_LEMMA1,G_FUN]); 627 628(* Already exists in theory "pair" *) 629 630val PAIR_SPLIT = store_thm("PAIR_SPLIT", 631 --`!(x1:'a) (y1:'b) x2 y2. 632 ((x1,y1) = (x2,y2)) = (x1 = x2) /\ (y1 = y2)`--, 633 REPEAT GEN_TAC 634 THEN EQ_TAC 635 THEN REPEAT STRIP_TAC 636 THEN ASM_REWRITE_TAC[] 637 THEN ASSUME_TAC (REWRITE_RULE [] 638 (AP_TERM (--`FST:('a#'b)->'a`--) 639 (ASSUME (--`(x1:'a,(y1:'b)) = (x2,y2)`--)))) 640 THEN ASSUME_TAC (REWRITE_RULE [] 641 (AP_TERM (--`SND:('a#'b)->'b`--) 642 (ASSUME (--`(x1:'a,(y1:'b)) = (x2,y2)`--)))) 643 THEN ASM_REWRITE_TAC[]); 644 645val MULT_CORRECTNESS = store_thm("MULT_CORRECTNESS", 646 --`MULT_IMP(i1,i2,o1,o2,done) /\ 647 NEXT(x,x + d) done /\ 648 STABLE(x,x + d)(\x'. i1 x',i2 x') /\ 649 done x ==> 650 (o2(x + d) = i1 x * i2 x)`--, 651 REPEAT STRIP_TAC 652 THEN IMP_RES_TAC NEXT_MULT_LEMMA4 653 THEN ASSUME_TAC (UNDISCH MULT_FUN_LEMMA2) 654 THEN IMP_RES_TAC EQ_TRANS 655 THEN IMP_RES_TAC(fst(EQ_IMP_RULE(SPEC_ALL PAIR_SPLIT)))); 656 657 658val _ = export_theory (); 659 660 661(*---------------------------------------------------------------------------* 662 * All done, print out time and inference rule breakdown. * 663 *---------------------------------------------------------------------------*) 664 665val _ = Lib.end_time timer; 666val _ = Count.report(Count.read meter); 667 668(* end; *) 669