indexed document

--- a/src/Doc/ProgProve/Basics.thy	Thu Feb 06 13:04:06 2014 +0000
+++ b/src/Doc/ProgProve/Basics.thy	Thu Feb 06 18:31:31 2014 +0100
@@ -78,8 +78,8 @@
 disambiguate terms involving overloaded functions such as @{text "+"}, @{text
 "*"} and @{text"\<le>"}.
 
-Finally there are the universal quantifier @{text"\<And>"} and the implication
-@{text"\<Longrightarrow>"}. They are part of the Isabelle framework, not the logic
+Finally there are the universal quantifier @{text"\<And>"}\index{$4@\isasymAnd} and the implication
+@{text"\<Longrightarrow>"}\index{$3@\isasymLongrightarrow}. They are part of the Isabelle framework, not the logic
 HOL. Logically, they agree with their HOL counterparts @{text"\<forall>"} and
 @{text"\<longrightarrow>"}, but operationally they behave differently. This will become
 clearer as we go along.
@@ -103,8 +103,8 @@
 All the Isabelle text that you ever type needs to go into a theory.
 The general format of a theory @{text T} is
 \begin{quote}
-\isacom{theory} @{text T}\\
-\isacom{imports} @{text "T\<^sub>1 \<dots> T\<^sub>n"}\\
+\indexed{\isacom{theory}}{theory} @{text T}\\
+\indexed{\isacom{imports}}{imports} @{text "T\<^sub>1 \<dots> T\<^sub>n"}\\
 \isacom{begin}\\
 \emph{definitions, theorems and proofs}\\
 \isacom{end}

--- a/src/Doc/ProgProve/Logic.thy	Thu Feb 06 13:04:06 2014 +0000
+++ b/src/Doc/ProgProve/Logic.thy	Thu Feb 06 18:31:31 2014 +0100
@@ -17,11 +17,11 @@
   @{const True} ~\mid~
   @{const False} ~\mid~
   @{prop "term = term"}\\
- &\mid& @{prop"\<not> form"} ~\mid~
-  @{prop "form \<and> form"} ~\mid~
-  @{prop "form \<or> form"} ~\mid~
-  @{prop "form \<longrightarrow> form"}\\
- &\mid& @{prop"\<forall>x. form"} ~\mid~  @{prop"\<exists>x. form"}
+ &\mid& @{prop"\<not> form"}\index{$HOL4@\isasymnot} ~\mid~
+  @{prop "form \<and> form"}\index{$HOL0@\isasymand} ~\mid~
+  @{prop "form \<or> form"}\index{$HOL1@\isasymor} ~\mid~
+  @{prop "form \<longrightarrow> form"}\index{$HOL2@\isasymlongrightarrow}\\
+ &\mid& @{prop"\<forall>x. form"}\index{$HOL6@\isasymforall} ~\mid~  @{prop"\<exists>x. form"}\index{$HOL7@\isasymexists}
 \end{array}
 \]
 Terms are the ones we have seen all along, built from constants, variables,
@@ -80,21 +80,21 @@
 \section{Sets}
 \label{sec:Sets}
 
