--- a/CookBook/FirstSteps.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/FirstSteps.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -171,19 +171,11 @@
 section {* Combinators\label{sec:combinators} *}
 
 text {*
-  (FIXME: maybe move before antiquotation section)
-
   For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
   the combinators. At first they seem to greatly obstruct the
   comprehension of the code, but after getting familiar with them, they
   actually ease the understanding and also the programming.
 
-  \begin{readmore}
-  The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
-  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
-  contains further information about combinators.
-  \end{readmore}
-
   The simplest combinator is @{ML I}, which is just the identity function defined as
 *}
 
@@ -341,6 +333,12 @@
 text {*
   
   (FIXME: find a good exercise for combinators)
+
+  \begin{readmore}
+  The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
+  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
+  contains further information about combinators.
+  \end{readmore}
  
 *}
 
@@ -874,12 +872,27 @@
   @{ML_file "Pure/thm.ML"}. 
   \end{readmore}
 
-  (FIXME: how to add case-names to goal states)
+  (FIXME: how to add case-names to goal states - maybe in the next section)
 *}
 
 
 section {* Theorem Attributes *}
 
+text {*
+  
+
+  If you want to print out all currently known attributes a theorem 
+  can have, you can use the function:
+
+  @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" 
+"COMP:  direct composition with rules (no lifting)
+HOL.dest:  declaration of Classical destruction rule
+HOL.elim:  declaration of Classical elimination rule 
+\<dots>"}
+
+*}
+
+
 section {* Theories and Local Theories *}
 
 text {*

--- a/CookBook/Package/Ind_Examples.thy	Thu Feb 19 14:44:53 2009 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,317 +0,0 @@
-theory Ind_Examples
-imports Main LaTeXsugar
-begin
-
-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 then also how to prove by hand characteristic properties
-  about them, such as introduction rules and induction principles. From
-  these examples, we will figure out a general method for defining inductive
-  predicates.  The aim in this section is \emph{not} to write proofs that are as
-  beautiful as possible, but as close as possible to the ML-code we will 
-  develop later.
-
-
-  As a first example, let us consider the transitive closure of a relation @{text
-  R}. It is an inductive predicate characterised by the two introduction rules:
-
-  \begin{center}
-  @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm}
-  @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
-  \end{center}
-
-  Note that the @{text trcl} predicate has two different kinds of parameters: the
-  first parameter @{text R} stays \emph{fixed} throughout the definition, whereas
-  the second and third parameter changes in the ``recursive call''. This will
-  become important later on when we deal with fixed parameters and locales. 
-
-  Since an inductively defined predicate is the least predicate closed under
-  a collection of introduction rules, we define the predicate @{text "trcl R x y"} in
-  such a way that it holds if and only if @{text "P x y"} holds for every predicate
-  @{text P} closed under the rules above. This gives rise to the definition 
-*}
-
-definition "trcl R x y \<equiv> 
-      \<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}. Note that we have to use the
-  object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for
-  stating this definition (there is no other way for definitions in
-  HOL). However, the introduction rules and induction principles derived later
-  should use the corresponding meta-connectives since they simplify the
-  reasoning for the user.
-
-  With this definition, the proof of the induction principle for the transitive
-  closure is almost immediate. It suffices to convert all the meta-level
-  connectives in the lemma to object-level connectives using the
-  proof method @{text atomize} (Line 4), expand the definition of @{text trcl}
-  (Line 5 and 6), eliminate the universal quantifier contained in it (Line 7),
-  and then solve the goal by assumption (Line 8).
-
-*}
-
-lemma %linenos trcl_induct:
-  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 asm)
-apply(unfold trcl_def)
-apply(drule spec[where x=P])
-apply(assumption)
-done
-
-text {*
-  The proofs for the introduction are slightly more complicated. We need to prove
-  the facs @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}.
-  In order to prove the first fact, 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 the goal state:
-*}
-
-(*<*)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. Thus the proof is:
-*}
-
-lemma trcl_base: "trcl R x x"
-apply(unfold trcl_def)
-apply(rule allI impI)+
-apply(drule spec)
-apply(assumption)
-done
-
-text {*
-  Since the second @{text trcl}-rule has premises, the proof of its
-  introduction rule is not as easy. After unfolding the definitions and
-  applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}, we get the
-  goal state:
-*}
-
-(*<*)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 correspond to the first and second
-  introduction rule, respectively, whereas the first and second assumption
-  corresponds to the pre\-mises of the introduction rule. Since we want to prove
-  the second introduction rule, we apply the fourth assumption to the goal
-  @{term "P x z"}. In order for the assumption to be applicable as a rule, we have to
-  eliminate the universal quantifier and turn the object-level implications
-  into meta-level ones. This can be accomplished using the @{text rule_format}
-  attribute. Applying the assumption produces the two new subgoals
-*}
-
-(*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
-apply (unfold trcl_def)
-apply (rule allI impI)+
-proof -
-  case (goal1 P)
-  have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
-  show ?case
-    apply (rule a4[rule_format])(*>*)
-txt {*@{subgoals [display]} *}
-(*<*)oops(*>*)
-
-text {* 
-  which can be
-  solved using the first and second assumption. The second assumption again
-  involves a quantifier and an implications that have to be eliminated before it
-  can be applied. To avoid potential problems with higher-order unification, 
-  we should explcitly instantiate the universally quantified
-  predicate variable to @{text "P"} and also match explicitly the implications
-  with the the third and fourth assumption. This gives the proof:
-*}
-
-
-lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
-apply(unfold trcl_def)
-apply(rule allI impI)+
-proof -
-  case (goal1 P)
-  have a1: "R x y" by fact
-  have a2: "\<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 y z" by fact
-  have a3: "\<forall>x. P x x" by fact
-  have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
-  show "P x z"
-    apply(rule a4[rule_format])
-    apply(rule a1)
-    apply(rule a2[THEN spec[where x=P], THEN mp, THEN mp, OF a3, OF a4])
-    done
-qed
-
-text {*
-  It might be surprising that we are not using the automatic tactics available in
-  Isabelle for proving this lemmas. After all @{text "blast"} would easily 
-  dispense of it.
-*}
-
-lemma trcl_step_blast: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
-apply(unfold trcl_def)
-apply(blast)
-done
-
-text {*
-  Experience has shown that it is generally a bad idea to rely heavily on
-  @{text blast}, @{text auto} and the like in automated proofs. The reason is
-  that you do not have precise control over them (the user can, for example,
-  declare new intro- or simplification rules that can throw automatic tactics
-  off course) and also it is very hard to debug proofs involving automatic
-  tactics whenever something goes wrong. Therefore if possible, automatic 
-  tactics should be avoided or sufficiently constrained.
-
-  The method of defining inductive predicates by impredicative quantification
-  also generalises to mutually inductive predicates. The next example defines
-  the predicates @{text even} and @{text odd} characterised by the following
-  rules:
- 
-  \begin{center}
-  @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
-  @{prop[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}
-  @{prop[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}
-  \end{center}
-  
-  Since the predicates are mutually inductive, each definition 
-  quantifies over both predicates, below named @{text P} and @{text Q}.
-*}
-
-definition "even n \<equiv> 
-  \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
-             \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
-
-definition "odd n \<equiv>
-  \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
-             \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"
-
-text {*
-  For proving the induction principles, we use exactly the same technique 
-  as in the transitive closure example, namely:
-*}
-
-lemma even_induct:
-  assumes asm: "even n"
-  shows "P 0 \<Longrightarrow> 
-             (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
-apply(atomize (full))
-apply(cut_tac asm)
-apply(unfold even_def)
-apply(drule spec[where x=P])
-apply(drule spec[where x=Q])
-apply(assumption)
-done
-
-text {*
-  We omit the other induction principle that has @{term "Q n"} as conclusion.
-  The proofs of the introduction rules are also very similar to the ones in the
-  @{text "trcl"}-example. We only show the proof of the second introduction rule.
-*}
-
-lemma evenS: "odd m \<Longrightarrow> even (Suc m)"
-apply (unfold odd_def even_def)
-apply (rule allI impI)+
-proof -
-  case (goal1 P)
-  have a1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
-                             \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact
-  have a2: "P 0" by fact
-  have a3: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact
-  have a4: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact
-  show "P (Suc m)"
-    apply(rule a3[rule_format])
-    apply(rule a1[THEN spec[where x=P], THEN spec[where x=Q],
-	THEN mp, THEN mp, THEN mp, OF a2, OF a3, OF a4])
-    done
-qed
-
-text {*
-  As a final example, we define the accessible part of a relation @{text R} characterised 
-  by the introduction rule
-  
-  \begin{center}
-  @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}
-  \end{center}
-
-  whose premise involves a universal quantifier and an implication. The
-  definition of @{text accpart} is:
-*}
-
-definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
-
-text {*
-  The proof of the induction principle is again straightforward.
-*}
-
-lemma accpart_induct:
-  assumes asm: "accpart R x"
-  shows "(\<And>x. (\<forall>y. R y x \<longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
-apply(atomize (full))
-apply(cut_tac asm)
-apply(unfold accpart_def)
-apply(drule spec[where x=P])
-apply(assumption)
-done
-
-text {*
-  Proving the introduction rule is a little more complicated, because the quantifier
-  and the implication in the premise. We first convert the meta-level universal quantifier
-  and implication to their object-level counterparts. Unfolding the definition of
-  @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
-  yields the following goal state:
-*}
-
-(*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
-apply (unfold accpart_def)
-apply (rule allI impI)+(*>*)
-txt {* @{subgoals [display]} *}
-(*<*)oops(*>*)
-
-text {*
-  Applying the second assumption produces a goal state with the new local assumption
-  @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the
-  first assumption.
-*}
-
-lemma %small accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
-apply (unfold accpart_def)
-apply (rule allI impI)+
-proof -
-  case (goal1 P)
-  have a1: "\<forall>y. R y x \<longrightarrow> 
-                   (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact
-  have a2: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact
-  show "P x"
-    apply(rule a2[rule_format])
-    proof -
-      case (goal1 y)
-      have a3: "R y x" by fact
-      show "P y"
-      apply(rule a1[THEN spec[where x=y], THEN mp, OF a3, 
-            THEN spec[where x=P], THEN mp, OF a2])
-      done
-  qed
-qed
-
-text {*
-  (FIXME check that the code works like as indicated)
-
-  The point of these examples is to get a feeling what the automatic proofs 
-  should do in order to solve all inductive definitions we throw at them. For this 
-  it is instructive to look at the general construction principle 
-  of inductive definitions, which we shall do in the next section.
-*}
-
-end

--- a/CookBook/Package/Ind_General_Scheme.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/Package/Ind_General_Scheme.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -5,6 +5,11 @@
 section{* The General Construction Principle \label{sec:ind-general-method} *}
 
 text {*
+  
+  The point of these examples is to get a feeling what the automatic proofs 
+  should do in order to solve all inductive definitions we throw at them. For this 
+  it is instructive to look at the general construction principle 
+  of inductive definitions, which we shall do in the next section.
 
   Before we start with the implementation, it is useful to describe the general
   form of inductive definitions that our package should accept.

--- a/CookBook/Package/Ind_Interface.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -2,54 +2,34 @@
 imports "../Base" "../Parsing" Simple_Inductive_Package
 begin
 
-section {* The Interface \label{sec:ind-interface} *}
-
-text {* 
-  The purpose of the package we show next is that the user just specifies the
-  inductive predicate by stating some introduction rules and then the packages
-  makes the equivalent definition and derives from it the needed properties.
-*}
-
-text {*
-  From a high-level perspective the package consists of 6 subtasks:
-
-  \begin{itemize}
-  \item reading the various parts of specification (i.e.~parser),
-  \item transforming the parser outut into an internal 
-  (typed) datastructure,
-  \item making the definitions, 
-  \item deriving the induction principles,
-  \item deriving the introduction rules, and
-  \item storing the results in the given theory. 
-  to the user. 
-  \end{itemize}
-
-*}
+section {* Parsing the Specification *}
 
 text {* 
   To be able to write down the specification in Isabelle, we have to introduce
   a new command (see Section~\ref{sec:newcommand}).  As the keyword for the new
-  command we chose \simpleinductive{}. The specifications corresponding to our
-  examples described earlier are:
+  command we chose \simpleinductive{}. We want that the package can cope with
+  specifications inside locales. For example it should be possible to declare
+
+*}
+
+locale rel =
+  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+
+text {*
+  and then define the transitive closure and the accessible part as follows:
 *}
 
-simple_inductive
-  trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  base: "trcl R x x"
-| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
 
-simple_inductive
-  even and odd
+simple_inductive (in rel) trcl' 
 where
-  even0: "even 0"
-| evenS: "odd n \<Longrightarrow> even (Suc n)"
-| oddS: "even n \<Longrightarrow> odd (Suc n)"
+  base: "trcl' x x"
+| step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"
 
-simple_inductive
-  accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+simple_inductive (in rel) accpart'
 where
-  accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
+
+
 
 text {*
   After the keyword we expect a constant (or constants) with possible typing 
@@ -70,27 +50,16 @@
   \begin{isabelle}
 *}
 simple_inductive
-  trcl' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
-  base: "trcl' R x x"
-| step: "trcl' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl' R x z"
+  base: "trcl'' R x x"
+| step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z"
 
 simple_inductive
-  accpart' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
-  accpartI: "(\<forall>y. R y x \<longrightarrow> accpart' R y) \<Longrightarrow> accpart' R x"
-
-locale rel =
-  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
 
-simple_inductive (in rel) trcl'' 
-where
-  base: "trcl'' x x"
-| step: "trcl'' x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' x z"
-
-simple_inductive (in rel) accpart''
-where
-  accpartI: "(\<forall>y. R y x \<longrightarrow> accpart'' y) \<Longrightarrow> accpart'' x"
 text_raw {*
   \end{isabelle}
   \caption{The first definition is for the transitive closure where the
@@ -435,6 +404,27 @@
   behaviour of the user interface, such as failure of the undo mechanism.
 *}
 
+text {*
+  Note that the @{text trcl} predicate has two different kinds of parameters: the
+  first parameter @{text R} stays \emph{fixed} throughout the definition, whereas
+  the second and third parameter changes in the ``recursive call''. This will
+  become important later on when we deal with fixed parameters and locales. 
+
+
+ 
+  The purpose of the package we show next is that the user just specifies the
+  inductive predicate by stating some introduction rules and then the packages
+  makes the equivalent definition and derives from it the needed properties.
+*}
+
+text {*
+  From a high-level perspective the package consists of 6 subtasks:
+
+
+
+*}
+
+
 (*<*)
 end
 (*>*)

--- a/CookBook/Package/Ind_Intro.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/Package/Ind_Intro.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -30,16 +30,16 @@
   such a package can be implemented.
 
   As a running example, we have chosen a rather simple package for defining
-  inductive predicates. To keep things really 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
-  induction principle for inductive predicates.
+  inductive predicates. To keep things really 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. 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 induction principle for inductive
+  predicates.
 *}
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Package/Ind_Prelims.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -0,0 +1,351 @@
+theory Ind_Prelims
+imports Main LaTeXsugar"../Base" Simple_Inductive_Package
+begin
+
+section{* Preliminaries *}
+  
+text {*
+  On the Isabelle level, the user will just give a specification of an
+  inductive predicate and expects from the package to produce a convenient
+  reasoning infrastructure. This infrastructure needs to be derived from the 
+  definition that correspond to the specified predicate. This will roughly 
+  mean that the package has three main parts, namely:
+
+
+  \begin{itemize}
+  \item parsing the specification and typing the parsed input,
+  \item making the definitions and deriving the reasoning infrastructure, and
+  \item storing the results in the theory. 
+  \end{itemize}
+
+  Before we start with explaining all parts,
+  let us first give three examples showing how to define inductive predicates
+  by hand and then also how to prove by hand important properties about
+  them. From these examples, we will figure out a general method for defining
+  inductive predicates.  The aim in this section is \emph{not} to write proofs
+  that are as beautiful as possible, but as close as possible to the ML-code
+  we will develop in later sections.
+
+  We first consider the transitive closure of a relation @{text R}. It is
+  an inductive predicate characterised by the two introduction rules:
+
+  \begin{center}\small
+  @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm}
+  @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
+  \end{center}
+
+  In Isabelle the user will state for @{term trcl\<iota>} the specification:
+*}
+
+simple_inductive
+  trcl\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "trcl\<iota> R x x"
+| step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z"
+
+text {*
+  As said above the package has to make an appropriate definition and provide
+  lemmas to reason about the predicate @{term trcl\<iota>}. Since an inductively
+  defined predicate is the least predicate closed under a collection of
+  introduction rules, the predicate @{text "trcl R x y"} can be defined so
+  that it holds if and only if @{text "P x y"} holds for every predicate
+  @{text P} closed under the rules above. This gives rise to the definition
+*}
+
+definition "trcl \<equiv> 
+     \<lambda>R x y. \<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}. We have to use the
+  object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for
+  stating this definition (there is no other way for definitions in
+  HOL). However, the introduction rules and induction principles 
+  should use the meta-connectives since they simplify the
+  reasoning for the user.
+
+  With this definition, the proof of the induction principle for @{term trcl}
+  closure is almost immediate. It suffices to convert all the meta-level
+  connectives in the lemma to object-level connectives using the
+  proof method @{text atomize} (Line 4), expand the definition of @{term trcl}
+  (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7),
+  and then solve the goal by assumption (Line 8).
+
+*}
+
+lemma %linenos trcl_induct:
+  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 asm)
+apply(unfold trcl_def)
+apply(drule spec[where x=P])
+apply(assumption)
+done
+
+text {*
+  The proofs for the introduction rules are slightly more complicated. 
+  For the first one, we need to prove the following lemma:
+*}
+
+lemma %linenos trcl_base: 
+  shows "trcl R x x"
+apply(unfold trcl_def)
+apply(rule allI impI)+
+apply(drule spec)
+apply(assumption)
+done
+
+text {*
+  We again unfold first the definition and apply introduction rules 
+  for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible (Lines 3 and 4).
+  We then end up in the goal state:
+*}
+
+(*<*)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. Thus, all we have
+  to do is to eliminate the universal quantifier in front of the first
+  assumption (Line 5), and then solve the goal by assumption (Line 6).
+*}
+
+text {*
+  Next we have to show that the second introduction rule also follows from the
+  definition.  Since this rule has premises, the proof is a bit more
+  involved. After unfolding the definitions and applying the introduction
+  rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}
+*}
+
+lemma trcl_step: 
+  shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+apply (unfold trcl_def)
+apply (rule allI impI)+
+
+txt {* 
+  we obtain the goal state
+
+  @{subgoals [display]} 
+
+  To see better where we are, let us explicitly name the assumptions 
+  by starting a subproof.
+*}
+
+proof -
+  case (goal1 P)
+  have p1: "R x y" by fact
+  have p2: "\<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 y z" by fact
+  have r1: "\<forall>x. P x x" by fact
+  have r2: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact
+  show "P x z"
+  
+txt {*
+  The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of
+  the second introduction rule; the assumptions @{text "r1"} and @{text "r2"}
+  correspond to the introduction rules. We apply @{text "r2"} to the goal
+  @{term "P x z"}. In order for the assumption to be applicable as a rule, we
+  have to eliminate the universal quantifier and turn the object-level
+  implications into meta-level ones. This can be accomplished using the @{text
+  rule_format} attribute. So we continue the proof with:
+
+*}
+
+    apply (rule r2[rule_format])
+
+txt {*
+  This gives us two new subgoals
+
+  @{subgoals [display]} 
+
+  which can be solved using assumptions @{text p1} and @{text p2}. The latter
+  involves a quantifier and implications that have to be eliminated before it
+  can be applied. To avoid potential problems with higher-order unification,
+  we explicitly instantiate the quantifier to @{text "P"} and also match
+  explicitly the implications with @{text "r1"} and @{text "r2"}. This gives
+  the proof:
+*}
+
+    apply(rule p1)
+    apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])
+    done
+qed
+
+text {*
+  Now we are done. It might be surprising that we are not using the automatic
+  tactics available in Isabelle for proving this lemmas. After all @{text
+  "blast"} would easily dispense of it.
+*}
+
+lemma trcl_step_blast: 
+  shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+apply(unfold trcl_def)
+apply(blast)
+done
+
+text {*
+  Experience has shown that it is generally a bad idea to rely heavily on
+  @{text blast}, @{text auto} and the like in automated proofs. The reason is
+  that you do not have precise control over them (the user can, for example,
+  declare new intro- or simplification rules that can throw automatic tactics
+  off course) and also it is very hard to debug proofs involving automatic
+  tactics whenever something goes wrong. Therefore if possible, automatic 
+  tactics should be avoided or sufficiently constrained.
+
+  The method of defining inductive predicates by impredicative quantification
+  also generalises to mutually inductive predicates. The next example defines
+  the predicates @{text even} and @{text odd} characterised by the following
+  rules:
+ 
+  \begin{center}\small
+  @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
+  @{prop[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm}
+  @{prop[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"}
+  \end{center}
+  
+  The user will state for this inductive definition the specification:
+*}
+
+simple_inductive
+  even\<iota> and odd\<iota>
+where
+  even0: "even\<iota> 0"
+| evenS: "odd\<iota> n \<Longrightarrow> even\<iota> (Suc n)"
+| oddS: "even\<iota> n \<Longrightarrow> odd\<iota> (Suc n)"
+
+text {*
+  Since the predicates @{term even} and @{term odd} are mutually inductive, each 
+  corresponding definition must quantify over both predicates (we name them 
+  below @{text "P"} and @{text "Q"}).
+*}
+
+definition "even \<equiv> 
+  \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
+                 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
+
+definition "odd \<equiv>
+  \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
+                 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"
+
+text {*
+  For proving the induction principles, we use exactly the same technique 
+  as in the transitive closure example, namely:
+*}
+
+lemma even_induct:
+  assumes asm: "even n"
+  shows "P 0 \<Longrightarrow> 
+             (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
+apply(atomize (full))
+apply(cut_tac asm)
+apply(unfold even_def)
+apply(drule spec[where x=P])
+apply(drule spec[where x=Q])
+apply(assumption)
+done
+
+text {*
+  The only difference with the proof @{text "trcl_induct"} is that we have to
+  instantiate here two universal quantifiers.  We omit the other induction
+  principle that has @{term "Q n"} as conclusion.  The proofs of the
+  introduction rules are also very similar to the ones in the @{text
+  "trcl"}-example. We only show the proof of the second introduction rule.
+
+*}
+
+lemma %linenos evenS: 
+  shows "odd m \<Longrightarrow> even (Suc m)"
+apply (unfold odd_def even_def)
+apply (rule allI impI)+
+proof -
+  case (goal1 P)
+  have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
+                             \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact
+  have r1: "P 0" by fact
+  have r2: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact
+  have r3: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact
+  show "P (Suc m)"
+    apply(rule r2[rule_format])
+    apply(rule p1[THEN spec[where x=P], THEN spec[where x=Q],
+	           THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3])
+    done
+qed
+
+text {*
+  In Line 13, we apply the assumption @{text "r2"} (since we prove the second
+  introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (if
+  the second introduction rule had more premises we have to do that for all
+  of them). In order for this assumption to be applicable, the quantifiers
+  need to be instantiated and then also the implications need to be resolved
+  with the other rules.
+
+
+  As a final example, we define the accessible part of a relation @{text R} characterised 
+  by the introduction rule
+  
+  \begin{center}\small
+  \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
+  \end{center}
+
+  whose premise involves a universal quantifier and an implication. The
+  definition of @{text accpart} is:
+*}
+
+definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
+
+text {*
+  The proof of the induction principle is again straightforward.
+*}
+
+lemma accpart_induct:
+  assumes asm: "accpart R x"
+  shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
+apply(atomize (full))
+apply(cut_tac asm)
+apply(unfold accpart_def)
+apply(drule spec[where x=P])
+apply(assumption)
+done
+
+text {*
+  Proving the introduction rule is a little more complicated, because the quantifier
+  and the implication in the premise. The proof is as follows.
+*}
+
+lemma %linenos accpartI: 
+  shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+apply (unfold accpart_def)
+apply (rule allI impI)+
+proof -
+  case (goal1 P)
+  have p1: "\<And>y. R y x \<Longrightarrow> 
+                   (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact
+  have r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact
+  show "P x"
+    apply(rule r1[rule_format])
+    proof -
+      case (goal1 y)
+      have r1_prem: "R y x" by fact
+      show "P y"
+	apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])
+      done
+  qed
+qed
+
+text {*
+  In Line 11, applying the assumption @{text "r1"} generates a goal state with
+  the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the 
+  proof above (Line 14). This local assumption will be used to solve
+  the goal @{term "P y"} using the assumption @{text "p1"}.
+
+  The point of these examples is to get a feeling what the automatic proofs 
+  should do in order to solve all inductive definitions we throw at them.
+  This is usually the first step in writing a package.
+
+*}
+
+end

--- a/CookBook/Parsing.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/Parsing.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -561,24 +561,35 @@
 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
 
   The function @{ML OuterParse.prop} is similar, except that it gives a different
-  error message, when parsing fails. Looking closer at the result string you will
-  have noticed that the parser not just returns the parsed string, but also some 
-  encoded information. You can see this better if you replace 
-  @{ML Position.none} by @{ML "(Position.line 42)"}, say.
+  error message, when parsing fails. As you can see, the parser not just returns 
+  the parsed string, but also some encoded information. You can decode the
+  information with the function @{ML YXML.parse}. For example
+
+  @{ML_response [display,gray]
+  "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
+  "XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
+
+  You can see better what is going on if you replace 
+  @{ML Position.none} by @{ML "Position.line 42"}, say:
 
 @{ML_response [display,gray]
 "let 
   val input = OuterSyntax.scan (Position.line 42) \"foo\"
 in 
-  OuterParse.term input
+  YXML.parse (fst (OuterParse.term input))
 end"
-"(\"\\^E\\^Ftoken\\^Fline=42\\^Fend_line=42\\^Efoo\\^E\\^F\\^E\", [])"}
+"XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
   
   The positional information is stored so that code called later on will be
   able to give more precise error messages. 
 
+  \begin{readmore}
+  The functions to do with input and outout of XML and YXML are defined 
+  in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
+  \end{readmore}
 *}
 
+
 section {* Parsing Specifications\label{sec:parsingspecs} *}
 
 text {*
@@ -707,15 +718,7 @@
  
   The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
   @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some 
-  attributes. If you want to print out all currently known attributes a theorem 
-  can have, you can use the function:
-
-  @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" 
-"COMP:  direct composition with rules (no lifting)
-HOL.dest:  declaration of Classical destruction rule
-HOL.elim:  declaration of Classical elimination rule 
-\<dots>"}
-
+  attributes. 
 
   For the inductive definitions described above only the attibutes @{text "[intro]"} and
   @{text "[simp]"} make sense.

--- a/CookBook/ROOT.ML	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/ROOT.ML	Fri Feb 20 23:19:41 2009 +0000
@@ -9,9 +9,9 @@
 use_thy "Tactical";
 
 use_thy "Package/Ind_Intro";
-use_thy "Package/Ind_Examples";
+use_thy "Package/Ind_Prelims";
+use_thy "Package/Ind_Interface";
 use_thy "Package/Ind_General_Scheme";
-use_thy "Package/Ind_Interface";
 use_thy "Package/Ind_Code";
 
 use_thy "Appendix";
@@ -23,6 +23,7 @@
 use_thy "Recipes/StoringData";
 use_thy "Recipes/ExternalSolver";
 use_thy "Recipes/Oracle";
+use_thy "Recipes/Sat";
 
 use_thy "Solutions";
 use_thy "Readme";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/Sat.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -0,0 +1,15 @@
+
+theory Sat
+imports Main
+begin
+
+
+section {* SAT Solver *}
+
+
+
+end
+  
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/USTypes.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -0,0 +1,15 @@
+
+theory USTypes
+imports Main
+begin
+
+
+section {* User Space Type-Systems *}
+
+
+
+end
+  
+
+
+

Binary file cookbook.pdf has changed