author nipkow Mon, 12 Mar 2001 18:17:45 +0100 changeset 11201 eddc69b55fac parent 11200 f43fa07536c0 child 11202 f8da11ca4c6e
*** empty log message ***
 doc-src/TutorialI/Inductive/even-example.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/fp.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/todo.tobias file | annotate | diff | comparison | revisions
--- 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 @@