1\chapter{How to program a proof tool}\label{tool} 2 3Users of \HOL{} can create their own theorem proving tools by combining 4predefined rules and tactics. The \ML{} type-discipline 5ensures that only logically sound methods can be used to create values 6of type \ml{thm}. 7In this chapter, a simple but real\footnote{The example 8is `real' in that the need for it came up last week.} example is described. 9 10Several implementations of the tool are given to illustrate various styles 11of proof programming. The first implementation is the obvious one, but 12is very slow because of the `brute force' method used. The second 13implementation produces a much more streamlined proof, but still has a 14brute force component, namely the use of a tautology checker from the 15library \ml{taut}. The third implementation replaces the general 16tautology checker with a special purpose derived inference rule. The 17fourth and final implementation uses an optimised implementation of 18the special purpose rule; understanding it is left as an exercise in 19using \DESCRIPTION. 20 21The timings in this chapter are based on Version 1.12. Later versions 22of \HOL{} have an optimised tautology checker library due to Richard 23Boulton. This new tautology checker is actually faster than the 24special purpose derived rule described in 25Section~\ref{bogus-optimization}. Thus with the new tautology checker 26the so called ``even more efficient implementation'' is actually 27slower than the program it replaces! This was only discovered (by 28Juanito Camilleri) during the preparation of Version 2 of the 29tutorial. Rather than completely rewriting the chapter, it was decided 30to leave it essentially as it was (except for the addition of this 31 paragraph). The methods 32that are described are still useful, and there is an important lesson 33here: optimizations can become obsolete. The really dedicated reader 34could learn a lot by studying the old and new tautology checker 35({\small\verb%contrib/icl-taut%} and 36{\small\verb%Library/taut%}, respectively) to find out how they work. 37Besides improving the tautology library, Richard Boulton also 38reimplemented rewriting using ideas from Tom Melham and Roger Fleming. 39As a result, in versions later than 1.12 the various rewriting tools 40are quite a bit faster and generate fewer intermediate theorems. 41 42 43It is sometimes claimed that `\LCF-style' systems can never be 44practical, because the efficiency needed to handle real examples can 45only be obtained with decision procedures coded as primitive rules. It 46is hoped that this chapter, as well as the \ml{taut} library, shows 47that the truth of such claims is not obvious. Research is currently in 48progress to see if a variety of practical decision algorithms can be 49implemented as efficient derived rules. 50 51The tool described here is a tactic that puts conjunctions into the 52normal form obtained by right associating, sorting the conjuncts into 53a canonical order and then removing repetitions. This canonical order 54uses the built-in polymorphic infix \ml{<<}, which orders any pair of 55\ML{} values with the same type. 56 57\section{A simple implementation} 58 59A first implementation uses `brute-force' rewriting with 60the equations: 61 62\begin{hol}\begin{verbatim} 63 |- (t1 /\ t2) /\ t3 = t1 /\ (t2 /\ t3) % Associativity % 64 65 |- t1 /\ t2 = t2 /\ t1 % Symmetry (if t2 << t1) % 66 |- t1 /\ (t2 /\ t3) = t2 /\ (t1 /\ t3) % Symmetry (if t2 << t1) % 67 68 |- t /\ t = t % Cancel repeated terms % 69 |- t1 /\ (t1 /\ t2) = t1 /\ t2 % Cancel repeated terms % 70\end{verbatim}\end{hol} 71 72\noindent These equations are easily proved using the 73library \ml{taut}. Note that \HOL{} Version 1.12 is used in 74this chapter. Versions of \HOL{} later than 1.12 contain improved 75rewriting tools and a new version of the library \ml{taut} (the old version 76of the library is preserved in the directory 77{\small\verb%contrib/icl-taut%}). 78 79 80\setcounter{sessioncount}{0} 81\begin{session}\begin{verbatim} 82scaup% hol 83 _ _ __ _ __ __ 84 |___ |__| | | | |__| |__| 85 | | | |__| |__ |__| |__| 86 87 Version 1.12 (Sun3/Franz), built on Feb 23 1991 88 89#load_library `taut`;; 90Loading library `taut` ... 91........................ 92Library `taut` loaded. 93() : void 94\end{verbatim}\end{session} 95 96\noindent The library \ml{taut} defines \ml{TAUT\_RULE}\footnote{The function \ml{TAUT\_RULE} has been replaced by a function called \ml{TAUT\_PROVE} 97in the new version of the \ml{taut} library available in versions of 98\HOL{} later than 1.12} 99which converts a term to the corresponding theorem, if the term is a tautology. 100\vfill 101\newpage 102\begin{session}\begin{verbatim} 103#let ASSOC = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3";; 104ASSOC = |- (t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3 105 106#let SYM1 = TAUT_RULE "t1 /\ t2 = t2 /\ t1";; 107SYM1 = |- t1 /\ t2 = t2 /\ t1 108 109#let SYM2 = TAUT_RULE "t1 /\ t2 /\ t3 = t2 /\ t1 /\ t3";; 110SYM2 = |- t1 /\ t2 /\ t3 = t2 /\ t1 /\ t3 111 112#let CANCEL1 = TAUT_RULE "t /\ t = t";; 113CANCEL1 = |- t /\ t = t 114 115#let CANCEL2 = TAUT_RULE "t1 /\ t1 /\ t2 = t1 /\ t2";; 116CANCEL2 = |- t1 /\ t1 /\ t2 = t1 /\ t2 117\end{verbatim}\end{session} 118 119\noindent One cannot just use \ml{REWRITE\_TAC} with \ml{SYM1} and 120\ml{SYM2}, because it would loop. What is needed is a special 121rewriting tool that will only apply symmetry when terms are out of 122order. Such a tool can be implemented as a {\it conversion\/}. 123 124Conversions are described in detail in \DESCRIPTION. The idea, which 125is due to Larry Paulson \cite{lcp-rewrite}, is that a conversion is an 126\ML{} function that maps a term $t_1$ to an equation: 127 128\medskip 129{\small\verb%|- %}$t_1${\small\verb% = %}$t_2$. 130\medskip 131 132\noindent The intention is that a conversion will only apply to a 133subset of terms: on members of this subset it will generate an 134equation, on all other terms it will fail. Because conversions are so 135central to theorem-proving in \HOL, the \ML{} type 136{\small\verb%term->thm%} is abbreviated to {\small\verb%conv%}. 137Conversions are applied using the function: 138 139\begin{hol}\begin{verbatim} 140 REWR_CONV : thm -> conv 141\end{verbatim}\end{hol} 142 143\noindent This takes an equation {\small\verb%|- %}$t_1${\small\verb% = %}$t_2$ 144and generates a conversion (\ie\ \ML{} function of type {\small\verb%term->thm%}) 145that maps any term $u$ that matches $t_1$ to the theorem 146{\small\verb%|- %}$u${\small\verb% = %}$v$, where $v$ is 147obtained by applying the substitution obtained by matching $u$ with $t_1$ to $t_2$. 148If $u$ doesn't match $t_1$ then the application of \ml{REWR\_CONV} fails. 149 150 151\begin{session}\begin{verbatim} 152#REWR_CONV ASSOC "(A /\ B) /\ C";; 153|- (A /\ B) /\ C = A /\ B /\ C 154 155#REWR_CONV ASSOC "A /\ (B /\ C)";; 156evaluation failed REWR_CONV: lhs of theorem doesn't match term 157 158#REWR_CONV SYM1 "B /\ A";; 159|- B /\ A = A /\ B 160 161#REWR_CONV SYM1 "A \/ B";; 162evaluation failed REWR_CONV: lhs of theorem doesn't match term 163\end{verbatim}\end{session} 164 165\noindent For our application, the required conversion should map 166a conjunction 167 168\medskip 169$t_1${\small\verb% /\ (%}$t_{2_1}${\small\verb% /\ %}$t_{2_2}${\small\verb%)%} 170\medskip 171 172\noindent in which 173$t_{2_1}${\small\verb% << %}$t_1$ to the equational theorem: 174 175\medskip 176 177{\small\verb%|- %}$t_1${\small\verb% /\ (%}$t_{2_1}${\small\verb% /\ %}$t_{2_2}${\small\verb%) = %} $t_{2_1}${\small\verb% /\ (%}$t_1${\small\verb% /\ %}$t_{2_2}${\small\verb%)%} 178 179\medskip 180 181\noindent If $t_1${\small\verb% << %}$t_{2_1}$ then the conversion fails 182(in the \ML{} sense) when applied to 183$t_1${\small\verb% /\ (%}$t_{2_1}${\small\verb% /\ %}$t_{2_2}${\small\verb%)%}. 184In addition, if the right conjunct is not itself a conjunction, then 185the conversion should reorder if necessary. More precisely, if the conversion 186is applied to $t_1${\small\verb% /\ %}$t_2$ where $t_2$ is not a conjunction and 187$t_2${\small\verb% << %}$t_1$, then it should generate the equation: 188 189\medskip 190{\small\verb%|- %}$t_1${\small\verb% /\ %}$t_2${\small\verb% = %}$t_2${\small\verb% /\ %}$t_1$ 191\medskip 192 193\noindent Such a conversion is easily implemented in \ML{} using 194\ml{SYM1} and \ml{SYM2} proved above, together with the \ML{} syntax 195processing functions \ml{is\_conj} and \ml{dest\_conj}, where: 196 197\begin{hol}\begin{verbatim} 198 is_conj : term -> bool 199 dest_conj : term -> (term # term) 200\end{verbatim}\end{hol} 201 202\noindent These are functions that test whether a term is a conjunction, and 203splits a term into its two conjuncts, respectively. For example: 204 205\begin{session}\begin{verbatim} 206#is_conj "A /\ B";; 207true : bool 208 209#is_conj "A \/ B";; 210false : bool 211 212#dest_conj "A /\ B";; 213("A", "B") : (term # term) 214 215#dest_conj "A \/ B";; 216evaluation failed dest_conj 217\end{verbatim}\end{session} 218 219The implementation of the special purpose conversion, 220\ml{CONJ\_ORD\_CONV}, is now straightforward. 221 222 223\begin{session}\begin{verbatim} 224#let CONJ_ORD_CONV t = 225# let t1,t2 = dest_conj t 226# in 227# if is_conj t2 228# then (let t21,t22 = dest_conj t2 229# in 230# if t21 << t1 then REWR_CONV SYM2 t else fail) 231# else (if t2 << t1 then REWR_CONV SYM1 t else fail);; 232CONJ_ORD_CONV = - : conv 233\end{verbatim}\end{session} 234 235\noindent This is illustrated by: 236 237\begin{session}\begin{verbatim} 238#"A:bool" << "B:bool";; 239true : bool 240 241#"B:bool" << "C:bool";; 242true : bool 243 244#CONJ_ORD_CONV "B /\ A";; 245|- B /\ A = A /\ B 246 247#CONJ_ORD_CONV "A /\ B";; 248evaluation failed fail 249\end{verbatim}\end{session} 250 251The process of normalizing a conjunction can be split into four phases: 252 253\begin{enumerate} 254\item Right associate the conjunction by repeatedly applying: 255\begin{quote} 256\ml{REWR\_CONV\ ASSOC} 257\end{quote} 258\item Put the conjuncts in canonical order by repeatedly applying: 259\begin{quote} 260\ml{CONJ\_ORD\_CONV} 261\end{quote} 262\item Remove repetitions of $t$ of the form $t${\small\verb% /\ %}$t$ 263by repeatedly applying: 264\begin{quote} 265\ml{REWR\_CONV\ CANCEL1} 266\end{quote} 267\item Remove repetitions of $t_1$ in 268$t_1${\small\verb% /\ (%}$t_1${\small\verb% /\ %}$t_2${\small\verb%)%} 269by repeatedly applying: 270\begin{quote} 271\ml{REWR\_CONV\ CANCEL2} 272\end{quote} 273\end{enumerate} 274 275 276To implement this, a method of repeatedly applying a conversion to 277subterms of a term is needed. This is provided by the operator 278 279\begin{hol}\begin{verbatim} 280 TOP_DEPTH_CONV : conv -> conv 281\end{verbatim}\end{hol} 282 283\noindent If $c$ is a conversion then \ml{TOP\_DEPTH\_CONV}~$c$ is a 284conversion that repeatedly applies $c$ to all subterms until $c$ is no 285longer applicable to any subterms. The function \ml{TOP\_DEPTH\_CONV} 286is one of a family of operators that apply conversions throughout 287terms. Members of this family differ in the order in which subterms 288are visited and the amount of repetition that is done. For more 289details, see the chapter on conversions in \DESCRIPTION. 290 291\begin{session}\begin{verbatim} 292#let ex1 = "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D";; 293ex1 = "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" : term 294 295#REWR_CONV ASSOC ex1;; 296evaluation failed REWR_CONV: lhs of theorem doesn't match term 297 298#TOP_DEPTH_CONV (REWR_CONV ASSOC) ex1;; 299|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = 300 A /\ B /\ C /\ A /\ C /\ A /\ D /\ D 301\end{verbatim}\end{session} 302 303\noindent The right hand side of this theorem is \ml{ex1} in right-associated 304form. The conclusion of a theorem can be extracted with the \ML{} function 305\ml{concl} and the right hand side of an equation can be extracted with 306\ml{rhs}. Thus, continuing the session: 307 308\begin{session}\begin{verbatim} 309#let ex2 = rhs(concl it);; 310ex2 = "A /\ B /\ C /\ A /\ C /\ A /\ D /\ D" : term 311 312#TOP_DEPTH_CONV CONJ_ORD_CONV ex2;; 313|- A /\ B /\ C /\ A /\ C /\ A /\ D /\ D = 314 A /\ A /\ A /\ B /\ C /\ C /\ D /\ D 315\end{verbatim}\end{session} 316 317\noindent The right hand side of this is the result of canonicalizing 318the order of the conjuncts in the left hand side. Next, the repetitions 319can be eliminated using \ml{CANCEL1} and \ml{CANCEL2}. 320 321\begin{session}\begin{verbatim} 322#let ex3 = rhs(concl it);; 323ex3 = "A /\ A /\ A /\ B /\ C /\ C /\ D /\ D" : term 324 325#TOP_DEPTH_CONV (REWR_CONV CANCEL1) ex3;; 326|- A /\ A /\ A /\ B /\ C /\ C /\ D /\ D = 327 A /\ A /\ A /\ B /\ C /\ C /\ D 328\end{verbatim}\end{session} 329 330\begin{session}\begin{verbatim} 331#let ex4 = rhs(concl it);; 332ex4 = "A /\ A /\ A /\ B /\ C /\ C /\ D" : term 333 334#TOP_DEPTH_CONV (REWR_CONV CANCEL2) ex4;; 335|- A /\ A /\ A /\ B /\ C /\ C /\ D = A /\ B /\ C /\ D 336\end{verbatim}\end{session} 337 338 339To make the conjunction normalizer, the four stages just described 340must be performed in sequence. Conversions can be applied in sequence using 341the infixed function: 342 343\begin{hol}\begin{verbatim} 344 THENC : conv -> conv -> conv 345\end{verbatim}\end{hol} 346 347 348\noindent If $c_1\ t_1$ evaluates to $\ml{ |- }t_1\ml{=}t_2$ and 349$c_2\ t_2$ evaluates to $\ml{ |- }t_2\ml{=}t_3$, then 350$\ml{(}c_1\ \ml{THENC}\ c_2\ml{)}\ t_1$ evaluates to 351$\ml{\ |-\ }t_1\ml{=}t_3$. If the 352evaluation of $c_1\ t_1$ or the evaluation of $c_2\ t_2$ fails, 353then so does the evaluation of $c_1\ \ml{THENC}\ c_2$. \ml{THENC} is 354justified by the transitivity of equality. 355 356Using \ml{THENC}, the normalizer is defined by 357 358\begin{session}\begin{verbatim} 359#let CONJ_NORM_CONV = 360# TOP_DEPTH_CONV(REWR_CONV ASSOC) THENC 361# TOP_DEPTH_CONV CONJ_ORD_CONV THENC 362# TOP_DEPTH_CONV(REWR_CONV CANCEL1) THENC 363# TOP_DEPTH_CONV(REWR_CONV CANCEL2);; 364 365CONJ_NORM_CONV = - : conv 366 367#CONJ_NORM_CONV ex1;; 368|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D 369\end{verbatim}\end{session} 370 371This conversion can now be converted to a rule or tactic using the functions 372\ml{CONV\_RULE} or \ml{CONV\_TAC}, respectively. 373 374 375\begin{hol} 376\begin{verbatim} 377 CONV_RULE : conv -> thm -> thm 378 CONV_TAC : conv -> tactic 379\end{verbatim} 380\end{hol} 381 382\noindent $\ml{CONV\_RULE}\ c\ \ml{(|- }t\ml{)}$ returns $\ml{|- }t'$, where 383$c\ t$ evaluates to the equation 384$\ml{|-}\ t\ml{=}t'$. 385$\ml{CONV\_TAC}\ c$ is a tactic that 386converts the conclusion of a goal using $c$. For more details see \DESCRIPTION. 387 388\begin{session}\begin{verbatim} 389#let CONJ_NORM_TAC = CONV_TAC CONJ_NORM_CONV;; 390CONJ_NORM_TAC = - : tactic 391\end{verbatim}\end{session} 392 393Here is an example. It uses {\it antiquotation\/}: if $x$ is an \ML\ 394indentifier bound to term, then occurrences of 395{\small\verb%^%}$x$ inside a quotation 396denotes the term bound to $x$. 397 398\begin{session}\begin{verbatim} 399#g "^ex1 ==> B";; 400"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==> B" 401 402() : void 403 404#e CONJ_NORM_TAC;; 405OK.. 406"A /\ B /\ C /\ D ==> B" 407\end{verbatim}\end{session} 408 409To summarize, here is the \ML{} code implementing the normalizer: 410 411\begin{hol}\begin{verbatim} 412 load_library `taut`;; 413 414 let ASSOC = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3" 415 and SYM1 = TAUT_RULE "t1 /\ t2 = t2 /\ t1" 416 and SYM2 = TAUT_RULE "t1 /\ t2 /\ t3 = t2 /\ t1 /\ t3" 417 and CANCEL1 = TAUT_RULE "t /\ t = t" 418 and CANCEL2 = TAUT_RULE "t1 /\ t1 /\ t2 = t1 /\ t2";; 419 420 let CONJ_ORD_CONV t = 421 let t1,t2 = dest_conj t 422 in 423 if is_conj t2 424 then (let t21,t22 = dest_conj t2 425 in 426 if t21 << t1 then REWR_CONV SYM2 t else fail) 427 else (if t2 << t1 then REWR_CONV SYM1 t else fail);; 428 429 let CONJ_NORM_CONV = 430 TOP_DEPTH_CONV(REWR_CONV ASSOC) THENC 431 TOP_DEPTH_CONV CONJ_ORD_CONV THENC 432 TOP_DEPTH_CONV(REWR_CONV CANCEL1) THENC 433 TOP_DEPTH_CONV(REWR_CONV CANCEL2);; 434 435 let CONJ_NORM_TAC = CONV_TAC CONJ_NORM_CONV;; 436\end{verbatim}\end{hol} 437 438\section{A more efficient implementation} 439 440The normalizer just given is rather slow. This can be shown by switching on the 441system timer using the function: 442 443\begin{hol}\begin{verbatim} 444 timer : bool -> bool 445\end{verbatim}\end{hol} 446 447\noindent Evaluating \ml{timer~true} switches on timing; evaluating 448\ml{timer~false} switches it off (the previous value of the timing flag 449is returned). Garbage collection times are also shown, together with a 450count of the number of intermediate theorems that are generated (which 451gives an estimate of the number of primitive inferences done). 452 453\begin{session}\begin{verbatim} 454#timer true;; 455false : bool 456Run time: 0.0s 457 458#CONJ_NORM_CONV ex1;; 459|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D 460Run time: 1.1s 461Garbage collection time: 0.5s 462Intermediate theorems generated: 73 463\end{verbatim}\end{session} 464 465\noindent Here is a bigger example: 466 467\begin{session}\begin{verbatim} 468#CONJ_NORM_CONV "^ex1 /\ (^ex1 /\ (^ex1 /\ ^ex1 /\ ^ex1) /\ ^ex1)";; 469|- (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 470 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 471 ((A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 472 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 473 A /\ 474 (B /\ C /\ A) /\ 475 (C /\ A /\ D) /\ 476 D) /\ 477 A /\ 478 (B /\ C /\ A) /\ 479 (C /\ A /\ D) /\ 480 D = 481 A /\ B /\ C /\ D 482Run time: 38.3s 483Garbage collection time: 11.5s 484Intermediate theorems generated: 16761 485\end{verbatim}\end{session} 486 487The reason that \ml{CONJ\_CANON\_CONV} is slow is because of the 488repeated pattern matching done during rewriting. A much more efficient 489approach is to normalize the conjunction by \ML{} programming outside 490the logic, and then to prove that the normalized term is equal to the 491original one. An even more efficient approach, which is not explored 492here, would be to avoid having to do this proof by verifing the 493normalization code by some sort of meta-theoretic 494reasoning about \ML. How to do this in 495\HOL{} is not clear, but work on this approach has been done in the 496context of {\small FOL} \cite{FOL}, the Boyer-Moore prover \cite{BoyerMoore} 497and Nuprl \cite{Nuprl}. These approaches all use logically 498sophisticated extra axioms, called reflection principles, that enable 499metatheorems to be `reflected' into the logic as object level 500theorems. 501 502To normalize the term by \ML{} programming, the conjuncts are extracted, 503repeated elements are deleted and the resulting list is sorted. 504 505\HOL{} already has a predefined function: 506 507\begin{hol}\begin{verbatim} 508 conjuncts : term -> term list 509\end{verbatim}\end{hol} 510 511\noindent for extracting conjuncts. 512\HOL{} also has a predefined \ML{} function for removing repeated elements of 513a list: 514 515 516\begin{hol}\begin{verbatim} 517 setify : * list -> * list 518\end{verbatim}\end{hol} 519 520\noindent Both \ml{conjuncts} and \ml{setify} are illustrated below: 521 522\begin{session}\begin{verbatim} 523#timer false;; 524true : bool 525 526#conjuncts ex1;; 527["A"; "B"; "C"; "A"; "C"; "A"; "D"; "D"] : term list 528 529#setify it;; 530["B"; "C"; "A"; "D"] : term list 531 532#let ex1_list = it;; 533ex1_list = ["B"; "C"; "A"; "D"] : term list 534\end{verbatim}\end{session} 535 536There is a predefined sorting function in \ML: 537 538\begin{session}\begin{verbatim} 539#sort;; 540sort = - : (((* # *) -> bool) -> * list -> * list) 541 542#sort $< [3;2;5;6;1;1;7;9;3];; 543[1; 1; 2; 3; 3; 5; 6; 7; 9] : int list 544 545#sort $<< ex1_list;; 546["A"; "B"; "C"; "D"] : term list 547\end{verbatim}\end{session} 548 549Using this function, the list of conjuncts of the normalization of a 550term is easily computed. The predefined \ML{} function: 551 552\begin{hol}\begin{verbatim} 553 list_mk_conj : term list -> term 554\end{verbatim}\end{hol} 555 556\noindent can then be used to build the normalized conjunction. 557 558 559\begin{session}\begin{verbatim} 560#ex1;; 561"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" : term 562 563#let ex1_norm = list_mk_conj(sort $<< (setify(conjuncts ex1)));; 564ex1_norm = "A /\ B /\ C /\ D" : term 565\end{verbatim}\end{session} 566 567\noindent The calculation of \ml{ex1\_norm} from \ml{ex1} has been 568done by (unverified) \ML{} code. What is required is the theorem 569asserting that they are equal. This can be proved using the tautology 570checker. 571 572\begin{session}\begin{verbatim} 573#TAUT_RULE "^ex1 = ^ex1_norm";; 574|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D 575\end{verbatim}\end{session} 576 577\noindent A conversion that normalizes conjunctions is thus: 578 579\begin{session}\begin{verbatim} 580#let CONJ_NORM_CONV2 t = 581# if is_conj t 582# then TAUT_RULE "^t = ^(list_mk_conj(sort $<< (setify(conjuncts t))))" 583# else fail;; 584CONJ_NORM_CONV2 = - : conv 585 586#CONJ_NORM_CONV2 ex1;; 587|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D 588\end{verbatim}\end{session} 589 590\noindent \ml{CONJ\_CANON\_CONV2} is more than an order of magnitude faster 591than \ml{CONJ\_CANON\_CONV}: 592 593 594\begin{session}\begin{verbatim} 595#timer true;; 596false : bool 597Run time: 0.0s 598 599#CONJ_NORM_CONV2 "^ex1 /\ (^ex1 /\ (^ex1 /\ ^ex1 /\ ^ex1) /\ ^ex1)";; 600|- (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 601 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 602 ((A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 603 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 604 A /\ 605 (B /\ C /\ A) /\ 606 (C /\ A /\ D) /\ 607 D) /\ 608 A /\ 609 (B /\ C /\ A) /\ 610 (C /\ A /\ D) /\ 611 D = 612 A /\ B /\ C /\ D 613Run time: 1.9s 614Garbage collection time: 0.5s 615Intermediate theorems generated: 1273 616\end{verbatim}\end{session} 617 618\section{An even more efficient implementation}\label{bogus-optimization} 619 620Although the implementation just given is much faster than the first 621naive one, it can be improved further by replacing the call to the 622general tautology checker with a special purpose conjunction-equivalence 623prover. 624 625To see how this works, the equivalence of \ml{ex1} and \ml{ex1\_norm} will first 626be proved manually. The general form of this proof will then be abstracted into 627a derived rule. 628 629The goal is to prove that \ml{ex1} and \ml{ex1\_norm} are equal. 630 631\begin{session}\begin{verbatim} 632#timer false;; 633true : bool 634 635#g "^ex1 = ^ex1_norm";; 636"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D" 637 638() : void 639\end{verbatim}\end{session} 640 641\noindent The predefined tactic \ml{EQ\_TAC} splits an equation into two 642implications (see Section~\ref{EQTAC}). 643 644\begin{session}\begin{verbatim} 645#e EQ_TAC;; 646OK.. 6472 subgoals 648"A /\ B /\ C /\ D ==> A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" 649 650"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==> A /\ B /\ C /\ D" 651 652() : void 653\end{verbatim}\end{session} 654 655\noindent Each of these can be solved by: 656\begin{enumerate} 657\item moving the antecedent of the 658implication to the assumption list (using \ml{DISCH\_TAC}, see 659Section~\ref{DISCHTAC}); 660\item breaking up the remaining 661goal (the consequent of the implication) into one subgoal per conjunct (using 662\ml{CONJ\_TAC}, see Section~\ref{CONJTAC}); 663\item solving each of these 664conjuncts using the antecedent (which is now an assumption) 665\end{enumerate} 666 667\noindent Step 1--3 are now done interactively. 668 669\begin{session}\begin{verbatim} 670#e DISCH_TAC;; 671OK.. 672"A /\ B /\ C /\ D" 673 [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ] 674 675() : void 676\end{verbatim}\end{session} 677 678\noindent \ml{CONJ\_TAC} is repeated using the tactical \ml{REPEAT} 679described in Section~\ref{THEN}. 680 681\begin{session}\begin{verbatim} 682#e (REPEAT CONJ_TAC);; 683OK.. 6844 subgoals 685"D" 686 [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ] 687 688"C" 689 [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ] 690 691"B" 692 [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ] 693 694"A" 695 [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ] 696 697() : void 698\end{verbatim}\end{session} 699 700\noindent The final step is to use the assumption 701{\small\verb%"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D"%} to solve each goal. 702To do this, the assumption is grabbed using the tactical: 703 704\begin{hol}\begin{verbatim} 705 POP_ASSUM : (thm -> tactic) -> tactic 706\end{verbatim}\end{hol} 707 708\noindent Given a function \ml{$f$ : thm -> tactic}, the tactic 709\ml{POP\_ASSUM}\ $f$ applies $f$ to the (assumed) first 710assumption of a goal 711and then applies the tactic created thereby to the original goal 712minus its top assumption: 713 714\begin{hol}\begin{alltt} 715 POP_ASSUM \(f\) ([\(t\sb{1}\);\(\ldots\);\(t\sb{n}\)],\(t\)) = \(f\) (ASSUME \(t\sb{1}\)) ([\(t\sb{2}\);\(\ldots\);\(t\sb{n}\)],\(t\)) 716\end{alltt}\end{hol} 717 718\noindent \ML{} functions such as $f$, 719with type \ml{thm -> tactic} are abbreviated to \ml{thm\_tactic} (see 720\DESCRIPTION\ for further details). 721 722After grabbing the assumption, it is split into its individual conjunctions 723using the predefined derived rule: 724 725\begin{hol}\begin{verbatim} 726 CONJUNCTS : thm -> thm list 727\end{verbatim}\end{hol} 728 729\noindent For example: 730 731 732\begin{session}\begin{verbatim} 733#CONJUNCTS(ASSUME "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D");; 734[. |- A; . |- B; . |- C; . |- A; . |- C; . |- A; . |- D; . |- D] 735: thm list 736\end{verbatim}\end{session} 737 738\noindent Among the individual conjuncts is the goal, which can thus be 739solved immediately using \ml{ACCEPT\_TAC} (see Section~\ref{ACCEPTTAC}). 740The appropriate assumption can be chosen with the predefined tactical 741\ml{MAP\_FIRST}, which 742is characterized by: 743 744\begin{hol}\begin{alltt} 745 MAP_FIRST \(f\) [\(x\sb{1}\); \(\ldots\) ;\(x\sb{n}\)] = \(f\)(\(x\sb{1}\)) ORELSE \(\ldots\) ORELSE \(f\)(\(x\sb{n}\)) 746\end{alltt}\end{hol} 747 748\noindent Returning to the proof: the final step is now performed by 749popping the assumption and applying to it the function obtained by 750composing \ml{CONJUNCTS} and \ml{MAP\_FIRST} using the \ML{} infixed 751function composition operator \ml{o} 752(where \ml{(}$f$~\ml{o}~$g$\ml{)}$x$~\ml{=}~$g$\ml{(}$f$\ml{(}$x$\ml{))}). 753 754\begin{session}\begin{verbatim} 755#e(POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS));; 756OK.. 757goal proved 758. |- A 759 760Previous subproof: 7613 subgoals 762"D" 763 [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ] 764 765"C" 766 [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ] 767 768"B" 769 [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ] 770 771() : void 772\end{verbatim}\end{session} 773 774 775\noindent The remaining subgoals are solved identically. Stitching together 776the tactics just used results in: 777 778\begin{hol}\begin{verbatim} 779 EQ_TAC THEN 780 DISCH_TAC THEN 781 REPEAT CONJ_TAC THEN 782 POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS) 783\end{verbatim}\end{hol} 784 785\noindent With this, the entire proof can be done in one step. 786 787\begin{session}\begin{verbatim} 788#g "^ex1 = ^ex1_norm";; 789"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D" 790 791() : void 792 793#e(EQ_TAC THEN 794# DISCH_TAC THEN 795# REPEAT CONJ_TAC THEN 796# POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS));; 797OK.. 798goal proved 799|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D 800 801Previous subproof: 802goal proved 803() : void 804\end{verbatim}\end{session} 805 806Using this tactic, a derived rule \ml{CONJ\_EQ} can be defined that proves 807two conjunctions equal. This is what is needed to replace the call to 808\ml{TAUT\_RULE}. 809\ml{CONJ\_EQ} is defined with the predefined function: 810 811\begin{hol}\begin{verbatim} 812 PROVE : term # tactic -> theorem 813\end{verbatim}\end{hol} 814 815\noindent \ml{PROVE}\ml{(}$t$\ml{,}$T$\ml{)} applies the tactic $T$ to 816the goal \ml{([],}$t$\ml{)}; if this goal is proved by $T$ then the 817resulting justification is applied to \ml{[]} to obtain the theorem 818\ml{|-}~$t$, which is returned. If $T$ does not solve the goal, then 819the application of \ml{PROVE} fails. Using \ml{PROVE}, the definition 820of \ml{CONJ\_EQ} is: 821 822\begin{hol}\begin{verbatim} 823 let CONJ_EQ t1 t2 = 824 PROVE ("^t1 = ^t2", 825 EQ_TAC THEN 826 DISCH_TAC THEN 827 REPEAT CONJ_TAC THEN 828 POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS)) 829\end{verbatim}\end{hol} 830 831 832\noindent Replacing the call to \ml{TAUT\_RULE} in the definition 833of \ml{CONJ\_NORM\_CONV2} results in: 834 835\begin{hol}\begin{verbatim} 836 let CONJ_NORM_CONV3 t = 837 if is_conj t 838 then CONJ_EQ t (list_mk_conj(sort $<< (setify(conjuncts t)))) 839 else fail 840\end{verbatim}\end{hol} 841 842\noindent Continuing the session: 843 844\begin{session}\begin{verbatim} 845#let CONJ_EQ t1 t2 = 846# PROVE ("^t1 = ^t2", 847# EQ_TAC THEN 848# DISCH_TAC THEN 849# REPEAT CONJ_TAC THEN 850# POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS));; 851CONJ_EQ = - : (term -> conv) 852 853#let CONJ_NORM_CONV3 t = 854# if is_conj t 855# then CONJ_EQ t (list_mk_conj(sort $<< (setify(conjuncts t)))) 856# else fail;; 857CONJ_NORM_CONV3 = - : conv 858\end{verbatim}\end{session} 859 860\noindent \ml{CONJ\_NORM\_CONV3} is almost twice 861as efficient as \ml{CONJ\_NORM\_CONV2}. To show this, the timer is switched 862back on. 863 864\begin{session}\begin{verbatim} 865#timer true;; 866false : bool 867Run time: 0.0s 868\end{verbatim}\end{session} 869 870\noindent Here is the big example with \ml{CONJ\_NORM\_CONV3}: 871 872\begin{session}\begin{verbatim} 873#CONJ_NORM_CONV3 "^ex1 /\ (^ex1 /\ (^ex1 /\ ^ex1 /\ ^ex1) /\ ^ex1)";; 874|- (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 875 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 876 ((A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 877 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 878 A /\ 879 (B /\ C /\ A) /\ 880 (C /\ A /\ D) /\ 881 D) /\ 882 A /\ 883 (B /\ C /\ A) /\ 884 (C /\ A /\ D) /\ 885 D = 886 A /\ B /\ C /\ D 887Run time: 1.0s 888Garbage collection time: 0.5s 889Intermediate theorems generated: 775 890\end{verbatim}\end{session} 891 892\section{Further optimizations} 893 894Further improvements are still possible. As an exercise the reader 895might want to decipher the following highly optimized definition of 896\ml{CONJ\_EQ}. 897 898The function \ml{PROVE\_CONJ}, defined below, 899converts a term $t$ to the theorem \ml{|-}~$t$ 900if that theorem occurs in a supplied list of theorems (\ml{ths} in the 901code below), or $t$ is a conjunction each of whose conjuncts occurs in 902the list. The definition of \ml{PROVE\_CONJ} uses the following 903predefined \ML{} functions: 904 905\begin{itemize} 906\item \ml{uncurry}~$f$~\ml{(}$x$\ml{,}$y$\ml{)}~~\ml{=}~~$f$~$x$~$y$ 907 908\item \ml{(}$f${\small\verb% # %}$g$\ml{)}\ml{(}$x$\ml{,}$y$\ml{)}~~\ml{=}~~\ml{(}$f\ x$~\ml{,}~$g\ y$\ml{)} 909 910\item \ml{find}~$p$~\ml{[}$x_1\ml{;}\ldots\ml{;}x_n$\ml{]}~~=~~{\it the first $x_i$ for which $p\ x_i$ is true\/} 911 912\end{itemize} 913 914\noindent and the inference rule \ml{CONJ}: 915 916 917\[ \Gamma_1\turn 918t_1\qquad\qquad\qquad\Gamma_2\turn t_2\over \Gamma_1\cup\Gamma_2 \turn t_1\conj 919t_2 \] 920 921 922\noindent Here is the definition of \ml{PROVE\_CONJ}: 923 924\begin{hol}\begin{verbatim} 925 letrec PROVE_CONJ ths tm = 926 (uncurry CONJ ((PROVE_CONJ ths # PROVE_CONJ ths) (dest_conj tm))) ? 927 find (\th. concl th = tm) ths 928\end{verbatim}\end{hol} 929 930\noindent Using this, the optimized \ml{CONJ\_EQ}, called 931\ml{CONJ\_EQ2}, is defined using \ml{IMP\_ANTISYM\_RULE} (a predefined rule): 932 933 934\[ \Gamma_1 \turn t_1 \imp t_2 \qquad\qquad \Gamma_2\turn t_2 \imp t_1\over 935\Gamma_1 \cup \Gamma_2 \turn t_1 = t_2\] 936 937\noindent The definition is: 938 939\begin{hol}\begin{verbatim} 940 let CONJ_EQ2 t1 t2 = 941 let imp1 = DISCH t1 (PROVE_CONJ (CONJUNCTS(ASSUME t1)) t2) 942 and imp2 = DISCH t2 (PROVE_CONJ (CONJUNCTS(ASSUME t2)) t1) 943 in IMP_ANTISYM_RULE imp1 imp2 944\end{verbatim}\end{hol} 945 946\noindent Loading these \ML{} function definitions into \HOL: 947 948\begin{session}\begin{verbatim} 949#letrec PROVE_CONJ ths tm = 950# (uncurry CONJ ((PROVE_CONJ ths # PROVE_CONJ ths) (dest_conj tm))) ? 951# find (\th. concl th = tm) ths;; 952PROVE_CONJ = - : (thm list -> conv) 953Run time: 0.0s 954 955#let CONJ_EQ2 t1 t2 = 956# let imp1 = DISCH t1 (PROVE_CONJ (CONJUNCTS(ASSUME t1)) t2) 957# and imp2 = DISCH t2 (PROVE_CONJ (CONJUNCTS(ASSUME t2)) t1) 958# in IMP_ANTISYM_RULE imp1 imp2;; 959CONJ_EQ2 = - : (term -> conv) 960Run time: 0.0s 961\end{verbatim}\end{session} 962 963 964\noindent A version of \ml{CONJ\_NORM\_CONV} that 965uses \ml{CONJ\_EQ2} is defined by: 966 967\begin{hol}\begin{verbatim} 968 let CONJ_NORM_CONV4 t = 969 if is_conj t 970 then CONJ_EQ2 t (list_mk_conj(sort $<< (setify(conjuncts t)))) 971 else fail 972\end{verbatim}\end{hol} 973 974 975\noindent Loading this into \ML: 976 977\begin{session}\begin{verbatim} 978#let CONJ_NORM_CONV4 t = 979# if is_conj t 980# then CONJ_EQ2 t (list_mk_conj(sort $<< (setify(conjuncts t)))) 981# else fail;; 982CONJ_NORM_CONV4 = - : conv 983Run time: 0.0s 984\end{verbatim}\end{session} 985 986\noindent This is even faster than \ml{CONJ\_NORM\_CONV3}: 987 988\begin{session}\begin{verbatim} 989#CONJ_NORM_CONV4 "^ex1 /\ (^ex1 /\ (^ex1 /\ ^ex1 /\ ^ex1) /\ ^ex1)";; 990|- (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 991 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 992 ((A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 993 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ 994 A /\ 995 (B /\ C /\ A) /\ 996 (C /\ A /\ D) /\ 997 D) /\ 998 A /\ 999 (B /\ C /\ A) /\ 1000 (C /\ A /\ D) /\ 1001 D = 1002 A /\ B /\ C /\ D 1003Run time: 0.4s 1004Intermediate theorems generated: 155 1005\end{verbatim}\end{session} 1006 1007\section{Normalizing all subterms} 1008 1009There is an important difference in the functionality of 1010\ml{CONJ\_NORM\_CONV} and the various optimised versions of it. The 1011difference is that \ml{CONJ\_NORM\_CONV} applies to any term, 1012normalizing all subterms that are conjunctions. However the functions 1013\ml{CONJ\_NORM\_CONV}{\small $n$} (where {\small $n = 2,3,4$}) all 1014fail on non-conjunctions. 1015 1016\begin{session}\begin{verbatim} 1017#CONJ_NORM_CONV "^ex1 ==> ^ex1";; 1018|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==> 1019 A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = 1020 A /\ B /\ C /\ D ==> A /\ B /\ C /\ D 1021Run time: 2.0s 1022Garbage collection time: 0.6s 1023Intermediate theorems generated: 1307 1024 1025#CONJ_NORM_CONV4 "^ex1 => ^ex1";; 1026need 2 nd branch to conditional 1027skipping: ex1 " ;; parse failed 1028 1029#CONJ_NORM_CONV4 "^ex1 ==> ^ex1";; 1030evaluation failed fail 1031\end{verbatim}\end{session} 1032 1033What is needed is a function that will apply a conversion to all 1034conjunctive subterms of a term. Such a function is \ml{TOP\_DEPTH\_CONV}, however 1035 1036\begin{hol}\begin{verbatim} 1037 TOP_DEPTH_CONV CONJ_NORM_CONV4 1038\end{verbatim}\end{hol} 1039 1040\noindent would loop, because \ml{CONJ\_NORM\_CONV4} never fails on 1041conjunctions, so \ml{TOP\_DEPTH\_CONV} would keep applying it forever! 1042This is easily got around using: 1043 1044\begin{hol}\begin{verbatim} 1045 CHANGED_CONV : conv -> conv 1046\end{verbatim}\end{hol} 1047 1048\noindent \ml{CHANGED\_CONV}~$c$ behaves like $c$, except that if $c$ 1049has no effect, then \ml{CHANGED\_CONV}~$c$ fails. 1050 1051\begin{session}\begin{verbatim} 1052#TOP_DEPTH_CONV(CHANGED_CONV CONJ_NORM_CONV4) "^ex1 ==> ^ex1";; 1053|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==> 1054 A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = 1055 A /\ B /\ C /\ D ==> A /\ B /\ C /\ D 1056Run time: 0.5s 1057Intermediate theorems generated: 292 1058\end{verbatim}\end{session} 1059 1060Although this works, the scanning through subterms done by 1061\ml{TOP\_DEPTH\_CONV} is a bit `brute force'. Further efficiency can 1062be obtained by writing a special scanning function that 1063just applies a conversion to maximal conjunctive subterms. 1064This is provided by the code below. 1065The understanding of this is a fairly hard exercise for the reader. The 1066section on conversions in \DESCRIPTION\ should be helpful. 1067 1068First, an auxiliary derived rule for combining two equations into 1069a single equation by conjoining the left hand sides and the 1070right hand sides. 1071 1072\begin{session}\begin{verbatim} 1073#let MK_CONJ th1 th2 = MK_COMB(AP_TERM "$/\" th1, th2);; 1074MK_CONJ = - : (thm -> thm -> thm) 1075Run time: 0.0s 1076\end{verbatim}\end{session} 1077 1078\noindent Next a function that conjoins the left hand sides and right 1079hand sides of lists of equations. 1080 1081\begin{session}\begin{verbatim} 1082#letrec MK_CONJL l = 1083# if null l then fail 1084# if null(tl l) then hd l 1085# else MK_CONJ (hd l) (MK_CONJL(tl l));; 1086MK_CONJL = - : proof 1087Run time: 0.0s 1088\end{verbatim}\end{session} 1089 1090\noindent Next, a function that applies a conversion $c$ to all 1091conjunctive subterms of a term. This uses the \ML{} function: 1092 1093\bigskip 1094\ml{map}~$f$~\ml{[}$x_1\ml{;}\ldots\ml{;}x_n$\ml{]}~~=~~\ml{[}$f\ x_1\ml{;}\ldots\ml{;}f\ x_n$\ml{]} 1095 1096\bigskip 1097 1098\noindent and the rules \ml{MK\_COMB}: 1099 1100 1101\[ \Gamma_1 \turn f = g \qquad\qquad \Gamma_2\turn x = y \over 1102\Gamma_1 \cup \Gamma_2 \turn f\ x = g\ y\] 1103 1104\noindent and \ml{MK\_ABS}: 1105 1106 1107\[ \Gamma \turn \forall x.\ t_1 = t_2 \over 1108\Gamma \turn (\lambda x.\ t_1) = (\lambda x.\ t_2)\] 1109 1110\noindent and \ml{GEN}: 1111 1112$$\Gamma\turn t\over\Gamma\turn\uquant{x} t$$ 1113\begin{itemize} 1114\item Where $x$ is not free in $\Gamma$. 1115\end{itemize} 1116 1117 1118\noindent and \ml{REFL}: 1119 1120$$ \over\turn t = t$$ 1121 1122\begin{itemize} 1123\item\ml{REFL}~$t$~~\ml{=}~~ $\turn t = t$. 1124\end{itemize} 1125 1126\noindent The definition of \ml{CONJ\_DEPTH\_CONV} also uses: 1127 1128\begin{hol}\begin{verbatim} 1129 is_comb : term -> bool 1130 dest_comb : term -> (term # term) 1131 1132 is_abs : term -> bool 1133 dest_abs : term -> (term # term) 1134\end{verbatim}\end{hol} 1135 1136\noindent which are the tests and destructors for combinations and 1137abstractions, respectively. 1138 1139\begin{session}\begin{verbatim} 1140#letrec CONJ_DEPTH_CONV c tm = 1141# if is_conj tm 1142# then (c THENC (MK_CONJL o map (CONJ_DEPTH_CONV c) o conjuncts)) tm 1143# if is_comb tm 1144# then (let rator,rand = dest_comb tm in 1145# MK_COMB (CONJ_DEPTH_CONV c rator, CONJ_DEPTH_CONV c rand)) 1146# if is_abs tm 1147# then (let bv,body = dest_abs tm in 1148# let bodyth = CONJ_DEPTH_CONV c body in 1149# MK_ABS (GEN bv bodyth)) 1150# else (REFL tm);; 1151CONJ_DEPTH_CONV = - : (conv -> conv) 1152Run time: 0.0s 1153\end{verbatim}\end{session} 1154 1155\noindent The next session shows that \ml{CONJ\_DEPTH\_CONV} is an 1156improvement over \ml{TOP\_DEPTH\_CONV}. 1157 1158\begin{session}\begin{verbatim} 1159#CONJ_DEPTH_CONV CONJ_NORM_CONV4 "^ex1 ==> ^ex1";; 1160|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==> 1161 A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = 1162 A /\ B /\ C /\ D ==> A /\ B /\ C /\ D 1163Run time: 0.4s 1164Intermediate theorems generated: 95 1165\end{verbatim}\end{session} 1166 1167\noindent However, the figures show that we are getting to a point of 1168diminishing returns. 1169 1170Finally, the tactic for normalizing all conjunctions in a goal is: 1171 1172\begin{session}\begin{verbatim} 1173#let CONJ_NORM_TAC = CONV_TAC (CONJ_DEPTH_CONV CONJ_NORM_CONV4);; 1174CONJ_NORM_TAC = - : tactic 1175Run time: 0.0s 1176\end{verbatim}\end{session} 1177 1178\noindent This is illustrated by: 1179 1180\begin{session}\begin{verbatim} 1181#g "^ex1 ==> ^ex1 /\ ^ex1_norm";; 1182"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==> 1183 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ A /\ B /\ C /\ D" 1184 1185() : void 1186Run time: 0.1s 1187 1188#e CONJ_NORM_TAC;; 1189OK.. 1190"A /\ B /\ C /\ D ==> A /\ B /\ C /\ D" 1191 1192() : void 1193Run time: 0.3s 1194Intermediate theorems generated: 110 1195\end{verbatim}\end{session} 1196 1197\noindent To show how much faster the optimized version is, here is 1198the last step repeated with the first version of the tool. The \ML\ 1199function \ml{b} backs up to the last goal. 1200 1201\begin{session}\begin{verbatim} 1202#b();; 1203"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==> 1204 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ A /\ B /\ C /\ D" 1205 1206() : void 1207Run time: 0.1s 1208\end{verbatim}\end{session} 1209 1210\noindent Expanding with the slow tactic: 1211 1212\begin{session}\begin{verbatim} 1213#e(CONV_TAC CONJ_NORM_CONV);; 1214OK.. 1215"A /\ B /\ C /\ D ==> A /\ B /\ C /\ D" 1216 1217() : void 1218Run time: 3.5s 1219Garbage collection time: 1.0s 1220Intermediate theorems generated: 1932 1221\end{verbatim}\end{session} 1222 1223\noindent it is 10 times slower and generates almost 20 times as many 1224primitive inference steps! 1225 1226 1227Here is the complete \ML{} program for the optimized normalizer. 1228 1229\begin{hol}\begin{verbatim} 1230 letrec insert ord x l = 1231 if null l 1232 then [x] 1233 if ord(x,hd l) 1234 then x.l 1235 else hd l.(insert ord x (tl l));; 1236 1237 letrec sort ord l = 1238 if null l 1239 then [] 1240 else insert ord (hd l) (sort ord (tl l));; 1241\end{verbatim}\end{hol} 1242 1243\begin{hol}\begin{verbatim} 1244 letrec PROVE_CONJ ths tm = 1245 (uncurry CONJ ((PROVE_CONJ ths # PROVE_CONJ ths) (dest_conj tm))) ? 1246 find (\th. concl th = tm) ths;; 1247 1248 let CONJ_EQ t1 t2 = 1249 let imp1 = DISCH t1 (PROVE_CONJ (CONJUNCTS(ASSUME t1)) t2) 1250 and imp2 = DISCH t2 (PROVE_CONJ (CONJUNCTS(ASSUME t2)) t1) 1251 in IMP_ANTISYM_RULE imp1 imp2;; 1252\end{verbatim}\end{hol} 1253 1254\begin{hol}\begin{verbatim} 1255 let CONJ_NORM_CONV t = 1256 if is_conj t 1257 then CONJ_EQ t (list_mk_conj(sort $<< (setify(conjuncts t)))) 1258 else fail;; 1259\end{verbatim}\end{hol} 1260 1261\begin{hol}\begin{verbatim} 1262 let MK_CONJ th1 th2 = MK_COMB(AP_TERM "$/\" th1, th2);; 1263 1264 letrec MK_CONJL l = 1265 if null l then fail 1266 if null(tl l) then hd l 1267 else MK_CONJ (hd l) (MK_CONJL(tl l));; 1268\end{verbatim}\end{hol} 1269 1270\begin{hol}\begin{verbatim} 1271 letrec CONJ_DEPTH_CONV c tm = 1272 if is_conj tm 1273 then (c THENC (MK_CONJL o map (CONJ_DEPTH_CONV c) o conjuncts)) tm 1274 if is_comb tm 1275 then (let rator,rand = dest_comb tm in 1276 MK_COMB (CONJ_DEPTH_CONV c rator, CONJ_DEPTH_CONV c rand)) 1277 if is_abs tm 1278 then (let bv,body = dest_abs tm in 1279 let bodyth = CONJ_DEPTH_CONV c body in 1280 MK_ABS (GEN bv bodyth)) 1281 else (REFL tm);; 1282\end{verbatim}\end{hol} 1283 1284\begin{hol}\begin{verbatim} 1285 let CONJ_NORM_TAC = CONV_TAC (CONJ_DEPTH_CONV CONJ_NORM_CONV);; 1286\end{verbatim}\end{hol} 1287 1288 1289Although the optimized implementation is much more efficient, it uses 1290less general methods. An advantage of the simple implementation based 1291on rewriting is that essentially the same algorithm can be used to 1292normalize terms built out of any associative, commutative and 1293idenpotent operation. The two exercises that follow (whose solutions are not 1294supplied) suggest that the reader try to extract general principles from the 1295conjunction normalizer and use these to implement generic tools. 1296 1297\subsection{Exercise 1} 1298 1299Implement a normalizer for any associative and commutative operator. 1300 1301\begin{hol}\begin{verbatim} 1302 AC_CANON_CONV : thm # thm -> conv 1303\end{verbatim}\end{hol} 1304 1305\noindent The two theorem arguments should be the 1306associative and commutative laws for the operator. For example: 1307 1308\begin{hol}\begin{verbatim} 1309 AC_CANON_CONV(ASSOC,SYM1) 1310\end{verbatim}\end{hol} 1311 1312\noindent would be a canonicalizer for conjunctions. 1313Use the `brute force' rewriting method described at the beginning of this chapter. 1314 1315\subsection{Exercise 2} 1316 1317 1318Implement an optimized canonicalizer: 1319 1320\begin{hol}\begin{verbatim} 1321 FAST_AC_CANON_CONV : thm # thm -> conv \end{verbatim}\end{hol} 1322\noindent This should use tuned rewriting (\eg\ a generalization of 1323\ml{CONJ\_DEPTH\_CONV}) and be as fast as possible. Try to think up 1324tricks to minimise the amount of general matching and to make every 1325inference count. 1326 1327 1328