# HG changeset patch
# User nipkow
# Date 984417465 -3600
# Node ID eddc69b55facb433a56dbcff99dce3ccefb02f53
# Parent  f43fa07536c0e943551a5a0d9fba6ab6b5d0cccd
*** empty log message ***

diff -r f43fa07536c0 -r eddc69b55fac doc-src/TutorialI/Inductive/even-example.tex
--- 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:
diff -r f43fa07536c0 -r eddc69b55fac doc-src/TutorialI/fp.tex
--- 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
diff -r f43fa07536c0 -r eddc69b55fac doc-src/TutorialI/todo.tobias
--- 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.