# HG changeset patch
# User nipkow
# Date 1391888050 -3600
# Node ID d459a63ca42f12147443fa3e64e30b012aad8d61
# Parent  8cd8668745902bdd1a638b33ae38cba14569f7c0
more indexing

diff -r 8cd866874590 -r d459a63ca42f src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Fri Feb 07 22:37:54 2014 +0100
+++ b/src/Doc/ProgProve/Isar.thy	Sat Feb 08 20:34:10 2014 +0100
@@ -249,7 +249,7 @@
   show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
 qed(*<*)oops(*>*)
 text_raw {* }
-\end{minipage}
+\end{minipage}\index{cases@@{text cases}}
 &
 \begin{minipage}[t]{.4\textwidth}
 \isa{%
@@ -290,7 +290,7 @@
 text_raw {* }
 \medskip
 \begin{isamarkuptext}%
-Proofs by contradiction:
+Proofs by contradiction (@{thm[source] ccontr} stands for ``classical contradiction''):
 \end{isamarkuptext}%
 \begin{tabular}{@ {}ll@ {}}
 \begin{minipage}[t]{.4\textwidth}
@@ -323,8 +323,6 @@
 \end{tabular}
 \medskip
 \begin{isamarkuptext}%
-The name @{thm[source] ccontr} stands for ``classical contradiction''.
-
 How to prove quantified formulas:
 \end{isamarkuptext}%
 \begin{tabular}{@ {}ll@ {}}
@@ -359,7 +357,7 @@
 \medskip
 \begin{isamarkuptext}%
 In the proof of \noquotes{@{prop[source]"\<forall>x. P(x)"}},
-the step \isacom{fix}~@{text x} introduces a locally fixed variable @{text x}
+the step \indexed{\isacom{fix}}{fix}~@{text x} introduces a locally fixed variable @{text x}
 into the subproof, the proverbial ``arbitrary but fixed value''.
 Instead of @{text x} we could have chosen any name in the subproof.
 In the proof of \noquotes{@{prop[source]"\<exists>x. P(x)"}},
@@ -619,8 +617,9 @@
 
 
 \section{Case Analysis and Induction}
-\index{case analysis}\index{induction}
+
 \subsection{Datatype Case Analysis}
+\index{case analysis|(}
 
 We have seen case analysis on formulas. Now we want to distinguish
 which form some term takes: is it @{text 0} or of the form @{term"Suc n"},
@@ -637,7 +636,7 @@
   thus ?thesis by simp
 qed
 
-text{* Function @{text tl} (''tail'') is defined by @{thm tl.simps(1)} and
+text{*\index{cases@@{text"cases"}|(}Function @{text tl} (''tail'') is defined by @{thm tl.simps(1)} and
 @{thm tl.simps(2)}. Note that the result type of @{const length} is @{typ nat}
 and @{prop"0 - 1 = (0::nat)"}.
 
@@ -645,7 +644,7 @@
 The goal has to be proved for each constructor @{text C}:
 \begin{quote}
 \isacom{fix} \ @{text"x\<^sub>1 \<dots> x\<^sub>n"} \isacom{assume} @{text"\"t = C x\<^sub>1 \<dots> x\<^sub>n\""}
-\end{quote}
+\end{quote}\index{case@\isacom{case}|(}
 Each case can be written in a more compact form by means of the \isacom{case}
 command:
 \begin{quote}
@@ -669,8 +668,11 @@
 for @{text"[]"} and @{text"#"}. The names of the assumptions
 are not used because they are directly piped (via \isacom{thus})
 into the proof of the claim.
+\index{case analysis|)}
 
 \subsection{Structural Induction}
+\index{induction|(}
+\index{structural induction|(}
 
 We illustrate structural induction with an example based on natural numbers:
 the sum (@{text"\<Sum>"}) of the first @{text n} natural numbers
@@ -719,7 +721,7 @@
 qed
 
 text{*
-The unknown @{text "?case"} is set in each case to the required
+The unknown @{text"?case"}\index{case?@@{text"?case"}|(} is set in each case to the required
 claim, i.e.\ @{text"?P 0"} and \mbox{@{text"?P(Suc n)"}} in the above proof,
 without requiring the user to define a @{text "?P"}. The general
 pattern for induction over @{typ nat} is shown on the left-hand side:
@@ -786,17 +788,19 @@
 Induction works for any datatype.
 Proving a goal @{text"\<lbrakk> A\<^sub>1(x); \<dots>; A\<^sub>k(x) \<rbrakk> \<Longrightarrow> P(x)"}
 by induction on @{text x} generates a proof obligation for each constructor
-@{text C} of the datatype. The command @{text"case (C x\<^sub>1 \<dots> x\<^sub>n)"}
+@{text C} of the datatype. The command \isacom{case}~@{text"(C x\<^sub>1 \<dots> x\<^sub>n)"}
 performs the following steps:
 \begin{enumerate}
 \item \isacom{fix} @{text"x\<^sub>1 \<dots> x\<^sub>n"}
-\item \isacom{assume} the induction hypotheses (calling them @{text C.IH})
- and the premises \mbox{@{text"A\<^sub>i(C x\<^sub>1 \<dots> x\<^sub>n)"}} (calling them @{text"C.prems"})
+\item \isacom{assume} the induction hypotheses (calling them @{text C.IH}\index{IH@@{text".IH"}})
+ and the premises \mbox{@{text"A\<^sub>i(C x\<^sub>1 \<dots> x\<^sub>n)"}} (calling them @{text"C.prems"}\index{prems@@{text".prems"}})
  and calling the whole list @{text C}
 \item \isacom{let} @{text"?case = \"P(C x\<^sub>1 \<dots> x\<^sub>n)\""}
 \end{enumerate}
+\index{structural induction|)}
 
 \subsection{Rule Induction}
+\index{rule induction|(}
 
 Recall the inductive and recursive definitions of even numbers in
 \autoref{sec:inductive-defs}:
@@ -892,7 +896,7 @@
 In general, let @{text I} be a (for simplicity unary) inductively defined
 predicate and let the rules in the definition of @{text I}
 be called @{text "rule\<^sub>1"}, \dots, @{text "rule\<^sub>n"}. A proof by rule
-induction follows this pattern:
+induction follows this pattern:\index{inductionrule@@{text"induction ... rule:"}}
 *}
 
 (*<*)
@@ -927,11 +931,11 @@
 In any induction, \isacom{case}~@{text name} sets up a list of assumptions
 also called @{text name}, which is subdivided into three parts:
 \begin{description}
-\item[@{text name.IH}] contains the induction hypotheses.
-\item[@{text name.hyps}] contains all the other hypotheses of this case in the
+\item[@{text name.IH}]\index{IH@@{text".IH"}} contains the induction hypotheses.
+\item[@{text name.hyps}]\index{hyps@@{text".hyps"}} contains all the other hypotheses of this case in the
 induction rule. For rule inductions these are the hypotheses of rule
 @{text name}, for structural inductions these are empty.
-\item[@{text name.prems}] contains the (suitably instantiated) premises
+\item[@{text name.prems}]\index{prems@@{text".prems"}} contains the (suitably instantiated) premises
 of the statement being proved, i.e. the @{text A\<^sub>i} when
 proving @{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}.
 \end{description}
@@ -949,9 +953,10 @@
 
 \subsection{Rule Inversion}
 \label{sec:rule-inversion}
+\index{rule inversion|(}
 
 Rule inversion is case analysis of which rule could have been used to
-derive some fact. The name \concept{rule inversion} emphasizes that we are
+derive some fact. The name \conceptnoidx{rule inversion} emphasizes that we are
 reasoning backwards: by which rules could some given fact have been proved?
 For the inductive definition of @{const ev}, rule inversion can be summarized
 like this:
@@ -1033,7 +1038,7 @@
 need to see the expanded version of the lemma. This is what we need to write:
 \begin{isabelle}
 \isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}\isanewline
-\isacom{proof}@{text"(induction \"r\" \"s\" \"t\" arbitrary: \<dots> rule: I.induct)"}
+\isacom{proof}@{text"(induction \"r\" \"s\" \"t\" arbitrary: \<dots> rule: I.induct)"}\index{inductionrule@@{text"induction ... rule:"}}\index{arbitrary@@{text"arbitrary:"}}
 \end{isabelle}
 Just like for rule inversion, cases that are impossible because of constructor clashes
 will not show up at all. Here is a concrete example: *}
@@ -1076,7 +1081,12 @@
 the induction hypotheses are instead found under the name @{text hyps}, like for the simpler
 @{text induct} method.
 \end{warn}
-
+\index{induction|)}
+\index{cases@@{text"cases"}|)}
+\index{case@\isacom{case}|)}
+\index{case?@@{text"?case"}|)}
+\index{rule induction|)}
+\index{rule inversion|)}
 
 \subsection*{Exercises}
 
diff -r 8cd866874590 -r d459a63ca42f src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Fri Feb 07 22:37:54 2014 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Sat Feb 08 20:34:10 2014 +0100
@@ -496,7 +496,7 @@
 
 
 \section{Inductive Definitions}
-\label{sec:inductive-defs}\index{inductive definition}
+\label{sec:inductive-defs}\index{inductive definition|(}
 
 Inductive definitions are the third important definition facility, after
 datatypes and recursive function.
@@ -531,7 +531,7 @@
 @{text "ev 0 \<Longrightarrow> ev (0 + 2) \<Longrightarrow> ev((0 + 2) + 2) = ev 4"}
 \end{quote}
 
-\subsubsection{Rule Induction}
+\subsubsection{Rule Induction}\index{rule induction|(}
 
 Showing that all even numbers have some property is more complicated.  For
 example, let us prove that the inductive definition of even numbers agrees
@@ -753,7 +753,7 @@
 apply(metis step)
 done
 
-text{*
+text{*\index{rule induction|)}
 
 \subsection{The General Case}
 
@@ -787,8 +787,8 @@
 additional premises not involving @{text I}, so-called \conceptidx{side
 conditions}{side condition}. In rule inductions, these side conditions appear as additional
 assumptions. The \isacom{for} clause seen in the definition of the reflexive
-transitive closure merely simplifies the form of the induction rule.
-
+transitive closure simplifies the induction rule.
+\index{inductive definition|)}
 
 \subsection*{Exercises}
 
diff -r 8cd866874590 -r d459a63ca42f src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Fri Feb 07 22:37:54 2014 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Sat Feb 08 20:34:10 2014 +0100
@@ -317,7 +317,7 @@
 but the induction hypothesis needs to be applied with
 @{term"a # ys"} instead of @{text ys}. Hence we prove the theorem
 for all @{text ys} instead of a fixed one. We can instruct induction
-to perform this generalization for us by adding @{text "arbitrary: ys"}.
+to perform this generalization for us by adding @{text "arbitrary: ys"}\index{arbitrary@@{text"arbitrary:"}}.
 *}
 (*<*)oops
 lemma "itrev xs ys = rev xs @ ys"