--- a/doc-src/IsarOverview/Isar/Induction.thy Mon Nov 12 14:20:21 2007 +0100
+++ b/doc-src/IsarOverview/Isar/Induction.thy Mon Nov 12 19:02:32 2007 +0100
@@ -45,8 +45,8 @@
text{*\noindent which is like the previous proof but instantiates
@{text ?P} right away with @{term A}. Thus we could prove the two
-cases in any order. The phrase `\isakeyword{case}~@{text True}'
-abbreviates `\isakeyword{assume}~@{text"True: A"}' and analogously for
+cases in any order. The phrase \isakeyword{case}~@{text True}
+abbreviates \isakeyword{assume}~@{text"True: A"} and analogously for
@{text"False"} and @{prop"\<not>A"}.
The same game can be played with other datatypes, for example lists,
@@ -60,19 +60,18 @@
next
case Cons thus ?thesis by simp
qed
-text{*\noindent Here `\isakeyword{case}~@{text Nil}' abbreviates
-`\isakeyword{assume}~@{text"Nil:"}~@{prop"xs = []"}' and
-`\isakeyword{case}~@{text Cons}'
-abbreviates `\isakeyword{fix}~@{text"? ??"}
-\isakeyword{assume}~@{text"Cons:"}~@{text"xs = ? # ??"}'
+text{*\noindent Here \isakeyword{case}~@{text Nil} abbreviates
+\isakeyword{assume}~@{text"Nil:"}~@{prop"xs = []"} and
+\isakeyword{case}~@{text Cons} abbreviates \isakeyword{fix}~@{text"? ??"}
+\isakeyword{assume}~@{text"Cons:"}~@{text"xs = ? # ??"},
where @{text"?"} and @{text"??"}
stand for variable names that have been chosen by the system.
Therefore we cannot refer to them.
Luckily, this proof is simple enough we do not need to refer to them.
However, sometimes one may have to. Hence Isar offers a simple scheme for
naming those variables: replace the anonymous @{text Cons} by
-@{text"(Cons y ys)"}, which abbreviates `\isakeyword{fix}~@{text"y ys"}
-\isakeyword{assume}~@{text"Cons:"}~@{text"xs = y # ys"}'.
+@{text"(Cons y ys)"}, which abbreviates \isakeyword{fix}~@{text"y ys"}
+\isakeyword{assume}~@{text"Cons:"}~@{text"xs = y # ys"}.
In each \isakeyword{case} the assumption can be
referred to inside the proof by the name of the constructor. In
Section~\ref{sec:full-Ind} below we will come across an example
@@ -154,6 +153,7 @@
behind the scenes.
\subsection{Inductive proofs of conditional formulae}
+\label{sec:full-Ind}
Induction also copes well with formulae involving @{text"\<Longrightarrow>"}, for example
*}
@@ -204,7 +204,6 @@
\subsection{Induction formulae involving @{text"\<And>"} or @{text"\<Longrightarrow>"}}
-\label{sec:full-Ind}
Let us now consider abstractly the situation where the goal to be proved
contains both @{text"\<And>"} and @{text"\<Longrightarrow>"}, say @{prop"\<And>x. P x \<Longrightarrow> Q x"}.
@@ -331,7 +330,7 @@
*}
(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
-by (induct xs rule: rot.induct, simp_all)
+by (induct xs rule: rot.induct) simp_all
(*<*)end(*>*)
(*
--- a/doc-src/IsarOverview/Isar/Logic.thy Mon Nov 12 14:20:21 2007 +0100
+++ b/doc-src/IsarOverview/Isar/Logic.thy Mon Nov 12 19:02:32 2007 +0100
@@ -156,57 +156,38 @@
way to the final \isakeyword{show}. This is the norm in nontrivial
proofs where one cannot bridge the gap between the assumptions and the
conclusion in one step. To understand how the proof works we need to
-explain more Isar details.
-
+explain more Isar details:
+\begin{itemize}
+\item
Method @{text rule} can be given a list of rules, in which case
@{text"(rule"}~\textit{rules}@{text")"} applies the first matching
-rule in the list \textit{rules}. Command \isakeyword{from} can be
+rule in the list \textit{rules}.
+\item Command \isakeyword{from} can be
followed by any number of facts. Given \isakeyword{from}~@{text
f}$_1$~\dots~@{text f}$_n$, the proof step
@{text"(rule"}~\textit{rules}@{text")"} following a \isakeyword{have}
or \isakeyword{show} searches \textit{rules} for a rule whose first
$n$ premises can be proved by @{text f}$_1$~\dots~@{text f}$_n$ in the
-given order. Finally one needs to know that ``..'' is short for
-@{text"by(rule"}~\textit{elim-rules intro-rules}@{text")"} (or
-@{text"by(rule"}~\textit{intro-rules}@{text")"} if there are no facts
-fed into the proof), i.e.\ elimination rules are tried before
-introduction rules.
-
-Thus in the above proof both \isakeyword{have}s are proved via
+given order.
+\item ``..'' is short for
+@{text"by(rule"}~\textit{elim-rules intro-rules}@{text")"}\footnote{or
+merely @{text"(rule"}~\textit{intro-rules}@{text")"} if there are no facts
+fed into the proof}, where \textit{elim-rules} and \textit{intro-rules}
+are the predefined elimination and introduction rule. Thus
+elimination rules are tried first (if there are incoming facts).
+\end{itemize}
+Hence in the above proof both \isakeyword{have}s are proved via
@{thm[source]conjE} triggered by \isakeyword{from}~@{text ab} whereas
in the \isakeyword{show} step no elimination rule is applicable and
the proof succeeds with @{thm[source]conjI}. The latter would fail had
we written \isakeyword{from}~@{text"a b"} instead of
\isakeyword{from}~@{text"b a"}.
-Proofs starting with a plain @{text proof} behave the same because the
-latter is short for @{text"proof (rule"}~\textit{elim-rules
-intro-rules}@{text")"} (or @{text"proof
-(rule"}~\textit{intro-rules}@{text")"} if there are no facts fed into
-the proof). *}
-
-subsection{*More constructs*}
+A plain \isakeyword{proof} with no argument is short for
+\isakeyword{proof}~@{text"(rule"}~\textit{elim-rules intro-rules}@{text")"}\footnotemark[1].
+This means that the matching rule is selected by the incoming facts and the goal exactly as just explained.
-text{* In the previous proof of @{prop"A \<and> B \<longrightarrow> B \<and> A"} we needed to feed
-more than one fact into a proof step, a frequent situation. Then the
-UNIX-pipe model appears to break down and we need to name the different
-facts to refer to them. But this can be avoided:
-*}
-lemma "A \<and> B \<longrightarrow> B \<and> A"
-proof
- assume ab: "A \<and> B"
- from ab have "B" ..
- moreover
- from ab have "A" ..
- ultimately show "B \<and> A" ..
-qed
-text{*\noindent You can combine any number of facts @{term A1} \dots\ @{term
-An} into a sequence by separating their proofs with
-\isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands
-for \isakeyword{from}~@{term A1}~\dots~@{term An}. This avoids having to
-introduce names for all of the sequence elements. *}
-
-text{* Although we have only seen a few introduction and elimination rules so
+Although we have only seen a few introduction and elimination rules so
far, Isar's predefined rules include all the usual natural deduction
rules. We conclude our exposition of propositional logic with an extended
example --- which rules are used implicitly where? *}
@@ -346,8 +327,21 @@
assume B show ?thesis ..
qed
qed
+text{*\noindent Alternatively one can feed @{prop"A \<or> B"} directly
+into the proof, thus triggering the elimination rule: *}
+lemma assumes AB: "A \<or> B" shows "B \<or> A"
+using AB
+proof
+ assume A show ?thesis ..
+next
+ assume B show ?thesis ..
+qed
+text{* \noindent Remember that eliminations have priority over
+introductions.
-text{* Too many names can easily clutter a proof. We already learned
+\subsection{Avoiding names}
+
+Too many names can easily clutter a proof. We already learned
about @{text this} as a means of avoiding explicit names. Another
handy device is to refer to a fact not by name but by contents: for
example, writing @{text "`A \<or> B`"} (enclosing the formula in back quotes)
@@ -356,19 +350,48 @@
of the previous proof *}
lemma assumes "A \<or> B" shows "B \<or> A"
-proof -
- from `A \<or> B` show ?thesis
+using `A \<or> B`
(*<*)oops(*>*)
text{*\noindent which continues as before.
Clearly, this device of quoting facts by contents is only advisable
for small formulae. In such cases it is superior to naming because the
reader immediately sees what the fact is without needing to search for
-it in the preceding proof text. *}
+it in the preceding proof text.
+
+The assumptions of a lemma can also be referred to via their
+predefined name @{text assms}. Hence the @{text"`A \<or> B`"} in the
+previous proof can also be replaced by @{text assms}. Note that @{text
+assms} refers to the list of \emph{all} assumptions. To pick out a
+specific one, say the second, write @{text"assms(2)"}.
+
+This indexing notation $name(.)$ works for any $name$ that stands for
+a list of facts, for example $f$@{text".simps"}, the equations of the
+recursively defined function $f$. You may also select sublists by writing
+$name(2-3)$.
-subsection{*Predicate calculus*}
+Above we recommended the UNIX-pipe model (i.e. @{text this}) to avoid
+the need to name propositions. But frequently we needed to feed more
+than one previously derived fact into a proof step. Then the UNIX-pipe
+model appears to break down and we need to name the different facts to
+refer to them. But this can be avoided: *}
+lemma assumes "A \<and> B" shows "B \<and> A"
+proof -
+ from `A \<and> B` have "B" ..
+ moreover
+ from `A \<and> B` have "A" ..
+ ultimately show "B \<and> A" ..
+qed
+text{*\noindent You can combine any number of facts @{term A1} \dots\ @{term
+An} into a sequence by separating their proofs with
+\isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands
+for \isakeyword{from}~@{term A1}~\dots~@{term An}. This avoids having to
+introduce names for all of the sequence elements.
-text{* Command \isakeyword{fix} introduces new local variables into a
+
+\subsection{Predicate calculus}
+
+Command \isakeyword{fix} introduces new local variables into a
proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to @{text"\<And>"}
(the universal quantifier at the
meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to
--- a/doc-src/IsarOverview/Isar/document/Induction.tex Mon Nov 12 14:20:21 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex Mon Nov 12 19:02:32 2007 +0100
@@ -110,8 +110,8 @@
\begin{isamarkuptext}%
\noindent which is like the previous proof but instantiates
\isa{{\isacharquery}P} right away with \isa{A}. Thus we could prove the two
-cases in any order. The phrase `\isakeyword{case}~\isa{True}'
-abbreviates `\isakeyword{assume}~\isa{True{\isacharcolon}\ A}' and analogously for
+cases in any order. The phrase \isakeyword{case}~\isa{True}
+abbreviates \isakeyword{assume}~\isa{True{\isacharcolon}\ A} and analogously for
\isa{False} and \isa{{\isasymnot}\ A}.
The same game can be played with other datatypes, for example lists,
@@ -149,19 +149,18 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Here `\isakeyword{case}~\isa{Nil}' abbreviates
-`\isakeyword{assume}~\isa{Nil{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}' and
-`\isakeyword{case}~\isa{Cons}'
-abbreviates `\isakeyword{fix}~\isa{{\isacharquery}\ {\isacharquery}{\isacharquery}}
-\isakeyword{assume}~\isa{Cons{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharquery}\ {\isacharhash}\ {\isacharquery}{\isacharquery}}'
+\noindent Here \isakeyword{case}~\isa{Nil} abbreviates
+\isakeyword{assume}~\isa{Nil{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} and
+\isakeyword{case}~\isa{Cons} abbreviates \isakeyword{fix}~\isa{{\isacharquery}\ {\isacharquery}{\isacharquery}}
+\isakeyword{assume}~\isa{Cons{\isacharcolon}}~\isa{xs\ {\isacharequal}\ {\isacharquery}\ {\isacharhash}\ {\isacharquery}{\isacharquery}},
where \isa{{\isacharquery}} and \isa{{\isacharquery}{\isacharquery}}
stand for variable names that have been chosen by the system.
Therefore we cannot refer to them.
Luckily, this proof is simple enough we do not need to refer to them.
However, sometimes one may have to. Hence Isar offers a simple scheme for
naming those variables: replace the anonymous \isa{Cons} by
-\isa{{\isacharparenleft}Cons\ y\ ys{\isacharparenright}}, which abbreviates `\isakeyword{fix}~\isa{y\ ys}
-\isakeyword{assume}~\isa{Cons{\isacharcolon}}~\isa{xs\ {\isacharequal}\ y\ {\isacharhash}\ ys}'.
+\isa{{\isacharparenleft}Cons\ y\ ys{\isacharparenright}}, which abbreviates \isakeyword{fix}~\isa{y\ ys}
+\isakeyword{assume}~\isa{Cons{\isacharcolon}}~\isa{xs\ {\isacharequal}\ y\ {\isacharhash}\ ys}.
In each \isakeyword{case} the assumption can be
referred to inside the proof by the name of the constructor. In
Section~\ref{sec:full-Ind} below we will come across an example
@@ -353,6 +352,7 @@
behind the scenes.
\subsection{Inductive proofs of conditional formulae}
+\label{sec:full-Ind}
Induction also copes well with formulae involving \isa{{\isasymLongrightarrow}}, for example%
\end{isamarkuptext}%
@@ -457,7 +457,6 @@
\subsection{Induction formulae involving \isa{{\isasymAnd}} or \isa{{\isasymLongrightarrow}}}
-\label{sec:full-Ind}
Let us now consider abstractly the situation where the goal to be proved
contains both \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}}, say \isa{{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ Q\ x}.
@@ -691,7 +690,7 @@
%
\isatagproof
\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
+\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
%
\endisatagproof
{\isafoldproof}%
--- a/doc-src/IsarOverview/Isar/document/Logic.tex Mon Nov 12 14:20:21 2007 +0100
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex Mon Nov 12 19:02:32 2007 +0100
@@ -396,90 +396,36 @@
way to the final \isakeyword{show}. This is the norm in nontrivial
proofs where one cannot bridge the gap between the assumptions and the
conclusion in one step. To understand how the proof works we need to
-explain more Isar details.
-
+explain more Isar details:
+\begin{itemize}
+\item
Method \isa{rule} can be given a list of rules, in which case
\isa{{\isacharparenleft}rule}~\textit{rules}\isa{{\isacharparenright}} applies the first matching
-rule in the list \textit{rules}. Command \isakeyword{from} can be
+rule in the list \textit{rules}.
+\item Command \isakeyword{from} can be
followed by any number of facts. Given \isakeyword{from}~\isa{f}$_1$~\dots~\isa{f}$_n$, the proof step
\isa{{\isacharparenleft}rule}~\textit{rules}\isa{{\isacharparenright}} following a \isakeyword{have}
or \isakeyword{show} searches \textit{rules} for a rule whose first
$n$ premises can be proved by \isa{f}$_1$~\dots~\isa{f}$_n$ in the
-given order. Finally one needs to know that ``..'' is short for
-\isa{by{\isacharparenleft}rule}~\textit{elim-rules intro-rules}\isa{{\isacharparenright}} (or
-\isa{by{\isacharparenleft}rule}~\textit{intro-rules}\isa{{\isacharparenright}} if there are no facts
-fed into the proof), i.e.\ elimination rules are tried before
-introduction rules.
-
-Thus in the above proof both \isakeyword{have}s are proved via
+given order.
+\item ``..'' is short for
+\isa{by{\isacharparenleft}rule}~\textit{elim-rules intro-rules}\isa{{\isacharparenright}}\footnote{or
+merely \isa{{\isacharparenleft}rule}~\textit{intro-rules}\isa{{\isacharparenright}} if there are no facts
+fed into the proof}, where \textit{elim-rules} and \textit{intro-rules}
+are the predefined elimination and introduction rule. Thus
+elimination rules are tried first (if there are incoming facts).
+\end{itemize}
+Hence in the above proof both \isakeyword{have}s are proved via
\isa{conjE} triggered by \isakeyword{from}~\isa{ab} whereas
in the \isakeyword{show} step no elimination rule is applicable and
the proof succeeds with \isa{conjI}. The latter would fail had
we written \isakeyword{from}~\isa{a\ b} instead of
\isakeyword{from}~\isa{b\ a}.
-Proofs starting with a plain \isa{proof} behave the same because the
-latter is short for \isa{proof\ {\isacharparenleft}rule}~\textit{elim-rules
-intro-rules}\isa{{\isacharparenright}} (or \isa{proof\ {\isacharparenleft}rule}~\textit{intro-rules}\isa{{\isacharparenright}} if there are no facts fed into
-the proof).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{More constructs%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In the previous proof of \isa{A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A} we needed to feed
-more than one fact into a proof step, a frequent situation. Then the
-UNIX-pipe model appears to break down and we need to name the different
-facts to refer to them. But this can be avoided:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ ab{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ ab\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{moreover}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ ab\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{ultimately}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with
-\isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands
-for \isakeyword{from}~\isa{A{\isadigit{1}}}~\dots~\isa{An}. This avoids having to
-introduce names for all of the sequence elements.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
+A plain \isakeyword{proof} with no argument is short for
+\isakeyword{proof}~\isa{{\isacharparenleft}rule}~\textit{elim-rules intro-rules}\isa{{\isacharparenright}}\footnotemark[1].
+This means that the matching rule is selected by the incoming facts and the goal exactly as just explained.
+
Although we have only seen a few introduction and elimination rules so
far, Isar's predefined rules include all the usual natural deduction
rules. We conclude our exposition of propositional logic with an extended
@@ -795,6 +741,47 @@
\endisadelimproof
%
\begin{isamarkuptext}%
+\noindent Alternatively one can feed \isa{A\ {\isasymor}\ B} directly
+into the proof, thus triggering the elimination rule:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}B\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{using}\isamarkupfalse%
+\ AB\isanewline
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ A\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ B\ \isacommand{show}\isamarkupfalse%
+\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent Remember that eliminations have priority over
+introductions.
+
+\subsection{Avoiding names}
+
Too many names can easily clutter a proof. We already learned
about \isa{this} as a means of avoiding explicit names. Another
handy device is to refer to a fact not by name but by contents: for
@@ -812,11 +799,8 @@
\endisadelimproof
%
\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ {\isacharbackquoteopen}A\ {\isasymor}\ B{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis%
+\isacommand{using}\isamarkupfalse%
+\ {\isacharbackquoteopen}A\ {\isasymor}\ B{\isacharbackquoteclose}%
\endisatagproof
{\isafoldproof}%
%
@@ -830,15 +814,67 @@
Clearly, this device of quoting facts by contents is only advisable
for small formulae. In such cases it is superior to naming because the
reader immediately sees what the fact is without needing to search for
-it in the preceding proof text.%
+it in the preceding proof text.
+
+The assumptions of a lemma can also be referred to via their
+predefined name \isa{assms}. Hence the \isa{{\isacharbackquote}A\ {\isasymor}\ B{\isacharbackquote}} in the
+previous proof can also be replaced by \isa{assms}. Note that \isa{assms} refers to the list of \emph{all} assumptions. To pick out a
+specific one, say the second, write \isa{assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}}.
+
+This indexing notation $name(.)$ works for any $name$ that stands for
+a list of facts, for example $f$\isa{{\isachardot}simps}, the equations of the
+recursively defined function $f$. You may also select sublists by writing
+$name(2-3)$.
+
+Above we recommended the UNIX-pipe model (i.e. \isa{this}) to avoid
+the need to name propositions. But frequently we needed to feed more
+than one previously derived fact into a proof step. Then the UNIX-pipe
+model appears to break down and we need to name the different facts to
+refer to them. But this can be avoided:%
\end{isamarkuptext}%
\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
%
-\isamarkupsubsection{Predicate calculus%
-}
-\isamarkuptrue%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{moreover}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{ultimately}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
%
\begin{isamarkuptext}%
+\noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with
+\isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands
+for \isakeyword{from}~\isa{A{\isadigit{1}}}~\dots~\isa{An}. This avoids having to
+introduce names for all of the sequence elements.
+
+
+\subsection{Predicate calculus}
+
Command \isakeyword{fix} introduces new local variables into a
proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to \isa{{\isasymAnd}}
(the universal quantifier at the