-Sets of elements of type @{typ 'a} have type @{typ"'a set"}.
+Sets of elements of type @{typ 'a} have type @{typ"'a set"}\index{set@@{text set}}.
 They can be finite or infinite. Sets come with the usual notation:
 \begin{itemize}
-\item @{term"{}"},\quad @{text"{e\<^sub>1,\<dots>,e\<^sub>n}"}
-\item @{prop"e \<in> A"},\quad @{prop"A \<subseteq> B"}
-\item @{term"A \<union> B"},\quad @{term"A \<inter> B"},\quad @{term"A - B"},\quad @{term"-A"}
+\item \indexed{@{term"{}"}}{$IMP042},\quad @{text"{e\<^sub>1,\<dots>,e\<^sub>n}"}
+\item @{prop"e \<in> A"}\index{$HOLSet0@\isasymin},\quad @{prop"A \<subseteq> B"}\index{$HOLSet2@\isasymsubseteq}
+\item @{term"A \<union> B"}\index{$HOLSet4@\isasymunion},\quad @{term"A \<inter> B"}\index{$HOLSet5@\isasyminter},\quad @{term"A - B"},\quad @{term"-A"}
 \end{itemize}
 (where @{term"A-B"} and @{text"-A"} are set difference and complement)
 and much more. @{const UNIV} is the set of all elements of some type.
-Set comprehension is written @{term"{x. P}"}
-rather than @{text"{x | P}"}.
+Set comprehension\index{set comprehension} is written
+@{term"{x. P}"}\index{$IMP042@@{term"{x. P}"}} rather than @{text"{x | P}"}.
 \begin{warn}
 In @{term"{x. P}"} the @{text x} must be a variable. Set comprehension
 involving a proper term @{text t} must be written
-\noquotes{@{term[source] "{t | x y. P}"}},
+\noquotes{@{term[source] "{t | x y. P}"}}\index{$IMP042@@{text"{t |x. P}"}},
 where @{text "x y"} are those free variables in @{text t}
 that occur in @{text P}.
 This is just a shorthand for @{term"{v. EX x y. v = t \<and> P}"}, where
@@ -114,7 +114,8 @@
 Sets also allow bounded quantifications @{prop"ALL x : A. P"} and
 @{prop"EX x : A. P"}.
 
-For the more ambitious, there are also @{text"\<Union>"} and @{text"\<Inter>"}:
+For the more ambitious, there are also @{text"\<Union>"}\index{$HOLSet6@\isasymUnion}
+and @{text"\<Inter>"}\index{$HOLSet7@\isasymInter}:
 \begin{center}
 @{thm Union_eq} \qquad @{thm Inter_eq}
 \end{center}
@@ -131,11 +132,11 @@
 Some other frequently useful functions on sets are the following:
 \begin{center}
 \begin{tabular}{l@ {\quad}l}
-@{const_typ set} & converts a list to the set of its elements\\
-@{const_typ finite} & is true iff its argument is finite\\
-@{const_typ card} & is the cardinality of a finite set\\
+@{const_typ set}\index{set@@{const set}} & converts a list to the set of its elements\\
+@{const_typ finite}\index{finite@@{const finite}} & is true iff its argument is finite\\
+@{const_typ card}\index{card@@{const card}} & is the cardinality of a finite set\\
  & and is @{text 0} for all infinite sets\\
-@{thm image_def} & is the image of a function over a set
+@{thm image_def}\index{$IMP042@@{term"f ` A"}} & is the image of a function over a set
 \end{tabular}
 \end{center}
 See \cite{Nipkow-Main} for the wealth of further predefined functions in theory
@@ -165,7 +166,7 @@
 
 \section{Proof Automation}
 
-So far we have only seen @{text simp} and @{text auto}: Both perform
+So far we have only seen @{text simp} and \indexed{@{text auto}}{auto}: Both perform
 rewriting, both can also prove linear arithmetic facts (no multiplication),
 and @{text auto} is also able to prove simple logical or set-theoretic goals:
 *}
@@ -195,7 +196,7 @@
 Hence all our proof methods only differ in how incomplete they are.
 
 A proof method that is still incomplete but tries harder than @{text auto} is
-@{text fastforce}.  It either succeeds or fails, it acts on the first
+\indexed{@{text fastforce}}{fastforce}.  It either succeeds or fails, it acts on the first
 subgoal only, and it can be modified just like @{text auto}, e.g.\
 with @{text "simp add"}. Here is a typical example of what @{text fastforce}
 can do:
@@ -210,7 +211,7 @@
 becomes more complicated. In a few cases, its slow version @{text force}
 succeeds where @{text fastforce} fails.
 
-The method of choice for complex logical goals is @{text blast}. In the
+The method of choice for complex logical goals is \indexed{@{text blast}}{blast}. In the
 following example, @{text T} and @{text A} are two binary predicates. It
 is shown that if @{text T} is total, @{text A} is antisymmetric and @{text T} is
 a subset of @{text A}, then @{text A} is a subset of @{text T}:
@@ -236,7 +237,7 @@
 Because of its strength in logic and sets and its weakness in equality reasoning, it complements the earlier proof methods.
 
 
-\subsection{Sledgehammer}
+\subsection{\concept{Sledgehammer}}
 
 Command \isacom{sledgehammer} calls a number of external automatic
 theorem provers (ATPs) that run for up to 30 seconds searching for a
@@ -256,7 +257,7 @@
 text{* We do not explain how the proof was found but what this command
 means. For a start, Isabelle does not trust external tools (and in particular
 not the translations from Isabelle's logic to those tools!)
-and insists on a proof that it can check. This is what @{text metis} does.
+and insists on a proof that it can check. This is what \indexed{@{text metis}}{metis} does.
 It is given a list of lemmas and tries to find a proof just using those lemmas
 (and pure logic). In contrast to @{text simp} and friends that know a lot of
 lemmas already, using @{text metis} manually is tedious because one has
@@ -284,7 +285,7 @@
 @{text"\<longleftrightarrow>"}. Strictly speaking, this is known as \concept{linear arithmetic}
 because it does not involve multiplication, although multiplication with
 numbers, e.g.\ @{text"2*n"} is allowed. Such formulas can be proved by
-@{text arith}:
+\indexed{@{text arith}}{arith}:
 *}
 
 lemma "\<lbrakk> (a::nat) \<le> x + b; 2*x < c \<rbrakk> \<Longrightarrow> 2*a + 1 \<le> 2*b + c"
@@ -378,7 +379,7 @@
 \end{enumerate}
 This is the command to apply rule @{text xyz}:
 \begin{quote}
-\isacom{apply}@{text"(rule xyz)"}
+\isacom{apply}@{text"(rule xyz)"}\index{rule@@{text rule}}
 \end{quote}
 This is also called \concept{backchaining} with rule @{text xyz}.
 
@@ -410,12 +411,12 @@
 Isabelle knows about these and a number of other introduction rules.
 The command
 \begin{quote}
-\isacom{apply} @{text rule}
+\isacom{apply} @{text rule}\index{rule@@{text rule}}
 \end{quote}
 automatically selects the appropriate rule for the current subgoal.
 
 You can also turn your own theorems into introduction rules by giving them
-the @{text"intro"} attribute, analogous to the @{text simp} attribute.  In
+the \indexed{@{text"intro"}}{intro} attribute, analogous to the @{text simp} attribute.  In
 that case @{text blast}, @{text fastforce} and (to a limited extent) @{text
 auto} will automatically backchain with those theorems. The @{text intro}
 attribute should be used with care because it increases the search space and
@@ -469,7 +470,7 @@
 Therefore @{text blast}, @{text fastforce} and @{text auto} support a modifier
 @{text dest} which instructs the proof method to use certain rules in a
 forward fashion. If @{text r} is of the form \mbox{@{text "A \<Longrightarrow> B"}}, the modifier
-\mbox{@{text"dest: r"}}
+\mbox{@{text"dest: r"}}\index{dest@@{text"dest:"}}
 allows proof search to reason forward with @{text r}, i.e.\
 to replace an assumption @{text A'}, where @{text A'} unifies with @{text A},
 with the correspondingly instantiated @{text B}. For example, @{thm[source,show_question_marks] Suc_leD} is the theorem \mbox{@{thm Suc_leD}}, which works well for forward reasoning:
@@ -495,7 +496,7 @@
 
 
 \section{Inductive Definitions}
-\label{sec:inductive-defs}
+\label{sec:inductive-defs}\index{inductive definition}
 
 Inductive definitions are the third important definition facility, after
 datatypes and recursive function.
@@ -624,7 +625,7 @@
 
 text{* \indent
 Rule induction is applied by giving the induction rule explicitly via the
-@{text"rule:"} modifier:*}
+@{text"rule:"} modifier:\index{inductionrule@@{text"induction ... rule:"}}*}
 
 lemma "ev m \<Longrightarrow> even m"
 apply(induction rule: ev.induct)
@@ -653,7 +654,8 @@
 text{* The rules for @{const ev} make perfect simplification and introduction
 rules because their premises are always smaller than the conclusion. It
 makes sense to turn them into simplification and introduction rules
-permanently, to enhance proof automation: *}
+permanently, to enhance proof automation. They are named @{thm[source] ev.intros}
+\index{intros@@{text".intros"}} by Isabelle: *}
 
 declare ev.intros[simp,intro]
 
