diff -r 4d0e2edd476d -r 8bb4eaa2ec92 CookBook/Package/Ind_Code.thy
--- a/CookBook/Package/Ind_Code.thy	Tue Mar 17 12:26:34 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Tue Mar 17 17:32:12 2009 +0100
@@ -4,8 +4,6 @@
 
 section {* Code *}
 
-subsection {* Definitions *}
-
 text {*
   @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
 
@@ -42,8 +40,8 @@
 
   @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 
-  We use the following wrapper function to make the definition via
-  @{ML LocalTheory.define}. The function takes a predicate name, a syntax
+  In order to make definitions, we use the following wrapper for 
+  @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
   annotation and a term representing the right-hand side of the definition.
 *}
 
@@ -56,15 +54,13 @@
 end*}
 
 text {*
-  It returns the definition (as theorem) and the local theory in which this definition has 
+  It returns the definition (as a theorem) and the local theory in which this definition has 
   been made. In Line 4 @{ML internalK in Thm} is just a flag attached to the 
-  theorem (others possibilities are @{ML definitionK in Thm} or @{ML axiomK in Thm}). 
+  theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}). 
   These flags just classify theorems and have no significant meaning, except 
-  for tools such as finding theorems in the theorem database. We also
+  for tools that, for example, find theorems in the theorem database. We also
   use @{ML empty_binding in Attrib} in Line 3, since the definition does 
-  not need any theorem attributes. Note the definition has not yet been 
-  stored in the theorem database. So at the moment we can only refer to it
-  via the return value. A testcase for this functions is
+  not need to have any theorem attributes. A testcase for this function is
 *}
 
 local_setup %gray {* fn lthy =>
@@ -76,23 +72,27 @@
 end *}
 
 text {*
-  which prints out the theorem @{prop "MyTrue \<equiv> True"}. Since we are
-  testing the function inside \isacommand{local\_setup} we have also
-  access to theorem associated with this definition.
+  which makes the difinition @{prop "MyTrue \<equiv> True"} and then prints it out. 
+  Since we are testing the function inside \isacommand{local\_setup}, i.e.~make
+  changes to the ambient theory, we can query the definition using the usual
+  command \isacommand{thm}:
 
   \begin{isabelle}
   \isacommand{thm}~@{text "MyTrue_def"}\\
   @{text "> MyTrue \<equiv> True"}
   \end{isabelle}
 
-  The next function constructs the term for the definition, namely 
+  The next two functions construct the terms we need for the definitions, namely 
+  terms of the form 
 
   @{text [display] "\<lambda>\<^raw:$zs$>. \<forall>preds. orules \<longrightarrow> pred \<^raw:$zs$>"}
 
-  The variables @{text "\<^raw:$zs$>"} need to be chosen so to not occur
-  in the @{text orules} and also be distinct from @{text "pred"}. The function
-  constructs the term for one particular predicate @{text "pred"}; the number
-  of @{text "\<^raw:$zs$>"} is determined by the nunber of types. 
+  The variables @{text "\<^raw:$zs$>"} need to be chosen so that they do not occur
+  in the @{text orules} and also be distinct from @{text "preds"}. 
+
+  The first function constructs the term for one particular predicate @{text
+  "pred"}; the number of arguments @{text "\<^raw:$zs$>"} of this predicate is
+  determined by the number of argument types of @{text "arg_tys"}.
 *}
 
 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
