# HG changeset patch # User wenzelm # Date 1307129568 -7200 # Node ID bd8d78745a7df25694ded67481f04172141b62d0 # Parent 3ba51a3acff01335fce082022aa7b70608bd0320 removed some old stuff; diff -r 3ba51a3acff0 -r bd8d78745a7d doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Thu Jun 02 14:11:24 2011 +0200 +++ b/doc-src/HOL/HOL.tex Fri Jun 03 21:32:48 2011 +0200 @@ -310,8 +310,7 @@ \begin{warn} The definitions above should never be expanded and are shown for completeness only. Instead users should reason in terms of the derived rules shown below -or, better still, using high-level tactics -(see~{\S}\ref{sec:HOL:generic-packages}). +or, better still, using high-level tactics. \end{warn} Some of the rules mention type variables; for example, \texttt{refl} @@ -880,13 +879,7 @@ on sets in the file \texttt{HOL/mono.ML}. -\section{Generic packages} -\label{sec:HOL:generic-packages} - -HOL instantiates most of Isabelle's generic packages, making available the -simplifier and the classical reasoner. - -\subsection{Simplification and substitution} +\section{Simplification and substitution} Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset (\texttt{simpset()}), which works for most purposes. A quite minimal @@ -932,7 +925,7 @@ equality throughout a subgoal and its hypotheses. This tactic uses HOL's general substitution rule. -\subsubsection{Case splitting} +\subsection{Case splitting} \label{subsec:HOL:case:splitting} HOL also provides convenient means for case splitting during rewriting. Goals @@ -989,115 +982,6 @@ \end{ttbox} for adding splitting rules to, and deleting them from the current simpset. -\subsection{Classical reasoning} - -HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as -classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall -Fig.\ts\ref{hol-lemmas2} above. - -The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and -{\tt Best_tac} refer to the default claset (\texttt{claset()}), which works -for most purposes. Named clasets include \ttindexbold{prop_cs}, which -includes the propositional rules, and \ttindexbold{HOL_cs}, which also -includes quantifier rules. See the file \texttt{HOL/cladata.ML} for lists of -the classical rules, -and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% -{Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods. - - -%FIXME outdated, both from the Isabelle and SVC perspective -% \section{Calling the decision procedure SVC}\label{sec:HOL:SVC} - -% \index{SVC decision procedure|(} - -% The Stanford Validity Checker (SVC) is a tool that can check the validity of -% certain types of formulae. If it is installed on your machine, then -% Isabelle/HOL can be configured to call it through the tactic -% \ttindex{svc_tac}. It is ideal for large tautologies and complex problems in -% linear arithmetic. Subexpressions that SVC cannot handle are automatically -% replaced by variables, so you can call the tactic on any subgoal. See the -% file \texttt{HOL/ex/svc_test.ML} for examples. -% \begin{ttbox} -% svc_tac : int -> tactic -% Svc.trace : bool ref \hfill{\bf initially false} -% \end{ttbox} - -% \begin{ttdescription} -% \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating -% it into a formula recognized by~SVC\@. If it succeeds then the subgoal is -% removed. It fails if SVC is unable to prove the subgoal. It crashes with -% an error message if SVC appears not to be installed. Numeric variables may -% have types \texttt{nat}, \texttt{int} or \texttt{real}. - -% \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac} -% to trace its operations: abstraction of the subgoal, translation to SVC -% syntax, SVC's response. -% \end{ttdescription} - -% Here is an example, with tracing turned on: -% \begin{ttbox} -% set Svc.trace; -% {\out val it : bool = true} -% Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \ttback -% \ttback a + #3*b <= #5 + #2*c --> #2 + #3*b <= #2*a + #6*c"; - -% by (svc_tac 1); -% {\out Subgoal abstracted to} -% {\out #3 * a <= #2 + #4 * b + #6 * c &} -% {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->} -% {\out #2 + #3 * b <= #2 * a + #6 * c} -% {\out Calling SVC:} -% {\out (=> (<= 0 (F_c) ) (=> (<= 0 (F_b) ) (=> (<= 0 (F_a) )} -% {\out (=> (AND (<= {* 3 (F_a) } {+ {+ 2 {* 4 (F_b) } } } -% {\out {* 6 (F_c) } } ) (AND (<= 11 {+ {+ {* 2 (F_a) } (F_b) }} -% {\out {* 2 (F_c) } } ) (<= {+ (F_a) {* 3 (F_b) } } {+ 5 } -% {\out {* 2 (F_c) } } ) ) ) (< {+ 2 {* 3 (F_b) } } {+ 1 {+ } -% {\out {* 2 (F_a) } {* 6 (F_c) } } } ) ) ) ) ) } -% {\out SVC Returns:} -% {\out VALID} -% {\out Level 1} -% {\out #3 * a <= #2 + #4 * b + #6 * c &} -% {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->} -% {\out #2 + #3 * b <= #2 * a + #6 * c} -% {\out No subgoals!} -% \end{ttbox} - - -% \begin{warn} -% Calling \ttindex{svc_tac} entails an above-average risk of -% unsoundness. Isabelle does not check SVC's result independently. Moreover, -% the tactic translates the submitted formula using code that lies outside -% Isabelle's inference core. Theorems that depend upon results proved using SVC -% (and other oracles) are displayed with the annotation \texttt{[!]} attached. -% You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of -% theorem~$th$, as described in the \emph{Reference Manual}. -% \end{warn} - -% To start, first download SVC from the Internet at URL -% \begin{ttbox} -% http://agamemnon.stanford.edu/~levitt/vc/index.html -% \end{ttbox} -% and install it using the instructions supplied. SVC requires two environment -% variables: -% \begin{ttdescription} -% \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC -% distribution directory. - -% \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and -% operating system. -% \end{ttdescription} -% You can set these environment variables either using the Unix shell or through -% an Isabelle \texttt{settings} file. Isabelle assumes SVC to be installed if -% \texttt{SVC_HOME} is defined. - -% \paragraph*{Acknowledgement.} This interface uses code supplied by S{\o}ren -% Heilmann. - - -% \index{SVC decision procedure|)} - - - \section{Types}\label{sec:HOL:Types} This section describes HOL's basic predefined types ($\alpha \times \beta$,