# HG changeset patch # User nipkow # Date 1391531934 -3600 # Node ID 834a84553e0289d6d74b13b7ae9e47dccea3ac6b # Parent 885500f4aa6a570fd046e96c3348a92d75cc94af started index diff -r 885500f4aa6a -r 834a84553e02 src/Doc/ProgProve/Basics.thy --- 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 \ 'b) list"}: postfix type constructors have precedence over @{text"\"}. -\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"\\<^sub>1 \ \\<^sub>2"} and @{text t} is a term of type @{text"\\<^sub>1"} then @{term"f t"} is a term of type @{text"\\<^sub>2"}. We write @{text "t :: \"} to mean that term @{text t} has type @{text \}. @@ -58,21 +58,21 @@ Terms may also contain @{text "\"}-abstractions. For example, @{term "\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"\"}, @{text"\"}, @{text"\"}, @{text"\"}. -\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 \ 'a \ bool"}. It also works for formulas, where it means ``if and only if''. -\concept{Quantifiers} are written @{prop"\x. P"} and @{prop"\x. P"}. +\conceptidx{Quantifiers}{quantifier} are written @{prop"\x. P"} and @{prop"\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 :: \"} as in +necessary to attach an explicit \concept{type constraint} (or \concept{type +annotation}) to a variable or term. The syntax is @{text "t :: \"} 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 \ 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. diff -r 885500f4aa6a -r 834a84553e02 src/Doc/ProgProve/Bool_nat_list.thy --- 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 "\"}, @{text "\"}, @{text "\"}, @{text "\"} 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, \, x\<^sub>n]"} is @{text"x\<^sub>1 # \ # 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 \ nat"} (with the obvious definition), -and the map function that applies a function to all elements of a list: +@{text"length :: 'a list \ 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 \ 'b) \ 'a list \ '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 \ 'a"}\\ @{prop"hd(x#xs) = x"} \end{isabelle} -\begin{isabelle} +\begin{isabelle}\index{tl@@{const tl}} \isacom{fun} @{text"tl :: 'a list \ 'a list"}\\ @{prop"tl [] = []"} @{text"|"}\\ @{prop"tl(x#xs) = xs"} diff -r 885500f4aa6a -r 834a84553e02 src/Doc/ProgProve/Isar.thy --- 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}} diff -r 885500f4aa6a -r 834a84553e02 src/Doc/ProgProve/Logic.thy --- 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 \ ?Q"} with \mbox{@{prop"a=b \ 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. \ \ A \ 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 \ B"} called +\indexed{@{text OF}}{OF} for applying one theorem to others. Given a theorem @{prop"A \ 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. diff -r 885500f4aa6a -r 834a84553e02 src/Doc/ProgProve/Types_and_funs.thy --- 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} diff -r 885500f4aa6a -r 834a84553e02 src/Doc/ProgProve/document/prelude.tex --- 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}{\\}%