started index

--- a/src/Doc/ProgProve/Basics.thy	Tue Feb 04 09:04:59 2014 +0000
+++ b/src/Doc/ProgProve/Basics.thy	Tue Feb 04 17:38:54 2014 +0100
@@ -17,7 +17,7 @@
 \begin{description}
 \item[base types,] 
 in particular @{typ bool}, the type of truth values,
-@{typ nat}, the type of natural numbers ($\mathbb{N}$), and @{typ int},
+@{typ nat}, the type of natural numbers ($\mathbb{N}$), and \indexed{@{typ int}}{int},
 the type of mathematical integers ($\mathbb{Z}$).
 \item[type constructors,]
  in particular @{text list}, the type of
@@ -33,7 +33,7 @@
 not @{typ"('a \<Rightarrow> 'b) list"}: postfix type constructors have precedence
 over @{text"\<Rightarrow>"}.
 
-\concept{Terms} are formed as in functional programming by
+\conceptidx{Terms}{term} are formed as in functional programming by
 applying functions to arguments. If @{text f} is a function of type
 @{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} and @{text t} is a term of type
 @{text"\<tau>\<^sub>1"} then @{term"f t"} is a term of type @{text"\<tau>\<^sub>2"}. We write @{text "t :: \<tau>"} to mean that term @{text t} has type @{text \<tau>}.
@@ -58,21 +58,21 @@
 Terms may also contain @{text "\<lambda>"}-abstractions. For example,
 @{term "\<lambda>x. x"} is the identity function.
 