@@ -735,7 +737,7 @@
 which we abbreviate by @{prop"P x y"}. These are our two subgoals:
 @{subgoals[display,indent=0]}
 The first one is @{prop"P x x"}, the result of case @{thm[source]refl},
-and it is trivial.
+and it is trivial:\index{assumption@@{text assumption}}
 *}
 apply(assumption)
 txt{* Let us examine subgoal @{text 2}, case @{thm[source] step}.

--- a/src/Doc/ProgProve/Types_and_funs.thy	Thu Feb 06 13:04:06 2014 +0000
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Thu Feb 06 18:31:31 2014 +0100
@@ -12,7 +12,7 @@
 
 type_synonym string = "char list"
 
-text{*
+text{*\index{string@@{text string}}
 Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader.
 
 \subsection{Datatypes}
@@ -21,7 +21,7 @@
 The general form of a datatype definition looks like this:
 \begin{quote}
 \begin{tabular}{@ {}rclcll}
-\isacom{datatype} @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}
+\indexed{\isacom{datatype}}{datatype} @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}
      & = & $C_1 \ @{text"\""}\tau_{1,1}@{text"\""} \dots @{text"\""}\tau_{1,n_1}@{text"\""}$ \\
      & $|$ & \dots \\
      & $|$ & $C_k \ @{text"\""}\tau_{k,1}@{text"\""} \dots @{text"\""}\tau_{k,n_k}@{text"\""}$
@@ -39,14 +39,14 @@
 \end{tabular}
 \end{itemize}
 The fact that any value of the datatype is built from the constructors implies
-the \concept{structural induction} rule: to show
+the \concept{structural induction}\index{induction} rule: to show
 $P~x$ for all $x$ of type @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"},
 one needs to show $P(C_i\ x_1 \dots x_{n_i})$ (for each $i$) assuming
 $P(x_j)$ for all $j$ where $\tau_{i,j} =$~@{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}.
 Distinctness and injectivity are applied automatically by @{text auto}
 and other proof methods. Induction must be applied explicitly.
 
-Datatype values can be taken apart with case-expressions, for example
+Datatype values can be taken apart with case expressions\index{case expression}\index{case expression@@{text "case ... of"}}, for example
 \begin{quote}
 \noquotes{@{term[source] "(case xs of [] \<Rightarrow> 0 | x # _ \<Rightarrow> Suc x)"}}
 \end{quote}
@@ -75,7 +75,7 @@
 An application of @{text auto} finishes the proof.
 
 A very simple but also very useful datatype is the predefined
-@{datatype[display] option}
+@{datatype[display] option}\index{option@@{text option}}\index{None@@{const None}}\index{Some@@{const Some}}
 Its sole purpose is to add a new element @{const None} to an existing
 type @{typ 'a}. To make sure that @{const None} is distinct from all the
 elements of @{typ 'a}, you wrap them up in @{const Some} and call
@@ -100,7 +100,7 @@
 \subsection{Definitions}
 
 Non recursive functions can be defined as in the following example:
-*}
+\index{definition@\isacom{definition}}*}
 
 definition sq :: "nat \<Rightarrow> nat" where
 "sq n = n * n"
@@ -111,7 +111,7 @@
 \subsection{Abbreviations}
 
 Abbreviations are similar to definitions:
-*}
+\index{abbreviation@\isacom{abbreviation}}*}
 
 abbreviation sq' :: "nat \<Rightarrow> nat" where
 "sq' n \<equiv> n * n"
