Merge branch 'master' of github.com:mn200/HOL

.gitignore

@@ -11,6 +11,7 @@
 *.grm-sig.sml
 *.grm.desc
 *.exe
+.DS_Store
 
 # LaTeX guff
 *.aux
@@ -89,6 +90,8 @@ src/HolSat/sat_solvers/zc2hs/*.h
 src/HolSat/sat_solvers/zc2hs/zc2hs
 src/HolSat/sat_solvers/minisat/minisat
 src/HolSat/sat_solvers/minisat/depend.mak
+src/num/termination/numheap
+src/num/termination/numheap.o
 src/pair/help
 src/parse/base_lexer.sml
 src/quotient/examples/*/*.html

INSTALL

@@ -171,12 +171,11 @@ Dealing with failure
       . version of Moscow ML or Poly/ML being used
       . version of HOL being built
 
-* Alternatively, use the Support tracker web-page at
+* Alternatively, use the github issues web-page at
 
-      http://sourceforge.net/tracker/?func=add&group_id=31790&atid=403398
+      http://github.com/mn200/HOL/issues
 
-  and submit a request for support.  You can also use the Bugs forum
-  on SourceForge.
+  and submit a description of the problem.
 
 * If a build attempt fails for some reason, you should attempt to invoke
 

Manual/Description/HolQbf.tex

@@ -19,8 +19,11 @@
   July 11--14, 2010.  Proceedings, volume 6172 of Lecture Notes in
   Computer Science, pages 466--480.  Springer, 2010.
 \item Ramana Kumar and Tjark Weber: {\it Validating QBF Validity in
-  HOL4}.  To appear at the Second International Conference on
-  Interactive Theorem Proving (ITP 2011).
+  HOL4}.  In Marko C.\ J.\ D.\ van Eekelen, Herman Geuvers, Julien Schmaltz,
+  and Freek Wiedijk, editors, Interactive Theorem Proving, Second International
+  Conference, ITP 2011, Berg en Dal, The Netherlands, August 22--25, 2011.
+  Proceedings, volue 6898 of Lecture Notes in Computer Science, pages 168--183.
+  Springer, 2011.
 \end{itemize}
 \ml{HolQbfLib} uses an external QBF solver, Squolem, to decide
 Quantified Boolean Formulae.
@@ -39,10 +42,10 @@ \subsection{Installing Squolem}
 \subsection{Interface}
 \label{qbf-interface}
 
-The library provides three functions, each of type \ml{term -> thm},
-to invoke Squolem: \ml{decide}, \ml{disprove}, and \ml{prove}.  These
-are defined in the \ml{HolQbfLib} structure, which is the library's
-main entry point.
+The library provides four functions, each of type \ml{term -> thm}, to invoke
+Squolem: \ml{decide}, \ml{decide\_prenex}, \ml{disprove}, and \ml{prove}.  These
+are defined in the \ml{HolQbfLib} structure, which is the library's main entry
+point.
 
 Calling \ml{prove $\phi$} will invoke Squolem on the QBF~$\phi$ to
 establish its validity.  If this succeeds, \ml{prove} will then
@@ -54,18 +57,24 @@ \subsection{Interface}
 will then validate the certificate of invalidity generated by Squolem
 in \HOL{} to return a theorem $\phi \vdash \bot$.
 
-\ml{decide $\phi$} combines the functionality of \ml{prove} and
+\ml{decide\_prenex $\phi$} combines the functionality of \ml{prove} and
 \ml{disprove} into a single function.  It will invoke Squolem on
 $\phi$ and return either $\vdash \phi$ or $\phi \vdash \bot$,
 depending on Squolem's answer.
 
+Finally, \ml{decide} does the same job as \ml{decide\_prenex} but accepts QBFs
+in a less restricted form. Restrictions on $\phi$ are described below.
+
 \begin{session}
 \begin{verbatim}
 - load "HolQbfLib";
+metis: r[+0+3]#
+r[+0+6]#
 > val it = () : unit
 
 - open HolQbfLib;
 > val decide = fn: term -> thm
+val decide_prenex = fn: term -> thm
 val disprove = fn: term -> thm
 val prove = fn: term -> thm
 
@@ -74,29 +83,38 @@ \subsection{Interface}
 
 - decide ``?x. x``;
 <<HOL message: HolQbfLib: calling external command
-  'squolem2 -c /tmp/filedH1K2x >& /dev/null'>>
+  'squolem2 -c /tmp/filedH1K2x >/dev/null 2>&1'>>
 > val it =  [] |- ?x. x: thm
 
