src/Doc/ProgProve/Bool_nat_list.thy

 
 These are the most important predefined types. We go through them one by one.
 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:
 *}
 
 fun conj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where

 "conj _ _ = False"
 
 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.
 There are many predefined functions: @{text "+"}, @{text "*"}, @{text
 "\<le>"}, etc. Here is how you could define your own addition:

 as informal text comprehensible to a reader familiar with traditional
 mathematical proofs. Later on we will introduce an Isabelle proof language
 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:
 *}
 (*<*)

 "rev (Cons x xs) = app (rev xs) (Cons x Nil)"
 
 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))"
 
 text{* yields the result @{value "rev(Cons True (Cons False Nil))"}. This works symbolically, too: *}
 

 theorem rev_rev [simp]: "rev(rev xs) = xs"
 
 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: *}
 
 apply(induction xs)
 

 \label{sec:predeflists}
 
 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"\" |"}\\
 @{text"\""}@{thm map.simps(2)}@{text"\""}
 \end{isabelle}
 
 \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"}
 \end{isabelle}
 Note that since HOL is a logic of total functions, @{term"hd []"} is defined,