--- a/src/Doc/ProgProve/Isar.thy Fri Feb 07 14:18:31 2014 +0100
+++ b/src/Doc/ProgProve/Isar.thy Fri Feb 07 22:37:43 2014 +0100
@@ -33,15 +33,15 @@
\medskip
\begin{tabular}{@ {}lcl@ {}}
-\textit{proof} &=& \isacom{by} \textit{method}\\
- &$\mid$& \isacom{proof} [\textit{method}] \ \textit{step}$^*$ \ \isacom{qed}
+\textit{proof} &=& \indexed{\isacom{by}}{by} \textit{method}\\
+ &$\mid$& \indexed{\isacom{proof}}{proof} [\textit{method}] \ \textit{step}$^*$ \ \indexed{\isacom{qed}}{qed}
\end{tabular}
\medskip
\begin{tabular}{@ {}lcl@ {}}
-\textit{step} &=& \isacom{fix} \textit{variables} \\
- &$\mid$& \isacom{assume} \textit{proposition} \\
- &$\mid$& [\isacom{from} \textit{fact}$^+$] (\isacom{have} $\mid$ \isacom{show}) \ \textit{proposition} \ \textit{proof}
+\textit{step} &=& \indexed{\isacom{fix}}{fix} \textit{variables} \\
+ &$\mid$& \indexed{\isacom{assume}}{assume} \textit{proposition} \\
+ &$\mid$& [\indexed{\isacom{from}}{from} \textit{fact}$^+$] (\indexed{\isacom{have}}{have} $\mid$ \indexed{\isacom{show}}{show}) \ \textit{proposition} \ \textit{proof}
\end{tabular}
\medskip
@@ -116,7 +116,7 @@
If you wonder why @{text 2} directly implies @{text False}: from @{text 2}
it follows that @{prop"a \<notin> f a \<longleftrightarrow> a \<in> f a"}.
-\subsection{@{text this}, \isacom{then}, \isacom{hence} and \isacom{thus}}
+\subsection{\indexed{@{text this}}{this}, \indexed{\isacom{then}}{then}, \indexed{\isacom{hence}}{hence} and \indexed{\isacom{thus}}{thus}}
Labels should be avoided. They interrupt the flow of the reader who has to
scan the context for the point where the label was introduced. Ideally, the
@@ -165,18 +165,18 @@
\medskip
\begin{tabular}{r@ {\quad=\quad}l}
-(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \isacom{using} \ \textit{facts}
+(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \indexed{\isacom{using}}{using} \ \textit{facts}
&
\isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\
-\isacom{with} \ \textit{facts} & \isacom{from} \ \textit{facts} \isa{this}
+\indexed{\isacom{with}}{with} \ \textit{facts} & \isacom{from} \ \textit{facts} \isa{this}
\end{tabular}
\medskip
\noindent The \isacom{using} idiom de-emphasizes the used facts by moving them
behind the proposition.
-\subsection{Structured Lemma Statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
-
+\subsection{Structured Lemma Statements: \indexed{\isacom{fixes}}{fixes}, \indexed{\isacom{assumes}}{assumes}, \indexed{\isacom{shows}}{shows}}
+\index{lemma@\isacom{lemma}}
Lemmas can also be stated in a more structured fashion. To demonstrate this
feature with Cantor's theorem, we rephrase @{prop"\<not> surj f"}
a little:
@@ -217,7 +217,7 @@
\end{warn}
Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the
-name @{text assms} that stands for the list of all assumptions. You can refer
+name \indexed{@{text assms}}{assms} that stands for the list of all assumptions. You can refer
to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"} etc,
thus obviating the need to name them individually.
@@ -436,7 +436,7 @@
This can make the text harder to read, write and maintain. Pattern matching
is an abbreviation mechanism to avoid such duplication. Writing
\begin{quote}
-\isacom{show} \ \textit{formula} @{text"("}\isacom{is} \textit{pattern}@{text")"}
+\isacom{show} \ \textit{formula} @{text"("}\indexed{\isacom{is}}{is} \textit{pattern}@{text")"}
\end{quote}
matches the pattern against the formula, thus instantiating the unknowns in
the pattern for later use. As an example, consider the proof pattern for
@@ -460,7 +460,7 @@
Pattern matching works wherever a formula is stated, in particular
with \isacom{have} and \isacom{lemma}.
-The unknown @{text"?thesis"} is implicitly matched against any goal stated by
+The unknown \indexed{@{text"?thesis"}}{thesis} is implicitly matched against any goal stated by
\isacom{lemma} or \isacom{show}. Here is a typical example: *}
lemma "formula"
@@ -470,7 +470,7 @@
qed
text{*
-Unknowns can also be instantiated with \isacom{let} commands
+Unknowns can also be instantiated with \indexed{\isacom{let}}{let} commands
\begin{quote}
\isacom{let} @{text"?t"} = @{text"\""}\textit{some-big-term}@{text"\""}
\end{quote}
@@ -497,12 +497,13 @@
\begin{quote}
\isacom{have} \ @{text"\"x > 0\""}\\
$\vdots$\\
-\isacom{from} @{text "`x>0`"} \dots
+\isacom{from} @{text "`x>0`"} \dots\index{$IMP053@@{text"`...`"}}
\end{quote}
Note that the quotes around @{text"x>0"} are \conceptnoidx{back quotes}.
They refer to the fact not by name but by value.
-\subsection{\isacom{moreover}}
+\subsection{\indexed{\isacom{moreover}}{moreover}}
+\index{ultimately@\isacom{ultimately}}
Sometimes one needs a number of facts to enable some deduction. Of course
one can name these facts individually, as shown on the right,
@@ -550,7 +551,7 @@
A lemma that shares the current context of assumptions but that
has its own assumptions and is generalized over its locally fixed
variables at the end. This is what a \concept{raw proof block} does:
-\begin{quote}
+\begin{quote}\index{$IMP053@@{text"{ ... }"} (proof block)}
@{text"{"} \isacom{fix} @{text"x\<^sub>1 \<dots> x\<^sub>n"}\\
\mbox{}\ \ \ \isacom{assume} @{text"A\<^sub>1 \<dots> A\<^sub>m"}\\
\mbox{}\ \ \ $\vdots$\\
@@ -584,7 +585,7 @@
also be named for later reference: you simply follow the block directly by a
\isacom{note} command:
\begin{quote}
-\isacom{note} \ @{text"name = this"}
+\indexed{\isacom{note}}{note} \ @{text"name = this"}
\end{quote}
This introduces a new name @{text name} that refers to @{text this},
the fact just proved, in this case the preceding block. In general,
@@ -618,7 +619,7 @@
\section{Case Analysis and Induction}
-
+\index{case analysis}\index{induction}
\subsection{Datatype Case Analysis}
We have seen case analysis on formulas. Now we want to distinguish