Merge remote-tracking branch 'origin/master'

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/Reference/theorems-intro.tex

@@ -2,7 +2,7 @@
 These include theorems proved and bound to \ML\ identifiers when the system is
 built, and theorems proved when the system is built and then stored in a
 built-in theory file.  The latter are usually (but not always) set up to
-autoload when their names are mentioned in \ML.  
+autoload when their names are mentioned in \ML.
 
 Theorems are listed in alphabetical order, by the name of the \ML\ identifier
 to which they are bound or the name under which they are stored in a built-in

Manual/Tutorial/binomial.tex

@@ -2,14 +2,14 @@
 %%%% Revised contents of Manual/Tutorial/binomial.tex %%%%
 \chapter{Example: the Binomial Theorem}\label{binomial}
 
-The Binomial Theorem in \HOL{} is a medium sized worked example whose subject 
-matter is more widely known than any specific piece of hardware or software. 
-This chapter introduces the small amount of algebra and mathematical notation 
-needed to state and prove the Binomial Theorem, shows how this is rendered 
+The Binomial Theorem in \HOL{} is a medium sized worked example whose subject
+matter is more widely known than any specific piece of hardware or software.
+This chapter introduces the small amount of algebra and mathematical notation
+needed to state and prove the Binomial Theorem, shows how this is rendered
 in \HOL{}, and outlines the structure of the proof.
 
 This chapter is also available as the self-contained case study \ml{binomial}
-in the directory {\small\verb%Training/studies%}. 
+in the directory {\small\verb%Training/studies%}.
 
 \def\self{chapter}
 \def\path{{\tt Training/studies/binomial}}

Manual/Tutorial/binomial/appendix.tex

@@ -18,10 +18,10 @@ \section{Principal lemmas}
 Algebraic laws:
 \begin{session}
 \begin{verbatim}
-RIGHT_CANCELLATION = 
+RIGHT_CANCELLATION =
 |- !plus. Group plus ==> (!a b c. (plus b a = plus c a) ==> (b = c))
 
-RING_0 = 
+RING_0 =
 |- !plus times.
     RING(plus,times) ==>
     (!a. times(Id plus)a = Id plus) /\ (!a. times a(Id plus) = Id plus)
@@ -34,12 +34,12 @@ \section{Principal lemmas}
 \begin{verbatim}
 POWER_1 = |- !plus. MONOID plus ==> (POWER plus 1 a = a)
 
-POWER_DISTRIB = 
+POWER_DISTRIB =
 |- !plus times.
     RING(plus,times) ==>
     (!a b n. times a(POWER plus n b) = POWER plus n(times a b))
 
-POWER_ADD = 
+POWER_ADD =
 |- !plus.
     MONOID plus ==>
     (!m n a. POWER plus(m + n)a = plus(POWER plus m a)(POWER plus n a))
@@ -49,18 +49,18 @@ \section{Principal lemmas}
 Reduction of lists:
 \begin{session}
 \begin{verbatim}
-REDUCE_APPEND = 
+REDUCE_APPEND =
 |- !plus.
     MONOID plus ==>
     (!as bs.
       REDUCE plus(APPEND as bs) = plus(REDUCE plus as)(REDUCE plus bs))
 
-REDUCE_MAP_MULT = 
+REDUCE_MAP_MULT =
 |- !plus times.
     RING(plus,times) ==>
     (!a bs. REDUCE plus(MAP(times a)bs) = times a(REDUCE plus bs))
 
