1\index{quantHeuristicsLib|(} 2\index{Quantifier Instantiation|see {quantHeuristicsLib}} 3 4\setcounter{sessioncount}{0} 5 6\subsection{Motivation} 7 8Often interactive proofs can be simplified by instantiating 9quantifiers. The \ml{Unwind} library\index{Unwind}, which is part of the simplifier, allows 10instantiations of ``trivial'' quantifiers: 11 12\[ \forall x_1\ \ldots x_i \ldots x_n.\ P_1 \wedge \ldots \wedge x_i = c \wedge \ldots \wedge P_n \Longrightarrow Q \] 13and 14\[ \exists x_1\ \ldots x_i \ldots x_n.\ P_1 \wedge \ldots \wedge x_i = 15c \wedge \ldots \wedge P_n \] can be simplified by 16instantiating $x_i$ with $c$. Because unwind-conversions are 17part of \holtxt{bool\_ss}, they are used with nearly every call of the simplifier 18and often simplify proofs considerably. However, the \ml{Unwind} library can only handle these common cases. If the term structure is 19only slightly more complicated, it fails. For example, $\exists x.\ P(x) \Longrightarrow (x = 2) \wedge Q(x)$ 20cannot be tackled. 21 22There is also the \ml{Satisfy} library\index{Satisfy}, which uses 23unification to show existentially quantified formulas. It can handle 24problems like $\exists x.\ P_1(x,c_1)\ \wedge \ldots P_n(x,c_n)$ if 25given theorems of the form $\forall x\ c.\ P_i(x, c)$. This is often 26handy, but still rather limited. 27 28The quantifier heuristics library (\ml{quantHeuristicsLib}) provides more power 29and flexibility. A few simple examples of what it can do 30are shown in Table~\ref{table-qh-examples}. Besides the power demonstrated 31by these examples, the library is highly flexible as well. At its 32core, there is a modular, syntax driven search for instantiation. 33This search consists of a collection of interleaved heuristics. Users 34can easily configure existing heuristics and add own ones. Thereby, it 35is easy to teach the library about new predicates, logical connectives 36or datatypes. 37 38\newcommand{\mytablehead}[1]{\\\multicolumn{2}{l}{\textit{#1}}\\} 39\begin{table}[h] 40\centering\scriptsize 41\begin{tabular}{lll} 42\textbf{Problem} & \textbf{Result} \\\hline 43 44\mytablehead{basic examples} 45$\exists x.\ x = 2 \wedge P (x)$ & $P(2)$ \\ 46$\forall x.\ x = 2 \Longrightarrow P (x)$ & $P(2)$ \\ 47 48\mytablehead{solutions and counterexamples} 49$\exists x.\ x = 2$ & $\textit{true}$ \\ 50$\forall x.\ x = 2$ & $\textit{false}$ \\ 51 52\mytablehead{complicated nestings of standard operators} 53$\exists x_1. \forall x_2.\ (x_1 = 2) \wedge P(x_1, x_2)$ & 54$\forall x_2.\ P(2, x_2)$ \\ 55 56$\exists x_1, x_2.\ P_1(x_2) \Longrightarrow (x_1 = 2) \wedge P(x_1, x_2)$ & 57$\exists x_2.\ P_1(x_2) \Longrightarrow P(2, x_2)$ \\ 58$\exists x.\ ((x = 2) \vee (2 = x)) \wedge P(x)$ & $P(2)$ \\ 59 60\mytablehead{exploiting unification} 61$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f(10))$ & $P (f(10))$ \\ 62$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f(x + 2))$ & $P (f(8 + 2))$ \\ 63$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f(x))$ & - (\textrm{no instantiation found}) \\ 64 65\mytablehead{partial instantiation for datatypes} 66$\forall p.\ c = \textsf{FST}(p) \Longrightarrow P(p)$ & $\forall p_2.\ P(c, p_2)$ \\ 67 68$\forall x.\ \textsf{IS\_NONE}(x) \vee P(x)$ & $\forall x'.\ P (\textsf{SOME}(x'))$ \\ 69 70$\forall l.\ l \neq [\,] \Longrightarrow P(l)$ & $\forall \textit{hd}, \textit{tl}.\ 71P(\textit{hd} :: \textit{tl})$ \\ 72 73\mytablehead{context} 74$P_1(c) \Longrightarrow \exists x.\ P_1(x) \vee P_2(x)$ & \textit{true} \\ 75$P_1(c) \Longrightarrow \forall x.\ \neg P_1(x) \wedge P_2(x)$ & $\neg P_1(c)$ \\ 76 77$(\forall x.\ P_1(x) \Rightarrow (x = 2)) \Longrightarrow (\forall x.\ P_1(x) \Rightarrow P_2(x))$ & 78$(\forall x.\ P_1(x) \Rightarrow (x = 2)) \Rightarrow (P_1(2) \Rightarrow P_2(2))$ \\ 79 80$\big((\forall x.\ P_1(x) \Rightarrow P_2(x)) \wedge P_1(2)\big) \Longrightarrow \exists x.\ P_2(x)$ & 81\textit{true} \\ 82\hline 83\end{tabular} 84\caption{Examples} 85\label{table-qh-examples} 86\end{table} 87 88\subsection{User Interface}\label{sec:qh-interface} 89 90The quantifier heuristics library can be found in the sub-directory 91\holtxt{src/quantHeuristics}. The entry point to the framework is the 92library \holtxt{quantHeuristicsLib}. 93 94\subsubsection{Conversions} 95Usually the library is used for 96converting a term containing quantifiers to an equivalent one. For this, 97the following high level entry points exists: 98\bigskip 99 100\noindent 101\begin{tabular}{@{}ll} 102\texttt{QUANT\_INSTANTIATE\_CONV} & \texttt{: quant\_param list -> conv} \\ 103\texttt{QUANT\_INST\_ss} & \texttt{: quant\_param list -> ssfrag} \\ 104\texttt{QUANT\_INSTANTIATE\_TAC} & \texttt{: quant\_param list -> tactic} \\ 105\texttt{ASM\_QUANT\_INSTANTIATE\_TAC} & \texttt{: quant\_param list -> tactic} 106\end{tabular} 107\bigskip 108 109All these functions get a list of \emph{quantifier heuristic parameters} as arguments. These 110parameters essentially configure, which heuristics are used during the guess-search. If 111an empty list is provided, the tools know about the standard Boolean combinators, equations and context. 112\texttt{std\_qp} adds support for common datatypes like pairs or lists. 113Quantifier heuristic parameters are explained in more detail in 114Section~\ref{quantHeu-subsec-qps}. 115 116So, some simple usage of the quantifier heuristic library looks like: 117 118\begin{session} 119\begin{verbatim} 120- QUANT_INSTANTIATE_CONV [] ``?x. (!z. Q z /\ (x=7)) /\ P x``; 121> val it = |- (?x. (!z. Q z /\ (x = 7)) /\ P x) <=> (!z. Q z) /\ P 7: thm 122 123- QUANT_INSTANTIATE_CONV [std_qp] ``!x. IS_SOME x ==> P x`` 124> val it = |- (!x. IS_SOME x ==> P x) <=> !x_x'. P (SOME x_x'): thm 125\end{verbatim} 126\end{session} 127 128Usually, the quantifier heuristics library is used together with the 129simplifier using \holtxt{QUANT\_INST\_ss}. Besides interleaving 130simplification and quantifier instantiation, this has the benefit of 131being able to use context information collected by the simplifier: 132 133\begin{session} 134\begin{verbatim} 135- QUANT_INSTANTIATE_CONV [] ``P m ==> ?n. P n`` 136Exception- UNCHANGED raised 137 138- SIMP_CONV (bool_ss ++ QUANT_INST_ss []) [] ``P m ==> ?n. P n`` 139> val it = |- P m ==> (?n. P n) <=> T: thm 140\end{verbatim} 141\end{session} 142 143It's usually best to use \holtxt{QUANT\_INST\_ss} 144together with e.\,g.\ \holtxt{SIMP\_TAC} when using the library with tactics. 145However, if free variables of the goal should be instantiated, then 146\holtxt{ASM\_QUANT\_INSTANTIATE\_TAC} should be used: 147 148\begin{session} 149\begin{verbatim} 150P x 151------------------------------------ 152 IS_SOME x 153 : proof 154 155- e (ASM_QUANT_INSTANTIATE_TAC [std_qp]) 156> P (SOME x_x') : proof 157\end{verbatim} 158\end{session} 159 160There is also \holtxt{QUANT\_INSTANTIATE\_TAC}. This tactic does not 161instantiate free variables. Neither does it take assumptions into consideration. 162It is just a shortcut for using \holtxt{QUANT\_INSTANTIATE\_CONV} as a tactic. 163 164 165\subsubsection{Unjustified Guesses} 166 167Most heuristics justify the guesses they produce and therefore allow to 168prove equivalences of e.\,g.\ the form $\exists x.\ P(x) \Leftrightarrow P(i)$. 169However, the implementation also supports unjustified guesses, which may be bogus. 170Let's consider e.\,g.\ the formula $\exists x.\ P(x) \Longrightarrow (x = 2)\ \wedge\ Q(x)$. 171Because nothing is known about $P$ and $Q$, we can't find a safe instantiation for $x$ here. 172However, $2$ looks tempting and is probably sensible in many situations. (Counterexample: 173$P(2)$, $\neg Q(2)$ and $\neg P(3)$ hold) 174 175\texttt{implication\_concl\_qp} is a quantifier parameter that looks for valid guesses in the conclusion of an implication. 176Then, it assumes without justification that these guesses are probably sensible for the whole implication as well. 177Because these guesses might be wrong, one can either use implications or 178expansion theorems like $\exists x.\ P(x)\ \Longleftrightarrow (\forall x.\ x \neg c \Rightarrow \neg P(x)) \Rightarrow P(c)$. 179 180\begin{session} 181\begin{verbatim} 182- QUANT_INSTANTIATE_CONV [implication_concl_qp] 183 ``?x. P x ==> (x = 2) /\ Q x`` 184Exception- UNCHANGED raised 185 186- QUANT_INSTANTIATE_CONSEQ_CONV [implication_concl_qp] 187 CONSEQ_CONV_STRENGTHEN_direction 188 ``?x. P x ==> (x = 2) /\ Q x`` 189> val it = 190 |- (P 2 ==> Q 2) ==> ?x. P x ==> (x = 2) /\ Q x: thm 191 192- EXPAND_QUANT_INSTANTIATE_CONV [implication_concl_qp] 193 ``?x. P x ==> (x = 2) /\ Q x`` 194> val it = |- (?x. P x ==> (x = 2) /\ Q x) <=> 195 (!x. x <> 2 ==> ~(P x ==> (x = 2) /\ Q 2)) ==> P 2 ==> Q 2 196 197- SIMP_CONV (std_ss++EXPAND_QUANT_INST_ss [implication_concl_qp]) [] 198 ``?x. P x ==> (x = 2) /\ Q x`` 199> val it = 200 |- (?x. P x ==> (x = 2) /\ Q x) <=> 201 (!x. x <> 2 ==> P x) ==> P 2 ==> Q 2: thm 202\end{verbatim} 203\end{session} 204 205The following entry points should be used to exploit unjustified guesses: 206\bigskip 207 208\noindent 209\begin{tabular}{@{}ll} 210\texttt{QUANT\_INSTANTIATE\_CONSEQ\_CONV} & \texttt{: quant\_param list -> directed\_conseq\_conv} \\ 211\texttt{EXPAND\_QUANT\_INSTANTIATE\_CONV} & \texttt{: quant\_param list -> conv} \\ 212\texttt{EXPAND\_QUANT\_INST\_ss} & \texttt{: quant\_param list -> ssfrag} \\ 213\texttt{QUANT\_INSTANTIATE\_CONSEQ\_TAC} & \texttt{: quant\_param list -> tactic} 214\end{tabular} 215 216 217\subsubsection{Explicit Instantiations} 218 219A special (degenerated) use of the framework, is turning guess search off completely and 220providing instantiations explicitly. The tactic \holtxt{QUANT\_TAC} allows this. This means that 221it allows to partially instantiate quantifiers at subpositions 222with explicitly given terms. As such, it can be seen as 223a generalisation of \holtxt{EXISTS\_TAC}\index{EXISTS\_TAC}. 224% 225\begin{session} 226\begin{verbatim} 227- val it = !x. (!z. P x z) ==> ?a b. Q a b z : proof 228 229> e( QUANT_INST_TAC [("z", `0`, []), ("a", `SUC a'`, [`a'`])] ) 230- val it = !x. ( P x 0) ==> ? b a'. Q (SUC a') b z : proof 231\end{verbatim} 232\end{session} 233% 234This tactic is implemented using unjustified guesses. It normally 235produces implications, which is fine when used as a tactic. There is 236also a conversion called \holtxt{INST\_QUANT\_CONV} with the same 237functionality. For a conversion, implications are 238problematic. Therefore, the simplifier and Metis are used to prove 239the validity of the explicitly given instantiations. This succeeds 240only for simple examples. 241 242\subsection{Simple Quantifier Heuristics} 243 244The full quantifier heuristics described above are powerful and very flexible. 245However, they are sometimes slow. 246The unwind library\footnote{see \texttt{src/simp/src/Unwind.sml}} on the other hand is limited, but fast. 247The simple version of the quantifier heuristics fills the gap in the middle. 248They just search for gap guesses without any free variables. 249Moreover, slow operations like recombining or automatically looking up datatype information is omitted. 250As a result, the conversion \texttt{SIMPLE\_QUANT\_INSTANTIATE\_CONV} (and corresponding \texttt{SIMPLE\_QUANT\_INST\_ss}) is nearly as fast as the corresponding unwind conversions. 251However, it supports more complicated syntax. Moreover, there is support for quantifiers, pairs, list and much more. 252 253\subsection{Quantifier Heuristic Parameters}\label{quantHeu-subsec-qps} 254 255Quantifier heuristic parameters play a similar role for the quantifier 256instantiation library as simpsets do for the simplifier. They contain 257theorems, ML code and general configuration parameters that allow to configure 258guess-search. There are predefined parameters that handle 259common constructs and the user can define own parameters. 260 261\subsubsection{Quantifier Heuristic Parameters for Common Datatypes} 262 263There are \holtxt{option\_qp}, \holtxt{list\_qp}, \holtxt{num\_qp} and \holtxt{sum\_qp} for option types, lists, 264natural numbers and sum types respectively. 265Some examples are displayed in the following table: 266% 267\[\begin{array}{r@{\quad \Longleftrightarrow \quad}l} 268\forall x.\ \holtxt{IS\_SOME}(x) \Rightarrow P(x) & \forall x'.\ P (\holtxt{SOME}(x')) \\ 269\forall x.\ \holtxt{IS\_NONE}(x)& \textit{false} \\ 270\forall l.\ l \neq [\,] \Rightarrow P(l)& \forall h, l'.\ P(h::l') \\ 271\forall x.\ x = c + 3& \textit{false} \\ 272\forall x.\ x \neq 0 \Rightarrow P(x)& \forall x'.\ P(\holtxt{SUC}(x')) 273\end{array}\] 274 275\subsubsection{Quantifier Heuristic Parameters for Tuples} 276 277For tuples the situation is peculiar, because each quantifier over a variable of a product type 278can be instantiated. The challenge is to decide which quantifiers should be instantiated and 279which new variable names to use for the components of the pair. 280There is a quantifier heuristic parameter called \holtxt{pair\_default\_qp}. It first looks for 281subterms of the form $(\lambda (x_1, \ldots, x_n).\ \ldots)\ x$. If such a term is found $x$ is instantiated with 282$(x_1, \ldots, x_n)$. Otherwise, subterms of the form $\holtxt{FST}(x)$ and $\holtxt{SND}(x)$ are searched. If such a term 283is found, $x$ is instantiated as well. This parameter therefore allows simplifications like: 284% 285\[\begin{array}{r@{\quad \Longleftrightarrow \quad}l} 286\forall p.\ (x = \holtxt{SND}(p)) \Rightarrow P(p)& \forall p_1.\ P(p_1, x) \\ 287\exists p.\ (\lambda (p_a, p_b, p_c). P(p_a, p_b, p_c))\ p & \exists p_a, p_b, p_c.\ P(p_a, p_b, p_c) 288\end{array}\] 289 290\holtxt{pair\_default\_qp} is implemented in terms of the more general 291quantifier heuristic parameter \holtxt{pair\_qp}, which allows the 292user to provide a list of ML functions. These functions get the 293variable and the term. If they return a tuple of variables, these 294variables are used for the instantiation, otherwise the next function 295in the list is called or - if there is no function left - the variable 296is not instantiated. In the example of $\exists p.\ (\lambda (p_a, 297p_b, p_c). P(p_a, p_b, p_c))\ p$ these functions are given the 298variable $p$ and the term $(\lambda (p_a, p_b, p_c). P(p_a, p_b, 299p_c))\ p$ and return $\holtxt{SOME} (p_a, p_b, p_c)$. This simple 300ML-interface gives the user full control over what quantifier over 301product types to expand and how to name the new variables. 302 303\subsubsection{Quantifier Heuristic Parameter for Records} 304 305Records are similar to pairs, because they can always be instantiated. Here, it is interesting that the necessary 306monochotomy lemma comes from HOL~4's \holtxt{Type\_Base} library. This means that \holtxt{record\_qp} is stateful. 307If a new record type is defined, the automatically proven monochotomy lemma is then automatically used 308by \holtxt{record\_qp}. In contrast to the pair parameter, the one for records gets only one function instead of a 309list of functions to decide which variables to instantiate. However, this function is simpler, because it just needs 310to return true or false. The names of the new variables are constructed from the field-names of the record. 311The quantifier heuristic parameter \holtxt{default\_record\_qp} expands all records. 312 313\subsubsection{Stateful Quantifier Heuristic Parameters} 314 315The parameter for records is stateful, as it uses knowledge from 316\holtxt{Type\_Base}. Such information is not only useful for records 317but for general datatypes. The quantifier heuristic parameter 318\holtxt{TypeBase\_qp} uses automatically proven theorems about new 319datatypes to exploit mono- and dichotomies. Moreover, there is also a 320stateful \holtxt{pure\_stateful\_qp} that allows the user to 321explicitly add other parameters to it. \holtxt{stateful\_qp} is a 322combination of \holtxt{pure\_stateful\_qp} and \holtxt{TypeBase\_qp}. 323 324\subsubsection{Standard Quantifier Heuristic Parameter} 325 326The standard quantifier heuristic parameter \holtxt{std\_qp} combines 327the parameters for lists, options, natural numbers, the default one 328for pairs and the default one for records. 329 330 331\subsection{User defined Quantifier Heuristic Parameters}\label{sec:qps-user} 332 333The user is also able to define own parameters. There 334is \holtxt{empty\_qp}, which does not contain any information. Several 335parameters can be combined using 336\holtxt{combine\_qps}. Together with the basic types of user defined 337parameters that are explained below, these functions provide an 338interface for user defined quantifier heuristic parameters. 339 340\subsubsection{Rewrites / Conversions} 341 342A very powerful, yet simple technique for teaching the guess search 343about new constructs are rewrite rules. For example, the standard rules 344for equations and basic logical operations 345cannot generate guesses for the predicate \holtxt{IS\_SOME}. By 346rewriting \holtxt{IS\_SOME(x)} to \holtxt{?x'. x = 347SOME(x')}, however, these rules fire. 348 349\holtxt{option\_qp} uses this rewrite to implement support for 350\holtxt{IS\_SOME}. Similarly support for predicates like \holtxt{NULL} is 351implemented using rewrites. Even adding 352rewrites like $\textsf{append}(l_1, l_2) = [\,] \Longleftrightarrow (l_1 = 353[\,]\ \wedge\ l_2 = [\,])$ for list-append turned out to be beneficial 354in practice. 355\bigskip 356 357\holtxt{rewrite\_qp} allows to provide rewrites in the form of rewrite theorems. 358For the example of \holtxt{IS\_SOME} this looks like: 359 360\begin{session} 361\begin{verbatim} 362> val thm = QUANT_INSTANTIATE_CONV [] ``!x. IS_SOME x ==> P x`` 363Exception- UNCHANGED raised 364 365> val IS_SOME_EXISTS = prove (``IS_SOME x = (?x'. x = SOME x')``, 366 Cases_on `x` THEN SIMP_TAC std_ss []); 367val IS_SOME_EXISTS = |- IS_SOME x <=> ?x'. x = SOME x': thm 368 369> val thm = QUANT_INSTANTIATE_CONV [rewrite_qp[IS_SOME_EXISTS]] 370 ``!x. IS_SOME x ==> P x`` 371val thm = |- (!x. IS_SOME x ==> P x) <=> 372 !x'. IS_SOME (SOME x') ==> P (SOME x'): thm 373\end{verbatim} 374\end{session} 375 376To clean up the result after instantiation, theorems used to rewrite the result after instantiation can be provided via 377\holtxt{final\_rewrite\_qp}. 378\begin{session} 379\begin{verbatim} 380> val thm = QUANT_INSTANTIATE_CONV [rewrite_qp[IS_SOME_EXISTS], 381 final_rewrite_qp[option_CLAUSES]] 382 ``!x. IS_SOME x ==> P x`` 383val thm = |- (!x. IS_SOME x ==> P x) <=> !x'. P (SOME x'): thm 384\end{verbatim} 385\end{session} 386 387If rewrites are not enough, \holtxt{conv\_qp} can be used to add conversions: 388\begin{session} 389\begin{verbatim} 390- val thm = QUANT_INSTANTIATE_CONV [] ``?x. (\y. y = 2) x`` 391Exception- UNCHANGED raised 392 393- val thm = QUANT_INSTANTIATE_CONV [convs_qp[BETA_CONV]] ``?x. (\y. y = 2) x`` 394> val thm = |- (?x. (\y. y = 2) x) <=> T: thm 395\end{verbatim} 396\end{session} 397 398\subsubsection{Strengthening / Weakening} 399 400In rare cases, equivalences that can be used for rewrites are unavailable. There might be just implications that 401can be used for strengthening or weakening. The function 402\holtxt{imp\_qp} might be used to provide such implication. 403 404\begin{session} 405\begin{verbatim} 406- val thm = QUANT_INSTANTIATE_CONV [list_qp] ``!l. 0 < LENGTH l ==> P l`` 407Exception- UNCHANGED raised 408 409- val LENGTH_LESS_IMP = prove (``!l n. n < LENGTH l ==> l <> []``, 410 Cases_on `l` THEN SIMP_TAC list_ss []); 411> val LENGTH_LESS_IMP = |- !l n. n < LENGTH l ==> l <> []: thm 412 413- val thm = QUANT_INSTANTIATE_CONV [imp_qp[LENGTH_LESS_IMP], list_qp] 414 ``!l. 0 < LENGTH l ==> P l`` 415> val thm = 416 |- (!l. 0 < LENGTH l ==> P l) <=> 417 !l_t l_h. 0 < LENGTH (l_h::l_t) ==> P (l_h::l_t): thm 418 419- val thm = SIMP_CONV (list_ss ++ 420 QUANT_INST_ss [imp_qp[LENGTH_LESS_IMP], list_qp]) [] 421 ``!l. SUC (SUC n) < LENGTH l ==> P l`` 422> val thm = 423 |- (!l. SUC (SUC n) < LENGTH l ==> P l) <=> 424 !l_h l_t_h l_t_t_t l_t_t_h. n < SUC (LENGTH l_t_t_t) ==> 425 P (l_h::l_t_h::l_t_t_h::l_t_t_t): thm 426\end{verbatim} 427\end{session} 428 429 430\subsubsection{Filtering} 431Sometimes, one might want to avoid to instantiate certain quantifiers. 432The function \holtxt{filter\_qp} allows to add ML-functions that filter the handled 433quantifiers. These functions are given a variable $x$ and a term $P(x)$. 434The tool only tries to instantiate $x$ in $P(x)$, if all filter functions 435return \textit{true}. 436 437\begin{session} 438\begin{verbatim} 439- val thm = QUANT_INSTANTIATE_CONV [] 440 ``?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x, y, z)`` 441> val thm = |- (?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x,y,z)) <=> 442 P (1,2,3): thm 443 444- val thm = QUANT_INSTANTIATE_CONV 445 [filter_qp [fn v => fn t => (v = ``y:num``)]] 446 ``?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x, y, z)`` 447> val thm = |- (?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x,y,z)) <=> 448 ?x z. (x = 1) /\ (z = 3) /\ P (x,2,z): thm 449\end{verbatim} 450\end{session} 451 452\subsubsection{Satisfying and Contradicting Instantiations} 453 454As the satisfy library demonstrates, it is often 455useful to use unification and explicitly given theorems to 456find instantiations. In addition to satisfying instantiations, the quantifier heuristics framework 457is also able to use contradicting ones. The theorems used for finding instantiations usually come from 458the context. However, \holtxt{instantiation\_qp} allows to add additional ones: 459 460\begin{session} 461\begin{verbatim} 462> val thm = SIMP_CONV (std_ss++QUANT_INST_ss[]) [] 463 ``P n ==> ?m:num. n <= m /\ P m`` 464Exception- UNCHANGED raised 465 466> val thm = SIMP_CONV (std_ss++ 467 QUANT_INST_ss[instantiation_qp[LESS_EQ_REFL]]) [] 468 ``P n ==> ?m:num. n <= m /\ P m`` 469> val thm = |- P n ==> ?m:num. n <= m /\ P m = T : thm 470\end{verbatim} 471\end{session} 472 473\subsubsection{Di- and Monochotomies} 474 475Dichotomies can be exploited for guess search. 476\holtxt{distinct\_qp} provides an interface to add theorems 477of the form $\forall x.\ c_1(x) \neq c_2(x)$. 478\holtxt{cases\_qp} expects theorems of the form 479$\forall x. \ (x = \exists \textit{fv}. c_1(\textit{fv}))\ \vee \ldots \vee (x = \exists \textit{fv}. c_n(\textit{fv}))$. 480However, only theorems for $n = 2$ and $n = 1$ are used. All other cases are currently ignored. 481 482\subsubsection{Oracle Guesses} 483 484Sometimes, the user does not want to justify guesses. The tactic 485\holtxt{QUANT\_TAC} is implemented using oracle guesses for example. 486A simple interface to oracle guesses is provided by \holtxt{oracle\_qp}. 487It expects a ML function that given a variable and a term returns 488a pair of an instantiation and the free variables in this instantiation. 489 490As an example, lets define a parameter that states that every list is non-empty: 491\begin{verbatim} 492 val dummy_list_qp = oracle_qp (fn v => fn t => 493 let 494 val (v_name, v_list_ty) = dest_var v; 495 val v_ty = listSyntax.dest_list_type v_list_ty; 496 497 val x = mk_var (v_name ^ "_hd", v_ty); 498 val xs = mk_var (v_name ^ "_tl", v_list_ty); 499 val x_xs = listSyntax.mk_cons (x, xs) 500 in 501 SOME (x_xs, [x, xs]) 502 end) 503\end{verbatim} 504 505\noindent 506Notice, that an option type is returned and that the function is 507allowed to throw \holtxt{HOL\_ERR} exceptions. 508With this definition, we get 509 510\begin{session} 511\begin{verbatim} 512- NORE_QUANT_INSTANTIATE_CONSEQ_CONV [dummy_list_qp] 513 CONSEQ_CONV_STRENGTHEN_direction ``?x:'a list y:'b. P (x, y)`` 514> val it = ?y x_hd x_tl. P (x_hd::x_tl,y)) ==> ?x y. P (x,y) : thm 515\end{verbatim} 516\end{session} 517 518\subsubsection{Lifting Theorems} 519 520The function \holtxt{inference\_qp} enables the 521user to provide theorems that allow lifting guesses over 522user defined connectives. As writing these lifting theorems requires 523deep knowledge about guesses, it is not discussed here. Please have a 524look at the detailed documentation of the quantifier heuristics library as 525well as its sources. You might also want to contact 526Thomas Tuerk (\url{tt291@cl.cam.ac.uk}). 527 528 529\subsubsection{User defined Quantifier Heuristics} 530 531At the lowest level, the tool searches guesses using ML-functions 532called \emph{quantifier heuristics}. Slightly simplified, such a 533quantifier heuristic gets a variable and a term and returns a set of 534guesses for this variable and term. Heuristics allow full 535flexibility. However, to write your own heuristics a lot of knowledge 536about the ML-datastructures and auxiliary functions is 537required. Therefore, no details are discussed here. Please have a look 538at the source code and contact Thomas Tuerk 539(\url{tt291@cl.cam.ac.uk}), if you have questions. 540\holtxt{heuristics\_qp} and \holtxt{top\_heuristics\_qp} provide 541interfaces to add user defined heuristics to a quantifier heuristics 542parameter. 543 544\index{quantHeuristicsLib|)} 545 546 547%%% Local Variables: 548%%% mode: latex 549%%% TeX-master: "description" 550%%% End: 551