--- a/doc-src/IsarRef/Thy/Generic.thy Sat Jun 04 22:09:42 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Sun Jun 05 20:15:47 2011 +0200
@@ -773,6 +773,111 @@
*}
+subsection {* Rule declarations *}
+
+text {* The proof tools of the Classical Reasoner depend on
+ collections of rules declared in the context, which are classified
+ as introduction, elimination or destruction and as \emph{safe} or
+ \emph{unsafe}. In general, safe rules can be attempted blindly,
+ while unsafe rules must be used with care. A safe rule must never
+ reduce a provable goal to an unprovable set of subgoals.
+
+ The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P
+ \<or> Q"} to @{text "P"}, which might turn out as premature choice of an
+ unprovable subgoal. Any rule is unsafe whose premises contain new
+ unknowns. The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is
+ unsafe, since it is applied via elim-resolution, which discards the
+ assumption @{text "\<forall>x. P x"} and replaces it by the weaker
+ assumption @{text "P t"}. The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is
+ unsafe for similar reasons. The quantifier duplication rule @{text
+ "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense:
+ since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to
+ looping. In classical first-order logic, all rules are safe except
+ those mentioned above.
+
+ The safe~/ unsafe distinction is vague, and may be regarded merely
+ as a way of giving some rules priority over others. One could argue
+ that @{text "(\<or>E)"} is unsafe, because repeated application of it
+ could generate exponentially many subgoals. Induction rules are
+ unsafe because inductive proofs are difficult to set up
+ automatically. Any inference is unsafe that instantiates an unknown
+ in the proof state --- thus matching must be used, rather than
+ unification. Even proof by assumption is unsafe if it instantiates
+ unknowns shared with other subgoals.
+
+ \begin{matharray}{rcl}
+ @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{attribute_def intro} & : & @{text attribute} \\
+ @{attribute_def elim} & : & @{text attribute} \\
+ @{attribute_def dest} & : & @{text attribute} \\
+ @{attribute_def rule} & : & @{text attribute} \\
+ @{attribute_def iff} & : & @{text attribute} \\
+ @{attribute_def swapped} & : & @{text attribute} \\
+ \end{matharray}
+
+ @{rail "
+ (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
+ ;
+ @@{attribute rule} 'del'
+ ;
+ @@{attribute iff} (((() | 'add') '?'?) | 'del')
+ "}
+
+ \begin{description}
+
+ \item @{command "print_claset"} prints the collection of rules
+ declared to the Classical Reasoner, i.e.\ the @{ML_type claset}
+ within the context.
+
+ \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
+ declare introduction, elimination, and destruction rules,
+ respectively. By default, rules are considered as \emph{unsafe}
+ (i.e.\ not applied blindly without backtracking), while ``@{text
+ "!"}'' classifies as \emph{safe}. Rule declarations marked by
+ ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
+ \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
+ of the @{method rule} method). The optional natural number
+ specifies an explicit weight argument, which is ignored by the
+ automated reasoning tools, but determines the search order of single
+ rule steps.
+
+ Introduction rules are those that can be applied using ordinary
+ resolution. Their swapped forms are generated internally, which
+ will be applied using elim-resolution. Elimination rules are
+ applied using elim-resolution. Rules are sorted by the number of
+ new subgoals they will yield; rules that generate the fewest
+ subgoals will be tried first. Otherwise, later declarations take
+ precedence over earlier ones.
+
+ Rules already present in the context with the same classification
+ are ignored. A warning is printed if the rule has already been
+ added with some other classification, but the rule is added anyway
+ as requested.
+
+ \item @{attribute rule}~@{text del} deletes all occurrences of a
+ rule from the classical context, regardless of its classification as
+ introduction~/ elimination~/ destruction and safe~/ unsafe.
+
+ \item @{attribute iff} declares logical equivalences to the
+ Simplifier and the Classical reasoner at the same time.
+ Non-conditional rules result in a safe introduction and elimination
+ pair; conditional ones are considered unsafe. Rules with negative
+ conclusion are automatically inverted (using @{text "\<not>"}-elimination
+ internally).
+
+ The ``@{text "?"}'' version of @{attribute iff} declares rules to
+ the Isabelle/Pure context only, and omits the Simplifier
+ declaration.
+
+ \item @{attribute swapped} turns an introduction rule into an
+ elimination, by resolving with the classical swap principle @{text
+ "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position. This is mainly for
+ illustrative purposes: the Classical Reasoner already swaps rules
+ internally as explained above.
+
+ \end{description} *}
+
+
subsection {* Basic methods *}
text {*
@@ -904,78 +1009,6 @@
*}
-subsection {* Declaring rules *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{attribute_def intro} & : & @{text attribute} \\
- @{attribute_def elim} & : & @{text attribute} \\
- @{attribute_def dest} & : & @{text attribute} \\
- @{attribute_def rule} & : & @{text attribute} \\
- @{attribute_def iff} & : & @{text attribute} \\
- \end{matharray}
-
- @{rail "
- (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
- ;
- @@{attribute rule} 'del'
- ;
- @@{attribute iff} (((() | 'add') '?'?) | 'del')
- "}
-
- \begin{description}
-
- \item @{command "print_claset"} prints the collection of rules
- declared to the Classical Reasoner, which is also known as
- ``claset'' internally \cite{isabelle-ref}.
-
- \item @{attribute intro}, @{attribute elim}, and @{attribute dest}
- declare introduction, elimination, and destruction rules,
- respectively. By default, rules are considered as \emph{unsafe}
- (i.e.\ not applied blindly without backtracking), while ``@{text
- "!"}'' classifies as \emph{safe}. Rule declarations marked by
- ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\
- \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
- of the @{method rule} method). The optional natural number
- specifies an explicit weight argument, which is ignored by automated
- tools, but determines the search order of single rule steps.
-
- \item @{attribute rule}~@{text del} deletes introduction,
- elimination, or destruction rules from the context.
-
- \item @{attribute iff} declares logical equivalences to the
- Simplifier and the Classical reasoner at the same time.
- Non-conditional rules result in a ``safe'' introduction and
- elimination pair; conditional ones are considered ``unsafe''. Rules
- with negative conclusion are automatically inverted (using @{text
- "\<not>"}-elimination internally).
-
- The ``@{text "?"}'' version of @{attribute iff} declares rules to
- the Isabelle/Pure context only, and omits the Simplifier
- declaration.
-
- \end{description}
-*}
-
-
-subsection {* Classical operations *}
-
-text {*
- \begin{matharray}{rcl}
- @{attribute_def swapped} & : & @{text attribute} \\
- \end{matharray}
-
- \begin{description}
-
- \item @{attribute swapped} turns an introduction rule into an
- elimination, by resolving with the classical swap principle @{text
- "(\<not> B \<Longrightarrow> A) \<Longrightarrow> (\<not> A \<Longrightarrow> B)"}.
-
- \end{description}
-*}
-
-
section {* Object-logic setup \label{sec:object-logic} *}
text {*
--- a/doc-src/IsarRef/Thy/document/Generic.tex Sat Jun 04 22:09:42 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sun Jun 05 20:15:47 2011 +0200
@@ -1172,6 +1172,145 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Rule declarations%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The proof tools of the Classical Reasoner depend on
+ collections of rules declared in the context, which are classified
+ as introduction, elimination or destruction and as \emph{safe} or
+ \emph{unsafe}. In general, safe rules can be attempted blindly,
+ while unsafe rules must be used with care. A safe rule must never
+ reduce a provable goal to an unprovable set of subgoals.
+
+ The rule \isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} is unsafe because it reduces \isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} to \isa{{\isaliteral{22}{\isachardoublequote}}P{\isaliteral{22}{\isachardoublequote}}}, which might turn out as premature choice of an
+ unprovable subgoal. Any rule is unsafe whose premises contain new
+ unknowns. The elimination rule \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}} is
+ unsafe, since it is applied via elim-resolution, which discards the
+ assumption \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}} and replaces it by the weaker
+ assumption \isa{{\isaliteral{22}{\isachardoublequote}}P\ t{\isaliteral{22}{\isachardoublequote}}}. The rule \isa{{\isaliteral{22}{\isachardoublequote}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}} is
+ unsafe for similar reasons. The quantifier duplication rule \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequote}}} is unsafe in a different sense:
+ since it keeps the assumption \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequote}}}, it is prone to
+ looping. In classical first-order logic, all rules are safe except
+ those mentioned above.
+
+ The safe~/ unsafe distinction is vague, and may be regarded merely
+ as a way of giving some rules priority over others. One could argue
+ that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F723E}{\isasymor}}E{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is unsafe, because repeated application of it
+ could generate exponentially many subgoals. Induction rules are
+ unsafe because inductive proofs are difficult to set up
+ automatically. Any inference is unsafe that instantiates an unknown
+ in the proof state --- thus matching must be used, rather than
+ unification. Even proof by assumption is unsafe if it instantiates
+ unknowns shared with other subgoals.
+
+ \begin{matharray}{rcl}
+ \indexdef{}{command}{print\_claset}\hypertarget{command.print-claset}{\hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
+ \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
+ \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
+ \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\
+ \indexdef{}{attribute}{iff}\hypertarget{attribute.iff}{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}} & : & \isa{attribute} \\
+ \indexdef{}{attribute}{swapped}\hypertarget{attribute.swapped}{\hyperlink{attribute.swapped}{\mbox{\isa{swapped}}}} & : & \isa{attribute} \\
+ \end{matharray}
+
+ \begin{railoutput}
+\rail@begin{3}{}
+\rail@bar
+\rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}}[]
+\rail@nextbar{2}
+\rail@term{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}}[]
+\rail@endbar
+\rail@bar
+\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
+\rail@nextbar{1}
+\rail@nextbar{2}
+\rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
+\rail@endbar
+\rail@end
+\rail@begin{1}{}
+\rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
+\rail@term{\isa{del}}[]
+\rail@end
+\rail@begin{3}{}
+\rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[]
+\rail@bar
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{add}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
+\rail@endbar
+\rail@nextbar{2}
+\rail@term{\isa{del}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+ \begin{description}
+
+ \item \hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}} prints the collection of rules
+ declared to the Classical Reasoner, i.e.\ the \verb|claset|
+ within the context.
+
+ \item \hyperlink{attribute.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.dest}{\mbox{\isa{dest}}}
+ declare introduction, elimination, and destruction rules,
+ respectively. By default, rules are considered as \emph{unsafe}
+ (i.e.\ not applied blindly without backtracking), while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' classifies as \emph{safe}. Rule declarations marked by
+ ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' coincide with those of Isabelle/Pure, cf.\
+ \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
+ of the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). The optional natural number
+ specifies an explicit weight argument, which is ignored by the
+ automated reasoning tools, but determines the search order of single
+ rule steps.
+
+ Introduction rules are those that can be applied using ordinary
+ resolution. Their swapped forms are generated internally, which
+ will be applied using elim-resolution. Elimination rules are
+ applied using elim-resolution. Rules are sorted by the number of
+ new subgoals they will yield; rules that generate the fewest
+ subgoals will be tried first. Otherwise, later declarations take
+ precedence over earlier ones.
+
+ Rules already present in the context with the same classification
+ are ignored. A warning is printed if the rule has already been
+ added with some other classification, but the rule is added anyway
+ as requested.
+
+ \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} deletes all occurrences of a
+ rule from the classical context, regardless of its classification as
+ introduction~/ elimination~/ destruction and safe~/ unsafe.
+
+ \item \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares logical equivalences to the
+ Simplifier and the Classical reasoner at the same time.
+ Non-conditional rules result in a safe introduction and elimination
+ pair; conditional ones are considered unsafe. Rules with negative
+ conclusion are automatically inverted (using \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{22}{\isachardoublequote}}}-elimination
+ internally).
+
+ The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' version of \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares rules to
+ the Isabelle/Pure context only, and omits the Simplifier
+ declaration.
+
+ \item \hyperlink{attribute.swapped}{\mbox{\isa{swapped}}} turns an introduction rule into an
+ elimination, by resolving with the classical swap principle \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ R\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequote}}} in the second position. This is mainly for
+ illustrative purposes: the Classical Reasoner already swaps rules
+ internally as explained above.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Basic methods%
}
\isamarkuptrue%
@@ -1439,113 +1578,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Declaring rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{print\_claset}\hypertarget{command.print-claset}{\hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{}{attribute}{intro}\hypertarget{attribute.intro}{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
- \indexdef{}{attribute}{elim}\hypertarget{attribute.elim}{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
- \indexdef{}{attribute}{dest}\hypertarget{attribute.dest}{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
- \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\
- \indexdef{}{attribute}{iff}\hypertarget{attribute.iff}{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}} & : & \isa{attribute} \\
- \end{matharray}
-
- \begin{railoutput}
-\rail@begin{3}{}
-\rail@bar
-\rail@term{\hyperlink{attribute.intro}{\mbox{\isa{intro}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{attribute.elim}{\mbox{\isa{elim}}}}[]
-\rail@nextbar{2}
-\rail@term{\hyperlink{attribute.dest}{\mbox{\isa{dest}}}}[]
-\rail@endbar
-\rail@bar
-\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
-\rail@nextbar{1}
-\rail@nextbar{2}
-\rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
-\rail@endbar
-\rail@end
-\rail@begin{1}{}
-\rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
-\rail@term{\isa{del}}[]
-\rail@end
-\rail@begin{3}{}
-\rail@term{\hyperlink{attribute.iff}{\mbox{\isa{iff}}}}[]
-\rail@bar
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{add}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
-\rail@endbar
-\rail@nextbar{2}
-\rail@term{\isa{del}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}
-
-
- \begin{description}
-
- \item \hyperlink{command.print-claset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}claset}}}} prints the collection of rules
- declared to the Classical Reasoner, which is also known as
- ``claset'' internally \cite{isabelle-ref}.
-
- \item \hyperlink{attribute.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.elim}{\mbox{\isa{elim}}}, and \hyperlink{attribute.dest}{\mbox{\isa{dest}}}
- declare introduction, elimination, and destruction rules,
- respectively. By default, rules are considered as \emph{unsafe}
- (i.e.\ not applied blindly without backtracking), while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' classifies as \emph{safe}. Rule declarations marked by
- ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' coincide with those of Isabelle/Pure, cf.\
- \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps
- of the \hyperlink{method.rule}{\mbox{\isa{rule}}} method). The optional natural number
- specifies an explicit weight argument, which is ignored by automated
- tools, but determines the search order of single rule steps.
-
- \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} deletes introduction,
- elimination, or destruction rules from the context.
-
- \item \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares logical equivalences to the
- Simplifier and the Classical reasoner at the same time.
- Non-conditional rules result in a ``safe'' introduction and
- elimination pair; conditional ones are considered ``unsafe''. Rules
- with negative conclusion are automatically inverted (using \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{22}{\isachardoublequote}}}-elimination internally).
-
- The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' version of \hyperlink{attribute.iff}{\mbox{\isa{iff}}} declares rules to
- the Isabelle/Pure context only, and omits the Simplifier
- declaration.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Classical operations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{attribute}{swapped}\hypertarget{attribute.swapped}{\hyperlink{attribute.swapped}{\mbox{\isa{swapped}}}} & : & \isa{attribute} \\
- \end{matharray}
-
- \begin{description}
-
- \item \hyperlink{attribute.swapped}{\mbox{\isa{swapped}}} turns an introduction rule into an
- elimination, by resolving with the classical swap principle \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Object-logic setup \label{sec:object-logic}%
}
\isamarkuptrue%
--- a/doc-src/Ref/classical.tex Sat Jun 04 22:09:42 2011 +0200
+++ b/doc-src/Ref/classical.tex Sun Jun 05 20:15:47 2011 +0200
@@ -5,110 +5,6 @@
\section{Classical rule sets}
\index{classical sets}
-Each automatic tactic takes a {\bf classical set} --- a collection of
-rules, classified as introduction or elimination and as {\bf safe} or {\bf
-unsafe}. In general, safe rules can be attempted blindly, while unsafe
-rules must be used with care. A safe rule must never reduce a provable
-goal to an unprovable set of subgoals.
-
-The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any
-rule is unsafe whose premises contain new unknowns. The elimination
-rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
-which discards the assumption $\forall x{.}P(x)$ and replaces it by the
-weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for
-similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense:
-since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
-In classical first-order logic, all rules are safe except those mentioned
-above.
-
-The safe/unsafe distinction is vague, and may be regarded merely as a way
-of giving some rules priority over others. One could argue that
-$({\disj}E)$ is unsafe, because repeated application of it could generate
-exponentially many subgoals. Induction rules are unsafe because inductive
-proofs are difficult to set up automatically. Any inference is unsafe that
-instantiates an unknown in the proof state --- thus \ttindex{match_tac}
-must be used, rather than \ttindex{resolve_tac}. Even proof by assumption
-is unsafe if it instantiates unknowns shared with other subgoals --- thus
-\ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
-
-\subsection{Adding rules to classical sets}
-Classical rule sets belong to the abstract type \mltydx{claset}, which
-supports the following operations (provided the classical reasoner is
-installed!):
-\begin{ttbox}
-empty_cs : claset
-print_cs : claset -> unit
-rep_cs : claset -> \{safeEs: thm list, safeIs: thm list,
- hazEs: thm list, hazIs: thm list,
- swrappers: (string * wrapper) list,
- uwrappers: (string * wrapper) list,
- safe0_netpair: netpair, safep_netpair: netpair,
- haz_netpair: netpair, dup_netpair: netpair\}
-addSIs : claset * thm list -> claset \hfill{\bf infix 4}
-addSEs : claset * thm list -> claset \hfill{\bf infix 4}
-addSDs : claset * thm list -> claset \hfill{\bf infix 4}
-addIs : claset * thm list -> claset \hfill{\bf infix 4}
-addEs : claset * thm list -> claset \hfill{\bf infix 4}
-addDs : claset * thm list -> claset \hfill{\bf infix 4}
-delrules : claset * thm list -> claset \hfill{\bf infix 4}
-\end{ttbox}
-The add operations ignore any rule already present in the claset with the same
-classification (such as safe introduction). They print a warning if the rule
-has already been added with some other classification, but add the rule
-anyway. Calling \texttt{delrules} deletes all occurrences of a rule from the
-claset, but see the warning below concerning destruction rules.
-\begin{ttdescription}
-\item[\ttindexbold{empty_cs}] is the empty classical set.
-
-\item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$,
- which is the rules. All other parts are non-printable.
-
-\item[\ttindexbold{rep_cs} $cs$] decomposes $cs$ as a record of its internal
- components, namely the safe introduction and elimination rules, the unsafe
- introduction and elimination rules, the lists of safe and unsafe wrappers
- (see \ref{sec:modifying-search}), and the internalized forms of the rules.
-
-\item[$cs$ addSIs $rules$] \indexbold{*addSIs}
-adds safe introduction~$rules$ to~$cs$.
-
-\item[$cs$ addSEs $rules$] \indexbold{*addSEs}
-adds safe elimination~$rules$ to~$cs$.
-
-\item[$cs$ addSDs $rules$] \indexbold{*addSDs}
-adds safe destruction~$rules$ to~$cs$.
-
-\item[$cs$ addIs $rules$] \indexbold{*addIs}
-adds unsafe introduction~$rules$ to~$cs$.
-
-\item[$cs$ addEs $rules$] \indexbold{*addEs}
-adds unsafe elimination~$rules$ to~$cs$.
-
-\item[$cs$ addDs $rules$] \indexbold{*addDs}
-adds unsafe destruction~$rules$ to~$cs$.
-
-\item[$cs$ delrules $rules$] \indexbold{*delrules}
-deletes~$rules$ from~$cs$. It prints a warning for those rules that are not
-in~$cs$.
-\end{ttdescription}
-
-\begin{warn}
- If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete
- it as follows:
-\begin{ttbox}
-\(cs\) delrules [make_elim \(rule\)]
-\end{ttbox}
-\par\noindent
-This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert
-the destruction rules to elimination rules by applying \ttindex{make_elim},
-and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively.
-\end{warn}
-
-Introduction rules are those that can be applied using ordinary resolution.
-The classical set automatically generates their swapped forms, which will
-be applied using elim-resolution. Elimination rules are applied using
-elim-resolution. In a classical set, rules are sorted by the number of new
-subgoals they will yield; rules that generate the fewest subgoals will be
-tried first (see {\S}\ref{biresolve_tac}).
For elimination and destruction rules there are variants of the add operations
adding a rule in a way such that it is applied only if also its second premise