# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1222890020 14400
# Node ID 2f1736cb8f2653162a7ca302bcc5b92c11da309e
# Parent  733614e236a34a6af342034f211aea5753fc76f4
various changes by Alex and Christian

diff -r 733614e236a3 -r 2f1736cb8f26 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Tue Sep 30 03:30:40 2008 -0400
+++ b/CookBook/FirstSteps.thy	Wed Oct 01 15:40:20 2008 -0400
@@ -1,12 +1,12 @@
 theory FirstSteps
 imports Main
 uses "antiquote_setup.ML"
-     ("comp_simproc")
 begin
 
 
 (*<*)
 
+
 ML {*
 local structure O = ThyOutput
 in
@@ -66,7 +66,7 @@
 
   During developments you might find it necessary to quickly inspect some data
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
-  the function @{ML "warning"}. For example
+  the function @{ML "warning"}. For example 
 *}
 
 ML {*
@@ -74,9 +74,21 @@
 *}
 
 text {*
-  will print out the string inside the response buffer of Isabelle.
+  will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
+  PolyML provides a convenient, though quick-and-dirty, method for converting 
+  arbitrary values into strings, for example: 
 *}
 
+ML {*
+  val _ = warning (makestring 1)
+*}
+
+text {*
+  However this only works if the type of what is printed is monomorphic and not 
+  a function.
+*}
+
+text {* (FIXME: add comment about including ML-files) *}
 
 
 section {* Antiquotations *}
@@ -94,11 +106,11 @@
 text {* 
   where @{text "@{theory}"} is an antiquotation that is substituted with the
   current theory (remember that we assumed we are inside the theory CookBook). 
-  The name of this theory can be extrated using a the function @{ML "Context.theory_name"}. 
+  The name of this theory can be extrated using the function @{ML "Context.theory_name"}. 
   So the code above returns the string @{ML "\"CookBook\""}.
 
   Note, however, that antiquotations are statically scoped, that is the value is
-  determined at ``compile-time'' not ``run-time''. For example the function
+  determined at ``compile-time'', not ``run-time''. For example the function
 
 *}
 
@@ -125,6 +137,7 @@
   In the course of this introduction, we will learn more about 
   these antoquotations: they greatly simplify Isabelle programming since one
   can directly access all kinds of logical elements from ML.
+
 *}
 
 section {* Terms *}
@@ -141,10 +154,10 @@
   representation of this term. This internal represenation corresponds to the 
   datatype defined in @{ML_file "Pure/term.ML"}.
   
-  The internal representation of terms uses the usual de-Bruijn indices mechanism where bound 
+  The internal representation of terms uses the usual de-Bruijn index mechanism where bound 
   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
-  binds the corresponding variable. However, the names of bound variables are 
+  binds the corresponding variable. However, in Isabelle the names of bound variables are 
   kept at abstractions for printing purposes, and so should be treated only as comments. 
 
   \begin{readmore}
@@ -153,7 +166,7 @@
   \end{readmore}
 
   Sometimes the internal representation can be surprisingly different
-  from what you see at the user level, because the layer of
+  from what you see at the user level, because the layers of
   parsing/type checking/pretty printing can be quite elaborate. 
 
   \begin{exercise}
@@ -170,54 +183,76 @@
   may omit parts of it by default. If you want to see all of it, you
   can use @{ML "print_depth 50"} to set the limit to a value high enough.
   \end{exercise}
+
+  The anti-quotation @{text "@prop"} constructs terms of proposition type, 
+  inserting the invisible @{text "Trueprop"} coercion when necessary. 
+  Consider for example
+
 *}
 
