--- a/doc-src/TutorialI/Inductive/even-example.tex Fri Mar 09 19:05:48 2001 +0100
+++ b/doc-src/TutorialI/Inductive/even-example.tex Mon Mar 12 18:17:45 2001 +0100
@@ -25,7 +25,9 @@
An inductive definition consists of introduction rules. The first one
above states that 0 is even; the second states that if $n$ is even, then so
is~$n+2$. Given this declaration, Isabelle generates a fixed point
-definition for \isa{even} and proves theorems about it. These theorems
+definition for \isa{even} and proves theorems about it,
+thus following the definitional approach (see \S\ref{sec:definitional}).
+These theorems
include the introduction rules specified in the declaration, an elimination
rule for case analysis and an induction rule. We can refer to these
theorems by automatically-generated names. Here are two examples:
--- a/doc-src/TutorialI/fp.tex Fri Mar 09 19:05:48 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Mon Mar 12 18:17:45 2001 +0100
@@ -269,6 +269,26 @@
\input{Misc/document/prime_def.tex}
+\section{The Definitional Approach}
+\label{sec:definitional}
+
+As we pointed out at the beginning of the chapter, asserting arbitrary
+axioms, e.g. $f(n) = f(n) + 1$, may easily lead to contradictions. In order
+to avoid this danger, this tutorial advocates the definitional rather than
+the axiomatic approach: introduce new concepts by definitions, thus
+preserving consistency. However, on the face of it, Isabelle/HOL seems to
+support many more constructs than just definitions, for example
+\isacommand{primrec}. The crucial point is that internally, everything
+(except real axioms) is reduced to a definition. For example, given some
+\isacommand{primrec} function definition, this is turned into a proper
+(nonrecursive!) definition, and the user-supplied recursion equations are
+derived as theorems from the definition. This tricky process is completely
+hidden from the user and it is not necessary to understand the details. The
+result of the definitional approach is that \isacommand{primrec} is as safe
+as pure \isacommand{defs} are, but more convenient. And this is not just the
+case for \isacommand{primrec} but also for the other commands described
+later, like \isacommand{recdef} and \isacommand{inductive}.
+
\chapter{More Functional Programming}
The purpose of this chapter is to deepen the reader's understanding of the
--- a/doc-src/TutorialI/todo.tobias Fri Mar 09 19:05:48 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Mon Mar 12 18:17:45 2001 +0100
@@ -57,8 +57,6 @@
Advanced recdef: explain recdef_tc?
-say something about definitional approach. In recdef section? At the end?
-
I guess we should say "HOL" everywhere, with a remark early on about the
differences between our HOL and the other one.