--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Feb 28 16:39:46 2009 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Feb 28 16:48:27 2009 +0100
@@ -771,6 +771,35 @@
*}
+section {* Intuitionistic proof search *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{method_def (HOL) "iprover"} & : & @{text method} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'iprover' ('!' ?) (rulemod *)
+ ;
+ \end{rail}
+
+ The @{method iprover} method performs intuitionistic proof search,
+ depending on specifically declared rules from the context, or given
+ as explicit arguments. Chained facts are inserted into the goal
+ before commencing proof search; ``@{method iprover}@{text "!"}''
+ means to include the current @{fact prems} as well.
+
+ Rules need to be classified as @{attribute (Pure) intro},
+ @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
+ ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
+ applied aggressively (without considering back-tracking later).
+ Rules declared with ``@{text "?"}'' are ignored in proof search (the
+ single-step @{method rule} method still observes these). An
+ explicit weight annotation may be given as well; otherwise the
+ number of rule premises will be taken into account here.
+*}
+
+
section {* Invoking automated reasoning tools -- The Sledgehammer *}
text {*
--- a/doc-src/IsarRef/Thy/Proof.thy Sat Feb 28 16:39:46 2009 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy Sat Feb 28 16:48:27 2009 +0100
@@ -683,7 +683,6 @@
@{method_def "assumption"} & : & @{text method} \\
@{method_def "this"} & : & @{text method} \\
@{method_def "rule"} & : & @{text method} \\
- @{method_def "iprover"} & : & @{text method} \\[0.5ex]
@{attribute_def (Pure) "intro"} & : & @{text attribute} \\
@{attribute_def (Pure) "elim"} & : & @{text attribute} \\
@{attribute_def (Pure) "dest"} & : & @{text attribute} \\
@@ -698,8 +697,6 @@
;
'rule' thmrefs?
;
- 'iprover' ('!' ?) (rulemod *)
- ;
rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
;
('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
@@ -758,27 +755,11 @@
default behavior of @{command "proof"} and ``@{command ".."}''
(double-dot) steps (see \secref{sec:proof-steps}).
- \item @{method iprover} performs intuitionistic proof search,
- depending on specifically declared rules from the context, or given
- as explicit arguments. Chained facts are inserted into the goal
- before commencing proof search; ``@{method iprover}@{text "!"}''
- means to include the current @{fact prems} as well.
-
- Rules need to be classified as @{attribute (Pure) intro},
- @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
- ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
- applied aggressively (without considering back-tracking later).
- Rules declared with ``@{text "?"}'' are ignored in proof search (the
- single-step @{method rule} method still observes these). An
- explicit weight annotation may be given as well; otherwise the
- number of rule premises will be taken into account here.
-
\item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
@{attribute (Pure) dest} declare introduction, elimination, and
- destruct rules, to be used with the @{method rule} and @{method
- iprover} methods. Note that the latter will ignore rules declared
- with ``@{text "?"}'', while ``@{text "!"}'' are used most
- aggressively.
+ destruct rules, to be used with method @{method rule}, and similar
+ tools. Note that the latter will ignore rules declared with
+ ``@{text "?"}'', while ``@{text "!"}'' are used most aggressively.
The classical reasoner (see \secref{sec:classical}) introduces its
own variants of these attributes; use qualified names to access the