493 @{method_def "fact"} & : & \isarmeth \\ |
493 @{method_def "fact"} & : & \isarmeth \\ |
494 @{method_def "assumption"} & : & \isarmeth \\ |
494 @{method_def "assumption"} & : & \isarmeth \\ |
495 @{method_def "this"} & : & \isarmeth \\ |
495 @{method_def "this"} & : & \isarmeth \\ |
496 @{method_def "rule"} & : & \isarmeth \\ |
496 @{method_def "rule"} & : & \isarmeth \\ |
497 @{method_def "iprover"} & : & \isarmeth \\[0.5ex] |
497 @{method_def "iprover"} & : & \isarmeth \\[0.5ex] |
498 @{attribute_def "intro"} & : & \isaratt \\ |
498 @{attribute_def (Pure) "intro"} & : & \isaratt \\ |
499 @{attribute_def "elim"} & : & \isaratt \\ |
499 @{attribute_def (Pure) "elim"} & : & \isaratt \\ |
500 @{attribute_def "dest"} & : & \isaratt \\ |
500 @{attribute_def (Pure) "dest"} & : & \isaratt \\ |
501 @{attribute_def "rule"} & : & \isaratt \\[0.5ex] |
501 @{attribute_def "rule"} & : & \isaratt \\[0.5ex] |
502 @{attribute_def "OF"} & : & \isaratt \\ |
502 @{attribute_def "OF"} & : & \isaratt \\ |
503 @{attribute_def "of"} & : & \isaratt \\ |
503 @{attribute_def "of"} & : & \isaratt \\ |
504 @{attribute_def "where"} & : & \isaratt \\ |
504 @{attribute_def "where"} & : & \isaratt \\ |
505 \end{matharray} |
505 \end{matharray} |
563 without facts is plain introduction, while with facts it becomes |
563 without facts is plain introduction, while with facts it becomes |
564 elimination. |
564 elimination. |
565 |
565 |
566 When no arguments are given, the @{method rule} method tries to pick |
566 When no arguments are given, the @{method rule} method tries to pick |
567 appropriate rules automatically, as declared in the current context |
567 appropriate rules automatically, as declared in the current context |
568 using the @{attribute intro}, @{attribute elim}, @{attribute dest} |
568 using the @{attribute (Pure) intro}, @{attribute (Pure) elim}, |
569 attributes (see below). This is the default behavior of @{command |
569 @{attribute (Pure) dest} attributes (see below). This is the |
570 "proof"} and ``@{command ".."}'' (double-dot) steps (see |
570 default behavior of @{command "proof"} and ``@{command ".."}'' |
571 \secref{sec:proof-steps}). |
571 (double-dot) steps (see \secref{sec:proof-steps}). |
572 |
572 |
573 \item [@{method iprover}] performs intuitionistic proof search, |
573 \item [@{method iprover}] performs intuitionistic proof search, |
574 depending on specifically declared rules from the context, or given |
574 depending on specifically declared rules from the context, or given |
575 as explicit arguments. Chained facts are inserted into the goal |
575 as explicit arguments. Chained facts are inserted into the goal |
576 before commencing proof search; ``@{method iprover}@{text "!"}'' |
576 before commencing proof search; ``@{method iprover}@{text "!"}'' |
577 means to include the current @{fact prems} as well. |
577 means to include the current @{fact prems} as well. |
578 |
578 |
579 Rules need to be classified as @{attribute intro}, @{attribute |
579 Rules need to be classified as @{attribute (Pure) intro}, |
580 elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator |
580 @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the |
581 refers to ``safe'' rules, which may be applied aggressively (without |
581 ``@{text "!"}'' indicator refers to ``safe'' rules, which may be |
582 considering back-tracking later). Rules declared with ``@{text |
582 applied aggressively (without considering back-tracking later). |
583 "?"}'' are ignored in proof search (the single-step @{method rule} |
583 Rules declared with ``@{text "?"}'' are ignored in proof search (the |
584 method still observes these). An explicit weight annotation may be |
584 single-step @{method rule} method still observes these). An |
585 given as well; otherwise the number of rule premises will be taken |
585 explicit weight annotation may be given as well; otherwise the |
586 into account here. |
586 number of rule premises will be taken into account here. |
587 |
587 |
588 \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}] |
588 \item [@{attribute (Pure) intro}, @{attribute (Pure) elim}, and |
589 declare introduction, elimination, and destruct rules, to be used |
589 @{attribute (Pure) dest}] declare introduction, elimination, and |
590 with the @{method rule} and @{method iprover} methods. Note that |
590 destruct rules, to be used with the @{method rule} and @{method |
591 the latter will ignore rules declared with ``@{text "?"}'', while |
591 iprover} methods. Note that the latter will ignore rules declared |
592 ``@{text "!"}'' are used most aggressively. |
592 with ``@{text "?"}'', while ``@{text "!"}'' are used most |
|
593 aggressively. |
593 |
594 |
594 The classical reasoner (see \secref{sec:classical}) introduces its |
595 The classical reasoner (see \secref{sec:classical}) introduces its |
595 own variants of these attributes; use qualified names to access the |
596 own variants of these attributes; use qualified names to access the |
596 present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}. |
597 present versions of Isabelle/Pure, i.e.\ @{attribute (Pure) |
|
598 "Pure.intro"}. |
597 |
599 |
598 \item [@{attribute rule}~@{text del}] undeclares introduction, |
600 \item [@{attribute rule}~@{text del}] undeclares introduction, |
599 elimination, or destruct rules. |
601 elimination, or destruct rules. |
600 |
602 |
601 \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some |
603 \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some |