-\concept{Formulas} are terms of type @{text bool}.
+\conceptidx{Formulas}{formula} are terms of type @{text bool}.
 There are the basic constants @{term True} and @{term False} and
 the usual logical connectives (in decreasing order of precedence):
 @{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"}, @{text"\<longrightarrow>"}.
 
-\concept{Equality} is available in the form of the infix function @{text "="}
+\conceptidx{Equality}{equality} is available in the form of the infix function @{text "="}
 of type @{typ "'a \<Rightarrow> 'a \<Rightarrow> bool"}. It also works for formulas, where
 it means ``if and only if''.
 
-\concept{Quantifiers} are written @{prop"\<forall>x. P"} and @{prop"\<exists>x. P"}.
+\conceptidx{Quantifiers}{quantifier} are written @{prop"\<forall>x. P"} and @{prop"\<exists>x. P"}.
 
 Isabelle automatically computes the type of each variable in a term. This is
 called \concept{type inference}.  Despite type inference, it is sometimes
-necessary to attach explicit \concept{type constraints} (or \concept{type
-annotations}) to a variable or term.  The syntax is @{text "t :: \<tau>"} as in
+necessary to attach an explicit \concept{type constraint} (or \concept{type
+annotation}) to a variable or term.  The syntax is @{text "t :: \<tau>"} as in
 \mbox{\noquotes{@{prop[source] "m < (n::nat)"}}}. Type constraints may be
 needed to
 disambiguate terms involving overloaded functions such as @{text "+"}, @{text
@@ -111,13 +111,13 @@
 \end{quote}
 where @{text "T\<^sub>1 \<dots> T\<^sub>n"} are the names of existing
 theories that @{text T} is based on. The @{text "T\<^sub>i"} are the
-direct \concept{parent theories} of @{text T}.
+direct \conceptidx{parent theories}{parent theory} of @{text T}.
 Everything defined in the parent theories (and their parents, recursively) is
 automatically visible. Each theory @{text T} must
 reside in a \concept{theory file} named @{text "T.thy"}.
 
 \begin{warn}
-HOL contains a theory @{text Main}, the union of all the basic
+HOL contains a theory @{theory Main}\index{Main@@{theory Main}}, the union of all the basic
 predefined theories like arithmetic, lists, sets, etc.
 Unless you know what you are doing, always include @{text Main}
 as a direct or indirect parent of all your theories.

--- a/src/Doc/ProgProve/Bool_nat_list.thy	Tue Feb 04 09:04:59 2014 +0000
+++ b/src/Doc/ProgProve/Bool_nat_list.thy	Tue Feb 04 17:38:54 2014 +0100
@@ -12,11 +12,11 @@
 Based on examples we learn how to define (possibly recursive) functions and
 prove theorems about them by induction and simplification.
 
-\subsection{Type @{typ bool}}
+\subsection{Type \indexed{@{typ bool}}{bool}}
 
 The type of boolean values is a predefined datatype
 @{datatype[display] bool}
-with the two values @{const True} and @{const False} and
+with the two values \indexed{@{const True}}{True} and \indexed{@{const False}}{False} and
 with many predefined functions:  @{text "\<not>"}, @{text "\<and>"}, @{text "\<or>"}, @{text
 "\<longrightarrow>"} etc. Here is how conjunction could be defined by pattern matching:
 *}
@@ -28,10 +28,10 @@
 text{* Both the datatype and function definitions roughly follow the syntax
 of functional programming languages.
 
-\subsection{Type @{typ nat}}
+\subsection{Type \indexed{@{typ nat}}{nat}}
 
 Natural numbers are another predefined datatype:
-@{datatype[display] nat}
+@{datatype[display] nat}\index{Suc@@{const Suc}}
 All values of type @{typ nat} are generated by the constructors
 @{text 0} and @{const Suc}. Thus the values of type @{typ nat} are
 @{text 0}, @{term"Suc 0"}, @{term"Suc(Suc 0)"} etc.
@@ -148,7 +148,7 @@
 that is closer to traditional informal mathematical language and is often
 directly readable.
 
-\subsection{Type @{text list}}
+\subsection{Type \indexed{@{text list}}{list}}
 
 Although lists are already predefined, we define our own copy just for
 demonstration purposes:
@@ -184,7 +184,7 @@
 text{* By default, variables @{text xs}, @{text ys} and @{text zs} are of
 @{text list} type.
 
-Command \isacom{value} evaluates a term. For example, *}
+Command \isacom{value}\indexed{{\sf\textbf{value}}}{value} evaluates a term. For example, *}
 
 value "rev(Cons True (Cons False Nil))"
 
@@ -240,7 +240,7 @@
 txt{* Commands \isacom{theorem} and \isacom{lemma} are
 interchangeable and merely indicate the importance we attach to a
 proposition. Via the bracketed attribute @{text simp} we also tell Isabelle
-to make the eventual theorem a \concept{simplification rule}: future proofs
+to make the eventual theorem a \conceptnoidx{simplification rule}: future proofs
 involving simplification will replace occurrences of @{term"rev(rev xs)"} by
 @{term"xs"}. The proof is by induction: *}
 
@@ -383,15 +383,15 @@
 Isabelle's predefined lists are the same as the ones above, but with
 more syntactic sugar:
 \begin{itemize}
-\item @{text "[]"} is @{const Nil},
-\item @{term"x # xs"} is @{term"Cons x xs"},
+\item @{text "[]"} is \indexed{@{const Nil}}{Nil},
+\item @{term"x # xs"} is @{term"Cons x xs"}\index{Cons@@{const Cons}},
 \item @{text"[x\<^sub>1, \<dots>, x\<^sub>n]"} is @{text"x\<^sub>1 # \<dots> # x\<^sub>n # []"}, and
 \item @{term "xs @ ys"} is @{term"app xs ys"}.
 \end{itemize}
 There is also a large library of predefined functions.
 The most important ones are the length function
-@{text"length :: 'a list \<Rightarrow> nat"} (with the obvious definition),
-and the map function that applies a function to all elements of a list:
+@{text"length :: 'a list \<Rightarrow> nat"}\index{length@@{const length}} (with the obvious definition),
+and the \indexed{@{const map}}{map} function that applies a function to all elements of a list:
 \begin{isabelle}
 \isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
 @{text"\""}@{thm map.simps(1)}@{text"\" |"}\\
@@ -401,11 +401,11 @@
 \ifsem
 Also useful are the \concept{head} of a list, its first element,
 and the \concept{tail}, the rest of the list:
-\begin{isabelle}
+\begin{isabelle}\index{hd@@{const hd}}
 \isacom{fun} @{text"hd :: 'a list \<Rightarrow> 'a"}\\
 @{prop"hd(x#xs) = x"}
 \end{isabelle}
-\begin{isabelle}
+\begin{isabelle}\index{tl@@{const tl}}
 \isacom{fun} @{text"tl :: 'a list \<Rightarrow> 'a list"}\\
 @{prop"tl [] = []"} @{text"|"}\\
 @{prop"tl(x#xs) = xs"}

--- a/src/Doc/ProgProve/Isar.thy	Tue Feb 04 09:04:59 2014 +0000
+++ b/src/Doc/ProgProve/Isar.thy	Tue Feb 04 17:38:54 2014 +0100
@@ -76,7 +76,7 @@
 \S\ref{sec:forward-proof}---hence the \dots\ in the above grammar.  Note
 that assumptions, intermediate \isacom{have} statements and global lemmas all
 have the same status and are thus collectively referred to as
-\concept{facts}.
+\conceptidx{facts}{fact}.
 
 Fact names can stand for whole lists of facts. For example, if @{text f} is
 defined by command \isacom{fun}, @{text"f.simps"} refers to the whole list of
@@ -499,7 +499,7 @@
 $\vdots$\\
 \isacom{from} @{text "`x>0`"} \dots
 \end{quote}
-Note that the quotes around @{text"x>0"} are \concept{back quotes}.
+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}}

