Intro/document/foundations.tex

469 Each Isabelle proof typically works within a single theory, which is
470 associated with the proof state.  However, many different theories may
496 {\bf Resolution}, in particular, is convenient for backward proof.
504 quantities often emerge from the proof.
518 resolution --- Isabelle's principal proof method.  Resolution yields both
519 forward and backward proof.  Backward proof works by unifying a goal with
520 the conclusion of a rule, whose premises become new subgoals.  Forward proof
537 proof procedure.
709 the assumptions in a natural deduction proof; lifting copies them into a rule's
768 \section{Backward proof by resolution}
769 \index{resolution!in backward proof}
772 forward from facts.  It can also support backward proof, where we start
776 expressing proof searches.  {\bf Tactics} refine subgoals while {\bf
790 the {\bf proof state}\index{proof state}
794 To prove the formula~$\phi$, take $\phi\Imp \phi$ as the initial proof
796 backward proof, a typical proof state is $\List{\phi@1; \ldots; \phi@n}
797 \Imp \phi$.  This proof state is a theorem, ensuring that the subgoals
800 instantiated during the proof; a proof state may be $\List{\phi@1; \ldots;
804 To refine subgoal~$i$ of a proof state by a rule, perform the following
806 \[ \infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}} \]
808 lifting over subgoal~$i$'s assumptions and parameters.  If the proof state
809 is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, then the new proof state is
813 Substitution~$s$ unifies $\psi'$ with~$\phi@i$.  In the proof state,
816 unknowns in the proof state.  Refinement by~$(\exists I)$, namely
821 the proof state.
825 In the course of a natural deduction proof, parameters $x@1$, \ldots,~$x@l$ and
837 models proof by assumption in natural deduction.
839 Isabelle automates the meta-inference for proof by assumption.  Its arguments
850 The premise represents a proof state with~$n$ subgoals, of which the~$i$th
853 meta-inference returns an instantiated proof state from which the $i$th
857 Consider the proof state
864 Here, proof by assumption affects the main goal.  It could also affect
870 \subsection{A propositional proof} \label{prop-proof}
876 Bear in mind that every proof state we derive will be a meta-theorem,
886 shortly see how to get rid of it!)  The new proof state is the following
895 Notice the unknowns in the proof state.  Because we have applied $(\disj E)$,
898 $\Var{Q@1}$ to~$P$ throughout the proof state:
905 steps, the proof state is $P\disj P\imp P$.
908 \subsection{A quantifier proof}
911 $(\exists x.P(f(x)))\imp(\exists x.P(x))$.  The initial proof
920 Both have the assumption $\exists x.P(f(x))$.  The new proof
948 proof state contains no subgoals: $(\exists x.P(f(x)))\imp(\exists x.P(x))$.
953 {\bf Tactics} perform backward proof.  Isabelle tactics differ from those
954 of {\sc lcf}, {\sc hol} and Nuprl by operating on entire proof states,
956 takes a proof state and returns a sequence (lazy list) of possible
958 technique~\cite{paulson-ml2}.  Isabelle represents proof states by theorems.
978 to a proof state, it returns all states reachable in two steps by applying
996 In principle, resolution and proof by assumption suffice to prove all
1028 In backward proof, a goal containing $P\disj Q$ on the left of the~$\turn$
1038   \item a proof state $\List{\phi@1; \ldots; \phi@n} \Imp \phi$
1057 Let us redo the example from~\S\ref{prop-proof}.  The elimination rule
1061 and the proof state is $(P\disj P\Imp P)\Imp (P\disj P\imp P)$.  The
1072 $\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$.  The new proof state
1094 \index{forward proof}
1100 and easy to use in forward proof.  The rules $({\disj}E)$, $({\bot}E)$ and
1101 $({\exists}E)$ work by discharging assumptions; they support backward proof
1115 proof, Isabelle provides a means of transforming a destruction rule such as
1143 Starting with a proof state $\phi\Imp\phi$, assumptions may accumulate,
1152 We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in
1166 The proof may use the meta-assumptions in any order, and as often as
1171 premature instantiation during the proof; we may now replace them by
1176   reasons.  Meta-assumptions remain fixed throughout a proof.