merged
authornipkow
Fri Feb 07 22:37:54 2014 +0100 (2014-02-07)
changeset 553608cd866874590
parent 55358 85d81bc281d0
parent 55359 2d8222c76020
child 55361 d459a63ca42f
merged
     1.1 --- a/src/Doc/ProgProve/Isar.thy	Fri Feb 07 17:43:47 2014 +0000
     1.2 +++ b/src/Doc/ProgProve/Isar.thy	Fri Feb 07 22:37:54 2014 +0100
     1.3 @@ -33,15 +33,15 @@
     1.4  \medskip
     1.5  
     1.6  \begin{tabular}{@ {}lcl@ {}}
     1.7 -\textit{proof} &=& \isacom{by} \textit{method}\\
     1.8 -      &$\mid$& \isacom{proof} [\textit{method}] \ \textit{step}$^*$ \ \isacom{qed}
     1.9 +\textit{proof} &=& \indexed{\isacom{by}}{by} \textit{method}\\
    1.10 +      &$\mid$& \indexed{\isacom{proof}}{proof} [\textit{method}] \ \textit{step}$^*$ \ \indexed{\isacom{qed}}{qed}
    1.11  \end{tabular}
    1.12  \medskip
    1.13  
    1.14  \begin{tabular}{@ {}lcl@ {}}
    1.15 -\textit{step} &=& \isacom{fix} \textit{variables} \\
    1.16 -      &$\mid$& \isacom{assume} \textit{proposition} \\
    1.17 -      &$\mid$& [\isacom{from} \textit{fact}$^+$] (\isacom{have} $\mid$ \isacom{show}) \ \textit{proposition} \ \textit{proof}
    1.18 +\textit{step} &=& \indexed{\isacom{fix}}{fix} \textit{variables} \\
    1.19 +      &$\mid$& \indexed{\isacom{assume}}{assume} \textit{proposition} \\
    1.20 +      &$\mid$& [\indexed{\isacom{from}}{from} \textit{fact}$^+$] (\indexed{\isacom{have}}{have} $\mid$ \indexed{\isacom{show}}{show}) \ \textit{proposition} \ \textit{proof}
    1.21  \end{tabular}
    1.22  \medskip
    1.23  
    1.24 @@ -116,7 +116,7 @@
    1.25  If you wonder why @{text 2} directly implies @{text False}: from @{text 2}
    1.26  it follows that @{prop"a \<notin> f a \<longleftrightarrow> a \<in> f a"}.
    1.27  
    1.28 -\subsection{@{text this}, \isacom{then}, \isacom{hence} and \isacom{thus}}
    1.29 +\subsection{\indexed{@{text this}}{this}, \indexed{\isacom{then}}{then}, \indexed{\isacom{hence}}{hence} and \indexed{\isacom{thus}}{thus}}
    1.30  
    1.31  Labels should be avoided. They interrupt the flow of the reader who has to
    1.32  scan the context for the point where the label was introduced. Ideally, the
    1.33 @@ -165,18 +165,18 @@
    1.34  \medskip
    1.35  
    1.36  \begin{tabular}{r@ {\quad=\quad}l}
    1.37 -(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \isacom{using} \ \textit{facts}
    1.38 +(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \indexed{\isacom{using}}{using} \ \textit{facts}
    1.39  &
    1.40  \isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\
    1.41 -\isacom{with} \ \textit{facts} & \isacom{from} \ \textit{facts} \isa{this}
    1.42 +\indexed{\isacom{with}}{with} \ \textit{facts} & \isacom{from} \ \textit{facts} \isa{this}
    1.43  \end{tabular}
    1.44  \medskip
    1.45  
    1.46  \noindent The \isacom{using} idiom de-emphasizes the used facts by moving them
    1.47  behind the proposition.
    1.48  
    1.49 -\subsection{Structured Lemma Statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
    1.50 -
    1.51 +\subsection{Structured Lemma Statements: \indexed{\isacom{fixes}}{fixes}, \indexed{\isacom{assumes}}{assumes}, \indexed{\isacom{shows}}{shows}}
    1.52 +\index{lemma@\isacom{lemma}}
    1.53  Lemmas can also be stated in a more structured fashion. To demonstrate this
    1.54  feature with Cantor's theorem, we rephrase @{prop"\<not> surj f"}
    1.55  a little:
    1.56 @@ -217,7 +217,7 @@
    1.57  \end{warn}
    1.58  
    1.59  Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the
    1.60 -name @{text assms} that stands for the list of all assumptions. You can refer
    1.61 +name \indexed{@{text assms}}{assms} that stands for the list of all assumptions. You can refer
    1.62  to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"} etc,
    1.63  thus obviating the need to name them individually.
    1.64  
    1.65 @@ -436,7 +436,7 @@
    1.66  This can make the text harder to read, write and maintain. Pattern matching
    1.67  is an abbreviation mechanism to avoid such duplication. Writing
    1.68  \begin{quote}
    1.69 -\isacom{show} \ \textit{formula} @{text"("}\isacom{is} \textit{pattern}@{text")"}
    1.70 +\isacom{show} \ \textit{formula} @{text"("}\indexed{\isacom{is}}{is} \textit{pattern}@{text")"}
    1.71  \end{quote}
    1.72  matches the pattern against the formula, thus instantiating the unknowns in
    1.73  the pattern for later use. As an example, consider the proof pattern for
    1.74 @@ -460,7 +460,7 @@
    1.75  Pattern matching works wherever a formula is stated, in particular
    1.76  with \isacom{have} and \isacom{lemma}.
    1.77  
    1.78 -The unknown @{text"?thesis"} is implicitly matched against any goal stated by
    1.79 +The unknown \indexed{@{text"?thesis"}}{thesis} is implicitly matched against any goal stated by
    1.80  \isacom{lemma} or \isacom{show}. Here is a typical example: *}
    1.81  
    1.82  lemma "formula"
    1.83 @@ -470,7 +470,7 @@
    1.84  qed
    1.85  
    1.86  text{* 
    1.87 -Unknowns can also be instantiated with \isacom{let} commands
    1.88 +Unknowns can also be instantiated with \indexed{\isacom{let}}{let} commands
    1.89  \begin{quote}
    1.90  \isacom{let} @{text"?t"} = @{text"\""}\textit{some-big-term}@{text"\""}
    1.91  \end{quote}
    1.92 @@ -497,12 +497,13 @@
    1.93  \begin{quote}
    1.94  \isacom{have} \ @{text"\"x > 0\""}\\
    1.95  $\vdots$\\
    1.96 -\isacom{from} @{text "`x>0`"} \dots
    1.97 +\isacom{from} @{text "`x>0`"} \dots\index{$IMP053@@{text"`...`"}}
    1.98  \end{quote}
    1.99  Note that the quotes around @{text"x>0"} are \conceptnoidx{back quotes}.
   1.100  They refer to the fact not by name but by value.
   1.101  
   1.102 -\subsection{\isacom{moreover}}
   1.103 +\subsection{\indexed{\isacom{moreover}}{moreover}}
   1.104 +\index{ultimately@\isacom{ultimately}}
   1.105  
   1.106  Sometimes one needs a number of facts to enable some deduction. Of course
   1.107  one can name these facts individually, as shown on the right,
   1.108 @@ -550,7 +551,7 @@
   1.109  A lemma that shares the current context of assumptions but that
   1.110  has its own assumptions and is generalized over its locally fixed
   1.111  variables at the end. This is what a \concept{raw proof block} does:
   1.112 -\begin{quote}
   1.113 +\begin{quote}\index{$IMP053@@{text"{ ... }"} (proof block)}
   1.114  @{text"{"} \isacom{fix} @{text"x\<^sub>1 \<dots> x\<^sub>n"}\\
   1.115  \mbox{}\ \ \ \isacom{assume} @{text"A\<^sub>1 \<dots> A\<^sub>m"}\\
   1.116  \mbox{}\ \ \ $\vdots$\\
   1.117 @@ -584,7 +585,7 @@
   1.118  also be named for later reference: you simply follow the block directly by a
   1.119  \isacom{note} command:
   1.120  \begin{quote}
   1.121 -\isacom{note} \ @{text"name = this"}
   1.122 +\indexed{\isacom{note}}{note} \ @{text"name = this"}
   1.123  \end{quote}
   1.124  This introduces a new name @{text name} that refers to @{text this},
   1.125  the fact just proved, in this case the preceding block. In general,
   1.126 @@ -618,7 +619,7 @@
   1.127  
   1.128  
   1.129  \section{Case Analysis and Induction}
   1.130 -
   1.131 +\index{case analysis}\index{induction}
   1.132  \subsection{Datatype Case Analysis}
   1.133  
   1.134  We have seen case analysis on formulas. Now we want to distinguish