--- a/src/Doc/ProgProve/Logic.thy	Tue Feb 04 09:04:59 2014 +0000
+++ b/src/Doc/ProgProve/Logic.thy	Tue Feb 04 17:38:54 2014 +0100
@@ -190,7 +190,7 @@
 \item They show you were they got stuck, giving you an idea how to continue.
 \item They perform the obvious steps but are highly incomplete.
 \end{itemize}
-A proof method is \concept{complete} if it can prove all true formulas.
+A proof method is \conceptnoidx{complete} if it can prove all true formulas.
 There is no complete proof method for HOL, not even in theory.
 Hence all our proof methods only differ in how incomplete they are.
 
@@ -331,11 +331,11 @@
 \subsection{Instantiating Unknowns}
 
 We had briefly mentioned earlier that after proving some theorem,
-Isabelle replaces all free variables @{text x} by so called \concept{unknowns}
+Isabelle replaces all free variables @{text x} by so called \conceptidx{unknowns}{unknown}
 @{text "?x"}. We can see this clearly in rule @{thm[source] conjI}.
 These unknowns can later be instantiated explicitly or implicitly:
 \begin{itemize}
-\item By hand, using \concept{@{text of}}.
+\item By hand, using \indexed{@{text of}}{of}.
 The expression @{text"conjI[of \"a=b\" \"False\"]"}
 instantiates the unknowns in @{thm[source] conjI} from left to right with the
 two formulas @{text"a=b"} and @{text False}, yielding the rule
@@ -345,20 +345,20 @@
 the unknowns in the theorem @{text th} from left to right with the terms
 @{text string\<^sub>1} to @{text string\<^sub>n}.
 
-\item By unification. \concept{Unification} is the process of making two
+\item By unification. \conceptidx{Unification}{unification} is the process of making two
 terms syntactically equal by suitable instantiations of unknowns. For example,
 unifying @{text"?P \<and> ?Q"} with \mbox{@{prop"a=b \<and> False"}} instantiates
 @{text "?P"} with @{prop "a=b"} and @{text "?Q"} with @{prop False}.
 \end{itemize}
 We need not instantiate all unknowns. If we want to skip a particular one we
 can just write @{text"_"} instead, for example @{text "conjI[of _ \"False\"]"}.
-Unknowns can also be instantiated by name using \concept{@{text "where"}}, for example
+Unknowns can also be instantiated by name using \indexed{@{text "where"}}{where}, for example
 @{text "conjI[where ?P = \"a=b\""} \isacom{and} @{text"?Q = \"False\"]"}.
 
 
 \subsection{Rule Application}
 
