src/Doc/ProgProve/Types_and_funs.thy

 imports Main
 begin
 (*>*)
 text{*
 \vspace{-5ex}
-\section{Type and function definitions}
+\section{Type and Function Definitions}
 
 Type synonyms are abbreviations for existing types, for example
 *}
 
 type_synonym string = "char list"

 if abused, they can lead to a confusing discrepancy between the internal and
 external view of a term.
 
 The ASCII representation of @{text"\<equiv>"} is \texttt{==} or \xsymbol{equiv}.
 
-\subsection{Recursive functions}
+\subsection{Recursive Functions}
 \label{sec:recursive-funs}
 
 Recursive functions are defined with \isacom{fun} by pattern matching
 over datatype constructors. The order of equations matters. Just as in
 functional programming languages. However, all HOL functions must be

 \end{quote}
 where typically there is a call @{text"f x\<^isub>1 \<dots> x\<^isub>n"} in the goal.
 But note that the induction rule does not mention @{text f} at all,
 except in its name, and is applicable independently of @{text f}.
 
-\section{Induction heuristics}
+\section{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
 the following heuristic in the proofs about the append function:
 \begin{quote}

 \end{array}
 \]
 Simplification is often also called \concept{rewriting}
 and simplification rules \concept{rewrite rules}.
 
-\subsection{Simplification rules}
+\subsection{Simplification Rules}
 
 The attribute @{text"simp"} declares theorems to be simplification rules,
 which the simplifier will use automatically. In addition,
 \isacom{datatype} and \isacom{fun} commands implicitly declare some
 simplification rules: \isacom{datatype} the distinctness and injectivity

 rules. Equations that may be counterproductive as simplification rules
 should only be used in specific proof steps (see \S\ref{sec:simp} below).
 Distributivity laws, for example, alter the structure of terms
 and can produce an exponential blow-up.
 
-\subsection{Conditional simplification rules}
+\subsection{Conditional Simplification Rules}
 
 Simplification rules can be conditional.  Before applying such a rule, the
 simplifier will first try to prove the preconditions, again by
 simplification. For example, given the simplification rules
 \begin{quote}

 @{prop "Suc n < m \<Longrightarrow> (n < m) = True"}
 \end{quote}
 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 @{text simp} Proof Method}
 \label{sec:simp}
 
 So far we have only used the proof method @{text auto}.  Method @{text simp}
 is the key component of @{text auto}, but @{text auto} can do much more. In
 some cases, @{text auto} is overeager and modifies the proof state too much.

 
 Note that @{text simp} acts only on subgoal 1, @{text auto} acts on all
 subgoals. There is also @{text simp_all}, which applies @{text simp} to
 all subgoals.
 
-\subsection{Rewriting with definitions}
+\subsection{Rewriting With Definitions}
 \label{sec:rewr-defs}
 
 Definitions introduced by the command \isacom{definition}
 can also be used as simplification rules,
 but by default they are not: the simplifier does not expand them

 \isacom{apply}@{text"(simp add: f_def)"}
 \end{quote}
 In particular, let-expressions can be unfolded by
 making @{thm[source] Let_def} a simplification rule.
 
-\subsection{Case splitting with @{text simp}}
+\subsection{Case Splitting With @{text simp}}
 
 Goals containing if-expressions are automatically split into two cases by
 @{text simp} using the rule
 \begin{quote}
 @{prop"P(if A then s else t) = ((A \<longrightarrow> P(s)) \<and> (~A \<longrightarrow> P(t)))"}