# HG changeset patch # User wenzelm # Date 1307297747 -7200 # Node ID 9d946de4112094a2d70d2c8db3c7c79e0233164d # Parent c40adab7568e33f9a1bdf4570f7d8251e13f0649 updated and re-unified classical rule declarations; diff -r c40adab7568e -r 9d946de41120 doc-src/IsarRef/Thy/Generic.thy --- 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 \ P \ Q"} is unsafe because it reduces @{text "P + \ 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 "\x. P x \ (P t \ Q) \ Q"} is + unsafe, since it is applied via elim-resolution, which discards the + assumption @{text "\x. P x"} and replaces it by the weaker + assumption @{text "P t"}. The rule @{text "P t \ \x. P x"} is + unsafe for similar reasons. The quantifier duplication rule @{text + "\x. P x \ (P t \ \x. P x \ Q) \ Q"} is unsafe in a different sense: + since it keeps the assumption @{text "\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 "(\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 \"} \\ + @{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 "\"}-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 + "\ P \ (\ R \ P) \ 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 \"} \\ - @{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 - "\"}-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 - "(\ B \ A) \ (\ A \ B)"}. - - \end{description} -*} - - section {* Object-logic setup \label{sec:object-logic} *} text {* diff -r c40adab7568e -r 9d946de41120 doc-src/IsarRef/Thy/document/Generic.tex --- 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% diff -r c40adab7568e -r 9d946de41120 doc-src/Ref/classical.tex --- 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