+ML {* @{term "P x"} *}
+
+ML {* @{prop "P x"} *}
+
+text {* and *}
+
+
+ML {* @{term "P x \<Longrightarrow> Q x"} *}
+
+ML {* @{prop "P x \<Longrightarrow> Q x"} *}
+
+section {* Construting Terms Manually *} 
+
+text {*
+
+  While antiquotations are very convenient for constructing terms, they can
+  only construct fixed terms. However, one often needs to construct terms dynamially. 
+  For example in order to write the function that returns the implication 
+  @{term "\<And>x. P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments, one can 
+  only write
+*}
+
+
 ML {*
-  @{const_name plus}
-*}
-
-ML {*
-  @{term "{ [x::int] | x. x \<le> -2 }"}
+  fun make_PQ_imp P Q =
+  let
+    val nat = HOLogic.natT
+    val x = Free ("x", nat)
+  in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
+                                    HOLogic.mk_Trueprop (Q $ x)))
+  end
 *}
 
 text {*
-  The internal names of constants like @{term "zero"} or @{text "+"} are
+
+  The reason is that one cannot pass the arguments @{term P} and @{term Q} into 
+  an antiquotation. 
+*}
+
+text {*
+
+   The internal names of constants like @{term "zero"} or @{text "+"} are
   often more complex than one first expects. Here, the extra prefixes
   @{text zero_class} and @{text plus_class} are present because the
   constants are defined within a type class. Guessing such internal
   names can be extremely hard, which is why the system provides
   another antiquotation: @{ML "@{const_name plus}"} gives just this
-  name.
+  name. For example 
 
-  FIXME: maybe explain @{text "@{prop \<dots>}"} as a special kind of terms 
 *}
 
-ML {* @{prop "True"} *}
+ML {* @{const_name plus} *}
+
+text {* produes the fully qualyfied name of the constant plus. *}
 
 
 
-section {* Possible Section on Construting Explicitly Terms *} 
 
 text {*
 
-  There is a disadvantage of using the @{text "@{term \<dots>}"} antiquotation
-  directly in order to construct terms. 
-*}
-
-ML {*
-
-  val nat = HOLogic.natT
-  val x = Free ("x", nat)
-  val t = Free ("t", nat)
-  val P = Free ("P", nat --> HOLogic.boolT)
-  val Q = Free ("Q", nat --> HOLogic.boolT)
-
-  val A1 = Logic.all x 
-           (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
-                              HOLogic.mk_Trueprop (Q $ x)))
-           
-
-  val A2 = HOLogic.mk_Trueprop (P $ t)
+  There are many funtions in @{ML_file "Pure/logic.ML"} and
+  @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms 
+  easier. Have a look ther and try to solve the following exercises:
 
 *}
 
@@ -229,7 +264,7 @@
   and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
   the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
   associates to the left. Try your function on some examples, and see if 
-  the result typechecks. (FIXME: clash with the type-checking section later)
+  the result typechecks. 
   \end{exercise}
 *}
 
@@ -259,14 +294,6 @@
 *}
 
 
-text {*
-  \begin{exercise}
-  Look at the functions defined in @{ML_file "Pure/logic.ML"} and
-  @{ML_file "HOL/hologic.ML"} and see if they can make your life
-  easier.
-  \end{exercise}
-*}
-
 
 section {* Type checking *}
 
@@ -282,8 +309,6 @@
   type-correct, and can only be constructed via the official
   interfaces.
 
-  (FIXME: Alex what do you mean concretely by ``official interfaces'')
-
   Type checking is always relative to a theory context. For now we can use
   the @{ML "@{theory}"} antiquotation to get hold of the current theory.
   For example we can write:
@@ -291,6 +316,17 @@
 
 ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *}
 
+ML {*
+  let
+    val natT = @{typ "nat"}
+    val zero = @{term "0::nat"}
+  in
+    cterm_of @{theory} 
+        (Const (@{const_name plus}, natT --> natT --> natT) 
+         $ zero $ zero)
+  end
+*}
+
 section {* Theorems *}
 
 text {*
@@ -343,11 +379,14 @@
 *}
 
 text {*
-  FIXME Explain this program more carefully (@{ML_text assume},  @{ML_text "forall_elim"} \ldots)
+  For how the functions @{text "assume"}, @{text "forall_elim"} and so on work
+  see \ichcite{sec:thms}. (FIXME correct name)
+
+
 *}
 
 
