1.1 --- a/doc-src/HOL/HOL.tex Thu Jun 02 14:11:24 2011 +0200
1.2 +++ b/doc-src/HOL/HOL.tex Fri Jun 03 21:32:48 2011 +0200
1.3 @@ -310,8 +310,7 @@
1.4 \begin{warn}
1.5 The definitions above should never be expanded and are shown for completeness
1.6 only. Instead users should reason in terms of the derived rules shown below
1.7 -or, better still, using high-level tactics
1.8 -(see~{\S}\ref{sec:HOL:generic-packages}).
1.9 +or, better still, using high-level tactics.
1.10 \end{warn}
1.11
1.12 Some of the rules mention type variables; for example, \texttt{refl}
1.13 @@ -880,13 +879,7 @@
1.14 on sets in the file \texttt{HOL/mono.ML}.
1.15
1.16
1.17 -\section{Generic packages}
1.18 -\label{sec:HOL:generic-packages}
1.19 -
1.20 -HOL instantiates most of Isabelle's generic packages, making available the
1.21 -simplifier and the classical reasoner.
1.22 -
1.23 -\subsection{Simplification and substitution}
1.24 +\section{Simplification and substitution}
1.25
1.26 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
1.27 (\texttt{simpset()}), which works for most purposes. A quite minimal
1.28 @@ -932,7 +925,7 @@
1.29 equality throughout a subgoal and its hypotheses. This tactic uses HOL's
1.30 general substitution rule.
1.31
1.32 -\subsubsection{Case splitting}
1.33 +\subsection{Case splitting}
1.34 \label{subsec:HOL:case:splitting}
1.35
1.36 HOL also provides convenient means for case splitting during rewriting. Goals
1.37 @@ -989,115 +982,6 @@
1.38 \end{ttbox}
1.39 for adding splitting rules to, and deleting them from the current simpset.
1.40
1.41 -\subsection{Classical reasoning}
1.42 -
1.43 -HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
1.44 -classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
1.45 -Fig.\ts\ref{hol-lemmas2} above.
1.46 -
1.47 -The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and
1.48 -{\tt Best_tac} refer to the default claset (\texttt{claset()}), which works
1.49 -for most purposes. Named clasets include \ttindexbold{prop_cs}, which
1.50 -includes the propositional rules, and \ttindexbold{HOL_cs}, which also
1.51 -includes quantifier rules. See the file \texttt{HOL/cladata.ML} for lists of
1.52 -the classical rules,
1.53 -and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
1.54 -{Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
1.55 -
1.56 -
1.57 -%FIXME outdated, both from the Isabelle and SVC perspective
1.58 -% \section{Calling the decision procedure SVC}\label{sec:HOL:SVC}
1.59 -
1.60 -% \index{SVC decision procedure|(}
1.61 -
1.62 -% The Stanford Validity Checker (SVC) is a tool that can check the validity of
1.63 -% certain types of formulae. If it is installed on your machine, then
1.64 -% Isabelle/HOL can be configured to call it through the tactic
1.65 -% \ttindex{svc_tac}. It is ideal for large tautologies and complex problems in
1.66 -% linear arithmetic. Subexpressions that SVC cannot handle are automatically
1.67 -% replaced by variables, so you can call the tactic on any subgoal. See the
1.68 -% file \texttt{HOL/ex/svc_test.ML} for examples.
1.69 -% \begin{ttbox}
1.70 -% svc_tac : int -> tactic
1.71 -% Svc.trace : bool ref \hfill{\bf initially false}
1.72 -% \end{ttbox}
1.73 -
1.74 -% \begin{ttdescription}
1.75 -% \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating
1.76 -% it into a formula recognized by~SVC\@. If it succeeds then the subgoal is
1.77 -% removed. It fails if SVC is unable to prove the subgoal. It crashes with
1.78 -% an error message if SVC appears not to be installed. Numeric variables may
1.79 -% have types \texttt{nat}, \texttt{int} or \texttt{real}.
1.80 -
1.81 -% \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}
1.82 -% to trace its operations: abstraction of the subgoal, translation to SVC
1.83 -% syntax, SVC's response.
1.84 -% \end{ttdescription}
1.85 -
1.86 -% Here is an example, with tracing turned on:
1.87 -% \begin{ttbox}
1.88 -% set Svc.trace;
1.89 -% {\out val it : bool = true}
1.90 -% Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \ttback
1.91 -% \ttback a + #3*b <= #5 + #2*c --> #2 + #3*b <= #2*a + #6*c";
1.92 -
1.93 -% by (svc_tac 1);
1.94 -% {\out Subgoal abstracted to}
1.95 -% {\out #3 * a <= #2 + #4 * b + #6 * c &}
1.96 -% {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
1.97 -% {\out #2 + #3 * b <= #2 * a + #6 * c}
1.98 -% {\out Calling SVC:}
1.99 -% {\out (=> (<= 0 (F_c) ) (=> (<= 0 (F_b) ) (=> (<= 0 (F_a) )}
1.100 -% {\out (=> (AND (<= {* 3 (F_a) } {+ {+ 2 {* 4 (F_b) } } }
1.101 -% {\out {* 6 (F_c) } } ) (AND (<= 11 {+ {+ {* 2 (F_a) } (F_b) }}
1.102 -% {\out {* 2 (F_c) } } ) (<= {+ (F_a) {* 3 (F_b) } } {+ 5 }
1.103 -% {\out {* 2 (F_c) } } ) ) ) (< {+ 2 {* 3 (F_b) } } {+ 1 {+ }
1.104 -% {\out {* 2 (F_a) } {* 6 (F_c) } } } ) ) ) ) ) }
1.105 -% {\out SVC Returns:}
1.106 -% {\out VALID}
1.107 -% {\out Level 1}
1.108 -% {\out #3 * a <= #2 + #4 * b + #6 * c &}
1.109 -% {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
1.110 -% {\out #2 + #3 * b <= #2 * a + #6 * c}
1.111 -% {\out No subgoals!}
1.112 -% \end{ttbox}
1.113 -
1.114 -
1.115 -% \begin{warn}
1.116 -% Calling \ttindex{svc_tac} entails an above-average risk of
1.117 -% unsoundness. Isabelle does not check SVC's result independently. Moreover,
1.118 -% the tactic translates the submitted formula using code that lies outside
1.119 -% Isabelle's inference core. Theorems that depend upon results proved using SVC
1.120 -% (and other oracles) are displayed with the annotation \texttt{[!]} attached.
1.121 -% You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of
1.122 -% theorem~$th$, as described in the \emph{Reference Manual}.
1.123 -% \end{warn}
1.124 -
1.125 -% To start, first download SVC from the Internet at URL
1.126 -% \begin{ttbox}
1.127 -% http://agamemnon.stanford.edu/~levitt/vc/index.html
1.128 -% \end{ttbox}
1.129 -% and install it using the instructions supplied. SVC requires two environment
1.130 -% variables:
1.131 -% \begin{ttdescription}
1.132 -% \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC
1.133 -% distribution directory.
1.134 -
1.135 -% \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and
1.136 -% operating system.
1.137 -% \end{ttdescription}
1.138 -% You can set these environment variables either using the Unix shell or through
1.139 -% an Isabelle \texttt{settings} file. Isabelle assumes SVC to be installed if
1.140 -% \texttt{SVC_HOME} is defined.
1.141 -
1.142 -% \paragraph*{Acknowledgement.} This interface uses code supplied by S{\o}ren
1.143 -% Heilmann.
1.144 -
1.145 -
1.146 -% \index{SVC decision procedure|)}
1.147 -
1.148 -
1.149 -
1.150
1.151 \section{Types}\label{sec:HOL:Types}
1.152 This section describes HOL's basic predefined types ($\alpha \times \beta$,