@@ -112,16 +112,17 @@
 end*}
 
 text {*
-  The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"} with which the 
-  predicate is applied. For this it pairs every type with a string @{text [quotes] "z"} 
-  (Line 7); then generates variants for all these strings (names) so that they are 
-  unique w.r.t.~to the orules and predicates; in Line 9 it generates the corresponding 
-  variable terms for the unique names.
+  The code in Lines 5 to 9 produce the fresh @{text "\<^raw:$zs$>"}. For this
+  it pairs every argument type with the string @{text [quotes] "z"} (Line 7);
+  then generates variants for all these strings so that they are unique
+  w.r.t.~to the @{text "orules"} and the predicates; in Line 9 it generates the
+  corresponding variable terms for the unique strings.
 
-  The unique free variables are applied to the predicate (Line 11); then
-  the @{text orules} are prefixed (Line 12); in Line 13 we
-  quantify over all predicates; and in line 14 we just abstract over all
-  the (fresh)  @{text "\<^raw:$zs$>"}, i.e.~the arguments of the predicate.
+  The unique free variables are applied to the predicate (Line 11) using the
+  function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in
+  Line 13 we quantify over all predicates; and in line 14 we just abstract
+  over all the @{text "\<^raw:$zs$>"}, i.e.~the fresh arguments of the
+  predicate.
 
   A testcase for this function is
 *}
@@ -140,16 +141,15 @@
 end *}
 
 text {*
-  It constructs the term for the predicate @{term "even"}. So we obtain as printout
-  the term
+  It constructs the left-hand side for the definition of @{term "even"}. So we obtain 
+  as printout the term
 
   @{text [display] 
 "\<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
                          \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"}
 
   The main function for the definitions now has to just iterate
-  the function @{ML defs_aux} over all predicates. THis is what the
-  next function does. 
+  the function @{ML defs_aux} over all predicates. 
 *}
 
 ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
@@ -162,14 +162,19 @@
 end*}
 
 text {*
-  The argument @{text "preds"} is the list of predicates as @{ML_type term}s;
+  The argument @{text "preds"} is again the the list of predicates as 
+  @{ML_type term}s;
   the argument @{text "prednames"} is the list of names of the predicates;
-  @{text "arg_tyss"} is the list of argument-type-lists. 
+  @{text "arg_tyss"} is the list of argument-type-lists for each predicate. 
   
-  In line 4 we generate the intro rules in the object logic; for this we have to 
-  obtain the theory behind the local theory (Line 3); with this we can
-  call @{ML defs_aux} to generate the terms for the left-hand sides.
-  The actual definitions are made in Line 7.
+  The user give the introduction rules using meta-implications and meta-quantifications.
+  In line 4 we transform the introduction rules into the object logic (definitions
+  cannot use them). To do the transformation we have to 
+  obtain the theory behind the local theory (Line 3); with this theory 
+  we can use the function @{ML ObjectLogic.atomize_term} to make the
+  transformation (Line 4). The call to @{ML defs_aux} in Line 5 produces all
+  left-hand sides of the definitions. The actual definitions are then made in Line 7.
+  As the result we obtain a list of theorems and a local theory. 
 
   A testcase for this function is 
 *}
@@ -185,29 +190,31 @@
   val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
   val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
 in
