--- a/doc-src/IsarRef/Thy/Generic.thy Sat Jun 11 14:27:23 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Sat Jun 11 15:03:31 2011 +0200
@@ -64,6 +64,8 @@
@{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
@{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
@{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def intro} & : & @{text method} \\
+ @{method_def elim} & : & @{text method} \\
@{method_def succeed} & : & @{text method} \\
@{method_def fail} & : & @{text method} \\
\end{matharray}
@@ -73,6 +75,8 @@
;
(@@{method erule} | @@{method drule} | @@{method frule})
('(' @{syntax nat} ')')? @{syntax thmrefs}
+ ;
+ (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
"}
\begin{description}
@@ -103,6 +107,12 @@
the plain @{method rule} method, with forward chaining of current
facts.
+ \item @{method intro} and @{method elim} repeatedly refine some goal
+ by intro- or elim-resolution, after having inserted any chained
+ facts. Exactly the rules given as arguments are taken into account;
+ this allows fine-tuned decomposition of a proof problem, in contrast
+ to common automated tools.
+
\item @{method succeed} yields a single (unchanged) result; it is
the identity of the ``@{text ","}'' method combinator (cf.\
\secref{sec:proof-meth}).
@@ -879,6 +889,39 @@
*}
+subsection {* Structured methods *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{method_def rule} & : & @{text method} \\
+ @{method_def contradiction} & : & @{text method} \\
+ \end{matharray}
+
+ @{rail "
+ @@{method rule} @{syntax thmrefs}?
+ "}
+
+ \begin{description}
+
+ \item @{method rule} as offered by the Classical Reasoner is a
+ refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
+ versions work the same, but the classical version observes the
+ classical rule context in addition to that of Isabelle/Pure.
+
+ Common object logics (HOL, ZF, etc.) declare a rich collection of
+ classical rules (even if these would qualify as intuitionistic
+ ones), but only few declarations to the rule context of
+ Isabelle/Pure (\secref{sec:pure-meth-att}).
+
+ \item @{method contradiction} solves some goal by contradiction,
+ deriving any result from both @{text "\<not> A"} and @{text A}. Chained
+ facts, which are guaranteed to participate, may appear in either
+ order.
+
+ \end{description}
+*}
+
+
subsection {* Automated methods *}
text {*
@@ -1041,47 +1084,6 @@
*}
-subsection {* Structured proof methods *}
-
-text {*
- \begin{matharray}{rcl}
- @{method_def rule} & : & @{text method} \\
- @{method_def contradiction} & : & @{text method} \\
- @{method_def intro} & : & @{text method} \\
- @{method_def elim} & : & @{text method} \\
- \end{matharray}
-
- @{rail "
- (@@{method rule} | @@{method intro} | @@{method elim}) @{syntax thmrefs}?
- "}
-
- \begin{description}
-
- \item @{method rule} as offered by the Classical Reasoner is a
- refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
- versions work the same, but the classical version observes the
- classical rule context in addition to that of Isabelle/Pure.
-
- Common object logics (HOL, ZF, etc.) declare a rich collection of
- classical rules (even if these would qualify as intuitionistic
- ones), but only few declarations to the rule context of
- Isabelle/Pure (\secref{sec:pure-meth-att}).
-
- \item @{method contradiction} solves some goal by contradiction,
- deriving any result from both @{text "\<not> A"} and @{text A}. Chained
- facts, which are guaranteed to participate, may appear in either
- order.
-
- \item @{method intro} and @{method elim} repeatedly refine some goal
- by intro- or elim-resolution, after having inserted any chained
- facts. Exactly the rules given as arguments are taken into account;
- this allows fine-tuned decomposition of a proof problem, in contrast
- to common automated tools.
-
- \end{description}
-*}
-
-
section {* Object-logic setup \label{sec:object-logic} *}
text {*
--- a/doc-src/IsarRef/Thy/document/Generic.tex Sat Jun 11 14:27:23 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sat Jun 11 15:03:31 2011 +0200
@@ -123,6 +123,8 @@
\indexdef{}{method}{erule}\hypertarget{method.erule}{\hyperlink{method.erule}{\mbox{\isa{erule}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
\indexdef{}{method}{drule}\hypertarget{method.drule}{\hyperlink{method.drule}{\mbox{\isa{drule}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
\indexdef{}{method}{frule}\hypertarget{method.frule}{\hyperlink{method.frule}{\mbox{\isa{frule}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
+ \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
+ \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
\indexdef{}{method}{succeed}\hypertarget{method.succeed}{\hyperlink{method.succeed}{\mbox{\isa{succeed}}}} & : & \isa{method} \\
\indexdef{}{method}{fail}\hypertarget{method.fail}{\hyperlink{method.fail}{\mbox{\isa{fail}}}} & : & \isa{method} \\
\end{matharray}
@@ -154,6 +156,17 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
+\rail@begin{2}{}
+\rail@bar
+\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
\end{railoutput}
@@ -182,6 +195,12 @@
the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method, with forward chaining of current
facts.
+ \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
+ by intro- or elim-resolution, after having inserted any chained
+ facts. Exactly the rules given as arguments are taken into account;
+ this allows fine-tuned decomposition of a proof problem, in contrast
+ to common automated tools.
+
\item \hyperlink{method.succeed}{\mbox{\isa{succeed}}} yields a single (unchanged) result; it is
the identity of the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}}'' method combinator (cf.\
\secref{sec:proof-meth}).
@@ -1311,6 +1330,48 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Structured methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
+ \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
+ \end{matharray}
+
+ \begin{railoutput}
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+ \begin{description}
+
+ \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
+ refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
+ versions work the same, but the classical version observes the
+ classical rule context in addition to that of Isabelle/Pure.
+
+ Common object logics (HOL, ZF, etc.) declare a rich collection of
+ classical rules (even if these would qualify as intuitionistic
+ ones), but only few declarations to the rule context of
+ Isabelle/Pure (\secref{sec:pure-meth-att}).
+
+ \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
+ deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
+ facts, which are guaranteed to participate, may appear in either
+ order.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Automated methods%
}
\isamarkuptrue%
@@ -1610,62 +1671,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Structured proof methods%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
- \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
- \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
- \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{3}{}
-\rail@bar
-\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
-\rail@nextbar{2}
-\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}
-
-
- \begin{description}
-
- \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
- refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
- versions work the same, but the classical version observes the
- classical rule context in addition to that of Isabelle/Pure.
-
- Common object logics (HOL, ZF, etc.) declare a rich collection of
- classical rules (even if these would qualify as intuitionistic
- ones), but only few declarations to the rule context of
- Isabelle/Pure (\secref{sec:pure-meth-att}).
-
- \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
- deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
- facts, which are guaranteed to participate, may appear in either
- order.
-
- \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
- by intro- or elim-resolution, after having inserted any chained
- facts. Exactly the rules given as arguments are taken into account;
- this allows fine-tuned decomposition of a proof problem, in contrast
- to common automated tools.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Object-logic setup \label{sec:object-logic}%
}
\isamarkuptrue%