
diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/Package/Ind_Code.thy
--- a/CookBook/Package/Ind_Code.thy	Tue Mar 17 17:32:12 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Wed Mar 18 03:03:51 2009 +0100
@@ -55,7 +55,7 @@
 
 text {*
   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 
+  been made. In Line 4, @{ML internalK in Thm} is a flag attached to the 
   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 that, for example, find theorems in the theorem database. We also
@@ -72,7 +72,7 @@
 end *}
 
 text {*
-  which makes the difinition @{prop "MyTrue \<equiv> True"} and then prints it out. 
+  which makes the definition @{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}:
@@ -82,17 +82,20 @@
   @{text "> MyTrue \<equiv> True"}
   \end{isabelle}
 
-  The next two functions construct the terms we need for the definitions, namely 
-  terms of the form 
+  The next two functions construct the terms we need for the definitions for
+  our \isacommand{simple\_inductive} command. These 
+  terms are 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 that they do not occur
-  in the @{text orules} and also be distinct from @{text "preds"}. 
+  in the @{text orules} and also be distinct from the @{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"}.
+  The first function constructs the term for one particular predicate, say
+  @{text "pred"}; the number of arguments of this predicate is
+  determined by the number of argument types of @{text "arg_tys"}. 
+  So it takes these two parameters as arguments. The other arguments are
+  all the @{text "preds"} and the @{text "orules"}.
 *}
 
 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
@@ -112,11 +115,13 @@
 end*}
 
 text {*
-  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 function in Line 3 is just a helper function for constructing universal
+  quantifications. The code in Lines 5 to 9 produces 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) using the
   function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in
@@ -132,7 +137,7 @@
   val orules = [@{prop "even 0"},
                 @{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
                 @{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] 
-  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}, @{term "z::nat"}]
   val pred = @{term "even::nat\<Rightarrow>bool"}
   val arg_tys = [@{typ "nat"}]
   val def = defs_aux lthy orules preds (pred, arg_tys)
@@ -141,15 +146,18 @@
 end *}
 
 text {*
-  It constructs the left-hand side for the definition of @{term "even"}. So we obtain 
+  It constructs the left-hand side for the definition of @{text "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. 
+  The main function for the definitions now has to just iterate the function
+  @{ML defs_aux} over all predicates. 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 for each predicate.
 *}
 
 ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
@@ -162,19 +170,16 @@
 end*}
 
 text {*
-  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 for each predicate. 
-  
-  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. 
+  The user will state the introduction rules using meta-implications and
+  meta-quanti\-fications. In Line 4, we transform these introduction rules into
+  the object logic (since definitions cannot be stated with
+  meta-connectives). To do this 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.  The result
+  of the function is a list of theorems and a local theory.
+
 
   A testcase for this function is 
 *}
@@ -194,6 +199,9 @@
 end *}
 
 text {*
+  where we feed into the functions all parameters corresponding to
+  the @{text even}-@{text odd} example. The definitions we obtain
+  are:
 
   \begin{isabelle}
   \isacommand{thm}~@{text "even_def odd_def"}\\
@@ -201,18 +209,16 @@
 "> 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"}
+>                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
   \end{isabelle}
 
 
-  This completes the code concerning the definitions. Next comes the code for
-  the induction principles. 
-
-  Let us now turn to the induction principles. Recall that the proof of the 
-  induction principle for @{term "even"} was:
+  This completes the code for making the definitions. Next we deal with
+  the induction principles. Recall that the proof of the induction principle 
+  for @{text "even"} was:
 *}
 
-lemma 
+lemma man_ind_principle: 
 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))
@@ -224,32 +230,35 @@
 done
 
 text {* 
-  We have to implement code that constructs the induction principle and then
-  a tactic that automatically proves it. 
+  The code for such induction principles has to accomplish two tasks: 
+  constructing the induction principles from the given introduction
+  rules and then automatically generating a proof of them using a tactic. 
   
   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}.
+  quantifiers. 
 *}
 
 ML{*fun inst_spec ctrm = 
  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
 
 text {*
-  For example we can use it in the following proof to instantiate the 
-  three quantifiers in the assumption. We use the tactic
+  This helper function instantiates the @{text "?x"} in the theorem 
+  @{thm spec} with a given @{ML_type cterm}. Together with 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"}. 
-  *}
+  we can use @{ML inst_spec} in the following proof to instantiate the 
+  three quantifiers in the assumption. 
+*}
 
-lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"
+lemma 
+  fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  shows "\<forall>x y z. P x y z \<Longrightarrow> True"
 apply (tactic {* 
-  inst_spec_tac  [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}] 1 *})
+  inst_spec_tac  [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
 txt {* 
   We obtain the goal state
 
@@ -271,8 +280,11 @@
           assume_tac]*}
 
 text {*
-  We only have to give it as arguments the premises and the instantiations.
-  A testcase for the tactic is
+  We only have to give it as arguments the definitions, the premise 
+  (like @{text "even n"}) 
+  and the instantiations. Compare this with the manual proof given for the
+  lemma @{thm [source] man_ind_principle}.  
+  A testcase for this tactic is the function
 *}
 
 ML{*fun test_tac prems = 
@@ -284,7 +296,7 @@
 end*}
 
 text {*
-  which indeed proves the induction principle. 
+  which indeed proves the induction principle: 
 *}
 
 lemma 
