Fri, 07 Feb 2014 22:37:54 +0100
changeset 55360 8cd866874590
parent 55358 85d81bc281d0 (current diff)
parent 55359 2d8222c76020 (diff)
child 55361 d459a63ca42f
--- a/src/Doc/ProgProve/Isar.thy	Fri Feb 07 17:43:47 2014 +0000
+++ b/src/Doc/ProgProve/Isar.thy	Fri Feb 07 22:37:54 2014 +0100
@@ -33,15 +33,15 @@
 \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}
 \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}
@@ -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 @@
 \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}
 \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}}
 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 @@
 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
-\isacom{show} \ \textit{formula} @{text"("}\isacom{is} \textit{pattern}@{text")"}
+\isacom{show} \ \textit{formula} @{text"("}\indexed{\isacom{is}}{is} \textit{pattern}@{text")"}
 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 @@
-Unknowns can also be instantiated with \isacom{let} commands
+Unknowns can also be instantiated with \indexed{\isacom{let}}{let} commands
 \isacom{let} @{text"?t"} = @{text"\""}\textit{some-big-term}@{text"\""}
@@ -497,12 +497,13 @@
 \isacom{have} \ @{text"\"x > 0\""}\\
-\isacom{from} @{text "`x>0`"} \dots
+\isacom{from} @{text "`x>0`"} \dots\index{$IMP053@@{text"`...`"}}
 Note that the quotes around @{text"x>0"} are \conceptnoidx{back quotes}.
 They refer to the fact not by name but by value.
 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}\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:
-\isacom{note} \ @{text"name = this"}
+\indexed{\isacom{note}}{note} \ @{text"name = this"}
 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