author paulson Wed, 30 Oct 1996 11:17:54 +0100 changeset 2137 afc15c2fd5b5 parent 2136 217ae06dc291 child 2138 056dead45ae8
 doc-src/ind-defs.tex file | annotate | diff | comparison | revisions
--- a/doc-src/ind-defs.tex	Wed Oct 30 11:15:09 1996 +0100
+++ b/doc-src/ind-defs.tex	Wed Oct 30 11:17:54 1996 +0100
@@ -1,5 +1,5 @@
\documentstyle[a4,alltt,iman,extra,proof209,12pt]{article}
-\newif\ifshort
+\newif\ifshort%''Short'' means a published version, not the documentation
\shortfalse%%%%%\shorttrue

\title{A Fixedpoint Approach to\\
@@ -170,7 +170,8 @@
thus accepting all provably monotone inductive definitions, including
iterated definitions.

-The package has been implemented in Isabelle~\cite{isabelle-intro} using
+The package has been implemented in
+Isabelle~\cite{paulson-markt,paulson-isa-book} using
\textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has
since been ported to Isabelle/\textsc{hol} (higher-order logic).  The
recursion equations are specified as introduction rules for the mutually
@@ -1299,9 +1300,10 @@
definitions (of arithmetic expressions, boolean expressions and commands) and
three inductive definitions (the corresponding operational rules).  Using
different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95}
-have both proved the Church-Rosser theorem.  A datatype specifies the set of
-$\lambda$-terms, while inductive definitions specify several reduction
-relations.
+have both proved the Church-Rosser theorem; inductive definitions specify
+several reduction relations on $\lambda$-terms.  Recently, I have applied
+inductive definitions to the analysis of cryptographic
+protocols~\cite{paulson-markt}.

To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the
consistency of the dynamic and static semantics for a small functional