519 The @{text "method"} category is essentially a parameter and may be |
519 The @{text "method"} category is essentially a parameter and may be |
520 populated later. Methods use the facts indicated by @{command |
520 populated later. Methods use the facts indicated by @{command |
521 "then"} or @{command using}, and then operate on the goal state. |
521 "then"} or @{command using}, and then operate on the goal state. |
522 Some basic methods are predefined: ``@{method "-"}'' leaves the goal |
522 Some basic methods are predefined: ``@{method "-"}'' leaves the goal |
523 unchanged, ``@{method this}'' applies the facts as rules to the |
523 unchanged, ``@{method this}'' applies the facts as rules to the |
524 goal, ``@{method "rule"}'' applies the facts to another rule and the |
524 goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and the |
525 result to the goal (both ``@{method this}'' and ``@{method rule}'' |
525 result to the goal (both ``@{method this}'' and ``@{method (Pure) rule}'' |
526 refer to @{inference resolution} of |
526 refer to @{inference resolution} of |
527 \secref{sec:framework-resolution}). The secondary arguments to |
527 \secref{sec:framework-resolution}). The secondary arguments to |
528 ``@{method rule}'' may be specified explicitly as in ``@{text "(rule |
528 ``@{method (Pure) rule}'' may be specified explicitly as in ``@{text "(rule |
529 a)"}'', or picked from the context. In the latter case, the system |
529 a)"}'', or picked from the context. In the latter case, the system |
530 first tries rules declared as @{attribute (Pure) elim} or |
530 first tries rules declared as @{attribute (Pure) elim} or |
531 @{attribute (Pure) dest}, followed by those declared as @{attribute |
531 @{attribute (Pure) dest}, followed by those declared as @{attribute |
532 (Pure) intro}. |
532 (Pure) intro}. |
533 |
533 |
534 The default method for @{command proof} is ``@{method rule}'' |
534 The default method for @{command proof} is ``@{method (Pure) rule}'' |
535 (arguments picked from the context), for @{command qed} it is |
535 (arguments picked from the context), for @{command qed} it is |
536 ``@{method "-"}''. Further abbreviations for terminal proof steps |
536 ``@{method "-"}''. Further abbreviations for terminal proof steps |
537 are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for |
537 are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for |
538 ``@{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text |
538 ``@{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text |
539 "method\<^sub>2"}'', and ``@{command ".."}'' for ``@{command |
539 "method\<^sub>2"}'', and ``@{command ".."}'' for ``@{command |
540 "by"}~@{method rule}, and ``@{command "."}'' for ``@{command |
540 "by"}~@{method (Pure) rule}, and ``@{command "."}'' for ``@{command |
541 "by"}~@{method this}''. The @{command unfolding} element operates |
541 "by"}~@{method this}''. The @{command unfolding} element operates |
542 directly on the current facts and goal by applying equalities. |
542 directly on the current facts and goal by applying equalities. |
543 |
543 |
544 \medskip Block structure can be indicated explicitly by ``@{command |
544 \medskip Block structure can be indicated explicitly by ``@{command |
545 "{"}~@{text "\<dots>"}~@{command "}"}'', although the body of a sub-proof |
545 "{"}~@{text "\<dots>"}~@{command "}"}'', although the body of a sub-proof |