more concise/precise documentation;
authorwenzelm
Sat Nov 03 19:07:07 2012 +0100 (2012-11-03)
changeset 50062e038198f7d08
parent 50061 7110422d4cb3
child 50063 7e491da6bcbd
more concise/precise documentation;
src/Doc/Ref/document/classical.tex
src/Provers/classical.ML
     1.1 --- a/src/Doc/Ref/document/classical.tex	Wed Nov 14 14:45:14 2012 +0100
     1.2 +++ b/src/Doc/Ref/document/classical.tex	Sat Nov 03 19:07:07 2012 +0100
     1.3 @@ -170,52 +170,6 @@
     1.4  resolution and also elim-resolution with the swapped form.
     1.5  \end{ttdescription}
     1.6  
     1.7 -
     1.8 -\section{Setting up the classical reasoner}\label{sec:classical-setup}
     1.9 -\index{classical reasoner!setting up}
    1.10 -Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, 
    1.11 -have the classical reasoner already set up.  
    1.12 -When defining a new classical logic, you should set up the reasoner yourself.  
    1.13 -It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the 
    1.14 -argument signature \texttt{CLASSICAL_DATA}:
    1.15 -\begin{ttbox} 
    1.16 -signature CLASSICAL_DATA =
    1.17 -  sig
    1.18 -  val mp             : thm
    1.19 -  val not_elim       : thm
    1.20 -  val swap           : thm
    1.21 -  val sizef          : thm -> int
    1.22 -  val hyp_subst_tacs : (int -> tactic) list
    1.23 -  end;
    1.24 -\end{ttbox}
    1.25 -Thus, the functor requires the following items:
    1.26 -\begin{ttdescription}
    1.27 -\item[\tdxbold{mp}] should be the Modus Ponens rule
    1.28 -$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
    1.29 -
    1.30 -\item[\tdxbold{not_elim}] should be the contradiction rule
    1.31 -$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
    1.32 -
    1.33 -\item[\tdxbold{swap}] should be the swap rule
    1.34 -$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
    1.35 -
    1.36 -\item[\ttindexbold{sizef}] is the heuristic function used for best-first
    1.37 -search.  It should estimate the size of the remaining subgoals.  A good
    1.38 -heuristic function is \ttindex{size_of_thm}, which measures the size of the
    1.39 -proof state.  Another size function might ignore certain subgoals (say,
    1.40 -those concerned with type-checking).  A heuristic function might simply
    1.41 -count the subgoals.
    1.42 -
    1.43 -\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
    1.44 -the hypotheses, typically created by \ttindex{HypsubstFun} (see
    1.45 -Chapter~\ref{substitution}).  This list can, of course, be empty.  The
    1.46 -tactics are assumed to be safe!
    1.47 -\end{ttdescription}
    1.48 -The functor is not at all sensitive to the formalization of the
    1.49 -object-logic.  It does not even examine the rules, but merely applies
    1.50 -them according to its fixed strategy.  The functor resides in {\tt
    1.51 -  Provers/classical.ML} in the Isabelle sources.
    1.52 -
    1.53  \index{classical reasoner|)}
    1.54  
    1.55  %%% Local Variables: 
     2.1 --- a/src/Provers/classical.ML	Wed Nov 14 14:45:14 2012 +0100
     2.2 +++ b/src/Provers/classical.ML	Sat Nov 03 19:07:07 2012 +0100
     2.3 @@ -24,8 +24,9 @@
     2.4    val not_elim: thm  (* ~P ==> P ==> R *)
     2.5    val swap: thm  (* ~ P ==> (~ R ==> P) ==> R *)
     2.6    val classical: thm  (* (~ P ==> P) ==> P *)
     2.7 -  val sizef: thm -> int  (* size function for BEST_FIRST *)
     2.8 -  val hyp_subst_tacs: (int -> tactic) list
     2.9 +  val sizef: thm -> int  (* size function for BEST_FIRST, typically size_of_thm *)
    2.10 +  val hyp_subst_tacs: (int -> tactic) list (* optional tactics for substitution in
    2.11 +    the hypotheses; assumed to be safe! *)
    2.12  end;
    2.13  
    2.14  signature BASIC_CLASSICAL =