-  warning (str_of_thms lthy' defs); lthy
+  warning (str_of_thms lthy' defs); lthy'
 end *}
 
 text {*
 
-  It prints out the two definitions
+  \begin{isabelle}
+  \isacommand{thm}~@{text "even_def odd_def"}\\
+  @{text [break]
+"> even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
+>                                 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,
+> odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
+>                                 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
+  \end{isabelle}
 
-  @{text [display] 
-"even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
-                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z, 
- odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 
-                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
 
   This completes the code concerning the definitions. Next comes the code for
   the induction principles. 
 
-  Recall the proof for the induction principle for @{term "even"}: 
+  Let us now turn to the induction principles. Recall that the proof of the 
+  induction principle for @{term "even"} was:
 *}
 
 lemma 
-  assumes prems: "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"
+assumes prems: "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 prems)
 apply(unfold even_def)
@@ -217,27 +224,34 @@
 done
 
 text {* 
-  To automate this proof we need to be able to instantiate universal 
-  quantifiers. For this we use the following helper function. It
-  instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}.
+  We have to implement code that constructs the induction principle and then
+  a tactic that automatically proves it. 
+  
+  The tactic will use the following helper function for instantiating universal 
+  quantifiers. This function instantiates the @{text "?x"} in the theorem 
+  @{thm spec} with a given @{ML_type cterm}.
 *}
 
 ML{*fun inst_spec ctrm = 
  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
 
 text {*
-  For example we can use it to instantiate an assumption:
+  For example we can use it in the following proof to instantiate the 
+  three quantifiers in the assumption. We use the tactic
 *}
 
+ML{*fun inst_spec_tac ctrms = 
+  EVERY' (map (dtac o inst_spec) ctrms)*}
+
+text {*
+  and then apply use it with the @{ML_type cterm}s @{text "y1\<dots>y3"}. 
+  *}
+
 lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"
 apply (tactic {* 
-  let 
-    val ctrms = [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}]
-  in 
-    EVERY1 (map (dtac o inst_spec) ctrms)
-  end *})
+  inst_spec_tac  [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] 1 *})
 txt {* 
-  where it produces the goal state
+  We obtain the goal state
 
   \begin{minipage}{\textwidth}
   @{subgoals} 
@@ -245,15 +259,15 @@
 (*<*)oops(*>*)
 
 text {*
-  Now the tactic for proving the induction rules can be implemented 
-  as follows
+  Now the complete tactic for proving the induction principles can 
+  be implemented as follows:
 *}
 
 ML %linenosgray{*fun induction_tac defs prems insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prems,
           K (rewrite_goals_tac defs),
-          EVERY' (map (dtac o inst_spec) insts),
+          inst_spec_tac insts,
           assume_tac]*}
 
 text {*
@@ -261,43 +275,47 @@
   A testcase for the tactic is
 *}
 
+ML{*fun test_tac prems = 
+let
+  val defs = [@{thm even_def}, @{thm odd_def}]
+  val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
+in 
+  induction_tac defs prems insts 
+end*}
+
+text {*
+  which indeed proves the induction principle. 
+*}
+
 lemma 
-  assumes prems: "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(tactic {* 
-  let
-     val defs = [@{thm even_def}, @{thm odd_def}]
-     val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
-  in 
-    induction_tac defs @{thms prems} insts 
-  end *})
+assumes prems: "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(tactic {* test_tac @{thms prems} *})
 done
 
-
 text {*
-  which indeed proves the lemma. 
-
   While the generic proof for the induction principle is relatively simple, 
-  it is a bit harder to set up the goals just from the given introduction 
-  rules. For this we have to construct for each predicate @{text "pred"}
+  it is a bit harder to construct the goals from just the introduction 
+  rules the user states. In general we have to construct for each predicate 
+  @{text "pred"} a goal of the form
 
   @{text [display] 
   "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$>\<^raw:$zs$>"}
 
-  where the given predicates @{text preds} are replaced by new distinct 
-  ones written as @{text "\<^raw:$Ps$>"}, and also need to be applied to
-  new variables @{text "\<^raw:$zs$>"}. 
+  where the given predicates @{text preds} are replaced in the introduction 
+  rule @{text "rules"} by new distinct variables written as @{text "\<^raw:$Ps$>"}. 
+  We also need to generate fresh arguments for the predicate @{text "pred"} and
+  the @{text "\<^raw:$P$>"} in the conclusion of the induction principle.
 
   The function below expects that the rules are already appropriately
-  replaced. The argument @{text "mrules"} stands for these modified
+  substitued. The argument @{text "srules"} stands for these substituted
   introduction rules; @{text cnewpreds} are the certified terms coresponding
   to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for
   which we prove the introduction principle; @{text "newpred"} is its
-  replacement and @{text "tys"} are the types of its argument.
+  replacement and @{text "tys"} are the argument types of this predicate.
 *}
 
