1(*****************************************************************************) 2(* The project starts off by loading the encoding library: acl2encodeLib *) 3(*****************************************************************************) 4 5load "acl2encodeLib"; 6open acl2encodeLib; 7 8(*****************************************************************************) 9(* We also load the example types and the example functions. *) 10(*****************************************************************************) 11 12load "testTypesTheory"; 13load "testFunctionsTheory"; 14 15(*---------------------------------------------------------------------------*) 16(* Simple functions: *) 17(*---------------------------------------------------------------------------*) 18 19(*****************************************************************************) 20(* We start by encoding simple functions, that is, functions that may be *) 21(* translated across their entire range (they are fully specified) and rely *) 22(* only on functions that may be encoded across their entire range. *) 23(* Functions may be given in clausal or equational (a single clause) *) 24(* form, where mutually recursive functions are given as conjunctions. *) 25(* *) 26(* Such functions are translated using the function: *) 27(* translate_simple_function : (term * string) list -> thm -> thm *) 28(* *) 29(* The first argument relates function constants to the names of translated *) 30(* functions and the second is the argument itself. *) 31(* *) 32(* The function EXP: *) 33(* |- (!m. m ** 0 = 1) /\ (!m n. m ** SUC n = m * m ** n) *) 34(* is translated as follows: *) 35(*****************************************************************************) 36 37val translated_exp = 38 translate_simple_function 39 [(``($**):num -> num -> num``,"exp")] 40 arithmeticTheory.EXP; 41 42(*****************************************************************************) 43(* val translated_exp = *) 44(* |- exp m arg = *) 45(* ite (andl [natp m; natp arg]) *) 46(* (ite (zp arg) (nat 1) *) 47(* (mult m (acl2_expt m (add arg (unary_minus (nat 1)))))) (nat 0) : thm *) 48(* *) 49(* This also produces the following theorem: *) 50(*****************************************************************************) 51 52val propagation_exp = fetch "-" "prop_exp"; 53 54(*****************************************************************************) 55(* val propagation_exp = |- nat (m ** arg) = exp (nat m) (nat arg) : thm *) 56(* *) 57(* This theorem is automatically added to the set of rewrites, *) 58(* functionEncodeLib.rewrites, using the function *) 59(* functionEncodeLib.add_standard_rewrite 0 "prop_exp" ... *) 60(* *) 61(* The function LENGTH (instantiated to operate on concrete lists of natural *) 62(* numbers) can also be converted using this form: *) 63(*****************************************************************************) 64 65val translated_length = 66 translate_simple_function 67 [(``LENGTH``,"length")] 68 (INST_TYPE [alpha |-> ``:num``] listTheory.LENGTH); 69 70val propagation_length = fetch "-" "prop_length"; 71 72(*****************************************************************************) 73(* val translated_length = *) 74(* |- length arg = *) 75(* ite (listnum arg) *) 76(* (ite (atom arg) (nat 0) (add (len (cdr arg)) (nat 1))) (nat 0) : thm *) 77(* *) 78(* val propagation_length = *) 79(* |- nat (LENGTH arg) = length (list nat arg) : thm *) 80(*****************************************************************************) 81 82(*---------------------------------------------------------------------------*) 83(* Flattening recognizers: *) 84(*---------------------------------------------------------------------------*) 85 86(*****************************************************************************) 87(* It should also be noted that the constant 'listnum' is automatically *) 88(* constructed to assist this definition. This is characterised by the *) 89(* following definitions: *) 90(*****************************************************************************) 91 92val translated_listnum = fetch "-" "translated_listnum"; 93 94val propagation_listnum = fetch "-" "prop_listnum"; 95 96(*****************************************************************************) 97(* val translated_listnum = *) 98(* |- listnum x = *) 99(* ite (consp x) *) 100(* (ite (consp x) (andl [natp (car x); listnum (cdr x)]) nil) *) 101(* (equal x nil) : thm *) 102(* *) 103(* val propagation_listnum = *) 104(* |- bool (listp (sexp_to_bool o natp) x) = listnum (I x) : thm *) 105(* *) 106(* 'listnum' is created using the function: *) 107(* flatten_recognizers : (hol_type -> string) -> hol_type -> thm list *) 108(* function creates recognition functions, suitable for export to ACL2, for *) 109(* the type supplied, and any types in mutual recursion with it. *) 110(* *) 111(* We can create a different translation using this function directly: *) 112(*****************************************************************************) 113 114val [translated_natp_list] = flatten_recognizers (K "natp_list") ``:num list``; 115 116val propagation_natp_list = fetch "-" "natp_list"; 117 118(*****************************************************************************) 119(* val translated_natp_list = *) 120(* |- natp_list x = *) 121(* ite (consp x) *) 122(* (ite (consp x) (andl [natp (car x); natp_list (cdr x)]) nil) *) 123(* (equal x nil) : thm *) 124(* *) 125(* val propagation_natp_list = *) 126(* |- !x. natp_list x = bool (listp (sexp_to_bool o natp) x) : thm *) 127(* *) 128(* To use this new definition, the previous definition should be removed: *) 129(*****************************************************************************) 130 131val _ = functionEncodeLib.remove_rewrite "listnum"; 132 133(*****************************************************************************) 134(* The rewrite names are displayed in the trace as, in this case, R(listnum) *) 135(* *) 136(* As rewrites for translated functions are automatically added to the *) 137(* rewrite set, functions relying on previous translations may also be *) 138(* easily translated. For example: *) 139(*****************************************************************************) 140 141val translated_append = 142 translate_simple_function 143 [(``$++``,"append")] 144 (INST_TYPE [alpha |-> ``:num``] listTheory.APPEND); 145 146val translated_reverse = 147 translate_simple_function 148 [(``REVERSE``,"reverse")] 149 (INST_TYPE [alpha |-> ``:num``] listTheory.REVERSE_DEF); 150 151(*****************************************************************************) 152(* val translated_append = *) 153(* |- append arg l2 = *) 154(* ite (andl [natp_list arg; natp_list l2]) *) 155(* (ite (atom arg) l2 (cons (car arg) (append (cdr arg) l2))) nil *) 156(* *) 157(* val translated_reverse = *) 158(* |- reverse arg = *) 159(* ite (natp_list arg) *) 160(* (ite (atom arg) nil *) 161(* (append (reverse (cdr arg)) (cons (car arg) nil))) nil *) 162(*****************************************************************************) 163 164(*---------------------------------------------------------------------------*) 165(* Conditional functions: *) 166(*---------------------------------------------------------------------------*) 167 168(*****************************************************************************) 169(* Some functions, such as DIV,MOD or %/int_div, can only be translated over *) 170(* a subset of their range. Therefore, functions defined using these can *) 171(* only be translated over a subset of their range OR guard calls to the *) 172(* restricted functions using conditional statements. *) 173(* *) 174(* The latter form of definitions are translated using: *) 175(* translate_conditional_function : *) 176(* (term * string) list -> thm list -> thm -> thm *) 177(* This is very similar to translate_simple_function except it takes a list *) 178(* of theorems to *assist* the translation. *) 179(* *) 180(* The function 'i2n' is defined as follows: *) 181(* |- !i l. i2n i l = *) 182(* Num (if 0 <= i then i % 2 ** l *) 183(* else (i + 1) rem 2 ** l - 1 + 2 ** l) : thm *) 184(* *) 185(* The functions 'rem' and '%' can only be translated if their second *) 186(* argument is non-zero. The propagation theorems are as follows: *) 187(*****************************************************************************) 188 189val INT_REM = extendTranslateTheory.INT_REM; 190 191val INT_MOD = extendTranslateTheory.INT_MOD; 192 193(*****************************************************************************) 194(* |- ~(b = 0) ==> (int (a rem b) = acl2_rem (int a) (int b)) : thm *) 195(* |- ~(b = 0) ==> (int (a % b) = acl2_mod (int a) (int b)) : thm *) 196(* *) 197(* To translate i2n we must prove that 0 <= i implies that the second *) 198(* arguments are non-zero: *) 199(*****************************************************************************) 200 201local 202open intLib integerTheory 203val i2n_lemma = prove(``0 <= (i + 1) rem 2 ** l - 1 + 2 ** l``, 204 REWRITE_TAC [ARITH_PROVE ``0i <= a - 1 + b = ~a < b``] THEN 205 MATCH_MP_TAC (ARITH_PROVE ``!a b c. a <= b /\ b < c ==> a < c:int``) THEN 206 Q.EXISTS_TAC `ABS ((i + 1) rem 2 ** l)` THEN 207 METIS_TAC [INT_REMQUOT,INT_ABS_NUM,INT_EXP,INT_EXP_EQ0, 208 ARITH_PROVE ``~(2 = 0i)``,INT_ABS,INT_NOT_LT,INT_NEGNEG,INT_LE_REFL, 209 INT_LE_NEGL]); 210in 211val thms = [INT_EXP_EQ0,ARITH_PROVE ``~(2 = 0i)``, 212 REWRITE_CONV [integerTheory.INT_POS,integerTheory.INT_EXP] 213 ``0 <= 2 ** a``, 214 prove(``~(b = 0) /\ 0i <= b ==> 0 <= a % b``, 215 METIS_TAC [INT_MOD_BOUNDS,INT_NOT_LT]),i2n_lemma] 216end; 217 218(*****************************************************************************) 219(* val thms = *) 220(* [|- !p n. (p ** n = 0) = (p = 0) /\ ~(n = 0), |- ~(2 = 0), *) 221(* |- 0 <= 2 ** a = T, |- ~(b = 0) /\ 0 <= b ==> 0 <= a % b, *) 222(* |- 0 <= (i + 1) rem 2 ** l - 1 + 2 ** l] *) 223(* *) 224(* The translation code employs a simple forward-chaining rewriter, that *) 225(* when translating the expression 'encode (if P then A else B)' with the *) 226(* extra theorem '|- P ==> Q' the expression 'A' will be encoded under the *) 227(* assumptions 'P' and 'Q'. *) 228(* *) 229(* A simple back-chaining rewriter is also employed that attempts to prove *) 230(* a term by repeatedly rewriting using the theorems given. *) 231(* *) 232(* By setting the trace level to 3 we can see that the back-chaining *) 233(* rewriter is employed a number of times. The syntax: *) 234(* backtracking... *) 235(* #0#1#2#3#4F#4#5#6F#3#4T#3T#2#3T *) 236(* indicates the depth of search at each node, and whether the term given *) 237(* was proven true or false. *) 238(*****************************************************************************) 239 240val translated_i2n = 241 translate_conditional_function 242 [(``i2n``,"I2N")] thms 243 signedintTheory.i2n_def; 244 245(*****************************************************************************) 246(* val translated_i2n = *) 247(* |- I2N i l = *) 248(* ite (andl [integerp i; natp l]) *) 249(* (ite (not (less i (int 0))) (acl2_mod i (acl2_expt (int 2) l)) *) 250(* (add *) 251(* (add (acl2_rem (add i (int 1)) (acl2_expt (int 2) l)) *) 252(* (unary_minus (int 1))) (acl2_expt (int 2) l))) (nat 0) : thm *) 253(*****************************************************************************) 254 255(*---------------------------------------------------------------------------*) 256(* Limit functions: *) 257(*---------------------------------------------------------------------------*) 258 259(*****************************************************************************) 260(* As mentioned earlier, certain functions may not be translated across *) 261(* their entire range. In the case of SEG this is because the function *) 262(* clauses 'SEG (SUC n) _ []' are left undefined. In the case of the *) 263(* function LOG this is given explicitly: *) 264(* |- !a x. 1 < a /\ 1 <= x ==> *) 265(* (LOG a x = if x < a then 0 else 1 + LOG a (x DIV a)) : thm *) 266(* *) 267(* When translating such functions two types of theorem are required: *) 268(* a) In the case of clausal functions, a proof that the limit avoids *) 269(* the specific constructors and *) 270(* b) A proof that the limit is conserved across recursive calls. *) 271(* (In the case of clausal functions these calls use destructors) *) 272(* *) 273(* When non-clausal functions are given (a) is not required. If the function *) 274(* is non-recursive then (b) is not required. *) 275(*****************************************************************************) 276 277(*---------------------------------------------------------------------------*) 278(* A word on constructors.... *) 279(* *) 280(* All constructors are given in POSITIVE form. Hence, in the example of SEG *) 281(* we write ``?n. a = SUC n`` and not ``~(a = 0)``. This is because theorems *) 282(* are automatically derived to convert limits to this form during *) 283(* translation. *) 284(* Note: Existentials should be given in left-right fashion... *) 285(* When a recursive call is made in a clausal function the function is *) 286(* translated to a form using DESTRUCTORS. These can be viewed, for the type *) 287(* t, using the function call: *) 288(* get_coding_theorem_precise ``:sexp`` t "destructors" *) 289(* *) 290(* Destructors can be modified using the call: *) 291(* set_destructors : thm list -> unit *) 292(* Set the destructors for a given type to the theorems given. *) 293(* These theorems should be of the form: |- D (C a b c...) = b ... *) 294(* Warning: In order to translate clausal functions using these destructors *) 295(* the destructors must be translated beforehand. *) 296(*---------------------------------------------------------------------------*) 297 298val destructors = 299 polytypicLib.get_coding_theorem_precise 300 ``:sexp`` ``:'a list`` "destructors"; 301 302(*****************************************************************************) 303(* val destructors = |- (!h t. HD (h::t) = h) /\ !h t. TL (h::t) = t : thm *) 304(* *) 305(* The function SEG can be converted by provided theorems to state that: *) 306(* a) The limit is correct (limit_correct), *) 307(* b) Recursing with the list intact preserves the limit *) 308(* (limit_recusive1) *) 309(* c) Recursing while the list is reducing preserves the limit *) 310(* (limit_recursive2) *) 311(* *) 312(* SEG is translated using the function: *) 313(* translate_limit_function : *) 314(* (term * string) list -> *) 315(* (term * term list) list -> thm list -> thm -> thm *) 316(* This acts like translate_conditional_function, except for each function *) 317(* constant it takes a list of terms of the form: *) 318(* ``\a b c d... . P a b c d...``. *) 319(* These are presented as limits to the resulting function. If the theorem *) 320(* |- !a b c d ... . P a b c d ... is given in the list then the limit is *) 321(* left in the definition, but is not required in either the propagation *) 322(* theorem or translation process. *) 323(*****************************************************************************) 324 325val limit_correct = 326 prove(``a + b <= LENGTH c ==> ~((?n. a = SUC n) /\ (c = []))``, 327 Cases_on `c` THEN RW_TAC arith_ss [listTheory.LENGTH]); 328 329val limit_recursive1 = 330 prove(``(?d. a = SUC d) /\ (b = 0) /\ 331 (?x y. c = x :: y) /\ a + b <= LENGTH c ==> 332 PRE a + 0 <= LENGTH (TL c)``, 333 Cases_on `c` THEN 334 RW_TAC arith_ss [listTheory.LENGTH,listTheory.TL,listTheory.NULL]); 335 336val limit_recursive2 = 337 prove(``(?d. a = SUC d) /\ (?d. b = SUC d) /\ 338 (?x y. c = x :: y) /\ a + b <= LENGTH c ==> 339 SUC (PRE a) + PRE b <= LENGTH (TL c)``, 340 Cases_on `c` THEN 341 RW_TAC arith_ss [listTheory.LENGTH,listTheory.TL,listTheory.NULL]); 342 343val translated_seg = 344 translate_limit_function 345 [(``SEG``,"seg")] 346 [(``SEG``,[``\a b c. a + b <= LENGTH c``])] 347 [limit_correct,limit_recursive1,limit_recursive2] 348 (INST_TYPE [alpha |-> ``:num``] rich_listTheory.SEG); 349 350(*****************************************************************************) 351(* val translated_seg = *) 352(* |- seg arg'' arg' arg = *) 353(* ite *) 354(* (andl *) 355(* [natp arg''; *) 356(* andl *) 357(* [natp arg'; *) 358(* andl *) 359(* [natp_list arg; not (less (len arg) (add arg'' arg'))]]]) *) 360(* (ite (zp arg'') nil *) 361(* (ite (zp arg') *) 362(* (cons (car arg) *) 363(* (seg (add arg'' (unary_minus (nat 1))) (nat 0) (cdr arg))) *) 364(* (seg arg'' (add arg' (unary_minus (nat 1))) (cdr arg)))) nil *) 365(* *) 366(* The LOG function is translated in a similar manner to SEG. However, as it *) 367(* is not clausal we do not need to demonstrate that the limit is correct. *) 368(* The theorem 'log_rec' is used to remove the second limit from the *) 369(* translation process whereas the theorem 'log_rec_ok' proves that the *) 370(* first limit is preserved across recursive calls. *) 371(*****************************************************************************) 372 373val log_compute = prove(``1 < a /\ 1 <= x ==> 374 (LOG a x = if x < a then 0 else 1 + LOG a (x DIV a))``, 375 RW_TAC std_ss [] THEN 376 FULL_SIMP_TAC std_ss [arithmeticTheory.NOT_LESS,logrootTheory.LOG_DIV] THEN 377 MATCH_MP_TAC logrootTheory.LOG_UNIQUE THEN 378 RW_TAC arith_ss [arithmeticTheory.EXP]); 379 380val log_rec = prove(``1 < a /\ 1 <= x ==> x DIV a < x``, 381 REPEAT (Induct_on `a` THEN 382 RW_TAC arith_ss [arithmeticTheory.DIV_LT_X,arithmeticTheory.ADD1, 383 arithmeticTheory.LEFT_ADD_DISTRIB])); 384 385val log_rec_ok = prove(``~(a = 0) /\ ~(x < a) ==> (1 <= x DIV a)``, 386 RW_TAC arith_ss [arithmeticTheory.NOT_LESS,arithmeticTheory.X_LE_DIV]); 387 388val translated_log = 389 translate_limit_function 390 [(``LOG``,"log")] 391 [(``LOG``,[``\a b. 1n < a /\ 1n <= b ``, 392 ``\a b. 1 < a /\ 1 <= b ==> b DIV a < b``])] 393 [GEN_ALL log_rec,DECIDE ``1 < a ==> ~(a = 0n)``,log_rec_ok] 394 log_compute; 395 396(*****************************************************************************) 397(* val translated_log = *) 398(* |- log a x = *) 399(* ite *) 400(* (andl *) 401(* [natp a; *) 402(* andl *) 403(* [natp x; *) 404(* andl *) 405(* [less (nat 1) a; *) 406(* andl *) 407(* [not (less x (nat 1)); *) 408(* implies (andl [less (nat 1) a; not (less x (nat 1))]) *) 409(* (less (acl2_floor x a) x)]]]]) *) 410(* (ite (less x a) (nat 0) (add (nat 1) (log a (acl2_floor x a)))) *) 411(* (nat 0) : thm *) 412(*****************************************************************************) 413 414(*---------------------------------------------------------------------------*) 415(* Instantiated higher order functions: *) 416(*---------------------------------------------------------------------------*) 417 418(*****************************************************************************) 419(* Instantiated Higher Order functions are translated in the same manner as *) 420(* normal functions. The translation procedure treats any closed term in *) 421(* the function definition as an instantiation, so the same technique works *) 422(* for higher-order and first-order functions. *) 423(* *) 424(* The following example demonstrates this technique in translating the *) 425(* function determining whether all elements are non-zero: *) 426(*****************************************************************************) 427 428val translated_everyless = 429 translate_simple_function 430 [(``EVERY``,"everyless")] 431 (CONJ (ISPEC ``\a. 0n < a`` (CONJUNCT1 listTheory.EVERY_DEF)) 432 (ISPEC ``\a. 0n < a`` (CONJUNCT2 listTheory.EVERY_DEF))); 433 434(*****************************************************************************) 435(* val translated_everyless = *) 436(* |- everyless arg = *) 437(* ite (natp_list arg) *) 438(* (ite (atom arg) t *) 439(* (andl [(\a'. not (zp a')) (car arg); everyless (cdr arg)])) t : thm *) 440(*****************************************************************************) 441 442 443(*---------------------------------------------------------------------------*) 444(* Polymorphic functions: *) 445(*---------------------------------------------------------------------------*) 446 447(*****************************************************************************) 448(* Polymorphic functions are translated in exactly the same way as *) 449(* monomorphic functions, except that one extra theorem must be supplied. *) 450(* Hence for simple functions we use: *) 451(* translate_simple_polymorphic_function : *) 452(* (term * string) list -> (term * thm) list -> thm -> thm *) 453(* The extra theorem supplied demonstrates that the function preserves map *) 454(* functions. For example, in the case of LENGTH this theorem is: *) 455(*****************************************************************************) 456 457val LENGTH_MAP = prove(``!x f. LENGTH (MAP f x) = LENGTH x``, 458 Induct THEN 459 FULL_SIMP_TAC std_ss 460 [listTheory.LENGTH,listTheory.MAP,combinTheory.o_THM]); 461 462(*****************************************************************************) 463(* val LENGTH_MAP = |- !x f. LENGTH (MAP f x) = LENGTH x : thm *) 464(* *) 465(* The corresponding theorems for APPEND and REVERSE are: *) 466(*****************************************************************************) 467 468val APPEND_MAP = prove(``!x y f. MAP f x ++ MAP f y = MAP f (x ++ y)``, 469 Induct THEN 470 RW_TAC std_ss [listTheory.MAP,listTheory.APPEND]); 471 472local 473open listTheory 474val REVERSE_APP_MAP = prove( 475 ``!x y f. REVERSE (MAP f x) ++ MAP f y = MAP f (REVERSE x ++ y)``, 476 Induct THEN RW_TAC std_ss [MAP,REVERSE_DEF,APPEND,GSYM APPEND_ASSOC] THEN 477 RW_TAC std_ss [GSYM MAP]); 478in 479val REVERSE_MAP = REWRITE_RULE [APPEND_NIL,MAP] 480 (Q.SPECL [`x`,`[]`] REVERSE_APP_MAP); 481end 482 483(*****************************************************************************) 484(* val APPEND_MAP = |- !x y f. MAP f x ++ MAP f y = MAP f (x ++ y) : thm *) 485(* val REVERSE_MAP = |- !f. REVERSE (MAP f x) = MAP f (REVERSE x) : thm *) 486(* *) 487(* All of these functions are translated in exactly the same manner as their *) 488(* monomorphic brethren, except the map theorem is provided. *) 489(*****************************************************************************) 490 491val translated_length = 492 translate_simple_polymorphic_function 493 [(``LENGTH``,"length_poly")] 494 [(``LENGTH``,LENGTH_MAP)] 495 listTheory.LENGTH; 496 497val translated_append = 498 translate_simple_polymorphic_function 499 [(``$++``,"append")] 500 [(``$++``,APPEND_MAP)] 501 listTheory.APPEND; 502 503val translated_reverse = 504 translate_simple_polymorphic_function 505 [(``REVERSE``,"reverse")] 506 [(``REVERSE``,REVERSE_MAP)] 507 listTheory.REVERSE_DEF; 508 509(*****************************************************************************) 510(* val translated_length = *) 511(* |- length_poly arg = *) 512(* ite (listANY arg) *) 513(* (ite (atom arg) (nat 0) (add (len (cdr arg)) (nat 1))) (nat 0) : thm *) 514(* *) 515(* val translated_append = *) 516(* |- append arg l2 = *) 517(* ite (andl [listANY arg; listANY l2]) *) 518(* (ite (atom arg) l2 (cons (car arg) (append (cdr arg) l2))) nil : thm *) 519(* *) 520(* val translated_reverse = *) 521(* |- reverse arg = *) 522(* ite (listANY arg) *) 523(* (ite (atom arg) nil *) 524(* (append (reverse (cdr arg)) (cons (car arg) nil))) nil : thm *) 525(* *) 526(* The propagation theorems have the same form as the monomorphic propgation *) 527(* theorems. However, they take a general function to recognise the type *) 528(* variable: *) 529(*****************************************************************************) 530 531val prop_reverse = fetch "-" "prop_reverse"; 532 533(*****************************************************************************) 534(* val prop_reverse = *) 535(* |- list encodea (REVERSE arg) = reverse (list encodea arg) : thm *) 536(* *) 537(* Things get a little bit more complicated when limits are involved, as we *) 538(* must also provide a theorem that demonstrates that the limit, as well as *) 539(* the function, preserves the map. In the case of SEG, this requires the *) 540(* theorem: *) 541(*****************************************************************************) 542 543val LIMIT_MAP = prove( 544 ``!c a b f. a + b <= LENGTH c ==> a + b <= LENGTH (MAP f c)``, 545 REWRITE_TAC [LENGTH_MAP]); 546 547(*****************************************************************************) 548(* val LIMIT_MAP = *) 549(* |- !c a b f. a + b <= LENGTH c ==> a + b <= LENGTH (MAP f c) : thm *) 550(* *) 551(* We still need the theorem for SEG of course: *) 552(*****************************************************************************) 553 554val SEG_MAP = prove( 555 ``!c a b. a + b <= LENGTH c ==> (SEG a b (MAP f c) = MAP f (SEG a b c))``, 556 Induct THEN1 557 RW_TAC std_ss [listTheory.LENGTH,listTheory.MAP,rich_listTheory.SEG] THEN 558 Induct_on `a` THEN Induct_on `b` THEN 559 RW_TAC std_ss [listTheory.LENGTH,listTheory.MAP,rich_listTheory.SEG] THEN 560 FIRST_ASSUM MATCH_MP_TAC THEN DECIDE_TAC); 561 562(*****************************************************************************) 563(* val SEG_MAP = *) 564(* |- !c a b. a + b <= LENGTH c ==> *) 565(* (SEG a b (MAP f c) = MAP f (SEG a b c)) : thm *) 566(* *) 567(* SEG is then converted as follows: *) 568(*****************************************************************************) 569 570val translated_seg = 571 translate_limit_polymorphic_function 572 [(``SEG``,"seg")] 573 [(``SEG``,SEG_MAP)] 574 [(``SEG``,[``\a b c. a + b <= LENGTH c``])] 575 [LIMIT_MAP,limit_correct,limit_recursive1,limit_recursive2] 576 rich_listTheory.SEG; 577 578(*****************************************************************************) 579(* val translated_seg = *) 580(* |- seg arg'' arg' arg = *) 581(* ite *) 582(* (andl *) 583(* [natp arg''; *) 584(* andl *) 585(* [natp arg'; *) 586(* andl [listANY arg; not (less (len arg) (add arg'' arg'))]]]) *) 587(* (ite (zp arg'') nil *) 588(* (ite (zp arg') *) 589(* (cons (car arg) *) 590(* (seg (add arg'' (unary_minus (nat 1))) (nat 0) (cdr arg))) *) 591(* (seg arg'' (add arg' (unary_minus (nat 1))) (cdr arg)))) nil *) 592(*****************************************************************************) 593 594(*---------------------------------------------------------------------------*) 595(* User defined datatypes *) 596(*---------------------------------------------------------------------------*) 597 598(*****************************************************************************) 599(* The polymorphic type 'a Tree is defined as follows: *) 600(* `Tree = TLeaf of 'a | TBranch of Tree => Tree`; *) 601(* Before functions can be translated, support functions for the type must *) 602(* be created. To do this, the following function is used: *) 603(* initialise_type : hol_type -> unit *) 604(*****************************************************************************) 605 606val _ = initialise_type ``:'a Tree``; 607 608(*****************************************************************************) 609(* This produces the following functions: *) 610(* map, all, encode, decode, detect and fix *) 611(* The following theorems: *) 612(* encode_detect_all : |- detect f o encode g = all (f o g) *) 613(* encode_map_encode : |- map f o encode g = encode (f o g) *) 614(* encode_decode_map : |- decode f o encode g = map (f o g) *) 615(* decode_encode_fix : |- encode f o decode g = fix (f o g) *) 616(* *) 617(* map_id : |- map I = I *) 618(* all_id : |- all (K T) = K T *) 619(* fix_id : |- (!x. p x ==> f x = x) ==> !x. detect p x ==> fix f x = x *) 620(* *) 621(* general_detect : |- !x. detect p x ==> detect (K T) x *) 622(* *) 623(* And the following rewrites: *) 624(* Constructor encoding : encode encodea (TLeaf a) = ... *) 625(* Decode then encode : encode encodea (decode decodea x) = x *) 626(* Destructor theorems : All destructors are given as follows... *) 627(* (FST o ... o SND o decode_pair o encode_type) (C a b c ...) *) 628(* *) 629(* Destructors can be specified exactly using 'set_destructors' and a *) 630(* COMPLETE list of destructor functions for a type's constructors. However, *) 631(* ALL destructors should be translated before functions using them are *) 632(* translated. *) 633(* *) 634(* We define the function 'FLATTEN_TREE' to convert trees to a lists, in a *) 635(* depth-first order, as follows: *) 636(* |- (FLATTEN_TREE (TLeaf a) = [a]) /\ *) 637(* (FLATTEN_TREE (TBranch t1 t2) = *) 638(* FLATTEN_TREE t1 ++ FLATTEN_TREE t2) : thm *) 639(* *) 640(* As this function is polymorphic, we must prove a map theorem. However, *) 641(* the map function was created automatically, so we must find it from the *) 642(* database. This is done using the database functions from polytypicLib: *) 643(* polytypicLib.get_source_function_def ``:'a Tree`` "map" *) 644(*****************************************************************************) 645 646val tree_map_def = polytypicLib.get_source_function_def ``:'a Tree`` "map"; 647 648(*****************************************************************************) 649(* val tree_map_def = *) 650(* |- (!mapa a. map mapa (TLeaf a) = TLeaf (mapa a)) /\ *) 651(* (!mapa a b. map mapa (TBranch a b) = *) 652(* TBranch (map mapa a) (map mapa b)) : thm *) 653(* *) 654(* We use this theorem to derive the map theorem: *) 655(*****************************************************************************) 656 657val FLATTEN_TREE_MAP = prove( 658 ``!x. FLATTEN_TREE (map f x) = MAP f (FLATTEN_TREE x)``, 659 Induct THEN 660 RW_TAC std_ss [testFunctionsTheory.FLATTEN_TREE_def,tree_map_def, 661 listTheory.MAP,listTheory.MAP_APPEND]); 662 663(*****************************************************************************) 664(* val FLATTEN_TREE_MAP = *) 665(* |- !x. FLATTEN_TREE (map f x) = MAP f (FLATTEN_TREE x) : thm *) 666(* *) 667(* We can then translate the function as follows: *) 668(*****************************************************************************) 669 670val translated_flatten = 671 translate_simple_polymorphic_function 672 [(``FLATTEN_TREE``,"flatten_tree")] 673 [(``FLATTEN_TREE``,FLATTEN_TREE_MAP)] 674 testFunctionsTheory.FLATTEN_TREE_def; 675 676(*****************************************************************************) 677(* val translated_flatten = *) 678(* |- flatten_tree arg = *) 679(* ite (TreeANY arg) *) 680(* (ite (zp (car arg)) (cons (cdr arg) nil) *) 681(* (append (flatten_tree (car (cdr arg))) *) 682(* (flatten_tree (cdr (cdr arg))))) nil : thm *) 683(* *) 684(* Conditional and limit functions are translated in exactly the same manner.*) 685(*****************************************************************************) 686 687(*---------------------------------------------------------------------------*) 688(* Finite Cartesian products: *) 689(*---------------------------------------------------------------------------*) 690 691(*****************************************************************************) 692(* Functions using finite cartesian products are translated in a different *) 693(* manner to standard functions. First, a term is derived which *should* be *) 694(* the translation of the function. Then, this term is proven termination *) 695(* and proven to be a valid translation. This order is necessary as the *) 696(* cardinality of the type variables used must be replaced with natural *) 697(* number arguments. *) 698(* *) 699(* An example of this procedure is the translation of the function word_div: *) 700(* |- !v w. v // w = n2w (w2n v DIV w2n w) : thm *) 701(* This function is only valid for ~(w = 0w), so we translate as a limit *) 702(* function. The FCP functions do not operate on mutually recursive *) 703(* definitions, as such the functions used are as follows: *) 704(* val translate_simple_fcp_function *) 705(* : string -> thm -> thm *) 706(* val translate_conditional_fcp_function *) 707(* : string -> thm list -> thm -> thm *) 708(* val translate_limit_fcp_function *) 709(* : string -> term list -> thm list -> thm -> thm *) 710(* The above functions only work on non-recursive functions, recursive *) 711(* functions are covered later. *) 712(*****************************************************************************) 713 714val translated_worddiv = 715 translate_limit_fcp_function 716 "WORDDIV" 717 [``\a b. ~(b = 0w)``] 718 [wordsTheory.w2n_eq_0] 719 wordsTheory.word_div_def; 720 721(*****************************************************************************) 722(* val translated_worddiv = *) 723(* |- !v w ABSa. *) 724(* WORDDIV v w ABSa = *) 725(* ite ( .... *) 726(* not (equal w (translated_extend (int 0) ABSa))]]) *) 727(* (translated_extend *) 728(* (acl2_floor (translated_i2n v ABSa) (translated_i2n w ABSa)) *) 729(* ABSa) (translated_extend (int 0) ABSa) : thm *) 730(* *) 731(* In the trace, the steps of the translation are described as follows: *) 732(* Unabstracted conversion : *) 733(* An attempt to translate the definition, aborting upon reaching the *) 734(* the term ``nat (dimindex (:'a))`` *) 735(* Recusion points : *) 736(* Terms that cannot be encoded, as they are recursive calls to the *) 737(* function itself. *) 738(* Terminals : *) 739(* Terms that involve the cardinality of a type variable, and must be *) 740(* replaced with a natural number argument. *) 741(* Abstracted definition : *) 742(* The resulting definition. This must be proved terminating then *) 743(* proved to match the HOL function. *) 744(* *) 745(*****************************************************************************) 746 747(*---------------------------------------------------------------------------*) 748(* Recognizers for finite cartesian products: *) 749(*---------------------------------------------------------------------------*) 750 751(*****************************************************************************) 752(* In the translation of word_div the recognition function, word_detect, is *) 753(* expanded out and translated. Instead, a more concise definition can be *) 754(* created by flattening the definition. As with normal types, the function *) 755(* flatten_fcp_recognizers : *) 756(* (hol_type -> string) -> hol_type -> thm list *) 757(* is used. *) 758(*****************************************************************************) 759 760val wordp_def = flatten_fcp_recognizers (K "wordp") ``:'a word``; 761 762(*****************************************************************************) 763(* val wordp_def = *) 764(* [|- !x ABSa. *) 765(* wordp x ABSa = *) 766(* andl *) 767(* [integerp x; *) 768(* andl *) 769(* [less x *) 770(* (acl2_expt (int 2) *) 771(* (nfix (add ABSa (unary_minus (nat 1))))); *) 772(* not *) 773(* (less x *) 774(* (unary_minus *) 775(* (acl2_expt (int 2) *) 776(* (nfix (add ABSa (unary_minus (nat 1)))))))]]] : thm *) 777(* *) 778(* This functions in the same way as the flattening of normal types, except *) 779(* an extra argument to represent the cardinality of the type is added. This *) 780(* gives the following propagation theorem: *) 781(*****************************************************************************) 782 783val propagate_wordp = fetch "-" "prop_wordp"; 784 785(*****************************************************************************) 786(* val propagate_wordp = *) 787(* |- bool (word_detect (:'a) x) = wordp x (nat (dimindex (:'a))) : thm *) 788(*****************************************************************************) 789 790(*---------------------------------------------------------------------------*) 791(* Recursive functions over finite cartesian products: *) 792(*---------------------------------------------------------------------------*) 793 794(*****************************************************************************) 795(* When converting a recursive FCP function two tactics must also be *) 796(* supplied: one to prove that the new definition terminates, and another to *) 797(* link the definition to the HOL definition. Additionally, a list of *) 798(* rewrite theorems is supplied that are used to rewrite the definition *) 799(* prior to the use of tDefine. *) 800(* *) 801(* Here, we are trying to translate the function 'addn' that adds the ith *) 802(* element of a list of arrays: *) 803(*****************************************************************************) 804 805val addn_def = 806 Define `(addn i [] = 0n) /\ (addn i (y::ys) = y %% i + addn i ys)`; 807 808(*****************************************************************************) 809(* Before this definition is translated we must translate the types involved.*) 810(* That is: ``:num ** 'b`` and ``:(num ** 'b) list``: *) 811(*****************************************************************************) 812 813val numarrayp_def = 814 flatten_fcp_recognizers (K "numarrayp") ``:num ** 'b``; 815val numarraylistp_def = 816 flatten_fcp_recognizers (K "numarraylistp") ``:(num ** 'b) list``; 817 818(*****************************************************************************) 819(* The first goal we are given to solve are as follows: *) 820(* ?R. WF R /\ *) 821(* !ABSa arg x. *) 822(* ~(andl [natp x; andl [numarraylistp arg ABSa; less x ABSa]] = nil) /\ *) 823(* (atom arg = nil) ==> *) 824(* R (x,cdr arg,ABSa) (x,arg,ABSa) *) 825(* This is solved using 'ENCODE_WF_REL_TAC'. This acts like 'WF_REL_TAC' *) 826(* except the relation is encoded to s-expressions. *) 827(*****************************************************************************) 828 829local 830open translateTheory sexpTheory hol_defaxiomsTheory; 831in 832val tactic1 = 833 ENCODE_WF_REL_TAC `measure (LENGTH o FST o SND)` THEN 834 FULL_SIMP_TAC std_ss [ANDL_REWRITE,TRUTH_REWRITES] THEN 835 Cases_on `arg` THEN 836 FULL_SIMP_TAC std_ss [atom_def,car_def,cdr_def,consp_def,not_def, 837 TRUTH_REWRITES,ite_def,sexp_to_list_def,listTheory.LENGTH] 838end 839 840(*****************************************************************************) 841(* The second goal is harder to prove: *) 842(* |- !x arg. *) 843(* x < dimindex (:'a) ==> *) 844(* (nat (addn x arg) = *) 845(* ADDN (nat x) *) 846(* (list (fcp_encode nat (:'a)) arg) (nat (dimindex (:'a)))) : thm *) 847(* Here, the tactic is supplied with the definition and the propagation *) 848(* theorem for the unabstracted definition. We then define the second tactic *) 849(* as follows: *) 850(*****************************************************************************) 851 852local 853open translateTheory sexpTheory hol_defaxiomsTheory 854open extendTranslateTheory 855in 856fun tactic2 definition prop_thm = 857 Induct_on `arg` THEN 858 ONCE_REWRITE_TAC [definition] THEN 859 RW_TAC std_ss [NATP_NAT,ANDL_REWRITE,TRUTH_REWRITES,ite_def,addn_def, 860 list_def,atom_def,not_def,GSYM (fetch "-" "prop_numarraylistp"), 861 listp_def,REWRITE_RULE [combinTheory.o_THM,FUN_EQ_THM] ENCDETALL_FCP, 862 ENCDETALL_NAT,ALLID_FCP,combinTheory.K_o_THM, 863 REWRITE_RULE [combinTheory.o_THM,FUN_EQ_THM] ENCDETALL_LIST, 864 ENCDETALL_FCP,ALLID_LIST,GSYM NAT_THMS] THEN 865 FULL_SIMP_TAC std_ss [arithmeticTheory.GREATER_DEF,NAT_THMS,cdr_def,car_def, 866 GSYM LIST_THMS,consp_def,TRUTH_REWRITES] THEN 867 METIS_TAC [FCP_INDEX] 868end; 869 870(*****************************************************************************) 871(* For general types, the functions: *) 872(* FULL_ENCODE_DECODE_THM, FULL_ENCODE_DECODE_MAP_THM etc... *) 873(* from encodeLib may be very useful in proving such theorems. *) 874(* *) 875(* Once we have the two tactics we can translate the final definition. In *) 876(* the following function call we translate 'addn' under the limit ensuring *) 877(* i is within the cardinality of :'a. No extra theorems (third argument) or *) 878(* rewrites (fifth argument) are required. *) 879(*****************************************************************************) 880 881val translated_addn = 882 translate_recursive_fcp_function 883 "ADDN" 884 [``\i y. i < dimindex (:'a)``] 885 [] addn_def [] 886 tactic1 tactic2; 887 888(*****************************************************************************) 889(* val translated_addn = *) 890(* |- !i arg ABSa. *) 891(* ADDN i arg ABSa = *) 892(* ite (andl [natp i; andl [numarraylistp arg ABSa; less i ABSa]]) *) 893(* (ite (atom arg) (nat 0) *) 894(* (add (car (acl2_nthcdr i (car arg))) (ADDN i (cdr arg) ABSa))) *) 895(* (nat 0) : thm *) 896(*****************************************************************************) 897