-- decide ``!x. ?y. x /\ y``;
+- decide ``(?y. x \/ y) ==> ~x``;
+> val it = [!x. (?y. x \/ y) ==> ~x] |- F: thm
+
+- decide ``~(?x. x ==> y) \/ (?x. y ==> x)``;
+<<HOL message: HolQbfLib: calling external command
+  'squolem2 -c /tmp/fileyap3oD >/dev/null 2>&1'>>
+> val it = [] |- ~(?x. x ==> y) \/ ?x. y ==> x: thm
+
+- decide_prenex ``!x. ?y. x /\ y``;
 <<HOL message: HolQbfLib: calling external command
-  'squolem2 -c /tmp/fileZAGj4m >& /dev/null'>>
+  'squolem2 -c /tmp/fileZAGj4m >/dev/null 2>&1'>>
 > val it = [!x. ?y. x /\ y] |- F : thm
 
 - disprove ``!x. ?y. x /\ y``;
 <<HOL message: HolQbfLib: calling external command
-  'squolem2 -c /tmp/file0Pw2Tg >& /dev/null'>>
+  'squolem2 -c /tmp/file0Pw2Tg >/dev/null 2>&1'>>
 > val it = [!x. ?y. x /\ y] |- F : thm
 
 - prove ``?x. x``;
 <<HOL message: HolQbfLib: calling external command
-  'squolem2 -c /tmp/fileKi4Lkz >& /dev/null'>>
+  'squolem2 -c /tmp/fileKi4Lkz >/dev/null 2>&1'>>
 - val it =  [] |- ?x. x: thm
 \end{verbatim}
 \end{session}
 
 \paragraph{Supported subset of higher-order logic}
+The argument given to \ml{decide} must be a Boolean term built using only conjunction, disjunction, implication, negation, universal/existential quantification, and variables. Free variables are considered universally quantified. Every quantified variable must occur.
 
-The argument given to either of these functions must be a QBF in
+The argument given to the other functions must be a QBF in
 prenex form, \ie, a term of the form $Q_1 x_1. \, Q_2 x_2. \, \ldots
 \, Q_n x_n. \, \phi$, where
 \begin{itemize}