-REDUCE_MAP = 
+REDUCE_MAP =
 |- !plus.
     MONOID plus /\ COMMUTATIVE plus ==>
     (!f g as.
@@ -84,31 +84,31 @@ \section{Principal lemmas}
 \begin{verbatim}
 SIGMA_ID = |- !plus m f. SIGMA(plus,m,0)f = Id plus
 
-SIGMA_LEFT_SPLIT = 
+SIGMA_LEFT_SPLIT =
 |- !plus m n f. SIGMA(plus,m,SUC n)f = plus(f m)(SIGMA(plus,SUC m,n)f)
 
-SIGMA_RIGHT_SPLIT = 
+SIGMA_RIGHT_SPLIT =
 |- !plus.
     MONOID plus ==>
     (!m n f. SIGMA(plus,m,SUC n)f = plus(SIGMA(plus,m,n)f)(f(m + n)))
 
-SIGMA_SHIFT = 
+SIGMA_SHIFT =
 |- !plus m n f. SIGMA(plus,SUC m,n)f = SIGMA(plus,m,n)(f o SUC)
 
-SIGMA_MULT_COMM = 
+SIGMA_MULT_COMM =
 |- !plus times.
     RING(plus,times) ==>
     (!m n a f.
       times a(SIGMA(plus,m,n)f) = SIGMA(plus,m,n)((times a) o f))
 
-SIGMA_PLUS_COMM = 
+SIGMA_PLUS_COMM =
 |- !plus.
     MONOID plus /\ COMMUTATIVE plus ==>
     (!f g m n.
       plus(SIGMA(plus,m,n)f)(SIGMA(plus,m,n)g) =
       SIGMA(plus,m,n)(\k. plus(f k)(g k)))
 
-SIGMA_EXT = 
+SIGMA_EXT =
 |- !plus.
     MONOID plus ==>
     (!f g m n.
@@ -120,12 +120,12 @@ \section{Principal lemmas}
 Terms from the Binomial Theorem:
 \begin{session}
 \begin{verbatim}
-BINTERM_0 = 
+BINTERM_0 =
 |- !plus times.
     RING(plus,times) ==>
     (!a b n. BINTERM plus times a b n 0 = POWER times n a)
 
-BINTERM_n = 
+BINTERM_n =
 |- !plus times.
     RING(plus,times) ==>
     (!a b n. BINTERM plus times a b n n = POWER times n b)

Manual/Tutorial/logic.tex

@@ -151,7 +151,7 @@ \chapter{The HOL Logic}\label{HOLlogic}
 \end{session}
 
 The constructors {\small\verb|mk_conj|} and {\small\verb|mk_imp|} construct
-conjunctions and implications respectively. A large collection of 
+conjunctions and implications respectively. A large collection of
 term constructors and destructors is available for the core theories
 in \HOL.
 
@@ -228,7 +228,7 @@ \chapter{The HOL Logic}\label{HOLlogic}
 
 \paragraph{Function application types}
 
-An application $(t_1\ t_2)$ is well-typed if $t_1$ is a function 
+An application $(t_1\ t_2)$ is well-typed if $t_1$ is a function
 with type $\tau_1 \to \tau_2$ and $t_2$ has type $\tau_1$. Contrarily,
 an application $(t_1\ t_2)$ is badly typed if $t_1$ is not a function:
 
@@ -262,7 +262,7 @@ \chapter{The HOL Logic}\label{HOLlogic}
 
 unification failure message: unify failed
 ! Uncaught exception:
-! HOL_ERR 
+! HOL_ERR
 \end{verbatim}\end{session}
 
 The dollar symbol in front of {\small\verb|~|} indicates that the
@@ -564,14 +564,14 @@ \section{Forward proof}
 - val Th5 = ASSUME ``t1``;
 <<HOL message: inventing new type variable names: 'a.>>
 ! Uncaught exception:
-! HOL_ERR 
+! HOL_ERR
 - val Th5 = ASSUME ``t1`` handle e => Raise e;
 <<HOL message: inventing new type variable names: 'a.>>
 
 Exception raised at Thm.ASSUME:
 not a proposition
 ! Uncaught exception:
-! HOL_ERR 
+! HOL_ERR
 
 - val Th5 = ASSUME ``t1:bool``;
 > val Th5 =  [.] |- t1 : thm
@@ -1032,7 +1032,7 @@ \section{Goal Oriented Proof: Tactics and Tacticals}
 are propagated unchanged to the two subgoals is indicated by the absence
 of assumptions in the notation.
 
-Another example is {\small\verb|numLib.INDUCT_TAC|}, the tactic for
+Another example is \ml{numLib.INDUCT_TAC},\footnote{Later, we will write \ml{INDUCT_TAC} on its own, without first prefixing it with \ml{numLib}.  To allow this we must issue the command \ml{open~numLib}.} the tactic for
 doing mathematical induction on the natural numbers:
 
 \begin{center}

Manual/Tutorial/proof-tools.tex

@@ -677,7 +677,7 @@ \subsection{Performance}
    (c_3 = c2_3) /\ (s_0 = s2_0) /\ (s_1 = s2_1) /\ (s_2 = s2_2)
 \end{verbatim}
 \end{hol}
-(if you want real speed, the built-in function \ml{tautLib.TAUT\_PROVE} does the above 
+(if you want real speed, the built-in function \ml{tautLib.TAUT\_PROVE} does the above
 in less than a second, by using  an external tool to generate the proof
  of unsatisfiability, and then translating that proof back into HOL).
 

Manual/Tutorial/tutorial.tex

@@ -27,6 +27,7 @@
 %\includeonly{Studies/int_mod/mod_arith_study/tutorial}
 %\includeonly{binomial}
 %\includeonly{parity}
+\usepackage[strings]{underscore}
 
 
 \begin{document}

developers/delete-trailing-ws

@@ -1,3 +1,3 @@
 #!/bin/sh
 
-find . \( -name '*.sml' -o -name '*.sig' \) \! -name '*Theory.sml' \! -name '*Theory.sig' -exec grep -q ' \+$' \{\} \; -print -exec perl -i -pe 's/ +$//;' \{\} +
+find . \( -name '*.sml' -o -name '*.sig' -o -name '*.tex' -o -name '*.ML' \) \! -name '*ML.sml' \! -name '*Theory.sml' \! -name '*Theory.sig' -exec grep -q ' \+$' \{\} \; -print -exec perl -i -pe 's/ +$//;' \{\} +

help/Docfiles/Conv.RESORT_EXISTS_CONV.doc

@@ -0,0 +1,38 @@
+\DOC
+
+\TYPE {RESORT_EXISTS_CONV : (term list -> term list) -> conv}
+
+\SYNOPSIS
+Reorders bound variables under existential quantifiers.
+
+\KEYWORDS
+
+\DESCRIBE
+
+A call to {RESORT_EXISTS_CONV f t} strips the outer
+existentially-quantified variables of {t}, giving a list {vs}, such that
+{t} is of the form {?vs. body}.  The list {vs} is then passed to the
+function argument {f}.  The result of the call {f vs} is expected to
+be a new list of variables {vs'}, and the result of the conversion is
+the theorem
+{
+   |- (?vs. body) <=> (?vs'. body)
+}
+The function {f} is generally expected to return a permutation of the
+variables appearing in the term {vs}, but may in fact introduce fresh
+variables that are fresh for {body}, and may also remove variables
+from {vs} that also don't appear in {body}.
+
+\FAILURE
+Given a term {t}, fails if {t} is not of boolean type.  Fails if when
+applied to the outermost existentially quantified variables (permitted
+to be the empty list) the function {f} returns a list of terms that
+are not all variables.  Also fails if either {f} returns a list that
+does not include variables from {vs} that appear in the body of {t},
+or if it includes variables that are in the body, but which were not
+originally bound.
+
+\SEEALSO
+Conv.RESORT_FORALL_CONV.
+
+\ENDDOC

help/Docfiles/Conv.RESORT_FORALL_CONV.doc

@@ -0,0 +1,38 @@
+\DOC
+
+\TYPE {RESORT_FORALL_CONV : (term list -> term list) -> conv}
+
+\SYNOPSIS
+Reorders bound variables under universal quantifiers.
+
+\KEYWORDS
+
+\DESCRIBE
+
+A call to {RESORT_FORALL_CONV f t} strips the outer
+universally-quantified variables of {t}, giving a list {vs}, such that
+{t} is of the form {!vs. body}.  The list {vs} is then passed to the
+function argument {f}.  The result of the call {f vs} is expected to
+be a new list of variables {vs'}, and the result of the conversion is
+the theorem
+{
+   |- (!vs. body) <=> (!vs'. body)
+}
+The function {f} is generally expected to return a permutation of the
+variables appearing in the term {vs}, but may in fact introduce fresh
+variables that are fresh for {body}, and may also remove variables
+from {vs} that also don't appear in {body}.
+
+\FAILURE
+Given a term {t}, fails if {t} is not of boolean type.  Fails if when
+applied to the outermost universally quantified variables (permitted
+to be the empty list) the function {f} returns a list of terms that
+are not all variables.  Also fails if either {f} returns a list that
+does not include variables from {vs} that appear in the body of {t},
+or if it includes variables that are in the body, but which were not
+originally bound.
+
+\SEEALSO
+Conv.RESORT_EXISTS_CONV.
+
+\ENDDOC