summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 12 Mar 2001 18:17:45 +0100 | |

changeset 11201 | eddc69b55fac |

parent 11200 | f43fa07536c0 |

child 11202 | f8da11ca4c6e |

*** empty log message ***

--- 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.