tuned sections;
authorwenzelm
Sat Jun 11 15:03:31 2011 +0200 (2011-06-11)
changeset 43365f8944cb2468f
parent 43364 9c392ea6a6e6
child 43366 9cbcab5c780a
tuned sections;
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/document/Generic.tex
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 14:27:23 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 15:03:31 2011 +0200
     1.3 @@ -64,6 +64,8 @@
     1.4      @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
     1.5      @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
     1.6      @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
     1.7 +    @{method_def intro} & : & @{text method} \\
     1.8 +    @{method_def elim} & : & @{text method} \\
     1.9      @{method_def succeed} & : & @{text method} \\
    1.10      @{method_def fail} & : & @{text method} \\
    1.11    \end{matharray}
    1.12 @@ -73,6 +75,8 @@
    1.13      ;
    1.14      (@@{method erule} | @@{method drule} | @@{method frule})
    1.15        ('(' @{syntax nat} ')')? @{syntax thmrefs}
    1.16 +    ;
    1.17 +    (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
    1.18    "}
    1.19  
    1.20    \begin{description}
    1.21 @@ -103,6 +107,12 @@
    1.22    the plain @{method rule} method, with forward chaining of current
    1.23    facts.
    1.24  
    1.25 +  \item @{method intro} and @{method elim} repeatedly refine some goal
    1.26 +  by intro- or elim-resolution, after having inserted any chained
    1.27 +  facts.  Exactly the rules given as arguments are taken into account;
    1.28 +  this allows fine-tuned decomposition of a proof problem, in contrast
    1.29 +  to common automated tools.
    1.30 +
    1.31    \item @{method succeed} yields a single (unchanged) result; it is
    1.32    the identity of the ``@{text ","}'' method combinator (cf.\
    1.33    \secref{sec:proof-meth}).
    1.34 @@ -879,6 +889,39 @@
    1.35  *}
    1.36  
    1.37  
    1.38 +subsection {* Structured methods *}
    1.39 +
    1.40 +text {*
    1.41 +  \begin{matharray}{rcl}
    1.42 +    @{method_def rule} & : & @{text method} \\
    1.43 +    @{method_def contradiction} & : & @{text method} \\
    1.44 +  \end{matharray}
    1.45 +
    1.46 +  @{rail "
    1.47 +    @@{method rule} @{syntax thmrefs}?
    1.48 +  "}
    1.49 +
    1.50 +  \begin{description}
    1.51 +
    1.52 +  \item @{method rule} as offered by the Classical Reasoner is a
    1.53 +  refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both
    1.54 +  versions work the same, but the classical version observes the
    1.55 +  classical rule context in addition to that of Isabelle/Pure.
    1.56 +
    1.57 +  Common object logics (HOL, ZF, etc.) declare a rich collection of
    1.58 +  classical rules (even if these would qualify as intuitionistic
    1.59 +  ones), but only few declarations to the rule context of
    1.60 +  Isabelle/Pure (\secref{sec:pure-meth-att}).
    1.61 +
    1.62 +  \item @{method contradiction} solves some goal by contradiction,
    1.63 +  deriving any result from both @{text "\<not> A"} and @{text A}.  Chained
    1.64 +  facts, which are guaranteed to participate, may appear in either
    1.65 +  order.
    1.66 +
    1.67 +  \end{description}
    1.68 +*}
    1.69 +
    1.70 +
    1.71  subsection {* Automated methods *}
    1.72  
    1.73  text {*
    1.74 @@ -1041,47 +1084,6 @@
    1.75  *}
    1.76  
    1.77  
    1.78 -subsection {* Structured proof methods *}
    1.79 -
    1.80 -text {*
    1.81 -  \begin{matharray}{rcl}
    1.82 -    @{method_def rule} & : & @{text method} \\
    1.83 -    @{method_def contradiction} & : & @{text method} \\
    1.84 -    @{method_def intro} & : & @{text method} \\
    1.85 -    @{method_def elim} & : & @{text method} \\
    1.86 -  \end{matharray}
    1.87 -
    1.88 -  @{rail "
    1.89 -    (@@{method rule} | @@{method intro} | @@{method elim}) @{syntax thmrefs}?
    1.90 -  "}
    1.91 -
    1.92 -  \begin{description}
    1.93 -
    1.94 -  \item @{method rule} as offered by the Classical Reasoner is a
    1.95 -  refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both
    1.96 -  versions work the same, but the classical version observes the
    1.97 -  classical rule context in addition to that of Isabelle/Pure.
    1.98 -
    1.99 -  Common object logics (HOL, ZF, etc.) declare a rich collection of
   1.100 -  classical rules (even if these would qualify as intuitionistic
   1.101 -  ones), but only few declarations to the rule context of
   1.102 -  Isabelle/Pure (\secref{sec:pure-meth-att}).
   1.103 -
   1.104 -  \item @{method contradiction} solves some goal by contradiction,
   1.105 -  deriving any result from both @{text "\<not> A"} and @{text A}.  Chained
   1.106 -  facts, which are guaranteed to participate, may appear in either
   1.107 -  order.
   1.108 -
   1.109 -  \item @{method intro} and @{method elim} repeatedly refine some goal
   1.110 -  by intro- or elim-resolution, after having inserted any chained
   1.111 -  facts.  Exactly the rules given as arguments are taken into account;
   1.112 -  this allows fine-tuned decomposition of a proof problem, in contrast
   1.113 -  to common automated tools.
   1.114 -
   1.115 -  \end{description}
   1.116 -*}
   1.117 -
   1.118 -
   1.119  section {* Object-logic setup \label{sec:object-logic} *}
   1.120  
   1.121  text {*
     2.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 14:27:23 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 15:03:31 2011 +0200
     2.3 @@ -123,6 +123,8 @@
     2.4      \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} \\
     2.5      \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} \\
     2.6      \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} \\
     2.7 +    \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
     2.8 +    \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
     2.9      \indexdef{}{method}{succeed}\hypertarget{method.succeed}{\hyperlink{method.succeed}{\mbox{\isa{succeed}}}} & : & \isa{method} \\
    2.10      \indexdef{}{method}{fail}\hypertarget{method.fail}{\hyperlink{method.fail}{\mbox{\isa{fail}}}} & : & \isa{method} \\
    2.11    \end{matharray}
    2.12 @@ -154,6 +156,17 @@
    2.13  \rail@endbar
    2.14  \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    2.15  \rail@end
    2.16 +\rail@begin{2}{}
    2.17 +\rail@bar
    2.18 +\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
    2.19 +\rail@nextbar{1}
    2.20 +\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
    2.21 +\rail@endbar
    2.22 +\rail@bar
    2.23 +\rail@nextbar{1}
    2.24 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    2.25 +\rail@endbar
    2.26 +\rail@end
    2.27  \end{railoutput}
    2.28  
    2.29  
    2.30 @@ -182,6 +195,12 @@
    2.31    the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method, with forward chaining of current
    2.32    facts.
    2.33  
    2.34 +  \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
    2.35 +  by intro- or elim-resolution, after having inserted any chained
    2.36 +  facts.  Exactly the rules given as arguments are taken into account;
    2.37 +  this allows fine-tuned decomposition of a proof problem, in contrast
    2.38 +  to common automated tools.
    2.39 +
    2.40    \item \hyperlink{method.succeed}{\mbox{\isa{succeed}}} yields a single (unchanged) result; it is
    2.41    the identity of the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}}'' method combinator (cf.\
    2.42    \secref{sec:proof-meth}).
    2.43 @@ -1311,6 +1330,48 @@
    2.44  \end{isamarkuptext}%
    2.45  \isamarkuptrue%
    2.46  %
    2.47 +\isamarkupsubsection{Structured methods%
    2.48 +}
    2.49 +\isamarkuptrue%
    2.50 +%
    2.51 +\begin{isamarkuptext}%
    2.52 +\begin{matharray}{rcl}
    2.53 +    \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
    2.54 +    \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
    2.55 +  \end{matharray}
    2.56 +
    2.57 +  \begin{railoutput}
    2.58 +\rail@begin{2}{}
    2.59 +\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
    2.60 +\rail@bar
    2.61 +\rail@nextbar{1}
    2.62 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    2.63 +\rail@endbar
    2.64 +\rail@end
    2.65 +\end{railoutput}
    2.66 +
    2.67 +
    2.68 +  \begin{description}
    2.69 +
    2.70 +  \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
    2.71 +  refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both
    2.72 +  versions work the same, but the classical version observes the
    2.73 +  classical rule context in addition to that of Isabelle/Pure.
    2.74 +
    2.75 +  Common object logics (HOL, ZF, etc.) declare a rich collection of
    2.76 +  classical rules (even if these would qualify as intuitionistic
    2.77 +  ones), but only few declarations to the rule context of
    2.78 +  Isabelle/Pure (\secref{sec:pure-meth-att}).
    2.79 +
    2.80 +  \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
    2.81 +  deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}.  Chained
    2.82 +  facts, which are guaranteed to participate, may appear in either
    2.83 +  order.
    2.84 +
    2.85 +  \end{description}%
    2.86 +\end{isamarkuptext}%
    2.87 +\isamarkuptrue%
    2.88 +%
    2.89  \isamarkupsubsection{Automated methods%
    2.90  }
    2.91  \isamarkuptrue%
    2.92 @@ -1610,62 +1671,6 @@
    2.93  \end{isamarkuptext}%
    2.94  \isamarkuptrue%
    2.95  %
    2.96 -\isamarkupsubsection{Structured proof methods%
    2.97 -}
    2.98 -\isamarkuptrue%
    2.99 -%
   2.100 -\begin{isamarkuptext}%
   2.101 -\begin{matharray}{rcl}
   2.102 -    \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
   2.103 -    \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
   2.104 -    \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
   2.105 -    \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
   2.106 -  \end{matharray}
   2.107 -
   2.108 -  \begin{railoutput}
   2.109 -\rail@begin{3}{}
   2.110 -\rail@bar
   2.111 -\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
   2.112 -\rail@nextbar{1}
   2.113 -\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
   2.114 -\rail@nextbar{2}
   2.115 -\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
   2.116 -\rail@endbar
   2.117 -\rail@bar
   2.118 -\rail@nextbar{1}
   2.119 -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
   2.120 -\rail@endbar
   2.121 -\rail@end
   2.122 -\end{railoutput}
   2.123 -
   2.124 -
   2.125 -  \begin{description}
   2.126 -
   2.127 -  \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
   2.128 -  refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both
   2.129 -  versions work the same, but the classical version observes the
   2.130 -  classical rule context in addition to that of Isabelle/Pure.
   2.131 -
   2.132 -  Common object logics (HOL, ZF, etc.) declare a rich collection of
   2.133 -  classical rules (even if these would qualify as intuitionistic
   2.134 -  ones), but only few declarations to the rule context of
   2.135 -  Isabelle/Pure (\secref{sec:pure-meth-att}).
   2.136 -
   2.137 -  \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
   2.138 -  deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}.  Chained
   2.139 -  facts, which are guaranteed to participate, may appear in either
   2.140 -  order.
   2.141 -
   2.142 -  \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
   2.143 -  by intro- or elim-resolution, after having inserted any chained
   2.144 -  facts.  Exactly the rules given as arguments are taken into account;
   2.145 -  this allows fine-tuned decomposition of a proof problem, in contrast
   2.146 -  to common automated tools.
   2.147 -
   2.148 -  \end{description}%
   2.149 -\end{isamarkuptext}%
   2.150 -\isamarkuptrue%
   2.151 -%
   2.152  \isamarkupsection{Object-logic setup \label{sec:object-logic}%
   2.153  }
   2.154  \isamarkuptrue%