-ML %linenosgray{* fun prove_induction lthy defs mrules cnewpreds ((pred, newpred), tys)  =
+ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), tys)  =
 let
   val zs = replicate (length tys) "z"
   val (newargnames, lthy') = Variable.variant_fixes zs lthy;
@@ -305,7 +323,7 @@
   
   val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
   val goal = Logic.list_implies 
-         (mrules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
+         (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
 in
   Goal.prove lthy' [] [prem] goal
   (fn {prems, ...} => induction_tac defs prems cnewpreds)
@@ -313,31 +331,37 @@
 end *}
 
 text {* 
-  In Line 3 we produce a list of names @{text "\<^raw:$zs$>"} according to the type 
-  list. Line 4 makes these names unique and declare them as \emph{free} (but fixed)
-  variables. These variables are free in the new theory @{text "lthy'"}. In Line 5
-  we just construct the terms corresponding to the variables. The term variables are
-  applied to the predicate in Line 7 (this is the first premise 
-  @{text "pred \<^raw:$zs$>"} of the induction principle). In Line 8 and 9
-  we first the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} and then add
-  the (modified) introduction rules as premises.
+  In Line 3 we produce a name @{text "\<^raw:$zs$>"} for each type in the 
+  argument type list. Line 4 makes these names unique and declares them as 
+  \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In 
+  Line 5 we just construct the terms corresponding to these variables. 
+  The term variables are applied to the predicate in Line 7 (this corresponds
+  to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle). 
+  In Line 8 and 9, we first construct the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} 
+  and then add the (modified) introduction rules as premises. In case that
+  no introduction rules are given, the conclusion of this implications needs
+  to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal
+  mechanism will fail. 
 
-  In Line 11 we set up the goal to be proved; call the induction tactic in
-  Line 13. This returns a theorem. However, it is a theorem proved inside
-  the local theory @{text "lthy'"} where the variables @{text "\<^raw:$zs$>"} are
-  fixed, but free. By exporting this theorem from @{text "lthy'"} (which does contain
-  the  @{text "\<^raw:$zs$>"} as free) to @{text "lthy"} (which does not), we
-  obtain the desired quantifications @{text "\<And>\<^raw:$zs$>"}.
+  In Line 11 we set up the goal to be proved; then call the tactic for proving the 
+  induction principle. This tactic expects the (certified) predicates with which
+  the introduction rules have been substituted. This will return a theorem. 
+  However, it is a theorem proved inside the local theory @{text "lthy'"} where 
+  the variables @{text "\<^raw:$zs$>"} are fixed, but free. By exporting this 
+  theorem from @{text "lthy'"} (which contains the  @{text "\<^raw:$zs$>"} 
+  as free) to @{text "lthy"} (which does not), we obtain the desired quantifications 
+  @{text "\<And>\<^raw:$zs$>"}.
 
-  So it is left to produce the modified rules and 
+  Now it is left to produce the new predicated with which the introduction
+  rules are substituted. 
 *}
 
-ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =
+ML %linenosgray{*fun inductions rules defs preds tyss lthy  =
 let
   val Ps = replicate (length preds) "P"
-  val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1
+  val (newprednames, lthy') = Variable.variant_fixes Ps lthy
   
-  val thy = ProofContext.theory_of lthy2
+  val thy = ProofContext.theory_of lthy'
 
   val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss
   val newpreds = map Free (newprednames ~~ tyss')
@@ -345,9 +369,9 @@
   val rules' = map (subst_free (preds ~~ newpreds)) rules
 
 in
-  map (prove_induction lthy2 defs rules' cnewpreds) 
+  map (prove_induction lthy' defs rules' cnewpreds) 
         (preds ~~ newpreds ~~ tyss)
-          |> ProofContext.export lthy2 lthy1
+          |> ProofContext.export lthy' lthy
 end*}
 
 ML {*
@@ -458,20 +482,10 @@
     |> snd
 end*}
 
-ML{*fun read_specification' vars specs lthy =
-let 
-  val specs' = map (fn (a, s) => (a, [s])) specs
-  val ((varst, specst), _) = 
-                   Specification.read_specification vars specs' lthy
-  val specst' = map (apsnd the_single) specst
-in   
-  (varst, specst')
-end*}
-
 ML{*fun add_inductive pred_specs rule_specs lthy =
 let
-  val (pred_specs', rule_specs') = 
-    read_specification' pred_specs rule_specs lthy
+  val ((pred_specs', rule_specs'), _) = 
+         Specification.read_spec pred_specs rule_specs lthy
 in
   add_inductive_i pred_specs' rule_specs' lthy
 end*}