1.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex Sun Jun 05 20:15:47 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Sun Jun 05 20:23:05 2011 +0200
1.3 @@ -1311,63 +1311,6 @@
1.4 \end{isamarkuptext}%
1.5 \isamarkuptrue%
1.6 %
1.7 -\isamarkupsubsection{Basic methods%
1.8 -}
1.9 -\isamarkuptrue%
1.10 -%
1.11 -\begin{isamarkuptext}%
1.12 -\begin{matharray}{rcl}
1.13 - \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
1.14 - \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
1.15 - \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
1.16 - \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
1.17 - \end{matharray}
1.18 -
1.19 - \begin{railoutput}
1.20 -\rail@begin{3}{}
1.21 -\rail@bar
1.22 -\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
1.23 -\rail@nextbar{1}
1.24 -\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
1.25 -\rail@nextbar{2}
1.26 -\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
1.27 -\rail@endbar
1.28 -\rail@bar
1.29 -\rail@nextbar{1}
1.30 -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.31 -\rail@endbar
1.32 -\rail@end
1.33 -\end{railoutput}
1.34 -
1.35 -
1.36 - \begin{description}
1.37 -
1.38 - \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
1.39 - refinement over the primitive one (see \secref{sec:pure-meth-att}).
1.40 - Both versions essentially work the same, but the classical version
1.41 - observes the classical rule context in addition to that of
1.42 - Isabelle/Pure.
1.43 -
1.44 - Common object logics (HOL, ZF, etc.) declare a rich collection of
1.45 - classical rules (even if these would qualify as intuitionistic
1.46 - ones), but only few declarations to the rule context of
1.47 - Isabelle/Pure (\secref{sec:pure-meth-att}).
1.48 -
1.49 - \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
1.50 - deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
1.51 - facts, which are guaranteed to participate, may appear in either
1.52 - order.
1.53 -
1.54 - \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
1.55 - by intro- or elim-resolution, after having inserted any chained
1.56 - facts. Exactly the rules given as arguments are taken into account;
1.57 - this allows fine-tuned decomposition of a proof problem, in contrast
1.58 - to common automated tools.
1.59 -
1.60 - \end{description}%
1.61 -\end{isamarkuptext}%
1.62 -\isamarkuptrue%
1.63 -%
1.64 \isamarkupsubsection{Automated methods%
1.65 }
1.66 \isamarkuptrue%
1.67 @@ -1578,6 +1521,62 @@
1.68 \end{isamarkuptext}%
1.69 \isamarkuptrue%
1.70 %
1.71 +\isamarkupsubsection{Structured proof methods%
1.72 +}
1.73 +\isamarkuptrue%
1.74 +%
1.75 +\begin{isamarkuptext}%
1.76 +\begin{matharray}{rcl}
1.77 + \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
1.78 + \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
1.79 + \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
1.80 + \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
1.81 + \end{matharray}
1.82 +
1.83 + \begin{railoutput}
1.84 +\rail@begin{3}{}
1.85 +\rail@bar
1.86 +\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
1.87 +\rail@nextbar{1}
1.88 +\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
1.89 +\rail@nextbar{2}
1.90 +\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
1.91 +\rail@endbar
1.92 +\rail@bar
1.93 +\rail@nextbar{1}
1.94 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.95 +\rail@endbar
1.96 +\rail@end
1.97 +\end{railoutput}
1.98 +
1.99 +
1.100 + \begin{description}
1.101 +
1.102 + \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
1.103 + refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
1.104 + versions work the same, but the classical version observes the
1.105 + classical rule context in addition to that of Isabelle/Pure.
1.106 +
1.107 + Common object logics (HOL, ZF, etc.) declare a rich collection of
1.108 + classical rules (even if these would qualify as intuitionistic
1.109 + ones), but only few declarations to the rule context of
1.110 + Isabelle/Pure (\secref{sec:pure-meth-att}).
1.111 +
1.112 + \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
1.113 + deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
1.114 + facts, which are guaranteed to participate, may appear in either
1.115 + order.
1.116 +
1.117 + \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
1.118 + by intro- or elim-resolution, after having inserted any chained
1.119 + facts. Exactly the rules given as arguments are taken into account;
1.120 + this allows fine-tuned decomposition of a proof problem, in contrast
1.121 + to common automated tools.
1.122 +
1.123 + \end{description}%
1.124 +\end{isamarkuptext}%
1.125 +\isamarkuptrue%
1.126 +%
1.127 \isamarkupsection{Object-logic setup \label{sec:object-logic}%
1.128 }
1.129 \isamarkuptrue%