408 to be \emph{proven}; the next command may refine it by some proof method |
408 to be \emph{proven}; the next command may refine it by some proof method |
409 ($\approx$ tactic), and enter a sub-proof to establish the final result. |
409 ($\approx$ tactic), and enter a sub-proof to establish the final result. |
410 \item [$proof(state)$] is like an internal theory mode: the context may be |
410 \item [$proof(state)$] is like an internal theory mode: the context may be |
411 augmented by \emph{stating} additional assumptions, intermediate result etc. |
411 augmented by \emph{stating} additional assumptions, intermediate result etc. |
412 \item [$proof(chain)$] is an intermediate mode between $proof(state)$ and |
412 \item [$proof(chain)$] is an intermediate mode between $proof(state)$ and |
413 $proof(prove)$: existing facts have been just picked up in order to use them |
413 $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just |
414 when refining the goal claimed next. |
414 picked up in order to use them when refining the goal claimed next. |
415 \end{descr} |
415 \end{descr} |
416 |
416 |
417 |
417 |
418 \subsection{Formal comments}\label{sec:formal-cmt-prf} |
418 \subsection{Formal comments}\label{sec:formal-cmt-prf} |
419 |
419 |
519 |
519 |
520 New facts are established either by assumption or proof of local statements. |
520 New facts are established either by assumption or proof of local statements. |
521 Any fact will usually be involved in further proofs, either as explicit |
521 Any fact will usually be involved in further proofs, either as explicit |
522 arguments of proof methods or when forward chaining towards the next goal via |
522 arguments of proof methods or when forward chaining towards the next goal via |
523 $\THEN$ (and variants). Note that the special theorem name |
523 $\THEN$ (and variants). Note that the special theorem name |
524 $facts$.\indexisarthm{facts} refers to the most recently established facts. |
524 $this$.\indexisarthm{this} refers to the most recently established facts. |
525 \begin{rail} |
525 \begin{rail} |
526 'note' thmdef? thmrefs comment? |
526 'note' thmdef? thmrefs comment? |
527 ; |
527 ; |
528 'then' comment? |
528 'then' comment? |
529 ; |
529 ; |
539 establish the goal claimed next. The initial proof method invoked to refine |
539 establish the goal claimed next. The initial proof method invoked to refine |
540 that will be offered these facts to do ``anything appropriate'' (see also |
540 that will be offered these facts to do ``anything appropriate'' (see also |
541 \S\ref{sec:proof-steps}). For example, method $rule$ (see |
541 \S\ref{sec:proof-steps}). For example, method $rule$ (see |
542 \S\ref{sec:pure-meth}) would do an elimination rather than an introduction. |
542 \S\ref{sec:pure-meth}) would do an elimination rather than an introduction. |
543 \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is |
543 \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is |
544 equivalent to $\FROM{facts}$. |
544 equivalent to $\FROM{this}$. |
545 \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward |
545 \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward |
546 chaining is from earlier facts together with the current ones. |
546 chaining is from earlier facts together with the current ones. |
547 \end{descr} |
547 \end{descr} |
548 |
548 |
549 Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect |
549 Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect |
550 multiple facts to be given in proper order, corresponding to a prefix of the |
550 multiple facts to be given in proper order, corresponding to a prefix of the |
551 premises of the rule involved. Note that positions may be easily skipped |
551 premises of the rule involved. Note that positions may be easily skipped |
552 using a form like $\FROM{_~a~b}$, for example. This involves the rule |
552 using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example. This involves |
553 $PROP~\psi \Imp PROP~\psi$, which is bound in Isabelle/Pure as ``_'' |
553 the rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure as |
554 (underscore).\indexisarthm{_@\texttt{_}} |
554 ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} |
555 |
555 |
556 |
556 |
557 \subsection{Goal statements} |
557 \subsection{Goal statements} |
558 |
558 |
559 \indexisarcmd{theorem}\indexisarcmd{lemma} |
559 \indexisarcmd{theorem}\indexisarcmd{lemma} |
591 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a |
591 \item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a |
592 theorem with the current assumption context as hypotheses. |
592 theorem with the current assumption context as hypotheses. |
593 \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some |
593 \item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some |
594 pending goal with the result \emph{exported} into the corresponding context. |
594 pending goal with the result \emph{exported} into the corresponding context. |
595 \item [$\HENCE{a}{\phi}$] abbreviates $\THEN~\HAVE{a}{\phi}$, i.e.\ claims a |
595 \item [$\HENCE{a}{\phi}$] abbreviates $\THEN~\HAVE{a}{\phi}$, i.e.\ claims a |
596 local goal to be proven by forward chaining the current facts. |
596 local goal to be proven by forward chaining the current facts. Note that |
597 \item [$\THUS{a}{\phi}$] abbreviates $\THEN~\SHOW{a}{\phi}$. |
597 $\HENCENAME$ is equivalent to $\FROM{this}~\HAVENAME$. |
|
598 \item [$\THUS{a}{\phi}$] abbreviates $\THEN~\SHOW{a}{\phi}$. Note that |
|
599 $\THUSNAME$ is equivalent to $\FROM{this}~\SHOWNAME$. |
598 \end{descr} |
600 \end{descr} |
599 |
601 |
600 |
602 |
601 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
603 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
602 |
604 |
637 |
639 |
638 \medskip |
640 \medskip |
639 |
641 |
640 Unless given explicitly by the user, the default initial method is |
642 Unless given explicitly by the user, the default initial method is |
641 ``$default$'', which is usually set up to apply a single standard elimination |
643 ``$default$'', which is usually set up to apply a single standard elimination |
642 or introduction rule according to the topmost symbol involved. The default |
644 or introduction rule according to the topmost symbol involved. There is no |
643 terminal method is ``$finish$''; it solves all goals by assumption. |
645 default terminal method; in any case the final step is to solve all remaining |
|
646 goals by assumption. |
644 |
647 |
645 \begin{rail} |
648 \begin{rail} |
646 'proof' interest? meth? comment? |
649 'proof' interest? meth? comment? |
647 ; |
650 ; |
648 'qed' meth? comment? |
651 'qed' meth? comment? |
671 $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both methods. |
674 $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both methods. |
672 Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply |
675 Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply |
673 expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually |
676 expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually |
674 sufficient to see what is going wrong. |
677 sufficient to see what is going wrong. |
675 \item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$. |
678 \item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$. |
676 \item [``$\DOT$''] is a \emph{trivial proof}; it abbreviates $\BY{-}$. |
679 \item [``$\DOT$''] is a \emph{trivial proof}; it abbreviates |
|
680 $\BY{assumption}$. |
677 \item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that |
681 \item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that |
678 \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve |
682 \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve |
679 the goal without further ado. Of course, the result is a fake theorem only, |
683 the goal without further ado. Of course, the result is a fake theorem only, |
680 involving some oracle in its internal derivation object (this is indicated |
684 involving some oracle in its internal derivation object (this is indicated |
681 as $[!]$ in the printed result). The main application of |
685 as $[!]$ in the printed result). The main application of |
732 or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$ |
736 or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$ |
733 etc.) with a list of patterns $\IS{p@1 \dots p@n}$. In both cases, |
737 etc.) with a list of patterns $\IS{p@1 \dots p@n}$. In both cases, |
734 higher-order matching is applied to bind extra-logical text |
738 higher-order matching is applied to bind extra-logical text |
735 variables\index{text variables}, which may be either of the form $\VVar{x}$ |
739 variables\index{text variables}, which may be either of the form $\VVar{x}$ |
736 (token class \railtoken{textvar}, see \S\ref{sec:lex-syntax}) or nameless |
740 (token class \railtoken{textvar}, see \S\ref{sec:lex-syntax}) or nameless |
737 dummies ``\verb,_,'' (underscore).\index{dummy variables} Note that in the |
741 dummies ``\texttt{_}'' (underscore).\index{dummy variables} Note that in the |
738 $\LETNAME$ form the patterns occur on the left-hand side, while the $\ISNAME$ |
742 $\LETNAME$ form the patterns occur on the left-hand side, while the $\ISNAME$ |
739 patterns are in postfix position. |
743 patterns are in postfix position. |
740 |
744 |
741 Term abbreviations are quite different from actual local definitions as |
745 Term abbreviations are quite different from actual local definitions as |
742 introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are |
746 introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are |