From f83d69f42a16095a9db09b3587a4c1df477ceb9e Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Fri, 7 Oct 2011 21:18:03 +1100 Subject: [PATCH 01/10] Make point in Tutorial that structures may need to be opened. In response to a comment from a user. --- Manual/Tutorial/logic.tex | 2 +- Manual/Tutorial/tutorial.tex | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/Manual/Tutorial/logic.tex b/Manual/Tutorial/logic.tex index 6fd0c20f1d..426aa82caf 100644 --- a/Manual/Tutorial/logic.tex +++ b/Manual/Tutorial/logic.tex @@ -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} diff --git a/Manual/Tutorial/tutorial.tex b/Manual/Tutorial/tutorial.tex index 5de40a8bab..caa88224fb 100644 --- a/Manual/Tutorial/tutorial.tex +++ b/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} From fca9a25794b71c72bd53e40c2817d99e554395ec Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Fri, 7 Oct 2011 21:18:24 +1100 Subject: [PATCH 02/10] Remove some trailing whitespace. --- Manual/Tutorial/logic.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Manual/Tutorial/logic.tex b/Manual/Tutorial/logic.tex index 426aa82caf..0ce54af4bd 100644 --- a/Manual/Tutorial/logic.tex +++ 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``; <> ! Uncaught exception: -! HOL_ERR +! HOL_ERR - val Th5 = ASSUME ``t1`` handle e => Raise e; <> Exception raised at Thm.ASSUME: not a proposition ! Uncaught exception: -! HOL_ERR +! HOL_ERR - val Th5 = ASSUME ``t1:bool``; > val Th5 = [.] |- t1 : thm From 30fca478651a9d7fa9f992729fde8d3b33d8326b Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Mon, 10 Oct 2011 10:37:21 +1100 Subject: [PATCH 03/10] Document GEN_ABS. Closes #3. --- help/Docfiles/Thm.GEN_ABS.doc | 59 +++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 help/Docfiles/Thm.GEN_ABS.doc diff --git a/help/Docfiles/Thm.GEN_ABS.doc b/help/Docfiles/Thm.GEN_ABS.doc new file mode 100644 index 0000000000..03084b0963 --- /dev/null +++ b/help/Docfiles/Thm.GEN_ABS.doc @@ -0,0 +1,59 @@ +\DOC + +\TYPE {GEN_ABS : term option -> term list -> thm -> thm} + +\SYNOPSIS +Rule of inference for building binder-equations. + +\KEYWORDS + +\DESCRIBE +The {GEN_ABS} function is, semantically at least, a derived rule that +combines applications of the primitive rules {ABS} and {MK_COMB}. +When the first argument, a term option, is the value {NONE}, the +effect is an iterated application of the rule {ABS} (as per {List.foldl}. Thus, +{ + G |- x = y + -------------------------------------------- GEN_ABS NONE [v1,v2,...,vn] + G |- (\v1 v2 .. vn. x) = (\v1 v2 .. vn. y) +} +If the first argument is {SOME b} for some term {b}, this term {b} is +to be a binder, usually of polymorphic type {:('a -> bool) -> bool}. +Then the effect is to interleave the effect of {ABS} and a call to +{AP_TERM}. For every variable {v} in the list, the following theorem +transformation will occur +{ + G |- x = y + ------------------------ ABS v + G |- (\v. x) = (\v. y) + ---------------------------- AP_TERM b' + G |- b (\v. x) = b (\v. x) +} +where {b'} is a version of {b} that has been instantiated to match the +type of the term to which it is applied ({AP_TERM} doesn't do this). + +\EXAMPLE +{ +- val th = REWRITE_CONV [] ``t /\ u /\ u`` +> val th = |- t /\ u /\ u = t /\ u : thm + +- GEN_ABS (SOME ``$!``) [``t:bool``, ``u:bool``] th; +> val it = |- (!t u. t /\ u /\ u) <=> (!t u. t /\ u) : thm +} + +\FAILURE +Fails if the theorem argument is not an equality. Fails if the second +argument (the list of terms) does not consist of variables. Fails if +any of the variables in the list appears in the hypotheses of the +theorem. Fails if the first argument is {SOME b} and the type of {b} +is either not of type {:('a -> bool) -> bool}, or some +{:(ty -> bool) -> bool} where all the variables have type {ty}. + +\COMMENTS +Though semantically a derived rule, a HOL kernel may implement this as +part of its core for reasons of efficiency. + +\SEEALSO +Thm.ABS, Thm.AP_TERM, Thm.MK_COMB. + +\ENDDOC From 9ee0a824a4e0f7480ce17fd33e162ab16d4c2ef9 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Tue, 11 Oct 2011 09:34:51 +1100 Subject: [PATCH 04/10] Remove trailing whitespace in src/num/termination/TotalDefn.sml --- src/num/termination/TotalDefn.sml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/num/termination/TotalDefn.sml b/src/num/termination/TotalDefn.sml index 2bc1d9bf09..a42ea254a0 100644 --- a/src/num/termination/TotalDefn.sml +++ b/src/num/termination/TotalDefn.sml @@ -113,18 +113,18 @@ fun mk_lex_reln argvars sizedlist arrangement = (* x.fld is a proper subterm of x. *) (*---------------------------------------------------------------------------*) -fun is_recd_proj tm1 tm2 = +fun is_recd_proj tm1 tm2 = let val (proj,a) = dest_comb tm1 val aty = type_of a - val projlist = mapfilter + val projlist = mapfilter (fst o dest_comb o boolSyntax.lhs o snd o strip_forall o concl) (TypeBase.accessors_of aty) in TypeBase.is_record_type aty andalso mem proj projlist end handle HOL_ERR _ => false; - + fun proper_subterm tm1 tm2 = - not(aconv tm1 tm2) + not(aconv tm1 tm2) andalso (Lib.can (find_term (aconv tm1)) tm2 orelse is_recd_proj tm1 tm2); From ec954cf792574872095edc7037822dd5a8fb459f Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Tue, 11 Oct 2011 14:23:37 +1100 Subject: [PATCH 05/10] Document RESORT_{FORALL,EXISTS}_CONV. Closes #5. --- help/Docfiles/Conv.RESORT_EXISTS_CONV.doc | 38 +++++++++++++++++++++++ help/Docfiles/Conv.RESORT_FORALL_CONV.doc | 38 +++++++++++++++++++++++ 2 files changed, 76 insertions(+) create mode 100644 help/Docfiles/Conv.RESORT_EXISTS_CONV.doc create mode 100644 help/Docfiles/Conv.RESORT_FORALL_CONV.doc diff --git a/help/Docfiles/Conv.RESORT_EXISTS_CONV.doc b/help/Docfiles/Conv.RESORT_EXISTS_CONV.doc new file mode 100644 index 0000000000..be7b24890c --- /dev/null +++ b/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 diff --git a/help/Docfiles/Conv.RESORT_FORALL_CONV.doc b/help/Docfiles/Conv.RESORT_FORALL_CONV.doc new file mode 100644 index 0000000000..e15ea6457c --- /dev/null +++ b/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 From d24a68ee55c80fec23e7a7e8eecb0df0ec29250d Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Tue, 11 Oct 2011 17:44:16 +0100 Subject: [PATCH 06/10] remove a bash-ism from HolQbfLib When /bin/sh is dash (e.g. on Ubuntu I think) HolQbfLib's system call to squolem2 won't work ("Syntax error: Bad fd number"). This should fix it. --- src/HolQbf/HolQbfLib.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/HolQbf/HolQbfLib.sml b/src/HolQbf/HolQbfLib.sml index f313b63138..98568ff823 100644 --- a/src/HolQbf/HolQbfLib.sml +++ b/src/HolQbf/HolQbfLib.sml @@ -9,7 +9,7 @@ structure HolQbfLib :> HolQbfLib = struct val path = FileSys.tmpName () val dict = QDimacs.write_qdimacs_file path t (* the actual system call to Squolem *) - val cmd = "squolem2 -c " ^ path ^ " >& /dev/null" + val cmd = "squolem2 -c " ^ path ^ " >/dev/null 2>&1" val _ = if !QbfTrace.trace > 1 then Feedback.HOL_MESG ("HolQbfLib: calling external command '" ^ cmd ^ "'") else () From f6a9ccd4f77172a2df3a1cec6425bc9ade3a01db Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Fri, 14 Oct 2011 11:04:12 +1100 Subject: [PATCH 07/10] Modify delete-trailing-ws tool to do its thing in .tex files too. --- developers/delete-trailing-ws | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/developers/delete-trailing-ws b/developers/delete-trailing-ws index 4b71abf307..33ec2fe6c0 100755 --- a/developers/delete-trailing-ws +++ b/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/ +$//;' \{\} + From a81fbe4f9269231fa1d68f0236a193de622b733c Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Fri, 14 Oct 2011 11:08:01 +1100 Subject: [PATCH 08/10] Remove trailing whitespace in a bunch of .tex files. --- Manual/Description/holCheck.tex | 10 +- Manual/Description/version2.tex | 246 +++++++++++++------------- Manual/Reference/theorems-intro.tex | 2 +- Manual/Tutorial/binomial.tex | 10 +- Manual/Tutorial/binomial/appendix.tex | 30 ++-- Manual/Tutorial/proof-tools.tex | 2 +- 6 files changed, 150 insertions(+), 150 deletions(-) diff --git a/Manual/Description/holCheck.tex b/Manual/Description/holCheck.tex index b5cdb9a648..e3cb2aa40f 100644 --- a/Manual/Description/holCheck.tex +++ b/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)`; diff --git a/Manual/Description/version2.tex b/Manual/Description/version2.tex index 76dca19c92..36cd2c5cee 100644 --- a/Manual/Description/version2.tex +++ b/Manual/Description/version2.tex @@ -71,16 +71,16 @@ \chapter{Version 2.0}\label{appendix} \con{Q} is a quantifier and if $x:\alpha$ then $p$ can be any term of type $\alpha\fun\bool$; this denotes the quantification of $x$ over those values -satisfying $p$. The qualifier {\small\verb%::%} can be used with +satisfying $p$. The qualifier {\small\verb%::%} can be used with {\small\verb%\%} and any binder, including user defined ones; the appropriate meanings are -predefined for {\small\verb%\%} and the built-in binders +predefined for {\small\verb%\%} and the built-in binders {\small\verb%!%}, {\small\verb%?%} and {\small\verb%@%}. This provides a method of simulating subtypes and dependent types; the qualifying predicate $p$ can be an arbitrary term containing parameters. For example: {\small\verb%!%}$w${\small\verb%::%}$\con{Word}(n)${\small\verb%. %}$t[w]$, for a suitable constant \con{Word}, simulates a quantification over the -`type' of $n$-bit words. Experiments are needed to establish how satisfactory +`type' of $n$-bit words. Experiments are needed to establish how satisfactory this approach is. The syntactic mechanism, although implemented initially to support restricted quantification, can also be used to support better approximations to notations like @@ -148,9 +148,9 @@ \section{Directory reorganization} \end{alltt}\end{hol} \noindent where $directory$ is the site-specific absolute pathname in which -the \HOL\ distribution directory (`\ml{hol}') resides. - -The \ML\ functions \ml{add\_to\_search\_path} and +the \HOL\ distribution directory (`\ml{hol}') resides. + +The \ML\ functions \ml{add\_to\_search\_path} and \ml{append\_to\_search\_path} are no longer built-in. Users may define them, if required, by: @@ -170,7 +170,7 @@ \section{Directory reorganization} \section{Location of libraries} -The function +The function \begin{holboxed}\index{library_pathname@\ml{library\_pathname}} \begin{verbatim} @@ -179,16 +179,16 @@ \section{Location of libraries} \noindent returns the internal pathname used by \HOL\ to load libraries. This pathname, which is site-specific and is given an initial -value when the system is built, should be the absolute pathname of the \HOL\ +value when the system is built, should be the absolute pathname of the \HOL\ system library directory. This pathname will typically have the form: \begin{hol}\begin{alltt} `\(directory\)/hol/Library` \end{alltt}\end{hol} -\noindent where $directory$ is the site-specific absolute pathname in which the \HOL\ -distribution directory (`\ml{hol}') resides. The value returned by -\ml{library\_pathname} can be changed by users only via the \ml{install} function. +\noindent where $directory$ is the site-specific absolute pathname in which the \HOL\ +distribution directory (`\ml{hol}') resides. The value returned by +\ml{library\_pathname} can be changed by users only via the \ml{install} function. The string returned by \ml{library\_pathname} is primarily used in library load-files to update the \HOL\ search path and help search @@ -198,12 +198,12 @@ \section{Location of libraries} search path as follows: \begin{hol}\begin{verbatim} - let path = library_pathname() ^ `/lib/help/` + let path = library_pathname() ^ `/lib/help/` in set_help_search_path (path . help_search_path()) \end{verbatim}\end{hol} -\noindent This will make the help files of the library \ml{lib} +\noindent This will make the help files of the library \ml{lib} available for online help whenever the library is loaded. @@ -255,10 +255,10 @@ \section{More flexible help system}\index{help@\ml{help}}\index{help system|(} help_search_path : void -> string list \end{verbatim}\end{holboxed} -\noindent have been added to the system for accessing the +\noindent have been added to the system for accessing the internal search path used by \HOL\ to find online help files. The help search path has precisely the same format as the regular search path, -and these two function are analogous to the \ML\ functions +and these two function are analogous to the \ML\ functions \ml{search\_path} and \ml{set\_search\_path}.\index{help system|)} @@ -270,7 +270,7 @@ \section{Syntax for restricted quantification} Syntactic support for restricted quantification and abstraction is now provided. This follows a suggestion discussed at the Second \HOL\ Users Meeting and implements a method of simulating subtypes and dependent -types with predicates. +types with predicates. Currently no derived rules are provided to support this notation, so any inferences will need to work on the underlying semantic @@ -289,12 +289,12 @@ \section{Syntax for restricted quantification} written between the binder and `\ml{.}` in the old notation. See the examples below. -The flag \ml{print\_restrict} has default \ml{true}, but if set to +The flag \ml{print\_restrict} has default \ml{true}, but if set to \ml{false} will disable the pretty printing. This is useful for seeing what the semantics of particular restricted abstractions are. -The constants \ml{RES\_ABSTRACT}, \ml{RES\_FORALL}, \ml{RES\_EXISTS} and +The constants \ml{RES\_ABSTRACT}, \ml{RES\_FORALL}, \ml{RES\_EXISTS} and \ml{RES\_SELECT} are defined in the theory \ml{bool} by: @@ -422,7 +422,7 @@ \section{Syntax for restricted quantification} #"DURING x::(m,n). p x";; no restriction constant associated with DURING -skipping: x " ;; parse failed +skipping: x " ;; parse failed #new_definition # (`RES_DURING`, "RES_DURING(m,n)p = !x. m<=x /\ x<=n ==> p x");; @@ -444,10 +444,10 @@ \section{Syntax for restricted quantification} \section{Syntax for sets}\index{set theory notation} -The special purpose set-theoretic notations +The special purpose set-theoretic notations {\small\verb%"{%}$t_1,t_2,\ldots,t_n${\small\verb%}"%} and {\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} are now available. -The normal interpretation of the former is the finite set containing +The normal interpretation of the former is the finite set containing $t_1,t_2,\ldots, t_n$ and the normal interpretation of the latter is the set of all $t$s such that $p$. These interpretations are predefined for the library \ml{sets}, but the user can use the syntax for other purposes if @@ -474,7 +474,7 @@ \section{Syntax for sets}\index{set theory notation} "\(c\sb{2}\) \(t\sb{1}\) (\(c\sb{2}\) \(t\sb{2}\) \(\cdots\) (\(c\sb{2}\) \(t\sb{n}\) \(c\sb{2}\)) \(\cdots\) ))" \end{alltt}\end{hol} -\noindent with failure if either $c_1$ or $c_2$ +\noindent with failure if either $c_1$ or $c_2$ is not the name of a constant. In the library \ml{sets}, the empty set is \ml{EMPTY} and @@ -558,7 +558,7 @@ \section{Syntax for sets}\index{set theory notation} \noindent will parse to: \begin{hol}\begin{verbatim} - "GSPEC(\(x,y,z). (x+(y+z), (x < y /\ y < z)))" + "GSPEC(\(x,y,z). (x+(y+z), (x < y /\ y < z)))" \end{verbatim}\end{hol} \noindent and @@ -574,22 +574,22 @@ \section{Syntax for sets}\index{set theory notation} \end{verbatim}\end{hol} -Note that the precedence of comma is increased in the contexts -``{\small\verb%{%}$\cdots${\small\verb%}%}'' and +Note that the precedence of comma is increased in the contexts +``{\small\verb%{%}$\cdots${\small\verb%}%}'' and ``{\small\verb%{%}$\cdots${\small\verb%|%}''. Terms will be printed in set notation if the flag \ml{print\_set} is \ml{true}. -Note that +Note that \medskip -\ml{"}$c${\small\verb%(\(%}$x_1$\ml{,}$\ldots$\ml{,}$x_n$\ml{).(}$t$\ml{,}$p$\ml{))"} +\ml{"}$c${\small\verb%(\(%}$x_1$\ml{,}$\ldots$\ml{,}$x_n$\ml{).(}$t$\ml{,}$p$\ml{))"} \medskip -\noindent will only print as -{\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} -if the variables $x_1$, $\ldots$ , +\noindent will only print as +{\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} +if the variables $x_1$, $\ldots$ , $x_n$ occur free in both $t$ and $p$ (and \ml{print\_set} is \ml{true}) . \section{Revised set theory libraries}\label{LIBRARY} @@ -621,10 +621,10 @@ \section{Revised set theory libraries}\label{LIBRARY} \begin{itemize} \item \ml{\{$x_1,\ldots,x_n$\}} denotes a finite set. -\item \ml{\{$x$|$P[x]$\}} denotes the set of all \ml{$x$} such that +\item \ml{\{$x$|$P[x]$\}} denotes the set of all \ml{$x$} such that \ml{$P[x]$}. -\item \ml{\{$t[x]$|$P[x]$\}} denotes the set of all \ml{$t[x]$} +\item \ml{\{$t[x]$|$P[x]$\}} denotes the set of all \ml{$t[x]$} such that \ml{$P[x]$}. \end{itemize} @@ -638,7 +638,7 @@ \section{Revised set theory libraries}\label{LIBRARY} \end{verbatim}\end{holboxed} \noindent which implements the axiom of specification for generalized set -specifications. +specifications. \ml{SET\_SPEC\_CONV} accepts two types of input. @@ -752,7 +752,7 @@ \section{Syntax blocks} #new_syntax_block(`<<`,`>>`, `foo`);; () : void - + #<< Mike >>;; Hello: Mike () : void @@ -768,8 +768,8 @@ \section{Syntax blocks} \end{verbatim}\end{holboxed} \noindent This changes the escape character in strings to be the character with the -supplied ascii code (initially this is {\small\verb%92%}, -viz. `{\small\verb%\%}`). +supplied ascii code (initially this is {\small\verb%92%}, +viz. `{\small\verb%\%}`). The old escape character is returned.\index{syntax blocks|)} \section{User-programmable quotation typechecker} @@ -782,28 +782,28 @@ \section{User-programmable quotation typechecker} it in the system. \index{preterms|(} -The \ML\ abstract type {\small\verb%preterm%} represents the parse trees of \HOL\ +The \ML\ abstract type {\small\verb%preterm%} represents the parse trees of \HOL\ terms. A typechecker is a function of type {\small\verb%preterm->term%}. If the flag \ml{preterm} is set to \ml{true} (the default is \ml{false}), then \HOL\ will use -whatever \ML\ function is currently bound to the name +whatever \ML\ function is currently bound to the name \ml{preterm\_handler} as the quotation typechecker. The way this works is that when \ml{preterm} is true the parser produces a preterm rather than a term, -and then wraps a call of \ml{preterm\_handler} -around the quotation.\index{type checking, in HOL logic@type checking, +and then wraps a call of \ml{preterm\_handler} +around the quotation.\index{type checking, in HOL logic@type checking, in \HOL\ logic!user programmed} Other uses of preterms are possible, for example -as patterns for describing terms. +as patterns for describing terms. The definition of the \ML\ type {\small\verb%preterm%} is: \begin{hol}\index{preterm@\ml{preterm}}\begin{alltt} - rectype preterm = - preterm_var of string \({\it Variables}\) - | preterm_const of string \({\it Constants}\) - | preterm_comb of preterm # preterm \({\it Combinations}\) - | preterm_abs of preterm # preterm \({\it Abstractions}\) - | preterm_typed of preterm # type \({\it Explicit typing}\) - | preterm_antiquot of term \({\it Antiquotation}\) + rectype preterm = + preterm_var of string \({\it Variables}\) + | preterm_const of string \({\it Constants}\) + | preterm_comb of preterm # preterm \({\it Combinations}\) + | preterm_abs of preterm # preterm \({\it Abstractions}\) + | preterm_typed of preterm # type \({\it Explicit typing}\) + | preterm_antiquot of term \({\it Antiquotation}\) \end{alltt}\end{hol} The function: @@ -826,7 +826,7 @@ \section{User-programmable quotation typechecker} #letref p_reg = preterm_var `x`;; p_reg = preterm_var `x` : preterm -#let preterm_handler p = p_reg:=p; +#let preterm_handler p = p_reg:=p; print_string `Typechecking ... `; print_newline(); preterm_to_term p;; @@ -882,7 +882,7 @@ \subsection{Generalized beta-reduction} \begin{hol} {\small\verb% "(\(%}$x_1, \ldots ,x_n${\small\verb%).%}$t${\small\verb%) (%}$t_1, \ldots ,t_n${\small\verb%)"%} \end{hol} - + \noindent \ml{PAIRED\_BETA\_CONV} proves that: \begin{hol} @@ -907,7 +907,7 @@ \subsection{Arithmetical conversions} \end{verbatim}\end{holboxed} \noindent does addition by formal proof. -If $n$ and $m$ are numerals then +If $n$ and $m$ are numerals then {\small\verb%ADD_CONV "%}$n\ $\ml{+}$\ m$\ml{"} returns the theorem {\small\verb%|- %}$n\ $\ml{+}$\ m\ $\ml{=}$\ s$, where $s$ is the numeral denoting the sum of $n$ and $m$. For example: @@ -927,14 +927,14 @@ \subsection{Arithmetical conversions} A new conversion has been added for deciding equality of natural number -constants. +constants. \begin{holboxed}\index{num_EQ_CONV@\ml{num\_EQ\_CONV}} \begin{verbatim} num_EQ_CONV : conv \end{verbatim}\end{holboxed} -\noindent If $n$ and $m$ are terms constructed from numeral constants +\noindent If $n$ and $m$ are terms constructed from numeral constants and the successor function \ml{SUC}, then: {\small\verb%num_EQ_CONV "%}$n$\ml{=}$m$\ml{"} returns: @@ -972,30 +972,30 @@ \subsection{List processing conversions} |- LENGTH [\(t\sb{1}\);\(\ldots\);\(t\sb{n}\)] = n \end{alltt}\end{hol} -The other conversion, \ml{list\_EQ\_CONV}, proves or disproves the -equality of two lists, given -a conversion for deciding the equality of elements. +The other conversion, \ml{list\_EQ\_CONV}, proves or disproves the +equality of two lists, given +a conversion for deciding the equality of elements. A call to: -\begin{hol}\begin{alltt} - list_EQ_CONV \(conv\) "[\(u\sb{1}\);\(\ldots\);\(u\sb{n}\)] = [\(v\sb{1}\);\(\ldots\);\(v\sb{m}\)]" +\begin{hol}\begin{alltt} + list_EQ_CONV \(conv\) "[\(u\sb{1}\);\(\ldots\);\(u\sb{n}\)] = [\(v\sb{1}\);\(\ldots\);\(v\sb{m}\)]" \end{alltt}\end{hol} -\noindent returns: {\small\verb%|- ([%}$u_1$\m{;}$\ldots$\ml{;}$u_n$\ml{]\ =\ [}$v_1$\ml{;}$\ldots$\ml{;}$v_m$\ml{])\ =\ F} if: +\noindent returns: {\small\verb%|- ([%}$u_1$\m{;}$\ldots$\ml{;}$u_n$\ml{]\ =\ [}$v_1$\ml{;}$\ldots$\ml{;}$v_m$\ml{])\ =\ F} if: \begin{myenumerate} \item \ml{~($n$=$m$)} or -\item \ml{$conv$} proves {\small\verb%|- (%}$u_i\ $\ml{=}$\ v_i$\ml{)\ =\ F} +\item \ml{$conv$} proves {\small\verb%|- (%}$u_i\ $\ml{=}$\ v_i$\ml{)\ =\ F} for any $1\leq i \leq m$. \end{myenumerate} - + \noindent {\small\verb%|- ([%}$u_1$\m{;}$\ldots$\ml{;}$u_n$\ml{]\ =\ [}$v_1$\ml{;}$\ldots$\ml{;}$v_m$\ml{])\ =\ T} is returned if: \begin{myenumerate} -\item \ml{($n$=$m$)} and \ml{$u_i$} is syntactically identical to +\item \ml{($n$=$m$)} and \ml{$u_i$} is syntactically identical to \ml{$v_i$} for $1\leq i \leq m$, or -\item \ml{($n$=$m$)} and \ml{$conv$} proves +\item \ml{($n$=$m$)} and \ml{$conv$} proves {\small\verb%|- (%}$u_i$\ml{=}$v_i$\ml{)=T} for $1\leq i \leq n$. \end{myenumerate} @@ -1020,7 +1020,7 @@ \subsection{Simplifying {\tt let}-terms} \begin{hol}\begin{alltt} |- let \(v\sb{1}\) = \(t\sb{1}\) and \(\cdots\) and \(v\sb{n}\) = \(t\sb{n}\) in \(t[v\sb{1},\ldots,v\sb{n}]\) = \(t[t\sb{1},\ldots,t\sb{n}]\) \end{alltt}\end{hol} - + \noindent The \ml{$v_i$}'s can take any one of the following forms: \begin{myenumerate} @@ -1052,7 +1052,7 @@ \subsection{Simplifying {\tt let}-terms} |- (let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))) = 6 #let_CONV "let f x y = x+y in f 1";; % NB: partial application % -|- (let f x y = x + y in f 1) = (\y. 1 + y) +|- (let f x y = x + y in f 1) = (\y. 1 + y) \end{verbatim}\end{session} \subsection{Skolemization}\index{Skolemization} @@ -1061,7 +1061,7 @@ \subsection{Skolemization}\index{Skolemization} Skolemization (using existentially quantified function variables rather than first-order Skolem constants). -The conversion +The conversion \begin{holboxed}\index{X_SKOLEM_CONV@\ml{X\_SKOLEM\_CONV}} \begin{verbatim} @@ -1075,8 +1075,8 @@ \subsection{Skolemization}\index{Skolemization} |- (!\(x\sb{1}\) \(\ldots\) \(x\sb{n}\). ?\(y\). \(t[x\sb{1},\ldots,x\sb{n},y]\) = (?\(f\). !\(x\sb{1}\) \(\ldots\) \(x\sb{n}\). \(t[x\sb{1},\ldots,x\sb{n},f x\sb{1}\ldots x\sb{n}]\) \end{alltt}\end{hol} -\noindent for any input term -\ml{!$x_1\ \ldots\ x_n$.\ ?$y$. $t[x_1,\ldots,x_n,y]$}. +\noindent for any input term +\ml{!$x_1\ \ldots\ x_n$.\ ?$y$. $t[x_1,\ldots,x_n,y]$}. Note that when $n=\ml{0}$, this is equivalent to alpha-conversion: @@ -1084,14 +1084,14 @@ \subsection{Skolemization}\index{Skolemization} |- (?\(y\). \(t[y]\)) = (?\(f\). \(t[f]\)) \end{alltt}\end{hol} -\noindent and that the conversion fails if there is already a free +\noindent and that the conversion fails if there is already a free variable \ml{$f$} of the appropriate type in the input term. For example: \begin{hol}\begin{alltt} X_SKOLEM_CONV "f:num->*" "!n:num. ?x:*. x = (f n)" \end{alltt}\end{hol} -\noindent will fail. The conversion \ml{SKOLEM\_CONV} is +\noindent will fail. The conversion \ml{SKOLEM\_CONV} is like \ml{X\_SKOLEM\_CONV}, except that it uses a primed variant of the name of the existentially quantified variable as the name of the skolem function it introduces. For example: @@ -1112,7 +1112,7 @@ \subsection{Quantifier movement conversions} \index{conversions!quantifier movement} A complete and systematically-named set of conversions for moving quantifiers -inwards and outwards through the logical connectives {\small\verb%~%}, +inwards and outwards through the logical connectives {\small\verb%~%}, {\small\verb%/\%}, {\small\verb%\/%}, and {\small\verb%==>%} has been added to the system. The naming scheme is based on the following atoms: @@ -1127,20 +1127,20 @@ \subsection{Quantifier movement conversions} The conversions for moving quantifiers inwards are called: -\begin{hol}\begin{alltt} +\begin{hol}\begin{alltt} <\(quant\)>_<\(conn\)>_CONV \end{alltt}\end{hol} -\noindent where the quantifier \ml{<$quant$>} is to be moved inwards +\noindent where the quantifier \ml{<$quant$>} is to be moved inwards through \ml{<$conn$>}. The conversions for moving quantifiers outwards are called: - -\begin{hol}\begin{alltt} + +\begin{hol}\begin{alltt} [\(dir\)]_<\(conn\)>_<\(quant\)>_CONV \end{alltt}\end{hol} - -\noindent where \ml{<$quant$>} is to be moved outwards + +\noindent where \ml{<$quant$>} is to be moved outwards through \ml{<$conn$>}, and the optional \ml{[$dir$]} identifies which operand (left or right) contains the quantifier. The complete set is: @@ -1167,14 +1167,14 @@ \subsection{Quantifier movement conversions} \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - FORALL_OR_CONV + FORALL_OR_CONV |- (!x.P \/ Q) = P \/ !x.Q [x not free in P] |- (!x.P \/ Q) = (!x.P) \/ Q [x not free in Q] |- (!x.P \/ Q) = (!x.P) \/ (!x.Q) [x not free in P or Q] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - OR_FORALL_CONV + OR_FORALL_CONV |- (!x.P) \/ (!x.Q) = (!x.P \/ Q) [x not free in P or Q] \end{verbatim}\end{hol} @@ -1184,14 +1184,14 @@ \subsection{Quantifier movement conversions} \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - EXISTS_AND_CONV + EXISTS_AND_CONV |- (?x.P /\ Q) = P /\ ?x.Q [x not free in P] |- (?x.P /\ Q) = (?x.P) /\ Q [x not free in Q] |- (?x.P /\ Q) = (?x.P) /\ (?x.Q) [x not free in P or Q] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - AND_EXISTS_CONV + AND_EXISTS_CONV |- (?x.P) /\ (?x.Q) = (?x.P /\ Q) [x not free in P or Q] \end{verbatim}\end{hol} @@ -1201,7 +1201,7 @@ \subsection{Quantifier movement conversions} \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - FORALL_IMP_CONV + FORALL_IMP_CONV |- (!x.P ==> Q) = P ==> !x.Q [x not free in P] |- (!x.P ==> Q) = (?x.P) ==> Q [x not free in Q] |- (!x.P ==> Q) = (?x.P) ==> (!x.Q) [x not free in P or Q] @@ -1213,7 +1213,7 @@ \subsection{Quantifier movement conversions} \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - EXISTS_IMP_CONV + EXISTS_IMP_CONV |- (?x.P ==> Q) = P ==> ?x.Q [x not free in P] |- (?x.P ==> Q) = (!x.P) ==> Q [x not free in Q] |- (?x.P ==> Q) = (!x.P) ==> (?x.Q) [x not free in P or Q] @@ -1243,7 +1243,7 @@ \subsection{New arithmetical theorems} \noindent have been deleted, and replaced by the constant specification: \begin{hol}\begin{verbatim} - DIVISION |- !n. 0 < n ==> + DIVISION |- !n. 0 < n ==> (!k. (k = ((k DIV n) * n) + (k MOD n)) /\ (k MOD n) < n) \end{verbatim}\end{hol} @@ -1266,13 +1266,13 @@ \subsection{New arithmetical theorems} ZERO_MOD |- !n. 0 < n ==> (0 MOD n = 0) MOD_MULT |- !n r. r < n ==> (!q. ((q * n) + r) MOD n = r) MOD_TIMES |- !n. 0 < n ==> (!q r. ((q * n) + r) MOD n = r MOD n) - MOD_PLUS |- !n. 0 < n ==> + MOD_PLUS |- !n. 0 < n ==> (!j k. ((j MOD n) + (k MOD n)) MOD n = (j + k) MOD n) MOD_MOD |- !n. 0 < n ==> (!k. (k MOD n) MOD n = k MOD n) \end{verbatim}\end{hol} - - - + + + The following miscellaneous arithmetical theorems are now pre-proved. @@ -1304,13 +1304,13 @@ \subsection{New arithmetical theorems} \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} SUB_LESS_EQ_ADD |- !m p. m <= p ==> (!n. (p - m) <= n = p <= (m + n)) - SUB_CANCEL |- !p n m. n <= p /\ m <= p ==> + SUB_CANCEL |- !p n m. n <= p /\ m <= p ==> ((p - n = p - m) = (n = m)) - CANCEL_SUB |- !p n m. p <= n /\ p <= m ==> + CANCEL_SUB |- !p n m. p <= n /\ p <= m ==> ((n - p = m - p) = (n = m)) NOT_EXP_0 |- !m n. ~((SUC n) EXP m = 0) ZERO_LESS_EXP |- !m n. 0 < ((SUC n) EXP m) - ODD_OR_EVEN |- !n. ?m. (n = (SUC(SUC 0)) * m) \/ + ODD_OR_EVEN |- !n. ?m. (n = (SUC(SUC 0)) * m) \/ (n = ((SUC(SUC 0)) * m) + 1) LESS_EXP_SUC_MONO |- !n m. ((SUC(SUC m)) EXP n)<((SUC(SUC m)) EXP (SUC n)) @@ -1325,7 +1325,7 @@ \subsection{New theorems about lists} \begin{hol}\begin{verbatim} LIST_NOT_EQ: |- !l1 l2. ~(l1 = l2) ==> (!h1 h2. ~(CONS h1 l1 = CONS h2 l2)) NOT_EQ_LIST: |- !h1 h2. ~(h1 = h2) ==> (!l1 l2. ~(CONS h1 l1 = CONS h2 l2)) - EQ_LIST |- !h1 h2. (h1 = h2) ==> + EQ_LIST |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==> (CONS h1 l1 = CONS h2 l2)) \end{verbatim}\end{hol} @@ -1341,7 +1341,7 @@ \subsection{New propositional theorems} OR_IMP_THM |- !t1 t2. (t1 = t2 \/ t1) = t2 ==> t1 NOT_IMP |- !t1 t2. ~(t1 ==> t2) = t1 /\ ~t2 COND_ID |- !b t. (b => t | t) = t - DISJ_ASSOC |- !t1 t2 t3. t1 \/ t2 \/ t3 = (t1 \/ t2) \/ t3 + DISJ_ASSOC |- !t1 t2 t3. t1 \/ t2 \/ t3 = (t1 \/ t2) \/ t3 \end{verbatim}\end{hol} @@ -1356,7 +1356,7 @@ \section{Additions and deletions}\label{adddel} hol/Versions/Versions.pre.1.12 \end{verbatim}\end{hol} -\noindent The file \ml{Version.$m$.$n$} (in the sources) documents \HOL\ +\noindent The file \ml{Version.$m$.$n$} (in the sources) documents \HOL\ Version \ml{$m$.$n$} and may contain details not in \DESCRIPTION\ or \REFERENCE. @@ -1369,7 +1369,7 @@ \subsection{Additions} \begin{hol}\begin{verbatim} get_const_type parity is_type mk_let dest_let is_let - bndvar body is_axiom + bndvar body is_axiom \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} mk_cons dest_cons is_cons @@ -1380,29 +1380,29 @@ \subsection{Additions} ancestors ancestry \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - prove_rep_fn_one_one prove_rep_fn_onto - prove_abs_fn_one_one prove_abs_fn_onto + prove_rep_fn_one_one prove_rep_fn_onto + prove_abs_fn_one_one prove_abs_fn_onto \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} define_finite_set_syntax define_set_abstraction_syntax associate_restriction \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - X_FUN_EQ_CONV COND_CONV PAIRED_BETA_CONV - BOOL_EQ_CONV ADD_CONV LENGTH_CONV - list_EQ_CONV num_EQ_CONV let_CONV + X_FUN_EQ_CONV COND_CONV PAIRED_BETA_CONV + BOOL_EQ_CONV ADD_CONV LENGTH_CONV + list_EQ_CONV num_EQ_CONV let_CONV EXISTS_LEAST_CONV X_SKOLEM_CONV SKOLEM_CONV - NOT_FORALL_CONV NOT_EXISTS_CONV + NOT_FORALL_CONV NOT_EXISTS_CONV EXISTS_NOT_CONV FORALL_NOT_CONV - FORALL_AND_CONV AND_FORALL_CONV + FORALL_AND_CONV AND_FORALL_CONV LEFT_AND_FORALL_CONV RIGHT_AND_FORALL_CONV - EXISTS_OR_CONV OR_EXISTS_CONV + EXISTS_OR_CONV OR_EXISTS_CONV LEFT_OR_EXISTS_CONV RIGHT_OR_EXISTS_CONV - FORALL_OR_CONV OR_FORALL_CONV + FORALL_OR_CONV OR_FORALL_CONV LEFT_OR_FORALL_CONV RIGHT_OR_FORALL_CONV - EXISTS_AND_CONV AND_EXISTS_CONV + EXISTS_AND_CONV AND_EXISTS_CONV LEFT_AND_EXISTS_CONV RIGHT_AND_EXISTS_CONV - FORALL_IMP_CONV EXISTS_IMP_CONV + FORALL_IMP_CONV EXISTS_IMP_CONV LEFT_IMP_FORALL_CONV RIGHT_IMP_FORALL_CONV LEFT_IMP_EXISTS_CONV RIGHT_IMP_EXISTS_CONV \end{verbatim}\end{hol} @@ -1414,9 +1414,9 @@ \subsection{Additions} set_help_search_path help_search_path \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - EQF_INTRO ISPEC ISPECL - EQF_ELIM EXISTENCE IMP_CONJ - EXIST_IMP + EQF_INTRO ISPEC ISPECL + EQF_ELIM EXISTENCE IMP_CONJ + EXIST_IMP \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} REPEAT_GTCL AP_THM_TAC @@ -1435,21 +1435,21 @@ \subsection{Deletions} pp_delete_theorem pp_theorems new_pp_theory close_pp_theory load_pp_theory extend_pp_theory new_pp_predicate - mk_quant mk_bool_comb space ascii_ize - dest_quant dest_bool_comb truth - mk_iff dest_iff is_iff + mk_quant mk_bool_comb space ascii_ize + dest_quant dest_bool_comb truth + mk_iff dest_iff is_iff \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - TOTALLY_AD_HOC_LEMMA + TOTALLY_AD_HOC_LEMMA \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - AND_CLAUSE1 AND_CLAUSE2 AND_CLAUSE3 + AND_CLAUSE1 AND_CLAUSE2 AND_CLAUSE3 AND_CLAUSE4 AND_CLAUSE5 - OR_CLAUSE1 OR_CLAUSE2 OR_CLAUSE3 + OR_CLAUSE1 OR_CLAUSE2 OR_CLAUSE3 OR_CLAUSE4 OR_CLAUSE5 - IMP_CLAUSE1 IMP_CLAUSE2 IMP_CLAUSE3 + IMP_CLAUSE1 IMP_CLAUSE2 IMP_CLAUSE3 IMP_CLAUSE4 IMP_CLAUSE5 - EQ_CLAUSE1 EQ_CLAUSE2 EQ_CLAUSE3 + EQ_CLAUSE1 EQ_CLAUSE2 EQ_CLAUSE3 EQ_CLAUSE4 COND_CLAUSE1 COND_CLAUSE2 \end{verbatim}\end{hol} @@ -1462,9 +1462,9 @@ \subsection{Deletions} paired_type_in_type paired_set_left paired_axiom paired_inst_type paired_set_right paired_inst_term paired_cons paired_variant paired_eq - paired_form_match paired_aconv_form paired_subst_form + paired_form_match paired_aconv_form paired_subst_form paired_subst_occs_form paired_term_freein_form paired_term_freein_form - paired_type_in_form paired_inst_form + paired_type_in_form paired_inst_form \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} new_curried_infix curried_infixes paired_infixes @@ -1497,7 +1497,7 @@ \subsection{Deletions} term_frees (equivalent to frees) term_vars (equivalent to vars) term_tyvars (equivalent to tyvars) - term_class + term_class \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} seg (now in library `eval`) @@ -1557,7 +1557,7 @@ \subsection{Deletions} HD_TL_SIMP list_gen_alpha ty_case variant_tyvar rotate_left rotate_right derive_existence_thm instantiate_existence_thm - mk_fn closeup + mk_fn closeup \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} CLOSE_UP save_open_thm @@ -1566,9 +1566,9 @@ \subsection{Deletions} loadx theories_dir_pathname \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} - IFF_DEF I FF_EQ_THM1 IFF_EQ_THM2 + IFF_DEF I FF_EQ_THM1 IFF_EQ_THM2 IFF_EQ IFF_EQ_RULE CONJ_IFF - IFF_CONJ IFF_THEN2 IFF_THEN + IFF_CONJ IFF_THEN2 IFF_THEN IFF_TAC EXISTS_REFL_TAC \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} diff --git a/Manual/Reference/theorems-intro.tex b/Manual/Reference/theorems-intro.tex index 2162ce9c1e..06cc10beec 100644 --- a/Manual/Reference/theorems-intro.tex +++ b/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 diff --git a/Manual/Tutorial/binomial.tex b/Manual/Tutorial/binomial.tex index bd516c1723..94cce9e746 100644 --- a/Manual/Tutorial/binomial.tex +++ b/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}} diff --git a/Manual/Tutorial/binomial/appendix.tex b/Manual/Tutorial/binomial/appendix.tex index 29ec35340e..07d228ec95 100644 --- a/Manual/Tutorial/binomial/appendix.tex +++ b/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) diff --git a/Manual/Tutorial/proof-tools.tex b/Manual/Tutorial/proof-tools.tex index 61445e687a..3577931f40 100644 --- a/Manual/Tutorial/proof-tools.tex +++ b/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). From 197e2081c310ea3a805d9a56023322d11857ab43 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Fri, 14 Oct 2011 11:08:26 +1100 Subject: [PATCH 09/10] Remove unused scripts (shell and sed) for Reference entry generation. This functionality is now provided by SML programs in help/src-sml. --- Manual/Reference/bin/doc-to-tex | 45 ----------------------------- Manual/Reference/bin/doc-to-tex.sed | 32 -------------------- 2 files changed, 77 deletions(-) delete mode 100644 Manual/Reference/bin/doc-to-tex delete mode 100644 Manual/Reference/bin/doc-to-tex.sed diff --git a/Manual/Reference/bin/doc-to-tex b/Manual/Reference/bin/doc-to-tex deleted file mode 100644 index 372662870b..0000000000 --- a/Manual/Reference/bin/doc-to-tex +++ /dev/null @@ -1,45 +0,0 @@ -#! /bin/sh -x -# -# Shell script to find, sort and translate all .doc files in a given -# directory into LaTeX sources. Executing: -# -# /bin/sh doc-to-tex -# -# Will translate all .doc files in the directory into LaTeX source, -# using the sed script whose pathname is . The results of the -# translation are appended onto the end of -# -# Modified 28.02.91 by JVT to take care of strange file names. -# Original code: -# -# for file in `cd $1; ls -1 *.doc | sed 's/.doc$//g' | sort -f` -# do -# sed -f doc-to-tex.sed $1/$file.doc >> $2 -# done -# -# The problem with this occurred when finding either *.doc or hidden -# files. -# 1) Hidden files (e.g. ..doc): -# These are not trapped by "ls -1 *.doc". The command was -# therefore changed to "ls -A1 | grep '\.doc". -# 2) *.doc: -# This caused a pattern match to all files when encountered -# inside "for file in `.......`". We therefore find all -# the files we're interested in, and put them in ".files". -# While doing this, we put single quotes around the names -# protect them from misinterpretation. In the "for" loop, -# we strip off these single quotes, and perform the "sed" -# that we're really interested in. These steps may seem -# to be over the top. But, they ensure that all the right -# files are found, and using their names has no adverse -# side effects. -# -# Modified 91.06.17 to take a pathname to the sed script as an argument. - -(cd $2;ls -A1 | grep '\.doc$' | sort -f -t . -k 2 | sed "s/.doc$/.doc'/g" | sed "s/^/'/g") > .files - -for file in `cat .files | sed "s/^'//g" | sed "s/.doc'/.doc/g"` - do - sed -f $1 $2/"$file" >> $3 - done -rm .files diff --git a/Manual/Reference/bin/doc-to-tex.sed b/Manual/Reference/bin/doc-to-tex.sed deleted file mode 100644 index 43a36d401a..0000000000 --- a/Manual/Reference/bin/doc-to-tex.sed +++ /dev/null @@ -1,32 +0,0 @@ -# doc-to-tex.sed: A sed script that transforms a .doc file into -# tex source code for a reference manual entry on -# Top 2 lines added to scrub Library and Keywords paragraphs [JRH 91.08.15] -# Lines for BLTYPE and ELTYPE added to deal with long types [RJB 91.09.24] -# Ugly hack to deal with 2n+1 adjacent braces added [JRH 91.10.02] -# put begin and end verbatim in separate lines [WW 93.07.20] -/^\\KEYWORDS/,/^ *$/d -/^\\LIBRARY/,/^ *$/d -/^\\STRUCTURE/,/^ *$/d -s/qr/qqr/g; s/~/pqr/g; -s/{{/~/g; s/\(~*\){/{\1/g; s/~/<<<<<>>>>>/g; -s/{/{\\small\\verb%/g; -s/}/%}/g; -s/^{\\small\\verb%[ ]*$/{\\par\\samepage\\setseps\\small\ -\\begin{verbatim}/g; -s/^%}[ ]*$/\\end{verbatim}\ -}/g; -/\\DOC.*/s/_/\\_/g; -/\\DOC.*/s/#/\\#/g; -/\\DOC.*/s/.DOC[ ]*/\\DOC{/g; -/\\DOC.*/s/$/}/g; -/\\TYPE.*/s/$/\\egroup/g; -/\\BLTYPE.*/s/\\BLTYPE[ ]*/{\\small\ -\\begin{verbatim}/g; -/\\ELTYPE.*/s/\\ELTYPE[ ]*/\\end{verbatim}\ -}\\egroup/g; -/\\THEOREM.*/s/_/\\_/g; -/\\THEOREM.*/s/\\none/{\\none}/g; -s/<<<<<>>>>>/}/g; From 173b0396884176f9ff2b2e462c4817fa7c1f18e8 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Mon, 17 Oct 2011 09:36:32 +1100 Subject: [PATCH 10/10] Remove some unused (and very old) simplification documentation. The documentation in the DESCRIPTION manual is more up-to-date. --- src/simp/doc/commands.tex | 288 ---------- src/simp/doc/misc/dproc.tex | 16 - src/simp/doc/misc/frags.tex | 167 ------ src/simp/doc/misc/junk.tex | 255 --------- src/simp/doc/simp.tex | 1035 ----------------------------------- 5 files changed, 1761 deletions(-) delete mode 100644 src/simp/doc/commands.tex delete mode 100644 src/simp/doc/misc/dproc.tex delete mode 100644 src/simp/doc/misc/frags.tex delete mode 100644 src/simp/doc/misc/junk.tex delete mode 100644 src/simp/doc/simp.tex diff --git a/src/simp/doc/commands.tex b/src/simp/doc/commands.tex deleted file mode 100644 index b98e4181c0..0000000000 --- a/src/simp/doc/commands.tex +++ /dev/null @@ -1,288 +0,0 @@ -% ===================================================================== -% -% Macros for typesetting the HOL system manual -% -% ===================================================================== - -% --------------------------------------------------------------------- -% Abbreviations for words and phrases -% --------------------------------------------------------------------- -\newcommand\VERSION{{\small\tt 2.0}} -\newcommand\TUTORIAL{{\footnotesize\sl TUTORIAL}} -\newcommand\DESCRIPTION{{\footnotesize\sl DESCRIPTION}} -\newcommand\REFERENCE{{\footnotesize\sl REFERENCE}} -\newcommand\LIBRARIES{{\footnotesize\sl LIBRARIES}} - -\def\HOL{{\small HOL}} -\def\HOLEIGHTY{{\small HOL}88} -\def\HOLNINETY{{\small HOL}90} -\def\HOLNINETYSIX{{\small HOL}96} -\def\HOLNINETYDIFF{\doublebox{\Large HOL90}} -\def\HOLEIGHTYDIFF{\doublebox{\Large HOL88}} -\def\TKHOL{\small TkHOL} -\def\LCF{{\small LCF}} -\def\LCFLSM{{\small LCF{\kern-.2em}{\normalsize\_}{\kern0.1em}LSM}} -\def\PPL{{\small PP}{\kern-.095em}$\lambda$} -\def\PPLAMBDA{{\small PPLAMBDA}} -\def\ML{{\small ML}} - -\newcommand\ie{\mbox{i{.}e{.}}} -\newcommand\eg{\mbox{e{.}g{.}}} -\newcommand\viz{\mbox{viz{.}}} -\newcommand\adhoc{\mbox{\it ad hoc}} -\newcommand\etal{{\it et al.\/}} -\newcommand\etc{\mbox{etc{.}}} -\def\see#1#2{{\em see\/} #1} - -% --------------------------------------------------------------------- -% Simple abbreviations and macros for mathematical typesetting -% --------------------------------------------------------------------- - -\newcommand\fun{{\to}} -\newcommand\prd{{\times}} - -\newcommand\conj{\ \wedge\ } -\newcommand\disj{\ \vee\ } -\newcommand\imp{ \Rightarrow } -\newcommand\eqv{\ \equiv\ } -\newcommand\cond{\rightarrow} -\newcommand\vbar{\mid} -\newcommand\turn{\ \vdash\ } -\newcommand\hilbert{\varepsilon} -\newcommand\eqdef{\ \equiv\ } - -\newcommand\natnums{\mbox{${\sf N}\!\!\!\!{\sf N}$}} -\newcommand\bools{\mbox{${\sf T}\!\!\!\!{\sf T}$}} - -\newcommand\p{$\prime$} -\newcommand\f{$\forall$\ } -\newcommand\e{$\exists$\ } - -\newcommand\orr{$\vee$\ } -\newcommand\negg{$\neg$\ } - -\newcommand\arrr{$\rightarrow$} -\newcommand\hex{$\sharp $} - -\newcommand{\uquant}[1]{\forall #1.\ } -\newcommand{\equant}[1]{\exists #1.\ } -\newcommand{\hquant}[1]{\hilbert #1.\ } -\newcommand{\iquant}[1]{\exists ! #1.\ } -\newcommand{\lquant}[1]{\lambda #1.\ } - -\newcommand{\leave}[1]{\\[#1]\noindent} -\newcommand\entails{\mbox{\rule{.3mm}{4mm}\rule[2mm]{.2in}{.3mm}}} - -% --------------------------------------------------------------------- -% Font-changing commands -% --------------------------------------------------------------------- - -\newcommand{\theory}[1]{\hbox{{\small\tt #1}}} - -\newcommand{\con}[1]{{\sf #1}} -\newcommand{\rul}[1]{{\tt #1}} -\newcommand{\ty}[1]{{\sl #1}} - -\newcommand{\ml}[1]{\mbox{{\def\_{\char'137}\small\tt #1}}} -\newcommand\ms{\tt} -\newcommand{\s}[1]{{\small #1}} - -\newcommand{\pin}[1]{{\bf #1}} -\def\m#1{\mbox{\normalsize$#1$}} - -% --------------------------------------------------------------------- -% Abbreviations for particular mathematical constants etc. -% --------------------------------------------------------------------- - -\newcommand\T{\con{T}} -\newcommand\F{\con{F}} -\newcommand\OneOne{\con{One\_One}} -\newcommand\OntoSubset{\con{Onto\_Subset}} -\newcommand\Onto{\con{Onto}} -\newcommand\TyDef{\con{Type\_Definition}} -\newcommand\Inv{\con{Inv}} -\newcommand\com{\con{o}} -\newcommand\Id{\con{I}} -\newcommand\MkPair{\con{Mk\_Pair}} -\newcommand\IsPair{\con{Is\_Pair}} -\newcommand\Fst{\con{Fst}} -\newcommand\Snd{\con{Snd}} -\newcommand\Suc{\con{Suc}} -\newcommand\Nil{\con{Nil}} -\newcommand\Cons{\con{Cons}} -\newcommand\Hd{\con{Hd}} -\newcommand\Tl{\con{Tl}} -\newcommand\Null{\con{Null}} -\newcommand\ListPrimRec{\con{List\_Prim\_Rec}} - - -\newcommand\SimpRec{\con{Simp\_Rec}} -\newcommand\SimpRecRel{\con{Simp\_Rec\_Rel}} -\newcommand\SimpRecFun{\con{Simp\_Rec\_Fun}} -\newcommand\PrimRec{\con{Prim\_Rec}} -\newcommand\PrimRecRel{\con{Prim\_Rec\_Rel}} -\newcommand\PrimRecFun{\con{Prim\_Rec\_Fun}} - -\newcommand\bool{\ty{bool}} -\newcommand\num{\ty{num}} -\newcommand\ind{\ty{ind}} -\newcommand\lst{\ty{list}} - -% --------------------------------------------------------------------- -% \minipagewidth = \textwidth minus 1.02 em -% --------------------------------------------------------------------- - -\newlength{\minipagewidth} -\setlength{\minipagewidth}{\textwidth} -\addtolength{\minipagewidth}{-1.02em} - -% --------------------------------------------------------------------- -% Environment for the items on the title page of a case study -% --------------------------------------------------------------------- - -\newenvironment{inset}[1]{\noindent{\large\bf #1}\begin{list}% -{}{\setlength{\leftmargin}{\parindent}% -\setlength{\topsep}{-.1in}}\item }{\end{list}\vskip .4in} - - -% --------------------------------------------------------------------- -% Environment for ``asides'' and ``warnings'' -% --------------------------------------------------------------------- - -\newenvironment{aside}% -{\begin{Sbox}\begin{minipage}}% -{\end{minipage}\end{Sbox}\shadowbox{\TheSbox}} - -\newenvironment{warning}% -{\vspace{4mm}\begin{minipage}{\Ovalbox{\Large !}}}% -{\end{minipage}\vspace{4mm}} - - -% --------------------------------------------------------------------- -% Macros for little HOL sessions displayed in boxes. -% -% Usage: (1) \setcounter{sessioncount}{1} resets the session counter -% -% (2) \begin{session}\begin{verbatim} -% . -% < lines from hol session > -% . -% \end{verbatim}\end{session} -% -% typesets the session in a numbered box. -% --------------------------------------------------------------------- - -\newlength{\hsbw} -\setlength{\hsbw}{\textwidth} -\addtolength{\hsbw}{-\arrayrulewidth} -\addtolength{\hsbw}{-\tabcolsep} -\newcommand\HOLSpacing{13pt} - -\newcounter{sessioncount} -\setcounter{sessioncount}{1} - -\newenvironment{session}{\begin{flushleft} - \begin{tabular}{@{}|c@{}|@{}}\hline - \begin{minipage}[b]{\hsbw} - \vspace*{-.5pt} - \begin{flushright} - \rule{0.01in}{.15in}\rule{0.3in}{0.01in}\hspace{-0.35in} - \raisebox{0.04in}{\makebox[0.3in][c]{\footnotesize\sl \thesessioncount}} - \end{flushright} - \vspace*{-.55in} - \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\ \hline - \end{tabular} - \end{flushleft} - \stepcounter{sessioncount}} - -% --------------------------------------------------------------------- -% Macro for boxed ML functions, etc. -% -% Usage: (1) \begin{boxed}\begin{verbatim} -% . -% < lines giving names and types of mk functions > -% . -% \end{verbatim}\end{boxed} -% -% typesets the given lines in a box. -% -% Conventions: lines are left-aligned under the "g" of begin, -% and used to highlight primary reference for the ml function(s) -% that appear in the box. -% --------------------------------------------------------------------- - -\newenvironment{boxed}{\begin{flushleft} - \begin{tabular}{@{}|c@{}|@{}}\hline - \begin{minipage}[b]{\hsbw} -% \vspace*{-.55in} - \vspace*{.06in} - \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\ \hline - \end{tabular} - \end{flushleft}} - -% --------------------------------------------------------------------- -% Macro for unboxed ML functions, etc. -% -% Usage: (1) \begin{hol}\begin{verbatim} -% . -% < lines giving names and types of mk functions > -% . -% \end{verbatim}\end{hol} -% -% typesets the given lines exactly like {boxed}, except there's -% no box. -% -% Conventions: lines are left-aligned under the "g" of begin, -% and used to display ML code in verbatim, left aligned. -% --------------------------------------------------------------------- - -\newenvironment{hol}{\begin{flushleft} - \begin{tabular}{c@{}@{}} - \begin{minipage}[b]{\hsbw} -% \vspace*{-.55in} - \vspace*{.06in} - \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\ - \end{tabular} - \end{flushleft}} - -% --------------------------------------------------------------------- -% Emphatic brackets -% --------------------------------------------------------------------- - -\newcommand\leb{\lbrack\!\lbrack} -\newcommand\reb{\rbrack\!\rbrack} - - -%These macros were included by jac1: they are used in two of the index entries - -\def\per{\ml{\%}} -\def\pes{\ml{\%<}} -\def\pee{\ml{>\%}} - - -%These macros were included by ap; they are used in Chapters 9 and 10 -%of the HOL DESCRIPTION - -\newcommand{\inds}%standard infinite set - {\mbox{\rm I}} - -\newcommand{\ch}%standard choice function - {\mbox{\rm ch}} - -\newcommand{\den}[1]%denotational brackets - {[\![#1]\!]} - -\newcommand{\two}%standard 2-element set - {\mbox{\rm 2}} - - - - - - - - - - - - diff --git a/src/simp/doc/misc/dproc.tex b/src/simp/doc/misc/dproc.tex deleted file mode 100644 index e9ab91ca56..0000000000 --- a/src/simp/doc/misc/dproc.tex +++ /dev/null @@ -1,16 +0,0 @@ -\chapter{Decision Procedures} - -\section{Linear Arithmetic} - -\section{Congruence Closure} - -\section{Combining Decision Procedures} - -\section{First Order Tableux Proof {\tt TAB\_TAC}} - -\section{Model Elimination {\tt MESON\_TAC}} - -\section{Satisfying Existentials} - -\label{solving-existentials} - diff --git a/src/simp/doc/misc/frags.tex b/src/simp/doc/misc/frags.tex deleted file mode 100644 index 8e000c511d..0000000000 --- a/src/simp/doc/misc/frags.tex +++ /dev/null @@ -1,167 +0,0 @@ - - -\section{Contextual Rewriting} - -Arbitrary extra contextual rewrites can be introduced by -using "congurence rules". These are theorems of a particular -shape. - -The general form must be: -\begin{verbatim} -|- !x1 x1' ... xn xn'. - (!v11...v1m. x1 v11 ... v1m = x1' v11 ... v1m) ==> - (!v21...v2m. [P[x1,v21,...v2m] ==>] x2 v21 ... v2m = x2' v21 ... v2m) ==> - ... - F[x1,x2,..,xn] = F[x1',x2',..,xn'] -\end{verbatim} -That probably doesn't make much sense. Think of F as the construct -over which you are expressing the congruence. Think of x1,x2,...xn -as the sub-constructs which are being rewritten, some of them under -additional assumptions. The implications (one on each line in the -sample above) state the necessary results which need to be derived -about the subcomponents before the congruence can be deduced. Some -of these subcomponenets may be rewritten with extra assumpions - this -is indicated by P[x1] above. - -Some subcomponents may also be functions - in this case we want -to rewrite them as applied to sets of variables v1...v1m etc. -See the rule for restricted quantifiers for examples. -The simplifier does a degree of higher order matching when -these variables are specified. - -Some examples: -\begin{verbatim} - |- !g g' t t' e e'. - (g = g') ==> - (g ==> (t = t')) ==> - (~g ==> (e = e')) ==> - ((g => t | e) = (g' => t' | e')) : thm - - |- !P P' Q Q'. - (!x. P x = P' x) ==> - (!x. P x ==> (Q x = Q' x)) ==> - (RES_EXISTS P Q = RES_EXISTS P' Q') : thm -\end{verbatim} - - - - -\section{Contextual Rewriting} - -Contextual rewriting lets you add assumptions to your rewrite -set as you descend into a term. - -The most obvious contextual rewrite is for terms of the form: -\begin{verbatim} - P ==> Q -\end{verbatim} -The simplifier can use any rewrites that come from P -when rewriting Q. - -Other contextual rewrites included are: -\begin{verbatim} - P => T1 | T2 (assume P when rewriting T1, ~P when rewriting T2) - !x::P. T1[x] (assume "P x" when rewriting T1[x]) - ?x::P. T1[x] (assume "P x" when rewriting T1[x]) - \x::P. T1[x] (assume "P x" when rewriting T1[x]) -\end{verbatim} - - -\section{Conditional Rewriting} - -Any theorem which can be converted to the form -\begin{verbatim} - |- P1[x1...xm] ==> ... Pm[x1...xm] ==> (T1[x1...xm] = T2 [x1...xm]) -\end{verbatim} -can potentially be used as a conditional rewrite. This is -like the existing conditional rewriting in HOL. However, the process -of producing conditional rewrites is automated by setting the "rewrite -maker" in your simpset. For example, res\_quan\_ss (the simpset -for the res\_quan library) extends the rewrite maker to be able to convert -theorems such as: -\begin{verbatim} -|- !n. !w ::(PWORDLEN n). NBWORD n (BNVAL w) = w : thm -\end{verbatim} -into conditional rewrites. The above theorem will become: -\begin{verbatim} -|- PWORDLEN n w ==> (NBWORD n (BNVAL w) = w) -\end{verbatim} -and will only be applied if "PWORDLEN n w" can be solved in the -context-of-application. Here "n" and "w" will be instantiated -to the correct arguments. - -\section{Adding Arbitrary Conversions} - -You can add conversions to the simpset which might (potentially) -get applied at every point in the term. - -Simpsets can contain arbitrary user conversions, as well as -rewrites and contextual-rewrites. Conversions are keyed by -term patterns (implemented using termnets). Thus a conversion -won't even be called if the target term doesn't match -(in the termnet sense of matching) it's key. This just acts -as a simple optimization/filter. - -For example, BETA\_CONV is keyed on the term -\begin{verbatim} -(--`(\x. t) y`--). -\end{verbatim} -\footnote{I'm not sure if the HOL implementation of term nets handles keys -which contain abstractions efficiently} - - -\section{AC Rewriting/Rewritng with Permutative Theorems} - -Normally, these rewrites such as: -\begin{verbatim} -ADD_SYM |- !x y. x + y = y + x -\end{verbatim} -cause {\tt REWRITE\_TAC} to loop. However, the simplifier only applies -them in certain situations, namely when the term they produce -is strictly less than the original term according to a built in -term ordering. \footnote{Note that the term ordering in hol90 -is broken, so a much less efficient term ordering is defined in -the simplifier. This should be fixed in the next release of hol90.} - -By putting three theorems in your simpset: associativity, commutativity and -left-commutativity, you get AC-normalization for free. You -have to be careful about this: -\begin{itemize} - \item The associative laws must always be oriented from left - to right, as in {\tt |- f(f(x,y),z)) = f(x,f(y,z))}. Otherwise - HOL will loop. - \item You need to add left-commutativity to get full normalization: - {\tt |- f(x,f(y,z)) = f(y,f(x,z))}. This follows easily - from associativity and commutativity. -\end{itemize} - -AC normalization with the simplifier is comparatively expensive. -Terms of 20 or more operations can take a long time to -normalize. Smaller terms are OK, but in general it may be a problem -to include AC normalization in all your simpsets. Experiment -and see! - -See the Isabelle reference manual chapter 10 for more details on -AC normalization. - -\subsection{Examples of AC Normalization} - -\begin{verbatim} -- SIMP_CONV ac_arithmetic_ss (--`(x + 3) + 4 + (y + 2)`--); -val it = |- (x + 3) + 4 + y + 2 = 2 + 3 + 4 + x + y : thm -\end{verbatim} - - -\chapter{Efficiency and Memory Usage} - -\section{Memory Usage} - -After loading hol\_ss, arith\_ss,reduce\_ss, taut\_ss, -res\_quan\_ss, and pred\_set\_ss: -\begin{verbatim} -[Major collection... 99% used (11674608/11678744), 2300 msec] -\end{verbatim} -Without these: -\begin{verbatim} -[Major collection... 99% used (10103312/10108132), 1950 msec] -\end{verbatim} diff --git a/src/simp/doc/misc/junk.tex b/src/simp/doc/misc/junk.tex deleted file mode 100644 index 7098eb2a44..0000000000 --- a/src/simp/doc/misc/junk.tex +++ /dev/null @@ -1,255 +0,0 @@ -\chapter*{Preface} - -The purpose of the chapters which follow is to document some of the -more advanced techniques that experienced users employ -when using the \HOL system. -Chapter~\ref{simplification} describes the \HOL\ simplifier, a -powerful new proof tool available with this release of \HOL. -%Chapter~\ref{abstract-theories} describes how abstract (or -%parameterized) theories -%can be developed in the \HOL\ system, for example theories -%for algebraic notions like groups and rings. -%Chapter~\ref{choice} describes utilities that are available for -%dealing with the troublesome Hilbert-choice operator, and also some techniques -%for avoiding its use altogether. -%Chapter~\ref{decision-procedures} describes some of the advanced -%decision procedures included with the \HOL\ system. -%Chapter~\ref{subtyping} describes the latest ideas on how -%subtyping and dependent types can be handled in the \HOL\ framework. -%Chapter~\ref{wisdom} is a distillation of some of the wisdom -%that has appeared on the \verb%info-hol% mailing list over the -%last 10 years. - - -Many of these topics are ongoing areas of research, and users are -invited to pursue better solutions than those -presented here. The \HOL\ system provides an -ideal environment for exploring solutions to these problems, -due to its high level of programmability and simple conceptual -framework. - -All of these tools are developed on top of the -core \HOL\ system, without changing the essential logical -basis being used. In different ways this demonstrates both -the power of the \HOL\ design philosophy --- a -simple core allows safe, easy extensibility via programming. -However, this can be also be seen as a weakness, as the advanced -facilities described here are needed in most applications, and -significant effort is needed to program them on top of the \HOL\ core. - - - -\chapter{Simplification} - -\label{simplification} -\label{simplifier} - -This chapter describes `simplification', which is a -powerful new proof technique available in the latest version -of \HOL. - -First a word of warning! As always, {\em the more you know about what -an automated tool can do for you, the more effective it will -be for you}. Users should ensure they have -a good understanding of what simplification is -before they make large sale use of it in their poofs. -This will help avoid the plethora of problems -that develop from the misapplication of automated tools. - -In particular, users new to theorem proving -systems should probably use simplification sparingly, -until they have a thorough understanding of the basics of how -a theorem proving system works. - -\section{What is simplification?} - - - -Some of the basic functions for creating and manipulating simpsets -are: -\begin{boxed} \begin{verbatim} - val addrewrs : simpset * thm list -> simpset - val addconvs : simpset * convdata list -> simpset - val addcongs : simpset * thm list -> simpset - val adddprocs : simpset * dproc list -> simpset -\end{verbatim} \end{boxed} -Some of inbuilt simpsets of the \HOL\ system are: -\begin{center} -\index{simpsets@!inbuilt} -\index{mk_vartype@\ml{mk\_vartype}} -\index{mk_type@\ml{mk\_type}} -\begin{tabular}{|l|l|} \hline -{\it Simpset} & {\it Purpose} \\ \hline - & \\ \hline -\ml{pure\_ss} & Used for building other simpsets \\ \hline -\ml{bool\_ss} & Simplifies ``basic'' constructs \\ \hline -\ml{pair\_ss} & Simplifies tupled expressions \\ \hline -\ml{list\_ss} & Simplifies list constructs \\ \hline -\ml{combin\_ss} & Simplifies combinator constructs \\ \hline -\ml{arith\_ss} & Simplification combined arithmetic decision procedures \\ \hline -\ml{hol\_ss} & Combines all inbuilt simplification strategies \\ \hline -\end{tabular} -\end{center} -Simpsets are usually constructed to perform a particular -task, e.g. to rewrite out all occurrences of a group of definitions, -or to apply a set of reductions which will always reduce a term -to a normal form. - -The above functions -are usually called using the \ml{|>} infix operator. For example: -\begin{session} \begin{verbatim} -- val BOOL_ss = - pure_ss |> addrewrs [FORALL_SIMP, EXISTS_SIMP, - IMP_CLAUSES, AND_CLAUSES, - COND_CLAUSES, OR_CLAUSES] - |> addcongs [imp_congrule, cond_congrule] -\end{verbatim} \end{session} - -The basic routines used to invoke simplification are: -\begin{boxed} \begin{verbatim} - val SIMP_CONV : simpset -> thm list -> conv - val SIMP_PROVE : simpset -> thm list -> term -> thm - val SIMP_RULE : simpset -> thm list -> thm -> thm - val SIMP_TAC : simpset -> thm list -> tactic - val ASM_SIMP_TAC : simpset -> thm list -> tactic - val FULL_SIMP_TAC : simpset -> thm list -> tactic -\end{verbatim} \end{boxed} - - - - - - -\subsection{Adding Decsion Procedures} - -\label{adding-dprocs} -During application, each decision procedure maintains -a private copy of the working context. -Each procedure is allowed to organise this data according to its needs. -For exampe, in the implementation of the simplification, the rewriter counts -as just one decision procedure, which happens to store its working -context as a term net. - -A decision procedure is added to a simpset using \ml{adddprocs} -and \ml{mk\_dproc}: -\begin{boxed} \begin{verbatim} - val adddprocs : simpset * dproc list -> simpset - val mk_dproc : { - name : string, - relation : term, - initial: context, - addcontext : context * Thm.thm list -> context, - apply: {solver:term -> thm, context: context} -> Abbrev.conv - } -> dproc -\end{verbatim} \end{boxed} -Do not be overwhelemed by the number of fields in \ml{mk\_dproc} --- only -\ml{initial}, \ml{addcontext}\ and \ml{apply}\ need much thought: -\begin{itemize} - \item \ml{name} field should be a unique name for the decision procedure - \item \ml{relation} should be the term \verb%(--`$=`--)% -(i.e equality), since we are always reducing under equality during -simplification. - \item \ml{initial} should return a value of type \ml{context}. This -is the value of the context storage for the decision procedure before -simplification starts. If the context is being stored as a list of -theorems, this should be \ml{THMLIST []}. - \item \ml{addcontext} is called every time a new fact becomes known -during simplification. Facts become known from three sources: - \begin{itemize} - \item Theorems passed as arguments to the simplification routines. - \item Theorems from the assumption list when using \ml{ASM\_SIMP\_TAC} -or \ml{FULL\_SIMP\_TAC}. - \item Facts derived because of contextual rewriting. - \end{itemize} - \ml{addcontext} is passed the previous working context and the new - facts. It is expected to return the next working context. - \item \ml{apply} is how the decision procedure is actually -invoked. The current working context is passed as an argument. -A {\em solver} is also provided which can be used to help solve -any side conditions that arise from applying the decision procedure. -\ml{apply} should return a theorem of the form \ml{|- $t_1$ = $t_2$}, -and it should also fail quickly for terms to which it does not apply. -\end{itemize}. - -Consider the example of \ml{ARITH}. This decision procedure can -make use of any contextual facts relating to Presburger arithmetic. -We shall store the context as a theorem list - hence we use the -constructor \ml{THMLIST} to produce values of type \ml{context}. -Assuming the the function \ml{is\_arith\_thm} determines if a -theorem expresses a fact about Presburger arithmetic, and the -function \ml{ARITH\_CCONV} accepts a list of theorems and a term, -calls the arithmetic decision procedure -and returns an equality theorem, then a simpset utilising the -decision procedure is created as follows: -\begin{session} \begin{verbatim} -val ARITH_DPROC = - let fun addcontext (THMLIST thms, newthms) = - let val thms' = flatten (map CONJUNCTS newthms - in THMLIST (filter is_arith_thm thms'@thms) - end - fun apply {context=THMLIST thms,solver} tm = ARITH_CCONV thms tm - in mk_reducer { - addcontext= addcontext, - apply=apply, - initial=THMLIST [], - name="ARITH", - relation = #const (const_decl "=") - } - end; - -val ARITH_ss = pure_ss |> adddprocs [ARITH_DPROC]; -\end{verbatim} \end{session} - -\shadowbox{The working context must be stored as a value of type \ml{context}. -This would seem to limit the ways in which the context can be organised, -however see the notes in the implementation for a method using -exceptions to allow the storage of arbitrary data.} - -\subsection{Programmable Hooks: Reduction Conversions and -Congruence Procedures} - - - -\subsection{Generalized Term Traversal} - -Simplification is implemented as specific instance of {\em -contextual term traversal}. Term traversal generalizes -simplification in that it is capable of reducing a term -under relations other than equality. - -Non-contextual term traversal -is essentially encompassed by the functions - -In many applications it is common to define equivalence or -preorder relations other than logical equality. For instance, for -a small embedded language we may define a relation -\verb%(--`$==: prog -> prog -> bool`--)% which tests -whether two expressions are observationally equivalent, -e.g. whether they have the same input/output characteristics. The -following theorems should then hold: -\begin{hol} \begin{verbatim} -|- (p == p) -|- (p1 == p2) /\ (p2 = p3) ==> (p1 == p3) -\end{verbatim} \end{hol} -which makes \ml{==} a preorder (it is, of course a congruence also). -These theorems, and appropriate congruence rules, are sufficient -to enable automated term traversal and reduction of a kind very similar -to that for simplification. The similarities are close enough that -they deserve to be implemented in the same mechanism. - -Some congruence rules for the above construct might be: -\begin{hol} \begin{verbatim} -|- (p == p') ==> (Succ p == Succ p') -|- (p == p') ==> (q == q') ==> (Appl p q == Appl p' q') -\end{verbatim} \end{hol} -Some theorems we might want to automatically apply are: -\begin{hol} \begin{verbatim} -|- (Skip ;; P) == P -|- (P ;; Skip) == P -\end{verbatim} \end{hol} -Other theorems may help normalize fully specified programs -to sequences of input/output actions, thus aiding automatic -proof of program equivalence. - - - diff --git a/src/simp/doc/simp.tex b/src/simp/doc/simp.tex deleted file mode 100644 index c31d09101b..0000000000 --- a/src/simp/doc/simp.tex +++ /dev/null @@ -1,1035 +0,0 @@ -\documentclass[a4]{article} -\bibliographystyle{plain} - -\title{A Simplifier/Programmable Grinder for hol98} -\author{Donald Syme\thanks{Myra VanInwegen provided additional -material. Konrad Slind updated this note for {\tt hol98}.}} - -% ask Don how to fix the code so that people don't have to say -% ``infix ++'' - -\include{commands} - -\begin{document} -\maketitle -% \tableofcontents - -This chapter describes `simplification', which is a powerful new proof -technique available in the latest version of \HOL. - -First a word of warning! As always, {\em the more you know about what an - automated tool can do for you, the more effective it will be for - you}. Users should ensure they have a good understanding of what - simplification is before they make large sale use of it in their - proofs. This will help avoid the plethora of problems that develop - from the misapplication of automated tools. - -In particular, users new to theorem proving systems should probably -use simplification sparingly, until they have a thorough understanding -of the basics of how a theorem proving system works. - -This simplifier is capable of doing a lot. However this also means it -is difficult to know exactly what it is doing, or why it stops -working. Because of this, extensive tracing is possible. - -This simplifier is based loosely on the Isabelle simplifier. The -original motivation for doing this work was that I was inspired by -reading the Isabelle reference manual (chapter 10) and wanted to see -how easy such a simplifier would be to implement in \HOL. - -\section{What is Simplification?} - -In its basic form, simplification is a more general kind of -rewriting. Like rewriting, simplification starts with some term, say -$t_1$, and repeatedly applies a collection of {\it reduction rules} to -the term and its subterms until no more reductions apply. This produces -the theorem \ml{|- $t_1$ = $t_2$}, which can be utilised in various -ways. - -Simplification is only concerned with the case where the reduction rules -prove that the term $t_1$ is {\it equal} to another term $t_2$. Thus -the domain of operation of simplification is most of what is encompassed -by {\it equational reasoning}. Simplification can be generalised to -reduction under preorders, but for the moment we need only be concerned -with the equality case. - -The simplification library is brought into an interactive session by -invoking -\begin{verbatim} - load "simpLib"; - open simpLib; -\end{verbatim} - -\section{Simpsets} - -The simplifier needs data to work with. This is specified in -{\em simpsets}. Simpsets are an extremely useful way to organise -your work and group theorems together. You should make it your -aim to develop good simpsets as part of your theories. -A simpset contains: -\begin{itemize} - \item A set of rewrite theorems, some of which may be conditional. - \item A set of congruence theorems which specify - contextual rewriting information. - \item A set of conversions which get applied to relevant terms. - \item A "rewrite maker" function. -\end{itemize} -Simpsets are created in two steps: -\begin{enumerate} - \item Fragments of simpsets (usually one per theory) are created -using the functions {\tt SIMPSET} or the shortcut {\tt rewrites}. - \item The fragments are composed (merged) using {\tt mk\_simpset} to -make a simpset, or added to an existing simpset using {\tt ++}. -\end{enumerate} -This two stage approach makes the implementation of the simplifier far -cleaner. However, it can be annoying to make large simpsets by -composing smaller fragments when you only want to add a few theorems. -Hence you can use the infix\footnote{At least it is intended that -\ml{++} be infix. Currently it isn't when you start up HOL, so you -must type \ml{infix ++} to make it so. This is a directive that perhaps -ought to be in your {\tt hol-init.sml} file.} operator \ml{++} to add -theorems to a simpset. This is useful when you are developing a -theory. - -For example, the following three methods are equivalent, except that the -first two create a reusable component {\tt SUMML\_ss}. The example is a -taken from the longer example at the end of this chapter. -\begin{verbatim} -val SUMML_ss = rewrites [SUMM_TAKE_LEFT,SUMM_1,SUMM_0]; -val summl_ss = mk_simpset [HOL_ss, SUMML_ss]; - -val SUMML_ss = rewrites [SUMM_TAKE_LEFT, SUMM_1,SUMM_0]; -val summl_ss = hol_ss ++ SUMML_ss; - -val summl_ss = hol_ss ++ rewrites [SUMM_TAKE_LEFT, SUMM_1,SUMM_0]; -\end{verbatim} -In general you should strive to build simpsets which solve/normalise a -particular class of terms rather than creating simpsets on-the-fly. - -\section{An example: List Equality} - -The following example shows how to add rewrites to an existing simpset -and apply the simpset to prove simple results. The simpset is made up -of a simple rewrite about lists, added to the basic reasoning -facilities in {\tt bool\_ss}. The final line indicates that these -rewrites are actually already present in the built-in simpset {\tt -hol\_ss}. {\tt hol\_ss} contains powerful arithmetic reasoning -simplification strategies and it is a workhorse simpset for many -verifications. -\begin{boxed} \begin{verbatim} -- load "simpLib"; (* load the simplification library *) - load "boolSimps"; (* contains bool_ss *) - load "listTheory"; (* the theory of lists *) - -- open simpLib listTheory; - infix ++; - -- CONS_11; -val it = |- !h h' t t'. (CONS h t = CONS h' t') = (h = h') - -- SIMP_CONV boolSimps.bool_ss [CONS_11] (Parse.Term`[x;y] = [1;2]`); -val it = |- ([x; y] = [1; 2]) = (x = 1) /\ (y = 2) : thm - -- load "HOLSimps"; (* A simpset for some common theories *) - open HOLSimps; - -- SIMP_PROVE hol_ss [] (Parse.Term`~([1;2;4] = [1;2;3])`); -val it = |- ~([1; 2; 4] = [1; 2; 3]) : thm -\end{verbatim} \end{boxed} -Here is the trace produced when tracing is turned on at a low level: -\begin{boxed} \begin{verbatim} -- Trace.trace_level := 1; - -- SIMP_PROVE hol_ss [] (Parse.Term`~([1;2;4] = [1;2;3])`); - rewriting [1; 2; 4] = [1; 2; 3] with - |- (CONS h t = CONS h' t') = (h = h') /\ (t = t') - rewriting 1 = 1 with |- (x = x) = T - rewriting [2; 4] = [2; 3] with - |- (CONS h t = CONS h' t') = (h = h') /\ (t = t') - rewriting 2 = 2 with |- (x = x) = T - rewriting [4] = [3] with - |- (CONS h t = CONS h' t') = (h = h') /\ (t = t') - 4 = 3 via cache hit! simplifies to: F - rewriting [] = [] with |- (x = x) = T - rewriting F /\ T with |- F /\ t = F - rewriting T /\ F with |- T /\ t = t - rewriting T /\ F with |- T /\ t = t - rewriting ~F with |- ~F = T -val it = |- ~([1; 2; 4] = [1; 2; 3]) : thm -\end{verbatim} \end{boxed} - - -\section{Built In Simpsets} - - -Some useful simpset fragments are included in the simplifier library. -These are based on existing HOL theories. They can automate a large -amount of ``trivial reasoning'' about HOL constructs that previously -needed special treatment. -\begin{boxed} -\begin{verbatim} - boolSimps.BOOL_ss : ssdata - boolSimps.CONG_ss : ssdata - boolSimps.NOT_ss : ssdata - pairSimps.PAIR_ss : ssdata - sumSimps.SUM_ss : ssdata - combinSimps.COMBIN_ss : ssdata - listSimps.list_ss : ssdata - ListSimps.LIST_ss : ssdata - arithSimps.ARITH_ss : ssdata - UnwindSimps.UNWIND_ss : ssdata - SatisfySimps.SATISFY_ss : ssdata -\end{verbatim} -\end{boxed} -\begin{description} -\item[{\tt BOOL\_ss}] The basic rewrites dealing with the boolean connectives - plus automatic beta conversion, and a couple of other trivial - theorems. - -\item[{\tt CONG\_ss}] Contains two very useful congruences, that - support contextual reasoning in the presence of implications and - conditional expressions. This ``simpset fragment'' combines with - {\tt BOOL\_ss} to make the {\tt bool\_ss} simpset. - -\item[{\tt NOT\_ss}] Rewrites for pushing negations inward, and for - simplifying disjunctions involving negations. - -\item[{\tt PAIR\_ss}] The useful rewrites from the core ``pair'' - theory. - -\item[{\tt SUM\_ss}] The useful rewrites from the ``sum'' theory, - including conditional rewrites for {\tt INR} and {\tt OUTR}. - -\item[{\tt COMBIN\_ss}] Standard theorems about K, S, I, o from the - ``combin'' theory. - -\item[{\tt list\_ss}] The most useful rewrites from the ``list'' - theory. Will reduce {\tt MAP}, {\tt APPEND}, {\tt EVERY} and so - on, where they are applied to concrete lists. - -\item[{\tt LIST\_ss}] The most useful rewrites from the ``List'' - library, as well as those from the ``list'' theory. - -\item[{\tt UNWIND\_ss}] Contains {\tt UNWIND\_FORALL\_CONV} and {\tt - UNWIND\_EXISTS\_CONV} for eliminating trivial universal and - existential quantifications. - -\item[{\tt SATISFY\_ss}] Does one-level (non-searching) prolog style - unification to help eliminate obvious existential quantifiers. This - is useful to help guess unknowns in side conditions. - -\item[{\tt ARITH\_ss}] This is the most powerful of the basic - simpset fragments. It has the following features: - \begin{itemize} - \item {\tt ARITH} is applied as a decision procedure - on all propositions that it may solve. - \item This application of {\tt ARITH} is ``context-aware'', in the - sense that any context from the assumption list (when using {\tt - ASM\_SIMP\_TAC}) or that has been collected via congruence rules - (e.g from the left-hand-side of an implication) which is - arithmetic is given to {\tt ARITH\_CONV} as well. - \item {\tt ARITH} is also used to collect linear like-terms together - within formulae. This is implemented via first symbolically - evaluating the formulae with an ML calculator, then using {\tt - ARITH\_CONV} to prove that the original formula equals this - result. - \item Calls to {\tt ARITH} are cached. - \end{itemize} - -\item[{\tt HOL\_ss}] This merges the fragments from {\tt BOOL\_ss}, - {\tt CONG\_ss}, {\tt NOT\_ss}, {\tt PAIR\_ss}, - {\tt SUM\_ss}, {\tt COMBIN\_ss}, {\tt SATISFY\_ss}, - {\tt UNWIND\_ss}, {\tt ARITH\_ss}, and {\tt LIST\_ss}. -\end{description} - -All of the above objects are {\em simpset fragments}, not simpsets. -Two actual simpsets are premade from these: -\begin{boxed} \begin{verbatim} - val HOLSimps.hol_ss : simpset - val boolSimps.bool_ss : simpset -\end{verbatim} \end{boxed} -{\tt hol\_ss} is made by combining all of the simpset fragments listed -above; indeed, it is directly constructed from {\tt HOL\_ss}. This is -what most users will initially use. - -%{\tt bool\_ss} contains {\tt BOOL\_ss} and {\tt CONG\_ss}. Using it is -%akin to using {\tt REWRITE\_TAC}, except that contextual rewriting using -%congruence rules for implications and conditional expressions is also -%performed. - -Notice that the above simpset fragments dwell in independent -structures. This allows the simplifier library to be used to work in a -theory without creating dependencies on extraneous theories. For -example, {\tt ARITH\_ss} can be used without making the theory of lists -an ancestor theory. This supports clean formalizations. - -\section{The Simplification Functions} - -The basic routines used to invoke simplification are: -\begin{boxed} \begin{verbatim} - val SIMP_CONV : simpset -> thm list -> conv - val SIMP_PROVE : simpset -> thm list -> term -> thm - val SIMP_RULE : simpset -> thm list -> thm -> thm - val SIMP_TAC : simpset -> thm list -> tactic - val ASM_SIMP_TAC : simpset -> thm list -> tactic - val FULL_SIMP_TAC : simpset -> thm list -> tactic -\end{verbatim} \end{boxed} - -In the examples below the theorems and definitions come from the -theories ``List'' and ``arithmetic'' except where noted. - -\ml{SIMP\_CONV} makes a simplification conversion from the given -simpset. The theorems in the second argument are used as additional -rewrites. The conversion uses a top-depth strategy for rewriting. It -sets both the solver and the depther to be \ml{SIMP\_CONV} itself. -\ml{SIMP\_CONV} never fails, though it may diverge. Beware of -divergence when trying to solve conditions to conditional rewrites. -Examples of its use are: -\begin{verbatim} -- SIMP_CONV hol_ss [] (--`TL[SUC 0;1 + 4; 2 * (3 + 2) + m]`--); -val it = |- TL [SUC 0; 1 + 4; 2 * (3 + 2) + m] = [5; m + 10] : thm - -- open arithmeticTheory; - SIMP_CONV hol_ss [LEFT_ADD_DISTRIB] (--`2 * (b + c) + a`--); -val it = |- 2 * (b + c) + a = a + 2 * b + 2 * c : thm -- SIMP_CONV hol_ss [] (--`(b + c + a) + d = (a + b) + (c + d)`--); -val it = |- ((b + c + a) + d = (a + b) + c + d) = T : thm -\end{verbatim} - -\ml{SIMP\_PROVE} invokes \ml{SIMP\_CONV} and then strips off the -\ml{= T} at the end of the theorem. For example: -\begin{verbatim} -- SIMP_PROVE hol_ss [] (--`(b + c + a) + d = (a + b) + (c + d)`--); -val it = |- (b + c + a) + d = (a + b) + c + d : thm -- SIMP_PROVE hol_ss [] (--`!m n p. (p + m = p + n) = (m = n)`--); -val it = |- !m n p. (p + m = p + n) = m = n : thm -\end{verbatim} - -\ml{SIMP\_RULE} invokes \ml{CONV\_RULE} with the conversion generated -by \ml{SIMP\_CONV} using the given simpset and additional rewrites. For -example: -\begin{verbatim} -- open ListTheory; - val th = SPEC (--`CONS (h:'a) t`--) LENGTH_BUTLAST; -val th = - |- ~(CONS h t = []) ==> - (LENGTH (BUTLAST (CONS h t)) = PRE (LENGTH (CONS h t))) : thm -- SIMP_RULE hol_ss [] th; -val it = |- LENGTH (BUTLAST (CONS h t)) = PRE (LENGTH t + 1) : thm -\end{verbatim} -Now, we would like to end up with \ml{LENGTH t} on the right hand side -instead of \ml{PRE (LENGTH t + 1)}. We could try the following: -\begin{verbatim} -- SIMP_RULE hol_ss [prim_recTheory.PRE] th; -val it = |- LENGTH (BUTLAST (CONS h t)) = PRE (LENGTH t + 1) : thm -\end{verbatim} -However, this doesn't work: the rules in \ml{hol\_ss} rewrite \ml{SUC n} to -\ml{n + 1}, and \ml{PRE} only works on \ml{SUC n}. One solution is to -create a simpset that doesn't include the arithmetic simplification: -\begin{verbatim} -val lss = mk_simpset [boolSimps.BOOL_ss, ListSimps.LIST_ss]; -= val lss = - : simpset -- SIMP_RULE lss [prim_recTheory.PRE] th; -val it = |- LENGTH (BUTLAST (CONS h t)) = LENGTH t : thm -\end{verbatim} - -\ml{SIMP\_TAC} makes a simplification tactic from the given simpset -and additional rewrite theorems. The tactic uses a top-depth strategy -for rewriting, and will be recursively reapplied when a simplification -step makes a change. Basically, it invokes \ml{CONV\_TAC} with the -conversion generated by \ml{SIMP\_CONV} using the given simpset and -additional rewrites. Here is an example of using \ml{SIMP\_TAC} (the -definitions are given below in Section \ref{extended-example}): -\begin{verbatim} -- set_goal ([], --`!f n. (SUMM f n n = f n)`--); -val it = - Status: 1 proof. - 1. Incomplete: - Initial goal: - ``!f n. SUMM f n n = f n`` - : proofs -- e (SIMP_TAC hol_ss [summ_DEF,SUMM_DEF]); -OK.. -1 subgoal: -val it = - ``!f n. summ (\k. f (k + n)) 1 = f n`` - : goalstack -\end{verbatim} - -\ml{ASM\_SIMP\_TAC} takes the terms in the assumption list, -\ml{ASSUME}s them, and adds them to the list of theorems used for -rewriting. The assumptions are also added to the context that will be -passed to conversions. - -\ml{FULL\_SIMP\_TAC} simplifies the assumptions one by one, before -simplifying the goal. The assumptions are simplified in the order -that they are found in the assumption list, and the simplification -of each assumption is used when simplifying the next assumption. - -\section{Rewrite Rules} - -\label{rewrite-rules} - -Rewrite rules are theorems which express an equality. They -are similar to the theorems -provided as input to the `plain' rewriter -\ml{REWRITE\_TAC}. Some examples are: -\begin{hol}\begin{verbatim} - |- !i j k. (i + j) + k = i + (j + k) - |- HD (CONS h t) = h - |- NULL [] = T - |- (!x. t) = t -\end{verbatim}\end{hol} -In each of the rules above, an infinite number of potential -reductions has been specified. For example the first rule -will act on any term which matches \ml{(--`($i$ + $j$) + $k$`--)}. - -Rewrite rules may also be {\em conditional}. For example: -\begin{hol}\begin{verbatim} -EL_CONS |- n > 0 ==> (EL n (CONS h t) = EL (n-1) t) -\end{verbatim}\end{hol} -This -rule applies to any term which matches \ml{(--`EL $n$ (CONS $h$ $t$)`--)}, -and will only be applied if the condition \ml{(--`$n$ > 0`--)} can be -solved for a particular $n$. Note that solving an arithmetic side condition -like this automatically will almost certainly -require a decision procedure to be present. - -A bit of care has to be taken when formulating conditional rewrites. -For example, say we want to use the fact that the function {\tt MAP2} -preserves the length of lists. One possible way to phrasing the -theorem is -\begin{hol} \begin{verbatim} -MY_LENGTH_MAP2 |- !f m l1 l2. (LENGTH l1 = m) /\ (LENGTH l2 = m) ==> - (LENGTH (MAP2 f l1 l2) = m) -\end{verbatim} \end{hol} - -However, this will not work as a congruence rule. In a proper rewrite -rule, the variables in the right hand side of the consequent must be -contained in the variables on the left hand side. It is not sufficient -that the values can be determined by the conditions. Thus the rule -must be reformulated, for example as: -\begin{hol} \begin{verbatim} -LENGTH_MAP2 |- !l1 l2. - (LENGTH l1 = LENGTH l2) ==> - (!f. (LENGTH (MAP2 f l1 l2) = LENGTH l1) /\ - (LENGTH (MAP2 f l1 l2) = LENGTH l2)) -\end{verbatim} \end{hol} - - -\subsection{How rewrite rules are made} - -Strictly speaking, each reduction rule in a simpset must specify an -equality. However, any theorem which is not already an -equality can be turned into a rewrite rule by simply -converting \ml{|- $t$} to \ml{|- $t$ = T}. -In fact, the process is a little more complex than this. -All theorems are processed by a {\em rewrite maker} -before being added to a simpset. The rewrite maker is -an attribute of the simpset. The default rewrite maker -performs the following transformations repeatedly: -\begin{itemize} - \item A conjunction in the final conclusion lead to - two reduction rules. Thus -\begin{hol} \begin{verbatim} - |- ... ==> x /\ y becomes - |- ... ==> x and - |- ... ==> y. -\end{verbatim} \end{hol} - - \item Negations \ml{~$t$} in the final conclusion become \ml{$t$ = F}: - \begin{hol} \begin{verbatim} - |- ... ==> ~t becomes - |- ... ==> (t = F). -\end{verbatim} \end{hol} - - \item Universal quantifiers get stripped off the - conclusion: - \begin{hol} \begin{verbatim} - |- ... ==> !x. t becomes - |- ... ==> t. -\end{verbatim} \end{hol} - - \item Ignoring conditions, a rewrite rule whose conclusion - is not an equality, universal quantification, - negation or conjunction becomes one rewrite rule: - \begin{hol} \begin{verbatim} - |- ... ==> x becomes - |- ... ==> (x = T). -\end{verbatim} \end{hol} - - \item All side conditions are transformed into a single condition, - where variables free in the condition but not in the equality - become existentially quantified. Thus - \begin{hol} \begin{verbatim} - |- IS_TYPE t ==> PROG x t ==> IS_PROG x becomes - |- (?t. IS_TYPE t /\ PROG x t) ==> (IS_PROG x = T) -\end{verbatim} \end{hol} -\end{itemize} - -Note that in general, some decision procedure or external routine must -be contained in the simpset in order to automatically choose an -appropriate value for these existential variables. Two routines are -provided in {\tt HOL\_ss} to handle this --- \ml{SATISFY} and -\ml{UNWIND\_EXISTS\_CONV}. - -\subsection{How rewrite rules are applied} - -Simplification works by: -\begin{itemize} - \item Descending the target term in a top-down -fashion. - \item At each subterm, the simplifier attempts to match -the current subterm with one of the rewrite -rules from the simpset. This is done -efficiently by using term nets to eliminate most -non-matches. - \item When a match is found, the simplifier attempts -to solve the conditions to the rewrite rule. It does this -by trying to simplify the conditions to the term \verb%"T"%. - \item If the conditions are solved, then the rewrite rule is applied and -the process continues on the new term. -\end{itemize} - -This is a somewhat simplified view of things - the exact term traversal -performed is dictated by the congruence rules being used - this is -explained further in Section~\ref{congruence-rules}. - - -\subsection{Matching and Higher Order Matching} - -For a rewrite rule \ml{|- $c_1$ ==> \ldots ==> $t_1$ = $t_2$}, -the simplifier will try to match subterms against $t_1$. The -matching performed is a limited version of {\it higher order -matching}. For many rewrite rules this will have no effect. However, -wherever function valued variables are free in $t_1$, then higher -order matching may come into play. - -Higher order matching allows a pattern such as -\ml{(--`!x. P x`--)} to match a term like \ml{(--`(!x. x = 3)`--)}. In -this example the variable $P$ will be instantiated to -\verb%(--`\x. x = 3`--)%. -Higher order matching allows rewrite rules to be far more expressive. -For example, beta reduction can be expressed as a rewrite rule: -\begin{hol} \begin{verbatim} - |- (\x. P x) y = P y -\end{verbatim} \end{hol} -Some other common higher order rewrite rules are: -\begin{hol} \begin{verbatim} - |- ~(!x. P x) = (?x. ~P x) - |- (!x. P x /\ Q) = (!x. P x) /\ Q - |- (!x. P x /\ Q x) = (!x. P x) /\ (!x. Q x) -\end{verbatim} \end{hol} -All of the quantifier movement conversions from Section~{quantifier-movement}\ -can be implemented using higher order rewrite rules. - -The limited higher order matching used in the simplifier -only allows function variables in the match to be parameterised -by variables which are quantified in the pattern. Thus \ml{(--`P x`--)} -will not match \ml{(--`x = 3`--)}, whereas \ml{(--`?x. P x`--)} will. -This ensures unique unifiers as the unifiers can be made maximal -over these variables. This -avoids many of the difficulties that arise with full higher order -matching. Note, however, that the simplifier -is sufficiently programmable to allow -other kinds of matching to be used instead of higher order matching. - -The higher order matching routines used by the simplifier are also available -for general use by other derived procedures. The relevant functions -are in the structure {\tt Ho\_match}. - - -\section{Contextual Rewriting} - -The discussion so far has assumed that the simplifier reduces -a term by traversing its subterms in a simple top-depth fashion. This -is how `plain rewriting' works in the \HOL\ system. In -this simple case, reductions -made to subterms are justified by the {\it congruence rules}: -$$\Gamma_1\turn l_1=l_2\qquad\qquad\qquad\Gamma_2\turn r_1=r_2\over -\Gamma\turn l_1\ r_1 = l_2\_r_2$$ -$$\Gamma_1\turn t_1=t_2\over -\Gamma\turn (\lquant{x}t_1) = (\lquant{x}t_2)$$ -which are in turn implemented by the conversional \ml{SUB\_CONV}. - -This process is straight forward to implement, but fails to do justice to the -fact that, when reducing certain subterms, it is desirable -to make use of additional facts which hold -locally. These `context theorems' can be used -in the rewrite process, or can be provided as extra input to -local calls to decision procedures. - -To take a simple yet important example, consider -the case when reducing the term $t_2$ within \ml{(--`$t_1$ ==> $t_2$`--)}. -It is reasonable to expect that an automatic tool can make use of any rewrite -rules that can be derived from $t_1$ when simplifying $t_2$. -In other words, $t_1$ is added to the ``current working context'' when -within $t_2$. \footnote{The notion of context turns out to be an important one -in theorem proving work, and provides one of the -motivations for the Window Inference proof style (see the -\HOL\ window inference library for more details on this). -Simplification can be seen as the fully automated, and thus -less controlled, version of window inference, restricted to the equality -relation.} - -As an example, consider the goal -\begin{verbatim} - (--`P x /\ ~(x = y) ==> ~([1;x;5] = [1;y;5])`--) -\end{verbatim} -goal is obviously true, but may require several tactics to solve -in the primitive \HOL\ system. - -The key observation is that when reducing the term on the right of the -implication, the ``theorems'' \ml{|- P x} and \ml{|- ~(x = y)} can -be assumed. During simplification, they are added as -rewrites to the current simpset. They are also added to the -working context of any co--operating decision procedures, but that -will be described in more detail later. - -To see this in practice, try: -\begin{boxed} \begin{verbatim} -- SIMP_PROVE hol_ss [CONS_11] - (--`P x /\ ~(x = y) ==> ~([1;x;5] = [1;y;5])`--); -val it = |- ~[1;x;5] = [1;y;5] : thm -\end{verbatim} \end{boxed} - - -\section{Ordered Rewriting} - -\label{ordered-rewriting} - -It is well known that some rewrite rules cause `plain rewriting' -(i.e. \ml {REWRITE\_TAC}) to loop, for instance: -\begin{hol} \begin{verbatim} -ADD_SYM |- x + y = y + x -INSERT_SYM |- x INSERT (y INSERT s) = y INSERT (x INSERT s) -\end{verbatim} \end{hol} -Both of these are {\em permutative rewrites}, in the sense that -the right hand side is a permutation of the pattern on the left. - -For such rewrites, the simplifier uses the common and -simple solution of only applying these rewrites when the term -to which they are being applied is strictly reduced according to a term -ordering. - -Ordered rewriting will also work for operations whose -commutative theorems have side conditions, as for partial functions: -\begin{hol} \begin{verbatim} -PUPDATE_SYM |- ~(x1 = x2) ==> - (PUPDATE (x1,y1) (PUPDATE (x2,y2) f) = - PUPDATE (x2,y2) (PUPDATE (x1,y1) f)) -\end{verbatim} \end{hol} - -\subsection{AC Rewriting} - -The \HOL\ simplifier supports AC (associative/commutative) rewriting, -in the style of the Isabelle simplifier. This will create a -normaliser for repeated applications of an associative/commutative -operator like \ml{+}.\footnote{Note that \HOL\ also includes AC\_CONV -for performing similar operations.} - -To enable AC ordered rewriting, the associativity and commutativity theorems -for the operation must be inserted in a simpset by making a \ml{ssdata} -object and merging it with an existing simpset. For example, to enable -AC rewriting over \ml{+}: -\begin{hol} \begin{verbatim} -ADD_ASSOC |- x + (y + z) = (x + y) + z -ADD_SYM |- x + y = y + x -\end{verbatim} \end{hol} -must be inserted in to a simpset:\footnote{Note that -the theorem \ml{ADD\_SYM} is misnamed in \HOL. It refers -to the commutativity of addition, and so should be called -\ml{ADD\_COMM}. -Symmetry is a notion that should only be used for relations such as -{\tt =}.} -\begin{boxed} \begin{verbatim} -- val ac_ss = bool_ss ++ SIMPSET {ac =[(ADD_ASSOC,ADD_SYM)], - convs=[],dprocs=[],filter=NONE,rewrs=[], - congs=[]}; - -- SIMP_CONV ac_ss ``(y + x) + 3 + 6 + (2 * x + 1)``; -val it = |- (y + x) + 3 + 6 + (2 * x + 1) = - 1 + 3 + 6 + y + x + 2 * x : thm - -- SIMP_CONV ac_ss ``x + 3 + y + 2 * x + 6 + 1``; -val it = |- x + 3 + y + 2 * x + 6 + 1 = - 1 + 3 + 6 + y + x + 2 * x : thm - -- SIMP_PROVE ac_ss ``(y + x) + 3 + 6 + (2 * x + 1) = - x + 3 + y + 2 * x + 6 + 1``; -val it = |- (y + x) + 3 + 6 + (2 * x + 1) = - x + 3 + y + 2 * x + 6 + 1 : thm -\end{verbatim} \end{boxed} - - -This is implemented using ordered rewriting, with a term ordering that -is AC compatible. Three rewrite rules are needed to implement AC -rewriting: -\begin{hol} \begin{verbatim} -ADD_SYM |- x + y = y + x -GSYM ADD_ASSOC |- (x + y) + z = x + (y + z) -ADD_LCOMM |- x + (y + z) = y + (x + z) -\end{verbatim} \end{hol} -The simplifier derives the third of these from the first two. -Also, note that the standard form for \HOL\ associativity theorems is the -wrong way round for the purposes of normalising AC nestings to -the right --- the simplifier reverses this automatically. - - -\section{Tracing} - -Simplification often involves many, many inferences, and complex -paths of deduction may occur, leading to almost magical results. -There is a down side to this - simplification is difficult -to understand, and even more difficult to debug when things -go wrong. - -The value provided to control tracing is: -\begin{boxed} \begin{verbatim} - val Trace.trace_level : int ref -\end{verbatim} \end{boxed} -The trace levels currently range from 0 to 5, where level -0 is no tracing and level 5 presents enormous quantities of information. -The aim has been to make trace level 1 produce sufficient information -to debug most problems. Trace levels 3 to 5 should only be needed -when debugging the simplifier itself. - - - -\section{Decision Procedures and Simplification} - -It is exceptionally useful to allow the integration {\it decision -procedures} with the simplification process, particularly arithmetic -decision procedures. - -In the context of this discussion, a decision procedure is a function -which performs complex computation before producing a reduction for a -term. The example we shall use is \ml{ARITH}, which determines the -truth of linear arithmetic formulae over the natural numbers. It is -easy to imagine decision procedures for other domains such as the -integer and real numbers. - -Decision procedures are integrated into the simplification process by -adding them to simpsets. They get invoked at low priority, in the sense -that all reductions via rewrite rules are performed before trying the -procedure on a term. All decision procedures are invoked for every -reducible subterm. - -See the examples in the source code for how to add a decision procedure -to a simpset. - -\section{Congruence Rules} - -\label{congruence-rules} - -We now fill in the details of the general process we have outlined -above. During simplification, facts get added to the current working -context because of the application of {\em congruence rules}. The user -is encouraged to learn to recognise when a certain construct allows -additional crucial assumptions to be made when simplifying subterms, and -to learn how to express this fact by a congruence rule. - -Congruence rules are contained within simpsets. User congruence rules -are usually theorems, although congruence rules may also be ML functions -(these are potentially useful for infinite families of congruence rules, -and are used for highly speed critical congruence rules such as those -for equality). - - -\subsection{Constructing Congruence Rules} - -Some sample congruence rules are: -\begin{hol} \begin{verbatim} -COND_CONG |- (g = g') ==> - (g' ==> (t = t')) ==> - (~g' ==> (e = e')) ==> - ((g => t | e) = (g' => t' | e')) - -RES_FORALL_CONG |- (R = R') ==> - (!x. R' x ==> (P x = P' x)) ==> - ((!x::R. P x) = (!x::R'. P' x)) -\end{verbatim} \end{hol} -These theorems are not hard to prove. -The principal difficulty is in {\it formulating} the rules -in the first place. The simplifier only accepts -congruence rules formulated in a certain way. -We shall examine the process of formulating -the first congruence rule in some detail. - -The purpose of a congruence rule is to state how a certain construct is -simplified by simplifying its subterms. The place to begin is with a -`template' of the construct to be simplified. In this case we are -interested in simplifying conditionals, thus the template is \ml{(--`$g$ -=> $t$ | $e$`--)}. - -Next, the final conclusion of the congruence rule -must state that the free subterms $g$, $t$ and $e$ get simplified, and -that the term produced is equal to the term we started with. -Thus the final conclusion is -\begin{hol} \begin{verbatim} -COND_CONG |- ... ==> - ((g => t | e) = (g' => t' | e')) - -\end{verbatim} \end{hol} -Next, the antecedents to this final conclusion specify how these -variables are related. They are -interpreted as instructions by the simplifier about the order -in which the subterms should be simplified, and what context assumptions may be -made for each subterm. -The first antecedent is simple enough: $g = g'$. The simplifier -interprets this as ``first starting with $g$, simplify it and get a new -$g'$''. The second is more complex: \ml{$g'$ ==> ($t$ = $t'$)}. -This is interpreted as ``simplify $t$ to some $t'$, adding the -fact $g'$ to the current context''. In other words, the antecedent -says that it is valid to assume $g'$ when simplifying $t$. -The third antecedent is similar: \ml{~$g$ ==> ($e$ = $e'$)}. This -allows the introduction of the context assumption \ml{~$g$}. - -After all three antecedents have been processed and discharged by the -simplifier, a theorem {\tt |- ($g$ => $t$ | $e$) = ($g'$ => $t'$ | $e'$} -will have been produced, where the values for $g'$, $t'$ and $e'$ have -been discovered by contextual simplification. This theorem is then used -by the simplifier to help reduce the entire term. - -Putting all this together gives the general congruence rule: -\begin{hol} \begin{verbatim} -COND_CONG |- (g = g') ==> - (g' ==> (t = t')) ==> - (~g' ==> (e = e')) ==> - ((g => t | e) = (g' => t' | e')) -\end{verbatim} \end{hol} - -\subsection{Bad congruence rules} - -Ill-formed congruence rules (i.e. congruence rules not in the form -specified above) will cause unpredictable and incorrect behaviour. The -user should study examples of congruence rules, consult the relevant -manual sections and communicate with other \HOL\ users should this be a -problem. - - -\section{Avoiding the Pitfalls of Simplification} - -Simplification is a powerful theorem proving technique, but is prone to -several major problems. This section is designed to make the user aware -of these in advance! - -The pitfalls of simplification can generally be -avoided by two techniques: -\begin{itemize} - \item Using well designed simpsets. - \item Using tracing extensively. -\end{itemize} -The behaviour of simplification is almost totally dependent on the -simpset being used. The user should stop and think about -exactly what reduction behaviour they are specifying when they -group together certain theorems, conversions and decision -procedures. A well designed simpset will work on a particular -class of problems, and in many cases will do a thorough job -of proving simple facts within that domain. A poorly -designed simpset constructed by throwing together random -theorems will create all sorts of problems at a later date. - -\subsection{Non-termination} - -Simplification will continue until no more reductions apply. It is very -easy to create simpsets which will result in non-termination when -applied to some terms. \HOL\ detects some simple cases of -non-terminating rewrites (e.g. it doesn't admit rewrites like \ml{|- x = -I x} since the pattern on the left occurs within the right). However, -there is no general protection against this. Generally problems arise -when two or more theorems interact to produce looping, such as \ml{|- x -> y = y < x} and \ml{y < x = x > y}. - -The best way to avoid non-termination is to ask the following question -about each rewrite you place in a simpset: {\it Is the rewrite actually -contributing toward bringing terms toward a particular normal form}. -For example, the rewrite \ml{|- x > y = y < x} should only be added to a -simpset if the normal form we are heading for involves only instances of -\ml{<} for all linear inequalities. - -\subsection{Backward Chaining} - -Conditional rewriting allows a limited degree of search when -rewriting, since the rewrite is not applied unless all conditions -are solved. The simplifier itself is used to solve these -conditions. This will often lead to looping if -theorems which contain the pattern within the conditions -are added as rewrite rules. The most obvious example is -transitivity theorems: -\begin{hol} \begin{verbatim} - |- (?z. x < z /\ z < y) ==> x < y -\end{verbatim} \end{hol} -Do not put these theorems into simpsets! - -\subsection{Non-confluence} - -When faced with a choice of two rewrite rules, both of which are -applicable to a given term, the simplifier will choose one and ignore -the other. This can lead to {\em confluence} problems, i.e. it may be -that a different final result will be produced depending on the order in -which rewrites are applied. Non-confluence is mainly a problem for the -long term maintainability of proofs. - -Some simpsets may be confluent regardless of the presence of conflicting -rewrite rules. An extensive literature exists on term rewriting system -and their properties such as termination and confluence, which the user -is encouraged to study if the subject proves particularly important. - -An example of non-confluence is given by the rewrites: -\begin{hol} \begin{verbatim} - -\end{verbatim} \end{hol} - -\subsection{Over-applicability} - -Consider the following potential rewrite rule, taken from -the underlying theory for the abstract theory of groups: -\begin{hol} \begin{verbatim} - |- (?G. GROUP (G,prod) /\ G x /\ G y /\ G z) ==> - (prod (prod x y) z = prod x (prod y z)) -\end{verbatim} \end{hol} -The theorem simply states that if $G$ and $prod$ are -together define a algebraic group, then $prod$ is associative. -Note there are no constants apart from \ml{GROUP} --- $G$ and -$prod$ are variables. - -The problem with such a rewrite rule is that the pattern -\ml{(--`prod (prod x y) z`--)} will produce many undesirable matches. -The problem is that the rewrite rule is over applicable. The -best solution at the moment is to make the intent of the rule -more clear, by replacing \ml{(--`prod`--)} with a function -to compute \ml{(--`prod`--)} for a given group: -\begin{hol} \begin{verbatim} - |- GROUP (G,prod) /\ G x /\ G y /\ G z ==> - (PROD (G,prod) (PROD (G,prod) x y) z = - PROD (G,prod) x (PROD (G,prod) y z)) -\end{verbatim} \end{hol} -The pattern \ml{(--`PROD (G,prod) (PROD (G,prod) x y) z`--)} will -now be suitably applicable. The use of \ml{PROD} may seem -redundant, but turns out to be a suitable generalisation. - -\section{Summary} - -To summarise the main points of this document: -\begin{itemize} - \item A powerful contextual, conditional simplifier is available - through the functions \ml{SIMP\_CONV}, \ml{SIMP\_RULE}, - \ml{SIMP\_TAC}, \ml{ASM\_SIMP\_TAC} etc. - \item Rewrite rules are organised in objects called {\it simpsets}. - The best simpsets are generally created by making small simpsets and - combining them with other simpset fragments to form powerful tools. - \item Rewrite rules are applied using a limited form of higher - order matching. Higher order matching allows general theorems about - functionals such as quantifiers to be applied without the use - of purpose built conversions. - \item Simpsets may also contain congruence rules. Congruence - rules dictate the term traversal strategy used during simplification - and the cause the production of context theorems - \item Simpsets may contain conversions which can act as infinite sets - of rewrite rules. This is useful for conversion schemas - which are essentially reduction but which cannot be formulated - as rewrite rules (e.g. \ml{REDUCE\_CONV}). - \item Simpsets may contain decision procedures. These are invoked - at lowest priority, and have access to the current working - context. The arithmetic decision procedure included with - \ml{arith\_ss} is an example of the use of this. -\end{itemize} - -\section{An extended example} -\label{extended-example} - -\begin{verbatim} - -new_theory "summ"; -infix ++; -Trace.trace_level := 1; - -val summ_DEF = new_recursive_definition { - def=(--`(summ f 0 = 0) /\ - (summ f (SUC n) = f n + summ f n)`--), - fixity=Prefix, - name="summ_DEF", - rec_axiom=prim_recTheory.num_Axiom}; - -(* now define the normal notion of summation *) - -val SUMM_DEF = new_definition("SUMM_DEF", - (--`SUMM f n m = summ (\k. f(n+k)) ((m+1)-n)`--)); - -(* The following is the actual way we want to define this - we could do this *) -(* with TFL. For now we'll just axiomatise it. *) -val summ = mk_thm([], - (--`(!f. summ f 0 = 0) /\ - (!f n. n > 0 ==> (summ f n = f 0 + (summ (\k. f (k+1)) (n-1))))`--)); - - -val SUMM_0 = prove((--`!f n m. (n = m + 1) ==> (SUMM f n m = 0)`--), - SIMP_TAC hol_ss [summ,SUMM_DEF]); -val SUMM_1 = prove((--`!f n m. (n = m) ==> (SUMM f n m = f n)`--), - SIMP_TAC hol_ss [summ,SUMM_DEF]); -val SUMM_TAKE_LEFT = prove( - (--`!f n m. (n < m) ==> (SUMM f n m = f n + SUMM f (n+1) m)`--), - SIMP_TAC hol_ss [SUMM_DEF,summ]); - -(* here's an example of using SIMP_TAC several times along with - small helper theorems *) -local - val thm = SIMP_PROVE hol_ss [] - (--`(n < m) ==> ((m + 1) - n = SUC (m - n))`--) -in -val SUMM_TAKE_RIGHT = TAC_PROOF - (([], --`!f n m. (n < m) ==> (SUMM f n m = SUMM f n (m-1) + f m)`--), - SIMP_TAC hol_ss [SUMM_DEF, summ_DEF] THEN - SIMP_TAC bool_ss [thm, summ_DEF] THEN - SIMP_TAC hol_ss [summ_DEF]) -end; - -(* sum from left - much more efficient as it uses addition not subtraction *) -val SUMML_ss = rewrites [SUMM_TAKE_LEFT, SUMM_1,SUMM_0]; -val summl_ss = hol_ss ++ SUMML_ss; - -val SUMMR_ss = rewrites [SUMM_TAKE_RIGHT, SUMM_1,SUMM_0]; -val summr_ss = hol_ss ++ SUMMR_ss; - - -(*------------------------------------------------------------------------- - * SUMM_x = |- !n. n >= 1 ==> (2 * SUMM (\x. x) 1 n = (n + 1) * n) : thm - *-----------------------------------------------------------------------*) - -add_theory_to_sml "arithmetic"; - -val SUMM_x = prove( - (--`!n. n >= 1 ==> (2*(SUMM (\x.x) 1 n) = (n + 1) * n)`--), - INDUCT_TAC - THENL [ - FULL_SIMP_TAC summr_ss [], - ASM_CASES_TAC (--`n=0`--) THEN - ASM_SIMP_TAC summr_ss [LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB] - ]); - - -(*------------------------------------------------------------------------- - * Using SIMP_CONV as a calculator for Sums - *-----------------------------------------------------------------------*) - -clear_arith_caches(); -SIMP_CONV summl_ss [] (--`2 * SUMM (\x. x) 1 10`--); -SIMP_CONV summr_ss [] (--`2 * SUMM (\x. x) 1 10`--); -SIMP_CONV summl_ss [] (--`2 * SUMM (\x. x) 1 15`--); -SIMP_CONV summl_ss [] (--`2 * SUMM (\x. x) 1 20`--); -SIMP_CONV summl_ss [] (--`2 * SUMM (\x. x) 1 30`--); -SIMP_CONV summl_ss [] (--`2 * SUMM (\x. x) 1 40`--); - - -SIMP_CONV summl_ss [] (--`SUMM (\x. x*x*x) 1 2`--); -SIMP_CONV summl_ss [] (--`SUMM (\x. x*x*x) 1 3`--); -SIMP_CONV summl_ss [] (--`SUMM (\x. x*x*x) 1 4`--); -SIMP_CONV summl_ss [] (--`SUMM (\x. x*x*x) 1 5`--); -SIMP_CONV summl_ss [] (--`SUMM (\x. x*x*x) 1 6`--); -SIMP_CONV summl_ss [] (--`SUMM (\x. x*x*x) 1 7`--); -SIMP_CONV summl_ss [] (--`SUMM (\x. x*y*y) 1 3`--); -SIMP_CONV summl_ss [] (--`SUMM (\x. x*y*y) 1 10`--); -\end{verbatim} - -\end{document}