-section {* Tactical reasoning *}
+section {* Tactical Reasoning *}
 
 text {*
   The goal-oriented tactical style is similar to the @{text apply}
@@ -355,31 +394,34 @@
   which is modified in a sequence of proof steps until it is solved.
 
   A goal (or goal state) is a special @{ML_type thm}, which by
-  convention is an implication:
+  convention is an implication of the form:
+
   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
-  Since the final result @{term C} could again be an implication, there is the
-  @{text "#"} around the final result, which protects its premises from being
+
+  Since the formula @{term C} could potentially be an implication, there is a
+  @{text "#"} wrapped around it, which prevents that premises are 
   misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
-  prop"} is just the identity and used as a syntactic marker.
+  prop"} is just the identity function and used as a syntactic marker. 
+  For more on this goals see \ichcite{sec:tactical-goals}. (FIXME name)
 
-  Now tactics are just functions that map a goal state to a (lazy)
+  Tactics are functions that map a goal state to a (lazy)
   sequence of successor states, hence the type of a tactic is
   @{ML_type[display] "thm -> thm Seq.seq"}
+  
+  \begin{readmore}
   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
-  sequences.
+  sequences. However one rarly onstructs sequences manually, but uses
+  the predefined tactic combinators (tacticals) instead 
+  (see @{ML_file "Pure/tctical.ML"}).
+  \end{readmore}
 
-  Of course, tactics are expected to behave nicely and leave the final
-  conclusion @{term C} intact. In order to start a tactical proof for
-  @{term A}, we
-  just set up the trivial goal @{text "A \<Longrightarrow> #(A)"} and run the tactic
-  on it. When the subgoal is solved, we have just @{text "#(A)"} and
-  can remove the protection.
-
-  The operations in @{ML_file "Pure/goal.ML"} do just that and we can use
-  them.
-
-  Let us transcribe a simple apply style proof from the
-  tutorial\cite{isa-tutorial} into ML:
+  Note, however, that tactics are expected to behave nicely and leave 
+  the final conclusion @{term C} intact (that is only work on the @{text "A\<^isub>i"} 
+  representing the subgoals to be proved) with the exception of possibly 
+  instantiating schematic variables. 
+ 
+  To see how tactics work, let us transcribe a simple apply-style proof from the
+  tutorial \cite{isa-tutorial} into ML:
 *}
 
 lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
@@ -390,6 +432,19 @@
 apply assumption
 done
 
+
+text {*
+  
+  To start the proof, the function  @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"}
+  sets up a goal state for proving @{text goal} under the assumptions @{text assms} with
+  additional variables @{text params} (the variables that are generalised once the
+  goal is proved); @{text "tac"} is a function that returns a tactic (FIXME see non-existing
+  explanation in the imp-manual). 
+
+*}
+
+
+
 ML {*
 let
   val ctxt = @{context}
@@ -404,391 +459,22 @@
 end
 *}
 