@@ -294,22 +306,23 @@
 done
 
 text {*
-  While the generic proof for the induction principle is relatively simple, 
-  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 
+  While the tactic for the induction principle is relatively simple, 
+  it is a bit harder to construct the goals from the introduction 
+  rules the user provides. 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$>"}
+  "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$> \<^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.
+  rules by new distinct variables written @{text "\<^raw:$Ps$>"}. 
+  We also need to generate fresh arguments for the predicate @{text "pred"} in
+  the premise and the @{text "\<^raw:$P$>"} in the conclusion. We achieve
+  that in two steps. 
 
-  The function below expects that the rules are already appropriately
-  substitued. The argument @{text "srules"} stands for these substituted
-  introduction rules; @{text cnewpreds} are the certified terms coresponding
+  The function below expects that the introduction rules are already appropriately
+  substituted. The argument @{text "srules"} stands for these substituted
+   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 argument types of this predicate.
@@ -331,64 +344,102 @@
 end *}
 
 text {* 
-  In Line 3 we produce a name @{text "\<^raw:$zs$>"} for each type in the 
+  In Line 3 we produce names @{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
+  and then add the (substituded) introduction rules as premises. In case that
+  no introduction rules are given, the conclusion of this implication 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; 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$>"}.
+  In Line 11 we set up the goal to be proved; in the next line call the tactic
+  for proving the induction principle. This tactic expects definitions, the
+  premise and 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$>"}.
 
-  Now it is left to produce the new predicated with which the introduction
+  (FIXME testcase)
+
+
+  Now it is left to produce the new predicates with which the introduction
   rules are substituted. 
 *}
 
-ML %linenosgray{*fun inductions rules defs preds tyss lthy  =
+ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy  =
 let
   val Ps = replicate (length preds) "P"
   val (newprednames, lthy') = Variable.variant_fixes Ps lthy
   
   val thy = ProofContext.theory_of lthy'
 
-  val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss
+  val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss
   val newpreds = map Free (newprednames ~~ tyss')
   val cnewpreds = map (cterm_of thy) newpreds
-  val rules' = map (subst_free (preds ~~ newpreds)) rules
+  val srules = map (subst_free (preds ~~ newpreds)) rules
 
 in
-  map (prove_induction lthy' defs rules' cnewpreds) 
-        (preds ~~ newpreds ~~ tyss)
+  map (prove_induction lthy' defs srules cnewpreds) 
+        (preds ~~ newpreds ~~ arg_tyss)
           |> ProofContext.export lthy' lthy
 end*}
 
-ML {*
-  let 
-    val rules = [@{prop "even (0::nat)"},
-                 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
-                 @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 
-    val defs = [@{thm even_def}, @{thm odd_def}]
-    val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
-    val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
-  in
-    inductions rules defs preds tyss @{context}
-  end
+text {*
+  In Line 3 we generate a string @{text [quotes] "P"} for each predicate. 
+  In Line 4, we use the same trick as in the previous function, that is making the 
+  @{text "\<^raw:$Ps$>"} fresh and declaring them as fixed but free in
+  the new local theory @{text "lthy'"}. From the local theory we extract
+  the ambient theory in Line 6. We need this theory in order to certify 
+  the new predicates. In Line 8 we calculate the types of these new predicates
+  using the argument types. Next we turn them into terms and subsequently
+  certify them. We can now produce the substituted introduction rules 
+  (Line 11). Line 14 and 15 just iterate the proofs for all predicates.
+  From this we obtain a list of theorems. Finally we need to export the 
+  fixed variables @{text "\<^raw:$Ps$>"} to obtain the correct quantification 
+  (Line 16).
+
+  A testcase for this function is
+*}
+
+local_setup %gray {* fn lthy =>
+let 
+  val rules = [@{prop "even (0::nat)"},
+               @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+               @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 
+  val defs = [@{thm even_def}, @{thm odd_def}]
+  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+  val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
+  val ind_thms = inductions rules defs preds tyss lthy
+in
+  warning (str_of_thms lthy ind_thms); lthy
+end  
 *}
 
 
-subsection {* Introduction Rules *}
+text {*
+  which prints out
+
+@{text [display]
+"> even z \<Longrightarrow> 
+>  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> P z,
+> odd z \<Longrightarrow> 
+>  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> Pa z"}
+
+
+  This completes the code for the induction principles. Finally we can 
+  prove the introduction rules. 
+
+*}
+
+ML {* ObjectLogic.rulify  *}
+
 
 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}
@@ -422,7 +473,7 @@
 fun introductions_tac defs rules preds i ctxt =
   EVERY1 [ObjectLogic.rulify_tac,
           K (rewrite_goals_tac defs),
-          REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
+          REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
           subproof1 rules preds i ctxt]*}
 
 lemma evenS: 
@@ -491,7 +542,6 @@
 end*} 
 
 ML{*val spec_parser = 
-   OuterParse.opt_target --
    OuterParse.fixes -- 
    Scan.optional 
      (OuterParse.$$$ "where" |--
@@ -501,10 +551,9 @@
 
 ML{*val specification =
   spec_parser >>
-    (fn ((loc, pred_specs), rule_specs) =>
-      Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*}
+    (fn ((pred_specs), rule_specs) => add_inductive pred_specs rule_specs)*}
 
-ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
+ML{*val _ = OuterSyntax.local_theory "simple_inductive" "define inductive predicates"
           OuterKeyword.thy_decl specification*}
 
 text {*