-\concept{Rule application} means applying a rule backwards to a proof state.
+\conceptidx{Rule application}{rule application} means applying a rule backwards to a proof state.
 For example, applying rule @{thm[source]conjI} to a proof state
 \begin{quote}
 @{text"1.  \<dots>  \<Longrightarrow> A \<and> B"}
@@ -385,7 +385,7 @@
 \subsection{Introduction Rules}
 
 Conjunction introduction (@{thm[source] conjI}) is one example of a whole
-class of rules known as \concept{introduction rules}. They explain under which
+class of rules known as \conceptidx{introduction rules}{introduction rule}. They explain under which
 premises some logical construct can be introduced. Here are some further
 useful introduction rules:
 \[
@@ -438,7 +438,7 @@
 Forward proof means deriving new theorems from old theorems. We have already
 seen a very simple form of forward proof: the @{text of} operator for
 instantiating unknowns in a theorem. The big brother of @{text of} is
-\concept{@{text OF}} for applying one theorem to others. Given a theorem @{prop"A \<Longrightarrow> B"} called
+\indexed{@{text OF}}{OF} for applying one theorem to others. Given a theorem @{prop"A \<Longrightarrow> B"} called
 @{text r} and a theorem @{text A'} called @{text r'}, the theorem @{text
 "r[OF r']"} is the result of applying @{text r} to @{text r'}, where @{text
 r} should be viewed as a function taking a theorem @{text A} and returning
@@ -782,8 +782,8 @@
 
 The above format for inductive definitions is simplified in a number of
 respects. @{text I} can have any number of arguments and each rule can have
-additional premises not involving @{text I}, so-called \concept{side
-conditions}. In rule inductions, these side-conditions appear as additional
+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.
 

--- a/src/Doc/ProgProve/Types_and_funs.thy	Tue Feb 04 09:04:59 2014 +0000
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Tue Feb 04 17:38:54 2014 +0100
@@ -359,14 +359,15 @@
 
 \section{Simplification}
 
-So far we have talked a lot about simplifying terms without explaining the concept. \concept{Simplification} means
+So far we have talked a lot about simplifying terms without explaining the concept.
+\conceptidx{Simplification}{simplification} means
 \begin{itemize}
 \item using equations $l = r$ from left to right (only),
 \item as long as possible.
 \end{itemize}
 To emphasize the directionality, equations that have been given the
-@{text"simp"} attribute are called \concept{simplification}
-rules. Logically, they are still symmetric, but proofs by
+@{text"simp"} attribute are called \conceptidx{simplification rules}{simplification rule}.
+Logically, they are still symmetric, but proofs by
 simplification use them only in the left-to-right direction.  The proof tool
 that performs simplifications is called the \concept{simplifier}. It is the
 basis of @{text auto} and other related proof methods.
@@ -393,7 +394,7 @@
 \end{array}
 \]
 Simplification is often also called \concept{rewriting}
-and simplification rules \concept{rewrite rules}.
+and simplification rules \conceptidx{rewrite rules}{rewrite rule}.
 
 \subsection{Simplification Rules}
 

--- a/src/Doc/ProgProve/document/prelude.tex	Tue Feb 04 09:04:59 2014 +0000
+++ b/src/Doc/ProgProve/document/prelude.tex	Tue Feb 04 17:38:54 2014 +0100
@@ -59,9 +59,14 @@
 \renewenvironment{isamarkuptxt}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}
 
 \newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}}
-\newcommand{\concept}[1]{\textbf{#1}}
 \newcommand{\xsymbol}[1]{\texttt{\char`\\\char`<#1>}}
 
+%index
+\newcommand{\conceptnoidx}[1]{\textbf{#1}}
+\newcommand{\concept}[1]{\conceptnoidx{#1}\index{#1}}
+\newcommand{\conceptidx}[2]{\conceptnoidx{#1}\index{#2}}
+\newcommand{\indexed}[2]{#1\index{#2@#1}}
+
 \newcommand{\isabox}{\fbox}
 \newcommand{\bigisabox}[1]
 {\isabox{\renewcommand{\isanewline}{\\}%