1.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon May 02 20:14:19 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon May 02 20:34:34 2011 +0200
1.3 @@ -445,7 +445,7 @@
1.4 facts in order to establish the goal to be claimed next. The
1.5 initial proof method invoked to refine that will be offered the
1.6 facts to do ``anything appropriate'' (see also
1.7 - \secref{sec:proof-steps}). For example, method \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}
1.8 + \secref{sec:proof-steps}). For example, method \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}
1.9 (see \secref{sec:pure-meth-att}) would typically do an elimination
1.10 rather than an introduction. Automatic methods usually insert the
1.11 facts into the goal state before operation. This provides a simple
1.12 @@ -472,7 +472,7 @@
1.13 effect apart from entering \isa{{\isaliteral{22}{\isachardoublequote}}prove{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} mode, since
1.14 \indexref{}{fact}{nothing}\hyperlink{fact.nothing}{\mbox{\isa{nothing}}} is bound to the empty list of theorems.
1.15
1.16 - Basic proof methods (such as \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}) expect multiple
1.17 + Basic proof methods (such as \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}) expect multiple
1.18 facts to be given in their proper order, corresponding to a prefix
1.19 of the premises of the rule involved. Note that positions may be
1.20 easily skipped using something like \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ b{\isaliteral{22}{\isachardoublequote}}}, for example. This involves the trivial rule
1.21 @@ -843,10 +843,10 @@
1.22 an intelligible manner.
1.23
1.24 Unless given explicitly by the user, the default initial method is
1.25 - ``\indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}'', which applies a single standard elimination
1.26 - or introduction rule according to the topmost symbol involved.
1.27 - There is no separate default terminal method. Any remaining goals
1.28 - are always solved by assumption in the very last step.
1.29 + \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} (or its classical variant \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}), which applies a single standard elimination or introduction
1.30 + rule according to the topmost symbol involved. There is no separate
1.31 + default terminal method. Any remaining goals are always solved by
1.32 + assumption in the very last step.
1.33
1.34 \begin{railoutput}
1.35 \rail@begin{2}{\isa{}}
1.36 @@ -943,11 +943,11 @@
1.37 \indexdef{}{method}{fact}\hypertarget{method.fact}{\hyperlink{method.fact}{\mbox{\isa{fact}}}} & : & \isa{method} \\
1.38 \indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\
1.39 \indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\
1.40 - \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
1.41 + \indexdef{Pure}{method}{rule}\hypertarget{method.Pure.rule}{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
1.42 \indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
1.43 \indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
1.44 \indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
1.45 - \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\[0.5ex]
1.46 + \indexdef{Pure}{attribute}{rule}\hypertarget{attribute.Pure.rule}{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\[0.5ex]
1.47 \indexdef{}{attribute}{OF}\hypertarget{attribute.OF}{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}} & : & \isa{attribute} \\
1.48 \indexdef{}{attribute}{of}\hypertarget{attribute.of}{\hyperlink{attribute.of}{\mbox{\isa{of}}}} & : & \isa{attribute} \\
1.49 \indexdef{}{attribute}{where}\hypertarget{attribute.where}{\hyperlink{attribute.where}{\mbox{\isa{where}}}} & : & \isa{attribute} \\
1.50 @@ -962,7 +962,7 @@
1.51 \rail@endbar
1.52 \rail@end
1.53 \rail@begin{2}{\isa{}}
1.54 -\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
1.55 +\rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[]
1.56 \rail@bar
1.57 \rail@nextbar{1}
1.58 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1.59 @@ -1013,7 +1013,7 @@
1.60 \rail@endbar
1.61 \rail@end
1.62 \rail@begin{1}{\isa{}}
1.63 -\rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
1.64 +\rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[]
1.65 \rail@term{\isa{del}}[]
1.66 \rail@end
1.67 \rail@begin{1}{\isa{}}
1.68 @@ -1063,7 +1063,7 @@
1.69 \item ``\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}'' (minus) does nothing but insert the forward
1.70 chaining facts as premises into the goal. Note that command
1.71 \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} without any method actually performs a single
1.72 - reduction step using the \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}} method; thus a plain
1.73 + reduction step using the \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method; thus a plain
1.74 \emph{do-nothing} proof step would be ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' rather than \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} alone.
1.75
1.76 \item \hyperlink{method.fact}{\mbox{\isa{fact}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} composes some fact from
1.77 @@ -1086,12 +1086,12 @@
1.78 \item \hyperlink{method.this}{\mbox{\isa{this}}} applies all of the current facts directly as
1.79 rules. Recall that ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' (dot) abbreviates ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{this}''.
1.80
1.81 - \item \hyperlink{method.rule}{\mbox{\isa{rule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some rule given as
1.82 + \item \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some rule given as
1.83 argument in backward manner; facts are used to reduce the rule
1.84 - before applying it to the goal. Thus \hyperlink{method.rule}{\mbox{\isa{rule}}} without facts
1.85 + before applying it to the goal. Thus \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} without facts
1.86 is plain introduction, while with facts it becomes elimination.
1.87
1.88 - When no arguments are given, the \hyperlink{method.rule}{\mbox{\isa{rule}}} method tries to pick
1.89 + When no arguments are given, the \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method tries to pick
1.90 appropriate rules automatically, as declared in the current context
1.91 using the \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}},
1.92 \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} attributes (see below). This is the
1.93 @@ -1100,7 +1100,7 @@
1.94
1.95 \item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
1.96 \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and
1.97 - destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar
1.98 + destruct rules, to be used with method \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}, and similar
1.99 tools. Note that the latter will ignore rules declared with
1.100 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'', while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' are used most aggressively.
1.101
1.102 @@ -1108,7 +1108,7 @@
1.103 own variants of these attributes; use qualified names to access the
1.104 present versions of Isabelle/Pure, i.e.\ \hyperlink{attribute.Pure.Pure.intro}{\mbox{\isa{Pure{\isaliteral{2E}{\isachardot}}intro}}}.
1.105
1.106 - \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
1.107 + \item \hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
1.108 elimination, or destruct rules.
1.109
1.110 \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some