@@ -132,7 +132,7 @@
 \subsection{Recursive Functions}
 \label{sec:recursive-funs}
 
-Recursive functions are defined with \isacom{fun} by pattern matching
+Recursive functions are defined with \indexed{\isacom{fun}}{fun} by pattern matching
 over datatype constructors. The order of equations matters. Just as in
 functional programming languages. However, all HOL functions must be
 total. This simplifies the logic---terms are always defined---but means
@@ -187,7 +187,7 @@
 \emph{Let @{text f} be a recursive function.
 If the definition of @{text f} is more complicated
 than having one equation for each constructor of some datatype,
-then properties of @{text f} are best proved via @{text "f.induct"}.}
+then properties of @{text f} are best proved via @{text "f.induct"}.\index{inductionrule@@{text".induct"}}}
 \end{quote}
 
 The general case is often called \concept{computation induction},
@@ -203,7 +203,7 @@
 \end{quote}
 If @{text "f :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> \<tau>"} then @{text"f.induct"} is applied like this:
 \begin{quote}
-\isacom{apply}@{text"(induction x\<^sub>1 \<dots> x\<^sub>n rule: f.induct)"}
+\isacom{apply}@{text"(induction x\<^sub>1 \<dots> x\<^sub>n rule: f.induct)"}\index{inductionrule@@{text"induction ... rule:"}}
 \end{quote}
 where typically there is a call @{text"f x\<^sub>1 \<dots> x\<^sub>n"} in the goal.
 But note that the induction rule does not mention @{text f} at all,
@@ -238,7 +238,7 @@
 \end{exercise}
 
 
-\section{Induction Heuristics}
+\section{Induction Heuristics}\index{induction heuristics}
 
 We have already noted that theorems about recursive functions are proved by
 induction. In case the function has more than one argument, we have followed
@@ -452,7 +452,7 @@
 leads to nontermination: when trying to rewrite @{prop"n<m"} to @{const True}
 one first has to prove \mbox{@{prop"Suc n < m"}}, which can be rewritten to @{const True} provided @{prop"Suc(Suc n) < m"}, \emph{ad infinitum}.
 
-\subsection{The @{text simp} Proof Method}
+\subsection{The \indexed{@{text simp}}{simp} Proof Method}
 \label{sec:simp}
 
 So far we have only used the proof method @{text auto}.  Method @{text simp}
@@ -530,9 +530,9 @@
 \isacom{apply}@{text"(simp split: nat.split)"}
 \end{quote}
 splits all case-expressions over natural numbers. For an arbitrary
-datatype @{text t} it is @{text "t.split"} instead of @{thm[source] nat.split}.
+datatype @{text t} it is @{text "t.split"}\index{split@@{text".split"}} instead of @{thm[source] nat.split}.
 Method @{text auto} can be modified in exactly the same way.
-The modifier @{text "split:"} can be followed by multiple names.
+The modifier \indexed{@{text "split:"}}{split} can be followed by multiple names.
 Splitting if or case-expressions in the assumptions requires 
 @{text "split: if_splits"} or @{text "split: t.splits"}.