-text {*
-  Tactics that affect only a certain subgoal, take a subgoal number as
-  an integer parameter. Here we always work on the first subgoal,
-  following exactly the @{text "apply"} script.
-
-  (Fixme: would it make sense to explain THEN' here)
-
-*}
-
-
-section {* Case Study: Relation Composition *}
-
-text {*
-  \emph{Note: This is completely unfinished. I hoped to have a section
-  with a nontrivial example, but I ran into several problems.}
-
-
-  Recall that HOL has special syntax for set comprehensions:
-  @{term "{ f x y |x y. P x y}"} abbreviates 
-  @{term[source] "{u. \<exists>x y. u = f x y \<and> P x y}"}. 
-
-  We will automatically prove statements of the following form:
-  
-  @{lemma[display] "{(l\<^isub>1 x, r\<^isub>1 x) |x. P\<^isub>1 x} O {(l\<^isub>2 x, r\<^isub>2 x) |x. P\<^isub>2 x}
-  = {(l\<^isub>2 x, r\<^isub>1 y) |x y. r\<^isub>2 x = l\<^isub>1 y \<and>
-  P\<^isub>2 x \<and> P\<^isub>1 y}" by auto}
-
-  In Isabelle, relation composition is defined to be consistent with
-  function composition, that is, the relation applied ``first'' is
-  written on the right hand side. This different from what many
-  textbooks do.
-
-  The above statement about composition is not proved automatically by
-  @{method simp}, and it cannot be solved by a fixed set of rewrite
-  rules, since the number of (implicit) quantifiers may vary. Here, we
-  only have one bound variable in each comprehension, but in general
-  there can be more. On the other hand, @{method auto} proves the
-  above statement quickly, by breaking the equality into two parts and
-  proving them separately. However, if e.g.\ @{term "P\<^isub>1"} is a
-  complicated expression, the automated tools may get confused.
-
-  Our goal is now to develop a small procedure that can compute (with proof) the
-  composition of two relation comprehensions, which can be used to
-  extend the simplifier.
-*}
-
-section {*A tactic *}
-
-text {* Let's start with a step-by-step proof of the above statement *}
-
-lemma "{(l\<^isub>1 x, r\<^isub>1 x) |x. P\<^isub>1 x} O {(l\<^isub>2
-  x, r\<^isub>2 x) |x. P\<^isub>2 x}
-  = {(l\<^isub>2 x, r\<^isub>1 y) |x y. r\<^isub>2 x = l\<^isub>1 y \<and> P\<^isub>2 x \<and> P\<^isub>1 y}"
-apply (rule set_ext)
-apply (rule iffI)
- apply (erule rel_compE)  -- {* @{text "\<subseteq>"} *}
- apply (erule CollectE)     -- {* eliminate @{text "Collect"}, @{text "\<exists>"}, @{text "\<and>"}, and pairs *}
- apply (erule CollectE)
- apply (erule exE)
- apply (erule exE)
- apply (erule conjE)
- apply (erule conjE)
- apply (erule Pair_inject)
- apply (erule Pair_inject)
- apply (simp only:)
-
- apply (rule CollectI)    -- {* introduce them again *}
- apply (rule exI)
- apply (rule exI)
- apply (rule conjI)
-  apply (rule refl)
- apply (rule conjI)
-  apply (rule sym)
-  apply (assumption)
- apply (rule conjI)
-  apply assumption
- apply assumption
-
-apply (erule CollectE)   -- {* @{text "\<subseteq>"} *}
-apply (erule exE)+
-apply (erule conjE)+
-apply (simp only:)
-apply (rule rel_compI)
- apply (rule CollectI)
- apply (rule exI)
- apply (rule conjI)
-  apply (rule refl)
- apply assumption
-
-apply (rule CollectI)
-apply (rule exI)
-apply (rule conjI)
-apply (subst Pair_eq)
-apply (rule conjI)
- apply assumption
-apply (rule refl)
-apply assumption
-done
-
-text {*
-  The reader will probably need to step through the proof and verify
-  that there is nothing spectacular going on here.
-  The @{text apply} script just applies the usual elimination and introduction rules in the right order.
-
-  This script is of course totally unreadable. But we are not trying
-  to produce pretty Isar proofs here. We just want to find out which
-  rules are needed and how they must be applied to complete the
-  proof. And a detailed apply-style proof can often be turned into a
-  tactic quite easily. Of course we must resist the temptation to use
-  @{method auto}, @{method blast} and friends, since their behaviour
-  is not predictable enough. But the simple @{method rule} and
-  @{method erule} methods are fine.
-
-  Notice that this proof depends only in one detail on the
-  concrete equation that we want to prove: The number of bound
-  variables in the comprehension corresponds to the number of
-  existential quantifiers that we have to eliminate and introduce
-  again. In fact this is the only reason why the equations that we
-  want to prove are not just instances of a single rule.
-
-  Here is the ML equivalent of the tactic script above:
-*}
+text {* An alternative way to transcribe this proof is as follows *}
 
 ML {*
-val compr_compose_tac =
-  rtac @{thm set_ext}
-  THEN' rtac @{thm iffI}
-  THEN' etac @{thm rel_compE}
-  THEN' etac @{thm CollectE}
-  THEN' etac @{thm CollectE}
-  THEN' (fn i => REPEAT (etac @{thm exE} i))
-  THEN' etac @{thm conjE}
-  THEN' etac @{thm conjE}
-  THEN' etac @{thm Pair_inject}
-  THEN' etac @{thm Pair_inject}
-  THEN' asm_full_simp_tac HOL_basic_ss
-  THEN' rtac @{thm CollectI}
-  THEN' (fn i => REPEAT (rtac @{thm exI} i))
-  THEN' rtac @{thm conjI}
-  THEN' rtac @{thm refl}
-  THEN' rtac @{thm conjI}
-  THEN' rtac @{thm sym}
-  THEN' assume_tac
-  THEN' rtac @{thm conjI}
-  THEN' assume_tac
-  THEN' assume_tac
-
-  THEN' etac @{thm CollectE}
-  THEN' (fn i => REPEAT (etac @{thm exE} i))
-  THEN' etac @{thm conjE}
-  THEN' etac @{thm conjE}
-  THEN' etac @{thm conjE}
-  THEN' asm_full_simp_tac HOL_basic_ss
-  THEN' rtac @{thm rel_compI}
-  THEN' rtac @{thm CollectI}
-  THEN' (fn i => REPEAT (rtac @{thm exI} i))
-  THEN' rtac @{thm conjI}
-  THEN' rtac @{thm refl}
-  THEN' assume_tac
-  THEN' rtac @{thm CollectI}
-  THEN' (fn i => REPEAT (rtac @{thm exI} i))
-  THEN' rtac @{thm conjI}
-  THEN' simp_tac (HOL_basic_ss addsimps [@{thm Pair_eq}])
-  THEN' rtac @{thm conjI}
-  THEN' assume_tac
-  THEN' rtac @{thm refl}
-  THEN' assume_tac
+let
+  val ctxt = @{context}
+  val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
+in
+  Goal.prove ctxt ["P", "Q"] [] goal (fn _ => 
+    (eresolve_tac [disjE] 
+    THEN' resolve_tac [disjI2] 
+    THEN' assume_tac 
+    THEN' resolve_tac [disjI1] 
+    THEN' assume_tac) 1)
+end
 *}
 
-lemma test1: "{(l\<^isub>1 x, r\<^isub>1 x) |x. P\<^isub>1 x} O {(l\<^isub>2
-  x, r\<^isub>2 x) |x. P\<^isub>2 x}
-  = {(l\<^isub>2 x, r\<^isub>1 y) |x y. r\<^isub>2 x = l\<^isub>1 y \<and> P\<^isub>2 x \<and> P\<^isub>1 y}"
-by (tactic "compr_compose_tac 1")
-
-lemma test3: "{(l\<^isub>1 x, r\<^isub>1 x) |x. P\<^isub>1 x} O {(l\<^isub>2 x z, r\<^isub>2 x z) |x z. P\<^isub>2 x z}
-  = {(l\<^isub>2 x z, r\<^isub>1 y) |x y z. r\<^isub>2 x z = l\<^isub>1 y \<and> P\<^isub>2 x z \<and> P\<^isub>1 y}"
-by (tactic "compr_compose_tac 1")
-
-text {*
-  So we have a tactic that works on at least two examples.
-  Getting it really right requires some more effort. Consider the goal
-*}
-lemma "{(n, Suc n) |n. n > 0} O {(n, Suc n) |n. P n}
-  = {(n, Suc m)|n m. Suc n = m \<and> P n \<and> m > 0}"
-
-(*lemma "{(l\<^isub>1 x, r\<^isub>1 x) |x. P\<^isub>1 x} O {(l\<^isub>2
-  x, r\<^isub>2 x) |x. P\<^isub>2 x}
-  = {(l\<^isub>2 x, r\<^isub>1 y) |x y. r\<^isub>2 x = l\<^isub>1 y \<and> P\<^isub>2 x \<and> P\<^isub>1 y}"*)
-txt {*
-  This is exactly an instance of @{fact test1}, but our tactic fails
-  on it with the usual uninformative
-  \emph{empty result requence}.
-
-  We are now in the frequent situation that we need to debug. One simple instrument for this is @{ML "print_tac"},
-  which is the same as @{ML all_tac} (the identity for @{ML_text "THEN"}),
-  i.e.\ it does nothing, but it prints the current goal state as a
-  side effect.
-  Another debugging option is of course to step through the interactive apply script.
-
-  Finding the problem could be taken as an exercise for the patient
-  reader, and we will go ahead with the solution.
-
-  The problem is that in this instance the simplifier does more than it did in the general version
-  of lemma @{fact test1}. Since @{text "l\<^isub>1"} and @{text "l\<^isub>2"} are just the identity function,
-  the equation corresponding to @{text "l\<^isub>1 y = r\<^isub>2 x "}
-  becomes @{text "m = Suc n"}. Then the simplifier eagerly replaces
-  all occurences of @{term "m"} by @{term "Suc n"} which destroys the
-  structure of the proof.
-
-  This is perhaps the most important lesson to learn, when writing tactics:
-  \textbf{Avoid automation at all cost!!!}.
-
-  Let us look at the proof state at the point where the simplifier is
-  invoked:
-  
-*}
-(*<*)
-apply (rule set_ext)
-apply (rule iffI)
- apply (erule rel_compE)
- apply (erule CollectE)
- apply (erule CollectE)
- apply (erule exE)
- apply (erule exE)
- apply (erule conjE)
- apply (erule conjE)
- apply (erule Pair_inject)
- apply (erule Pair_inject)(*>*)
-txt {*
-  
-  @{subgoals[display]}
-  
-  Like in the apply proof, we now want to eliminate the equations that
-  ``define'' @{term x}, @{term xa} and @{term z}. The other equations
-  are just there by coincidence, and we must not touch them.
-  
-  For such purposes, there is the internal tactic @{text "hyp_subst_single"}.
-  Its job is to take exactly one premise of the form @{term "v = t"},
-  where @{term v} is a variable, and replace @{term "v"} in the whole
-  subgoal. The hypothesis to eliminate is given by its position.
-
-  We can use this tactic to eliminate @{term x}:
-*}
-apply (tactic "single_hyp_subst_tac 0 1")
-txt {*
-  @{subgoals[display]}
-*}
-apply (tactic "single_hyp_subst_tac 2 1")
-apply (tactic "single_hyp_subst_tac 2 1")
-apply (tactic "single_hyp_subst_tac 3 1")
- apply (rule CollectI)    -- {* introduce them again *}
- apply (rule exI)
- apply (rule exI)
- apply (rule conjI)
-  apply (rule refl)
- apply (rule conjI)
-  apply (assumption)
- apply (rule conjI)
-  apply assumption
- apply assumption
-
-apply (erule CollectE)   -- {* @{text "\<subseteq>"} *}
-apply (erule exE)+
-apply (erule conjE)+
-apply (tactic "single_hyp_subst_tac 0 1")
-apply (rule rel_compI)
- apply (rule CollectI)
- apply (rule exI)
- apply (rule conjI)
-  apply (rule refl)
- apply assumption
+section {* Storing and Changing Theorems and so on *}
 
