--- a/CookBook/Package/Ind_Examples.thy	Fri Feb 13 01:05:09 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy	Fri Feb 13 01:05:31 2009 +0000
@@ -5,16 +5,15 @@
 section{* Examples of Inductive Definitions \label{sec:ind-examples} *}
 
 text {*
+  Let us first give three examples showing how to define inductive predicates
+  by hand and prove characteristic properties such as introduction rules and
+  an induction rule. From these examples, we will then figure out a general
+  method for defining inductive predicates.  The aim in this section is not to
+  write proofs that are as beautiful as possible, but as close as possible to
+  the ML-code producing the proofs that we will develop later.
 
-  In this section, we will give three examples showing how to define inductive
-  predicates by hand and prove characteristic properties such as introduction
-  rules and an induction rule. From these examples, we will then figure out a
-  general method for defining inductive predicates.  It should be noted that
-  our aim in this section is not to write proofs that are as beautiful as
-  possible, but as close as possible to the ML code producing the proofs that
-  we will develop later.  As a first example, we consider the transitive
-  closure of a relation @{text R}. It is an inductive predicate characterized
-  by the two introduction rules
+  As a first example, we consider the transitive closure of a relation @{text
+  R}. It is an inductive predicate characterized by the two introduction rules
 
   \begin{center}
   @{term[mode=Axiom] "trcl R x x"} \hspace{5mm}
@@ -37,79 +36,72 @@
       \<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y"
 
 text {*
-  where we quantify over the predicate @{text P}.
+  where we quantify over the predicate @{text P}. Note that we have to use the
+  object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for stating
+  this definition. 
 
-  Since the predicate @{term "trcl R x y"} yields an element of the type of object
-  level truth values @{text bool}, the meta-level implications @{text "\<Longrightarrow>"} in the
-  above introduction rules have to be converted to object-level implications
-  @{text "\<longrightarrow>"}. Moreover, we use object-level universal quantifiers @{text "\<forall>"}
-  rather than meta-level universal quantifiers @{text "\<And>"} for quantifying over
-  the variable parameters of the introduction rules. Isabelle already offers some
-  infrastructure for converting between meta-level and object-level connectives,
-  which we will use later on.
-
-  With this definition of the transitive closure, the proof of the (weak) induction
+  With this definition of the transitive closure, the proof of the induction
   theorem is almost immediate. It suffices to convert all the meta-level connectives
   in the induction rule to object-level connectives using the @{text atomize} proof
   method, expand the definition of @{text trcl}, eliminate the universal quantifier
   contained in it, and then solve the goal by assumption.
+
+  (FIXME: add linenumbers to the proof below and the text above)
 *}
 
 lemma trcl_induct:
-  assumes trcl: "trcl R x y"
+  assumes asm: "trcl R x y"
   shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
-  apply (atomize (full))
-  apply (cut_tac trcl)
-  apply (unfold trcl_def)
-  apply (drule spec [where x=P])
-  apply assumption
-  done
-(*<*)
-lemma "trcl R x x"
-  apply (unfold trcl_def)
-  apply (rule allI impI)+
-(*>*)
+apply(atomize (full))
+apply(cut_tac asm)
+apply(unfold trcl_def)
+apply(drule spec[where x=P])
+apply(assumption)
+done
 
-txt {*
-
-  The above induction rule is \emph{weak} in the sense that the induction step may
-  only be proved using the assumptions @{term "R x y"} and @{term "P y z"}, but not
-  using the additional assumption \mbox{@{term "trcl R y z"}}. A stronger induction rule
-  containing this additional assumption can be derived from the weaker one with the
-  help of the introduction rules for @{text trcl}.
-
+text {*
   We now turn to the proofs of the introduction rules, which are slightly more complicated.
   In order to prove the first introduction rule, we again unfold the definition and
   then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible.
   We then end up in a proof state of the following form:
-  
-  @{subgoals [display]}
+
+*}
 
-  The two assumptions correspond to the introduction rules, where @{term "trcl R"} has been
-  replaced by @{term "P"}. Thus, all we have to do is to eliminate the universal quantifier
-  in front of the first assumption, and then solve the goal by assumption:
-  *}
+(*<*)lemma "trcl R x x"
+  apply (unfold trcl_def)
+  apply (rule allI impI)+(*>*)
+txt {* @{subgoals [display]} *}
 (*<*)oops(*>*)
 
+text {*
+  The two assumptions correspond to the introduction rules, where @{text "trcl
+  R"} has been replaced by P. Thus, all we have to do is to eliminate the
+  universal quantifier in front of the first assumption, and then solve the
+  goal by assumption:
+*}
+
+
 lemma trcl_base: "trcl R x x"
-  apply (unfold trcl_def)
-  apply (rule allI impI)+
-  apply (drule spec)
-  apply assumption
-  done
+apply(unfold trcl_def)
+apply(rule allI impI)+
+apply(drule spec)
+apply(assumption)
+done
 
-(*<*)
-lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
-  apply (unfold trcl_def)
-  apply (rule allI impI)+
-(*>*)
-
-txt {*
-
+text {*
   Since the second introduction rule has premises, its proof is not as easy as the previous
   one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"}
   and @{text "\<longrightarrow>"}, we get the proof state
-  @{subgoals [display]}
+*}
+
+
+(*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+  apply (unfold trcl_def)
+  apply (rule allI impI)+(*>*)
+txt {*@{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {*
   The third and fourth assumption corresponds to the first and second introduction rule,
   respectively, whereas the first and second assumption corresponds to the premises of
   the introduction rule. Since we want to prove the second introduction rule, we apply
@@ -122,7 +114,7 @@
   with higher order unification, it is advisable to provide an instantiation for the
   universally quantified predicate variable in the assumption.
 *}
-(*<*)oops(*>*)
+
 
 lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
   apply (unfold trcl_def)

--- a/CookBook/Package/Ind_Interface.thy	Fri Feb 13 01:05:09 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Fri Feb 13 01:05:31 2009 +0000
@@ -2,7 +2,7 @@
 imports "../Base" Simple_Inductive_Package
 begin
 
-section{* The Interface \label{sec:ind-interface} *}
+section {* The Interface \label{sec:ind-interface} *}
 
 text {*
 
@@ -25,7 +25,7 @@
   invoking the package are reflected in its ML programming interface, which
   consists of two functions:
 
-  @{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE}
+  @{ML_chunk [display,gray] SIMPLE_INDUCTIVE_PACKAGE}
 *}
 
 text {*

--- a/CookBook/Package/Ind_Intro.thy	Fri Feb 13 01:05:09 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy	Fri Feb 13 01:05:31 2009 +0000
@@ -15,89 +15,31 @@
   \end{flushright}
 
   \medskip
-  HOL is based on just a few primitive constants, like equality, implication,
-  and the description operator, whose properties are described as axioms. All
-  other concepts, such as inductive predicates, datatypes, or recursive
-  functions are defined in terms of those constants, and the desired
-  properties, for example induction theorems, or recursion equations are
-  derived from the definitions by a formal proof. Since it would be very
-  tedious for a user to define complex inductive predicates or datatypes ``by
-  hand'' just using the primitive operators of higher order logic,
-  Isabelle/HOL already contains a number of packages automating such
-  work. Thanks to those packages, the user can give a high-level
-  specification, like a list of introduction rules or constructors, and the
-  package then does all the low-level definitions and proofs behind the
-  scenes. In this chapter we explain how such a package can be implemented.
-
-
-  %The packages are written in Standard ML, the implementation
-  %language of Isabelle, and can be invoked by the user from within theory documents
-  %written in the Isabelle/Isar language via specific commands. Most of the time,
-  %when using Isabelle for applications, users do not have to worry about the inner
-  %workings of packages, since they can just use the packages that are already part
-  %of the Isabelle distribution. However, when developing a general theory that is
-  %intended to be applied by other users, one may need to write a new package from
-  %scratch. Recent examples of such packages include the verification environment
-  %for sequential imperative programs by Schirmer \cite{Schirmer-LPAR04}, the
-  %package for defining general recursive functions by Krauss \cite{Krauss-IJCAR06},
-  %as well as the nominal datatype package by Berghofer and Urban \cite{Urban-Berghofer06}.
+  HOL is based on just a few primitive constants, like equality and
+  implication, whose properties are described by a few axioms. All other
+  concepts, such as inductive predicates, datatypes, or recursive functions
+  are defined in terms of those constants, and the desired properties, for
+  example induction theorems, or recursion equations are derived from the
+  definitions by a formal proof. Since it would be very tedious for a user to
+  define complex inductive predicates or datatypes ``by hand'' just using the
+  primitive operators of higher order logic, packages have been implemented
+  automating such work. Thanks to those packages, the user can give a
+  high-level specification, like a list of introduction rules or constructors,
+  and the package then does all the low-level definitions and proofs behind
+  the scenes. In this chapter we explain how such a package can be
+  implemented.
 
-  %The scientific value of implementing a package should not be underestimated:
-  %it is often more than just the automation of long-established scientific
-  %results. Of course, a carefully-developed theory on paper is indispensable
-  %as a basis. However, without an implementation, such a theory will only be of
-  %very limited practical use, since only an implementation enables other users
-  %to apply the theory on a larger scale without too much effort. Moreover,
-  %implementing a package is a bit like formalizing a paper proof in a theorem
-  %prover. In the literature, there are many examples of paper proofs that
-  %turned out to be incomplete or even faulty, and doing a formalization is
-  %a good way of uncovering such errors and ensuring that a proof is really
-  %correct. The same applies to the theory underlying definitional packages.
-  %For example, the general form of some complicated induction rules for nominal
-  %datatypes turned out to be quite hard to get right on the first try, so
-  %an implementation is an excellent way to find out whether the rules really
-  %work in practice.
-
-  Writing a package is a particularly difficult task for users that are new
-  to Isabelle, since its programming interface consists of thousands of functions.
-  Rather than just listing all those functions, we give a step-by-step tutorial
-  for writing a package, using an example that is still simple enough to be
-  easily understandable, but at the same time sufficiently complex to demonstrate
-  enough of Isabelle's interesting features. As a running example, we have
-  chosen a rather simple package for defining inductive predicates. To keep
-  things simple, we will not use the general Knaster-Tarski fixpoint
-  theorem on complete lattices, which forms the basis of Isabelle's standard
-  inductive definition package originally due to Paulson \cite{Paulson-ind-defs}.
-  Instead, we will use a simpler \emph{impredicative} (i.e.\ involving
-  quantification on predicate variables) encoding of inductive predicates
-  suggested by Melham \cite{Melham:1992:PIR}. Due to its simplicity, this
-  package will necessarily have a reduced functionality. It does neither
-  support introduction rules involving arbitrary monotone operators, nor does
-  it prove case analysis (or inversion) rules. Moreover, it only proves a weaker
-  form of the rule induction theorem.
-
-  %Reading this article does not require any prior knowledge of Isabelle's programming
-  %interface. However, we assume the reader to already be familiar with writing
-  %proofs in Isabelle/HOL using the Isar language. For further information on
-  %this topic, consult the book by Nipkow, Paulson, and Wenzel
-  %\cite{isa-tutorial}. Moreover, in order to understand the pieces of
-  %code given in this tutorial, some familiarity with the basic concepts of the Standard
-  %ML programming language, as described for example in the textbook by Paulson
-  %\cite{paulson-ml2}, is required as well.
-
-  %The rest of this chapter is structured as follows. In \S\ref{sec:ind-examples},
-  %we will illustrate the ``manual'' definition of inductive predicates using
-  %some examples. Starting from these examples, we will describe in
-  %\S\ref{sec:ind-general-method} how the construction works in general.
-  %The following sections are then dedicated to the implementation of a
-  %package that carries out the construction of such inductive predicates.
-  %First of all, a parser for a high-level notation for specifying inductive
-  %predicates via a list of introduction rules is developed in \S\ref{sec:ind-interface}.
-  %Having parsed the specification, a suitable primitive definition must be
-  %added to the theory, which will be explained in \S\ref{sec:ind-definition}.
-  %Finally, \S\ref{sec:ind-proofs} will focus on methods for proving introduction
-  %and induction rules from the definitions introduced in \S\ref{sec:ind-definition}.
-
+  As a running example, we have chosen a rather simple package for defining
+  inductive predicates. To keep things simple, we will not use the general
+  Knaster-Tarski fixpoint theorem on complete lattices, which forms the basis
+  of Isabelle's standard inductive definition package.  Instead, we will use a
+  simpler \emph{impredicative} (i.e.\ involving quantification on predicate
+  variables) encoding of inductive predicates suggested by Melham
+  \cite{Melham:1992:PIR}. Due to its simplicity, this package will necessarily
+  have a reduced functionality. It does neither support introduction rules
+  involving arbitrary monotone operators, nor does it prove case analysis (or
+  inversion) rules. Moreover, it only proves a weaker form of the rule
+  induction theorem.
 *}
 
 end

Binary file cookbook.pdf has changed