Intro/document/getting.tex

3 Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however.
5 applying certain \ML{} functions, which update a stored proof state.
21 \section{Forward proof}\label{sec:forward} \index{forward proof|(}
23 and demonstrates forward proof.  The examples are set in first-order logic.
53 for (free) type variables, which remain fixed during a proof.
187 Free variables in a goal remain fixed throughout the proof.  After the
188 proof is finished, Isabelle converts them to scheme variables in the
190 during the proof, supporting answer extraction, program synthesis, and so
308 occasionally become attached to a proof state; more frequently, they appear
378 \index{forward proof|)}
380 \section{Backward proof}
383 conducting a backward proof using tactics.
402   is the basic resolution tactic, used for most proof steps.  The $thms$
404   proof state.  For each rule, resolution forms next states by unifying the
416   \index{forward proof}\index{destruct-resolution}
422 \subsection{Commands for backward proof}
425 proof state and manages the proof construction.  It allows interactive
426 backtracking through the proof space, going away to prove lemmas, etc.; of
430 begins a new proof, where the {\it formula\/} is written as an \ML\ string.
433 applies the {\it tactic\/} to the current proof
437   reverts to the previous proof state.  Undo can be repeated but cannot be
445 \item[\ttindex{qed} {\it name};] is the usual way of ending a proof.
470 first-order logic.  Let us try the example from \S\ref{prop-proof},
478 \end{ttbox}\index{level of a proof}
479 Isabelle responds by printing the initial proof state, which has $P\disj
490 In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$.
502 deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using
526 Isabelle tells us that there are no longer any subgoals: the proof is
533 variable~{\tt?P}\@.  Free variables in the proof state remain fixed
534 throughout the proof.  Isabelle finally converts them to scheme variables
537 As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how
538 instantiations affect the proof state.
560 \ttindex{eresolve_tac} deletes the assumption after use.  The resulting proof
596 Two calls of \texttt{assume_tac} can finish the proof.  The
621 Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an
622 attempted proof of the non-theorem $\exists y.\forall x.x=y$.  The former
623 proof succeeds, and the latter fails, because of the scope of quantified
629 \paragraph{The successful proof.}
630 The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules
670 \paragraph{The unsuccessful proof.}
699 There can be no proof of $\exists y.\forall x.x=y$ by the soundness of
710 the wrong order, the proof will fail.
757 proof by assumption will fail.
765 To do this proof, the rules must be applied in the correct order.
767 \ttindex{choplev} command returns to an earlier stage of the proof;
809 \paragraph{A one-step proof using tacticals.}
834 \subsection{A realistic quantifier proof}
931 Sceptics may examine the proof by calling the package's single-step