-apply (rule CollectI)
-apply (rule exI)
-apply (rule conjI)
-apply (subst Pair_eq)
-apply (rule conjI)
- apply assumption
-apply (rule refl)
-apply assumption
-done
-
-ML {*
-val compr_compose_tac =
-  rtac @{thm set_ext}
-  THEN' rtac @{thm iffI}
-  THEN' etac @{thm rel_compE}
-  THEN' etac @{thm CollectE}
-  THEN' etac @{thm CollectE}
-  THEN' (fn i => REPEAT (etac @{thm exE} i))
-  THEN' etac @{thm conjE}
-  THEN' etac @{thm conjE}
-  THEN' etac @{thm Pair_inject}
-  THEN' etac @{thm Pair_inject}
-  THEN' single_hyp_subst_tac 0
-  THEN' single_hyp_subst_tac 2
-  THEN' single_hyp_subst_tac 2
-  THEN' single_hyp_subst_tac 3
-  THEN' rtac @{thm CollectI}
-  THEN' (fn i => REPEAT (rtac @{thm exI} i))
-  THEN' rtac @{thm conjI}
-  THEN' rtac @{thm refl}
-  THEN' rtac @{thm conjI}
-  THEN' assume_tac
-  THEN' rtac @{thm conjI}
-  THEN' assume_tac
-  THEN' assume_tac
-
-  THEN' etac @{thm CollectE}
-  THEN' (fn i => REPEAT (etac @{thm exE} i))
-  THEN' etac @{thm conjE}
-  THEN' etac @{thm conjE}
-  THEN' etac @{thm conjE}
-  THEN' single_hyp_subst_tac 0
-  THEN' rtac @{thm rel_compI}
-  THEN' rtac @{thm CollectI}
-  THEN' (fn i => REPEAT (rtac @{thm exI} i))
-  THEN' rtac @{thm conjI}
-  THEN' rtac @{thm refl}
-  THEN' assume_tac
-  THEN' rtac @{thm CollectI}
-  THEN' (fn i => REPEAT (rtac @{thm exI} i))
-  THEN' rtac @{thm conjI}
-  THEN' stac @{thm Pair_eq}
-  THEN' rtac @{thm conjI}
-  THEN' assume_tac
-  THEN' rtac @{thm refl}
-  THEN' assume_tac
-*}
-
-lemma "{(n, Suc n) |n. n > 0 \<and> A} O {(n, Suc n) |n m. P m n}
-  = {(n, Suc m)|n m' m. Suc n = m \<and> P m' n \<and> (m > 0 \<and> A)}"
-apply (tactic "compr_compose_tac 1")
-done
-
-text {*
-  The next step is now to turn this tactic into a simplification
-  procedure. This just means that we need some code that builds the
-  term of the composed relation.
-*}
-
-use "comp_simproc"
-
-(*<*)
-(*simproc_setup mysp ("x O y") = {* compose_simproc *}*)
-
-lemma "{(n, Suc n) |n. n > 0 \<and> A} O {(n, Suc n) |n m. P m n} = x"
-(*apply (simp del:ex_simps)*)
-oops
-
-
-lemma "({(g m, k) | m k. Q m k} 
-O {(h j, f j) | j. R j}) = x"
-(*apply (simp del:ex_simps) *)
-oops
-
-lemma "{uu. \<exists>j m k. uu = (h j, k) \<and> f j = g m \<and> R j \<and> Q m k}
-O {(h j, f j) | j. R j} = x"
-(*apply (simp del:ex_simps)*)
-oops
-
-lemma "
-  { (l x, r x) | x. P x \<and> Q x \<and> Q' x }
-O { (l1 x, r1 x) | x. P1 x \<and> Q1 x \<and> Q1' x }
-= A"
-(*apply (simp del:ex_simps)*)
-oops
-
-lemma "
-  { (l x, r x) | x. P x }
-O { (l1 x, r1 x) | x. P1 x }
-O { (l2 x, r2 x) | x. P2 x }
-= A"
-(*
-apply (simp del:ex_simps)*)
-oops
-
-lemma "{(f n, m) |n m. P n m} O ({(g m, k) | m k. Q m k} 
-O {(h j, f j) | j. R j}) = x"
-(*apply (simp del:ex_simps)*)
-oops
-
-lemma "{u. \<exists>n. u=(f n, g n)} O {u. \<exists>n. u=(h n, j n)} = A"
-oops
-
-
-(*>*)
 end
\ No newline at end of file
diff -r 733614e236a3 -r 2f1736cb8f26 CookBook/Intro.thy
--- a/CookBook/Intro.thy	Tue Sep 30 03:30:40 2008 -0400
+++ b/CookBook/Intro.thy	Wed Oct 01 15:40:20 2008 -0400
@@ -39,10 +39,10 @@
   \item[The Isabelle Reference Manual] is an older document that used
   to be the main reference at a time when all proof scripts were written 
   on the ML level. Many parts of this manual are outdated now, but some 
-  parts, mainly the chapters on tactics, are still useful.
+  parts, particularly the chapters on tactics, are still useful.
   \end{description}
 
-  Then of ourse there is:
+  Then of course there is:
 
   \begin{description}
   \item[The code] is of course the ultimate reference for how
diff -r 733614e236a3 -r 2f1736cb8f26 CookBook/NamedThms.thy
--- a/CookBook/NamedThms.thy	Tue Sep 30 03:30:40 2008 -0400
+++ b/CookBook/NamedThms.thy	Wed Oct 01 15:40:20 2008 -0400
@@ -53,8 +53,7 @@
 
 text {* 
   \begin{readmore}
-  XXX
-
+  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
   \end{readmore}
  *}
 
diff -r 733614e236a3 -r 2f1736cb8f26 CookBook/ROOT.ML
--- a/CookBook/ROOT.ML	Tue Sep 30 03:30:40 2008 -0400
+++ b/CookBook/ROOT.ML	Wed Oct 01 15:40:20 2008 -0400
@@ -4,3 +4,4 @@
 use_thy "FirstSteps";
 use_thy "Parsing";
 use_thy "NamedThms";
+use_thy "Transformation";
\ No newline at end of file
diff -r 733614e236a3 -r 2f1736cb8f26 CookBook/Transformation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Transformation.thy	Wed Oct 01 15:40:20 2008 -0400
@@ -0,0 +1,18 @@
+
+theory Transformation
+imports Main
+begin
+
+
+text_raw {* 
+
+\section*{Ad-hoc Transformation of Theorems} 
+*}
+
+
+
+end
+  
+
+
+
diff -r 733614e236a3 -r 2f1736cb8f26 cookbook.pdf
Binary file cookbook.pdf has changed