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