@@ -159,14 +177,6 @@ \subsection{Wishlist}
 additional feature requests (or code contributions) via
 \url{http://hol.sf.net}.
 
-\paragraph{Transformation of QBF into prenex form}
-
-\ml{HolQbfLib} at present only supports QBF in prenex form (see the
-description of the supported subset of higher-order logic given in
-Section~\ref{qbf-interface}).  A transformation (implemented in \HOL)
-that converts arbitrary QBF into prenex form would greatly enhance
-\ml{HolQbfLib}'s applicability.
-
 \paragraph{Support for other QBF solvers}
 
 So far, Squolem is the only QBF solver that has been integrated with

Manual/Description/definitions.tex

@@ -798,13 +798,19 @@ \section{Quotient Types}\label{quotients}
 \section{Case Expressions}\label{CaseExp}
 \index{case expressions|(}
 
-Within the HOL{} logic,
-case expressions provide a very compact and convenient notation
-for multi-way selection among the values of several expressions.
-This is modeled on the case constructs in functional programming
-languages such as Standard ML.  Such case expressions can simplify
-the expression of complicated branches between different cases or
-combinations of cases.
+Within the HOL{} logic, case expressions provide a very compact and convenient notation for multi-way selection among the values of several expressions.
+This is modeled on the case constructs in functional programming languages such as Standard ML.
+Such case expressions can simplify the expression of complicated branches between different cases or combinations of cases.
+The basic syntax (where the non-terminal $\mathit{term}$ stands for any \HOL{} term) is
+\begin{eqnarray*}
+\mathit{term} & ::= & \texttt{case}\;\mathit{term}\;\texttt{of}\;\mathit{cases}\\
+\mathit{cases} &::= & \mathit{case}_1 \;\mathit{morecases}\\
+\mathit{case}_1 & ::= & \texttt{\bfseries |}\;\mathit{case} \;\;\;|\;\;\;\mathit{case}\\
+\mathit{morecases} & ::= & \varepsilon\;\;\;|\;\;\;\texttt{|}\;\mathit{case}\;\mathit{morecases}\\
+\mathit{case} & ::= & \mathit{term} \;\texttt{=>}\; \mathit{term}
+\end{eqnarray*}
+The choice in the rule for the first case ($\mathit{case}_1$) allows the use of more uniform syntax, where every case is preceded by a vertical bar.
+Omitting the bar, which is what the pretty-printer does when the syntax is printed, conforms with the syntax used by SML.
 
 Based on the value of a test expression, a list of pattern expressions
 are considered in sequence to see if they match the test expression.
@@ -834,11 +840,11 @@ \section{Case Expressions}\label{CaseExp}
 \begin{hol}
 \begin{verbatim}
   case spouse(employee) of
-     NONE   => "single"
-   | SOME s => "married to " ^ name_of s
+   | NONE   => "single"
+   | SOME s => "married to " ++ name_of s
 \end{verbatim}
 \end{hol}
-%
+(This example uses the optional bar in front of the first case.)
 
 HOL{} supports a rich structure of case expressions using a single
 notation.  The format is related to that of definitions of recursive

Manual/Description/holCheck.tex

@@ -10,9 +10,9 @@
 \usepackage{graphicx}
 \usepackage{url}
 
-% ---------------------------------------------------------------------                                                                                     
-% Input defined macros and commands                                                                                                                         
-% ---------------------------------------------------------------------                                                                                     
+% ---------------------------------------------------------------------
+% Input defined macros and commands
+% ---------------------------------------------------------------------
 \input{../LaTeX/commands}
 
 \newcommand{\tsu}[1]{\textsf{\textup{#1}}}
@@ -62,7 +62,7 @@ \subsection{Quick Usage Overview}
 
 This section provides a quick look at a typical use of \hc{}. We choose a simple mod-8 counter as our example, which starts at 0 and counts up to 7, and then loops from 0 again. We wish to show that the most significant bit eventually goes high.
 
-First we load the \hc{} library: 
+First we load the \hc{} library:
 \begin{session}\begin{verbatim}
 - load "holCheckLib"; open holCheckLib;
   (* we don't show the output from the "open" here *)
@@ -72,7 +72,7 @@ \subsection{Quick Usage Overview}
 (string, term) pairs, where each string is a transition label and
 each term represents a transition relation (three booleans
 required to encode numbers 0-7; next-state variable values
-indicated by priming; note we expand the xor, since \hc{} 
+indicated by priming; note we expand the xor, since \hc{}
 currently requires purely propositional terms) :
 \begin{session}\begin{verbatim}
 - val xor_def = Define `xor x y = (x \/ y) /\ ~(x=y)`;

Manual/Description/misc.tex

@@ -636,6 +636,71 @@ \subsection{Using a make-file with \holmake}
 such variable in the environment, then the variable is silently given
 the empty string as its value.
 
+\paragraph{Conditional Parts of Makefiles}
+\index{Holmake@\holmake!conditional inclusion of sections}
+As in GNU~\textsf{make}, parts of a \texttt{Holmakefile} can be included or excluded dynamically, depending on tests that can be performed on strings including variables.
+%
+This is similar to the way directives such as \texttt{\#ifdef} can be used to control the C~preprocessor.
+
+There are four possible directives in a \texttt{Holmakefile}: \texttt{ifdef}, \texttt{ifndef}, \texttt{ifeq} and \texttt{ifneq}.
+%
+The versions including the extra `n' character reverse the boolean sense of the test.
+%
+Conditional directives can be chained together with \texttt{else} directives, and must be terminated by the \texttt{endif} command.
+%
+The following example is a file that only has any content if the \texttt{POLY} variable is defined, which happens when Poly/ML is the underlying \ML{} system.
+\begin{hol}
+\begin{verbatim}
+ifdef POLY
+TARGETS = target1 target2
+
+target1: dependency1
+      build_command -o target1 dependency1
+endif
+\end{verbatim}
+\end{hol}
+The next example includes chained \texttt{else} commands:
+\begin{hol}
+\begin{verbatim}
+ifeq "$(HOLDIR)" "foo"
+VAR = X
+else ifneq "$(HOLDIR)" "bar"
+VAR = Y
+else
+VAR = Z
+endif
+\end{verbatim}
+\end{hol}
+\index{ifeq (Holmake directive)@\texttt{ifeq} (Holmake directive)}
+\index{ifneq (Holmake directive)@\texttt{ifneq} (Holmake directive)}
+The \texttt{ifneq} and \texttt{ifeq} forms test for string equality.
+%
+They can be passed their arguments as in the example, or delimited with apostrophes, or in parentheses with no delimiters, as in:
+\begin{hol}
+\begin{verbatim}
+ifeq ($(HOLDIR),$(OTHERDIR))
+VAR = value
+endif
+\end{verbatim}
+\end{hol}
+
+\index{ifdef (Holmake directive)@\texttt{ifdef} (Holmake directive)}
+\index{ifndef (Holmake directive)@\texttt{ifndef} (Holmake directive)}
+The definedness tests \texttt{ifdef} and \texttt{ifndef} test if a name has a non-null expansion in the current environment.
+%
+This test is just of one level of expansion.
+%
+In the following example, \texttt{VAR} is defined even though it ultimately expands to the emptry string, but \texttt{NULL} is not.
+%
+The variable \texttt{FOOBAR} is also not defined.
+\begin{hol}
+\begin{verbatim}
+NULL =
+VAR = $(NULL)
+\end{verbatim}
+\end{hol}
+Note that environment variables with non-empty values are also considered to be defined.
+
 \index{Holmake@\holmake|)}