diff -r 17b1512f51af -r db8e302f44c8 ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Wed Mar 25 15:09:04 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Thu Mar 26 19:00:51 2009 +0000
@@ -1,104 +1,8 @@
 theory Ind_Code
-imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims
+imports "../Base" "../FirstSteps" Ind_General_Scheme 
 begin
 
-datatype trm =
-  Var "string"
-| App "trm" "trm"
-| Lam "string" "trm"
-
-simple_inductive 
-  fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" ("_ \<sharp> _" [100,100] 100)
-where
-  "a\<noteq>b \<Longrightarrow> a\<sharp>Var b"
-| "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
-| "a\<sharp>Lam a t"
-| "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b t"
-
-section {* Code *}
-
-text {*
-  
-  @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
-
-  @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}
-
-  @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
-  
-  @{text [display] "ind ::= \<And>zs. pred zs \<Longrightarrow> rules[preds::=Ps] \<Longrightarrow> P zs"}
-
-  @{text [display] "oind ::= \<forall>zs. pred zs \<longrightarrow> orules[preds::=Ps] \<longrightarrow> P zs"}
-
-  \underline{Induction proof}
-  
-  After ``objectivication'' we have 
-   @{text "pred zs"} and @{text "orules[preds::=Ps]"}; and have to show
-  @{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\<forall>preds. orules \<longrightarrow> pred zs"}.
-  Instantiating the @{text "preds"} with @{text "Ps"} gives
-  @{text "orules[preds::=Ps] \<longrightarrow> P zs"}. So we can conclude with @{text "P zs"}.
-
-  \underline{Intro proof}
-
-  Assume we want to prove the $i$th intro rule. 
-
-  We have to show @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"};
-  expanding the defs, gives 
-  
-  @{text [display]
-  "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow>  (\<forall>preds. orules \<longrightarrow> pred ts"}
-  
-  By applying as many allI and impI as possible, we have
-  
-  @{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},
-  @{text "orules"}; and have to show @{text "pred ts"}
-
-  the $i$th @{text "orule"} is of the 
-  form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}.
-  
-  So we apply the $i$th @{text "orule"}, but we have to show the @{text "As"} (by assumption)
-  and all @{text "(\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>*"}. For the latter we use the assumptions
-  @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"} and @{text "orules"}.
-
-
-  \begin{center}
-  ****************************
-  \end{center}
-*}
-
-
-text {*
-  For building testcases let us give some shorthands for the definitions of @{text "even/odd"} and
-  @{text "fresh"}. (FIXME put in a figure)
-*}
-  
-ML{*val eo_defs = [@{thm even_def}, @{thm odd_def}]
-val eo_rules =  
-  [@{prop "even 0"},
-   @{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"},
-   @{prop "\<And>n. even n \<Longrightarrow> odd (Suc n)"}]
-val eo_orules =  
-  [@{prop "even 0"},
-   @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"},
-   @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}]
-val eo_preds =  [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] 
-val eo_prednames = [@{binding "even"}, @{binding "odd"}]
-val eo_syns = [NoSyn, NoSyn] 
-val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] *}
-
-
-ML{*val fresh_defs = [@{thm fresh_def}]
-val fresh_rules =  
-  [@{prop "\<And>a b. a\<noteq>b \<Longrightarrow> a\<sharp>Var b"},
-   @{prop "\<And>a s t. a\<sharp>t \<Longrightarrow> a\<sharp>s \<Longrightarrow> a\<sharp>App t s"},
-   @{prop "\<And>a t. a\<sharp>Lam a t"},
-   @{prop "\<And>a b t. a\<noteq>b \<Longrightarrow> a\<sharp>t \<Longrightarrow> a\<sharp>Lam b t"}]
-val fresh_orules =  
-  [@{prop "\<forall>a b. a\<noteq>b \<longrightarrow> a\<sharp>Var b"},
-   @{prop "\<forall>a s t. a\<sharp>t \<longrightarrow> a\<sharp>s \<longrightarrow> a\<sharp>App t s"},
-   @{prop "\<forall>a t. a\<sharp>Lam a t"},
-   @{prop "\<forall>a b t. a\<noteq>b \<longrightarrow> a\<sharp>t \<longrightarrow> a\<sharp>Lam b t"}]
-val fresh_preds =  [@{term "fresh::string\<Rightarrow>trm\<Rightarrow>bool"}] *}
-
+section {* The Gory Details *} 
 
 subsection {* Definitions *}
 
@@ -113,7 +17,7 @@
   annotation and a term representing the right-hand side of the definition.
 *}
 
-ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy =
+ML %linenosgray{*fun make_defn ((predname, syn), trm) lthy =
 let 
   val arg = ((predname, syn), (Attrib.empty_binding, trm))
   val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
@@ -124,23 +28,24 @@
 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 a flag attached to the 
-  theorem (others possibilities are the flags @{ML definitionK in Thm} and @{ML axiomK in Thm}). 
+  theorem (others possibile flags 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
-  use @{ML empty_binding in Attrib} in Line 3, since the definition does 
-  not need to have any theorem attributes. A testcase for this function is
+  use @{ML empty_binding in Attrib} in Line 3, since for our inductive predicates 
+  the definitions do not need to have any theorem attributes. A testcase for this 
+  function is
 *}
 
 local_setup %gray {* fn lthy =>
 let
   val arg = ((@{binding "MyTrue"}, NoSyn), @{term True})
-  val (def, lthy') = make_defs arg lthy 
+  val (def, lthy') = make_defn arg lthy 
 in
   warning (str_of_thm_no_vars lthy' def); lthy'
 end *}
 
 text {*
-  which makes the definition @{prop "MyTrue \<equiv> True"} and then prints it out. 
+  which introduces 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 with the usual
   command \isacommand{thm}:
@@ -160,13 +65,13 @@
   "preds"}.
 
 
-  The first function constructs the term for one particular predicate, say
-  @{text "pred"}. The number of arguments of this predicate is
+  The first function constructs the term for one particular predicate (the
+  argument @{text "pred"} in the code belo). The number of arguments of this predicate is
   determined by the number of argument types given in @{text "arg_tys"}. 
   The other arguments are all the @{text "preds"} and the @{text "orules"}.
 *}
 
-ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
+ML %linenosgray{*fun defn_aux lthy orules preds (pred, arg_tys) =
 let 
   fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
 
@@ -202,34 +107,52 @@
 let
   val pred = @{term "even::nat\<Rightarrow>bool"}
   val arg_tys = [@{typ "nat"}]
-  val def = defs_aux lthy eo_orules eo_preds (pred, arg_tys)
+  val def = defn_aux lthy eo_orules eo_preds (pred, arg_tys)
 in
   warning (Syntax.string_of_term lthy def); lthy
 end *}
 
 text {*
-  The testcase  calls @{ML defs_aux} for the predicate @{text "even"} and prints
+  The testcase  calls @{ML defn_aux} for the predicate @{text "even"} and prints
   out the generated definition. So we obtain as printout 
 
   @{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"}
 
+  If we try out the function for the definition of freshness
+*}
+
+local_setup %gray{* fn lthy =>
+ (warning (Syntax.string_of_term lthy
+    (defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys)));
+  lthy) *}
+
+text {*
+  we obtain
+
+  @{term [display] 
+"\<lambda>z za. \<forall>fresh. (\<forall>a b. \<not> a = b \<longrightarrow> fresh a (Var b)) \<longrightarrow>
+               (\<forall>a s t. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>
+                (\<forall>a t. fresh a (Lam a t)) \<longrightarrow>
+                (\<forall>a b t. \<not> a = b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh z za"}
+
+
   The second function for the definitions has to just iterate the function
-  @{ML defs_aux} over all predicates. The argument @{text "preds"} is again
+  @{ML defn_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 syns} are the
   syntax annotations for each predicate; @{text "arg_tyss"} is
   the list of argument-type-lists for each predicate.
 *}
 
-ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
+ML %linenosgray{*fun defns rules preds prednames syns arg_typss lthy =
 let
   val thy = ProofContext.theory_of lthy
   val orules = map (ObjectLogic.atomize_term thy) rules
-  val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) 
+  val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) 
 in
-  fold_map make_defs (prednames ~~ syns ~~ defs) lthy
+  fold_map make_defn (prednames ~~ syns ~~ defs) lthy
 end*}
 
 text {*
@@ -239,7 +162,7 @@
   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 right-hand sides of the
+  to @{ML defn_aux} in Line 5 produces all right-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 
@@ -248,7 +171,7 @@
 local_setup %gray {* fn lthy =>
 let
   val (defs, lthy') = 
-    definitions eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy
+    defns eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy
 in
   warning (str_of_thms_no_vars lthy' defs); lthy
 end *}
@@ -258,32 +181,30 @@
   the @{text even}-@{text odd} example. The definitions we obtain
   are:
 
-  \begin{isabelle}
-  @{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, 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"}
 
   Note that in the testcase we return the local theory @{text lthy} 
   (not the modified @{text lthy'}). As a result the test case has no effect
-  on the ambient theory. The reason is that if we make again the
-  definition, we pollute the name space with two versions of @{text "even"} 
+  on the ambient theory. The reason is that if we introduce the
+  definition again, we pollute the name space with two versions of @{text "even"} 
   and @{text "odd"}.
 
-  This completes the code for making the definitions. Next we deal with
+  This completes the code for introducing the definitions. Next we deal with
   the induction principles. 
 *}
 
-subsection {* Introduction Rules *}
+subsection {* Induction Principles *}
 
 text {*
   Recall that the proof of the induction principle 
   for @{text "even"} was:
 *}
 
-lemma manual_ind_prin: 
+lemma manual_ind_prin_even: 
 assumes prem: "even z"
 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"
 apply(atomize (full))
@@ -338,7 +259,7 @@
   be implemented as follows:
 *}
 
-ML %linenosgray{*fun induction_tac defs prem insts =
+ML %linenosgray{*fun ind_tac defs prem insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prem,
           K (rewrite_goals_tac defs),
@@ -346,42 +267,47 @@
           assume_tac]*}
 
 text {*
-  We have to give it as arguments the definitions, the premise 
-  (for example @{text "even n"}) and the instantiations. Compare this with the 
-  manual proof given for the lemma @{thm [source] manual_ind_prin}: 
-  as you can see there is almost a one-to-one correspondence between the \isacommand{apply}-script 
-  and the @{ML induction_tac}. A testcase for this tactic is the function
-*}
-
-ML{*fun test_tac prem = 
-let
-  val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
-in 
-  induction_tac eo_defs prem insts 
-end*}
-
-text {*
-  which indeed proves the induction principle: 
+  We have to give it as arguments the definitions, the premise (this premise
+  is @{text "even n"} in lemma @{thm [source] manual_ind_prin_even}) and the
+  instantiations. Compare this tactic with the manual for the lemma @{thm
+  [source] manual_ind_prin_even}: as you can see there is almost a one-to-one
+  correspondence between the \isacommand{apply}-script and the @{ML
+  ind_tac}. Two testcases for this tactic are:
 *}
 
-lemma automatic_ind_prin:
+lemma automatic_ind_prin_even:
 assumes prem: "even z"
 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"
-apply(tactic {* test_tac @{thms prem} *})
-done
+by (tactic {* ind_tac eo_defs @{thms prem} 
+                    [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})
+
+lemma automatic_ind_prin_fresh:
+assumes prem: "fresh z za" 
+shows "(\<And>a b. a \<noteq> b \<Longrightarrow> P a (Var b)) \<Longrightarrow> 
+        (\<And>a t s. \<lbrakk>P a t; P a s\<rbrakk> \<Longrightarrow> P a (App t s)) \<Longrightarrow>
+        (\<And>a t. P a (Lam a t)) \<Longrightarrow> 
+        (\<And>a b t. \<lbrakk>a \<noteq> b; P a t\<rbrakk> \<Longrightarrow> P a (Lam b t)) \<Longrightarrow> P z za"
+by (tactic {* ind_tac @{thms fresh_def} @{thms prem} 
+                    [@{cterm "P::string\<Rightarrow>trm\<Rightarrow>bool"}] *})
+
 
 text {*
-  This gives the theorem:
+  Let us have a closer look at the first proved theorem:
 
   \begin{isabelle}
-  \isacommand{thm}~@{thm [source] automatic_ind_prin}\\
-  @{text "> "}~@{thm automatic_ind_prin}
+  \isacommand{thm}~@{thm [source] automatic_ind_prin_even}\\
+  @{text "> "}~@{thm automatic_ind_prin_even}
   \end{isabelle}
 
-  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
+  The variables @{text "z"}, @{text "P"} and @{text "Q"} are schematic
+  variables (since they are not quantified in the lemma). These schematic
+  variables are needed so that they can be instantiated by the user later
+  on. We have to take care to also generate these schematic variables when
+  generating the goals for the induction principles. While the tactic for
+  proving the induction principles is relatively simple, it will be a bit
+  of work 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] 
   "pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
@@ -397,12 +323,12 @@
   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 "?Ps"}; @{text
-  "pred"} is the predicate for which we prove the introduction principle;
+  "pred"} is the predicate for which we prove the induction principle;
   @{text "newpred"} is its replacement and @{text "arg_tys"} are the argument
   types of this predicate.
 *}
 
-ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys) =
+ML %linenosgray{*fun prove_ind lthy defs srules cnewpreds ((pred, newpred), arg_tys) =
 let
   val zs = replicate (length arg_tys) "z"
   val (newargnames, lthy') = Variable.variant_fixes zs lthy;
@@ -413,15 +339,16 @@
          (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
 in
   Goal.prove lthy' [] [prem] goal
-  (fn {prems, ...} => induction_tac defs prems cnewpreds)
+      (fn {prems, ...} => ind_tac defs prems cnewpreds)
   |> singleton (ProofContext.export lthy' lthy)
 end *}
 
 text {* 
   In Line 3 we produce names @{text "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 construct the terms corresponding to these variables. 
+  \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. 
+  That means they are not (yet) schematic variables.
+  In Line 5 we construct the terms corresponding to these variables. 
   The variables are applied to the predicate in Line 7 (this corresponds
   to the first premise @{text "pred zs"} of the induction principle). 
   In Line 8 and 9, we first construct the term  @{text "P zs"} 
@@ -437,43 +364,40 @@
   lines will return a theorem. However, it is a theorem
   proved inside the local theory @{text "lthy'"}, where the variables @{text
   "zs"} are fixed, but free (see Line 4). By exporting this theorem from @{text
-  "lthy'"} (which contains the @{text "zs"} as free) to @{text
+  "lthy'"} (which contains the @{text "zs"} as free variables) to @{text
   "lthy"} (which does not), we obtain the desired schematic variables @{text "?zs"}.
   A testcase for this function is
 *}
 
 local_setup %gray{* fn lthy =>
 let
-  val srules = [@{prop "P (0::nat)"},
-                @{prop "\<And>n::nat. Q n \<Longrightarrow> P (Suc n)"},
-                @{prop "\<And>n::nat. P n \<Longrightarrow> Q (Suc n)"}] 
+  val newpreds = [@{term "P::nat\<Rightarrow>bool"}, @{term "Q::nat\<Rightarrow>bool"}]
   val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
-  val pred = @{term "even::nat\<Rightarrow>bool"}
+  val srules =  map (subst_free (eo_preds ~~ newpreds)) eo_rules
   val newpred = @{term "P::nat\<Rightarrow>bool"}
-  val arg_tys = [@{typ "nat"}]
   val intro = 
-    prove_induction lthy eo_defs srules cnewpreds ((pred, newpred), arg_tys)
+       prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
 in
   warning (str_of_thm lthy intro); lthy
-end *} 
+end *}
 
 text {*
-  This prints out:
+  This prints out the theorem:
 
   @{text [display]
   " \<lbrakk>even ?z; P 0; \<And>n. Q n \<Longrightarrow> P (Suc n); \<And>n. P n \<Longrightarrow> Q (Suc n)\<rbrakk> \<Longrightarrow> P ?z"}
 
-  Note that the export from @{text lthy'} to @{text lthy} in Line 13 above 
-  has turned the free, but fixed, @{text "z"} into a schematic 
+  The export from @{text lthy'} to @{text lthy} in Line 13 above 
+  has correctly turned the free, but fixed, @{text "z"} into a schematic 
   variable @{text "?z"}; the variables @{text "P"} and @{text "Q"} are not yet
   schematic. 
 
   We still have to produce the new predicates with which the introduction
-  rules are substituted and iterate @{ML prove_induction} over all
+  rules are substituted and iterate @{ML prove_ind} over all
   predicates. This is what the second function does: 
 *}
 
-ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy  =
+ML %linenosgray{*fun inds rules defs preds arg_tyss lthy  =
 let
   val Ps = replicate (length preds) "P"
   val (newprednames, lthy') = Variable.variant_fixes Ps lthy
@@ -486,7 +410,7 @@
   val srules = map (subst_free (preds ~~ newpreds)) rules
 
 in
-  map (prove_induction lthy' defs srules cnewpreds) 
+  map (prove_ind lthy' defs srules cnewpreds) 
         (preds ~~ newpreds ~~ arg_tyss)
           |> ProofContext.export lthy' lthy
 end*}
@@ -511,7 +435,7 @@
 
 local_setup %gray {* fn lthy =>
 let 
-  val ind_thms = inductions eo_rules eo_defs eo_preds eo_arg_tyss lthy
+  val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy
 in
   warning (str_of_thms lthy ind_thms); lthy
 end *}
@@ -521,23 +445,25 @@
   which prints out
 
 @{text [display]
-"> even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow> 
-> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,
-> odd ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>
-> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}
+"even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow> 
+ (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,
+odd ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>
+ (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}
 
   Note that now both, the @{text "?Ps"} and the @{text "?zs"}, are schematic
-  variables. The numbers have been introduced by the pretty-printer and are 
-  not significant.
+  variables. The numbers attached to these variables have been introduced by 
+  the pretty-printer and are \emph{not} important for the user. 
 
-  This completes the code for the induction principles.  
+  This completes the code for the induction principles. The final peice
+  of reasoning infrastructure we need are the introduction rules. 
 *}
 
 subsection {* Introduction Rules *}
 
 text {*
-  Finally we can prove the introduction rules. Their proofs are quite a bit
-  more involved. To ease these proofs somewhat we use the following two helper
+  The proofs of the introduction rules are quite a bit
+  more involved than the ones for the induction principles. 
+  To ease somewhat our work here, we use the following two helper
   functions.
 
 *}
@@ -555,17 +481,15 @@
   shows "\<forall>x y z. P x y z" sorry
 
 lemma imp_elims_test:
-  fixes A B C::"bool"
   shows "A \<longrightarrow> B \<longrightarrow> C" sorry
 
 lemma imp_elims_test':
-  fixes A::"bool"
   shows "A" "B" sorry
 
 text {*
   The function @{ML all_elims} takes a list of (certified) terms and instantiates
   theorems of the form @{thm [source] all_elims_test}. For example we can instantiate
-  the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows
+  the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:
 
   @{ML_response_fake [display, gray]
 "let
@@ -577,98 +501,338 @@
   "P a b c"}
 
   Similarly, the function @{ML imp_elims} eliminates preconditions from implications. 
-  For example: 
+  For example we can eliminate the preconditions @{text "A"} and @{text "B"} from
+  @{thm [source] imp_elims_test}:
 
   @{ML_response_fake [display, gray]
 "warning (str_of_thm_no_vars @{context} 
             (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
   "C"}
 
-  We now look closely at the proof for the introduction rule
+  To explain the proof for the introduction rule, our running example will be
+  the rule:
 
   \begin{isabelle}
-  @{term "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"}
+  @{prop "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
   \end{isabelle}
   
+  for freshness of applications. We set up the proof as follows:
 *}
 
-
 lemma fresh_App:
-  shows "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
-apply(tactic {* ObjectLogic.rulify_tac 1 *})
-apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *})
-apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
-apply(tactic {* print_tac "" *})
+  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+(*<*)oops(*>*)
+
+text {*
+  The first step will be to expand the definitions of freshness
+  and then introduce quantifiers and implications. For this we
+  will use the tactic
+*}
+
+ML{*fun expand_tac defs =
+  ObjectLogic.rulify_tac 1
+  THEN rewrite_goals_tac defs
+  THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
+
+text {*
+  The first step of ``rulifying'' the lemma will turn out important
+  later on. Applying this tactic 
+*}
+
+(*<*)
+lemma fresh_App:
+  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+(*>*)
+apply(tactic {* expand_tac @{thms fresh_def} *})
 
 txt {*
+  we end up in the goal state
+
   \begin{isabelle}
-  @{subgoals}
+  @{subgoals [display]}
   \end{isabelle}
+
+  As you can see, there are parameters (namely @{text "a"}, @{text "b"} 
+  and @{text "t"}) which come from the introduction rule and parameters
+  (in the case above only @{text "fresh"}) which come from the universal
+  quantification in the definition @{term "fresh a (App t s)"}.
+  Similarly, there are preconditions
+  that come from the premises of the rule and premises from the
+  definition. We need to treat these 
+  parameters and preconditions differently. In the code below
+  we will therefore separate them into @{text "params1"} and @{text params2},
+  respectively @{text "prems1"} and @{text "prems2"}. To do this 
+  separation, it is best to open a subproof with the tactic 
+  @{ML SUBPROOF}, since this tactic provides us
+  with the parameters (as list of @{ML_type cterm}s) and the premises
+  (as list of @{ML_type thm}s). The problem we have to overcome 
+  with @{ML SUBPROOF} is that this tactic always expects us to completely 
+  discharge with the goal (see Section ???). This is inconvenient for
+  our gradual explanation of the proof. To circumvent this inconvenience
+  we use the following modified tactic: 
+*}
+(*<*)oops(*>*)
+ML{*fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac*}
+
+text {*
+  If the tactic inside @{ML SUBPROOF} fails, then the overall tactic will
+  still succeed. With this testing tactic, we can gradually implement
+  all necessary proof steps.
+*}
+
+text_raw {*
+\begin{figure}[t]
+\begin{minipage}{\textwidth}
+\begin{isabelle}
+*}
+ML{*fun chop_print params1 params2 prems1 prems2 ctxt =
+let 
+  val s = ["Params1 from the rule:", str_of_cterms ctxt params1] 
+        @ ["Params2 from the predicate:", str_of_cterms ctxt params2] 
+        @ ["Prems1 from the rule:"] @ (map (str_of_thm ctxt) prems1) 
+        @ ["Prems2 from the predicate:"] @ (map (str_of_thm ctxt) prems2) 
+in 
+  s |> separate "\n"
+    |> implode
+    |> warning
+end*}
+text_raw{*
+\end{isabelle}
+\end{minipage}
+\caption{FIXME\label{fig:chopprint}}
+\end{figure}
+*}
+
+text {*
+  First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
+  from @{text "params"} and @{text "prems"}, respectively. To see what is
+  going in our example, we will print out the values using the printing
+  function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will
+  supply us the @{text "params"} and @{text "prems"} as lists, we can 
+  separate them using the function @{ML chop}. 
+*}
+
+ML{*fun chop_test_tac preds rules =
+  SUBPROOF_test (fn {params, prems, context, ...} =>
+  let
+    val (params1, params2) = chop (length params - length preds) params
+    val (prems1, prems2) = chop (length prems - length rules) prems
+  in
+    chop_print params1 params2 prems1 prems2 context; no_tac
+  end) *}
+
+text {* 
+  For the separation we can rely on that Isabelle deterministically 
+  produces parameter and premises in a goal state. The last parameters
+  that were introduced, come from the quantifications in the definitions.
+  Therefore we only have to subtract the number of predicates (in this
+  case only @{text "1"} from the lenghts of all parameters. Similarly
+  with the @{text "prems"}. The last premises in the goal state must
+  come from unfolding of the conclusion. So we can just subtract
+  the number of rules from the number of all premises. Applying
+  this tactic in our example 
 *}
 
-ML_prf {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}
+(*<*)
+lemma fresh_App:
+  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+apply(tactic {* expand_tac @{thms fresh_def} *})
+(*>*)
+apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} *})
+(*<*)oops(*>*)
+
+text {*
+  gives
 
-apply(tactic {* SUBPROOF_test (fn {params, prems, ...} =>
-   let
-     val (prems1, prems2) = chop (length prems - length fresh_rules) prems
-     val (params1, params2) = chop (length params - length fresh_preds) params
-   in
-     no_tac
-   end) @{context} *})
-oops
+  \begin{isabelle}
+  @{text "Params1 from the rule:"}\\
+  @{text "a, b, t"}\\
+  @{text "Params2 from the predicate:"}\\
+  @{text "fresh"}\\
+  @{text "Prems1 from the rule:"}\\
+  @{term "a \<noteq> b"}\\
+  @{text [break]
+"\<forall>fresh.
+      (\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>
+      (\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>
+      (\<forall>a t. fresh a (Lam a t)) \<longrightarrow> 
+      (\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\
+   @{text "Prems2 from the predicate:"}\\
+   @{term "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}\\
+   @{term "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}\\
+   @{term "\<forall>a t. fresh a (Lam a t)"}\\
+   @{term "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}
+  \end{isabelle}
 
 
-ML{*fun subproof2 prem params2 prems2 =  
- SUBPROOF (fn {prems, ...} =>
-   let
-     val prem' = prems MRS prem;
-     val prem'' = 
-       case prop_of prem' of
+  We now have to select from @{text prems2} the premise 
+  that corresponds to the introduction rule we prove, namely:
+
+  @{term [display] "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}
+
+  To use this premise with @{ML rtac}, we need to instantiate its 
+  quantifiers (with @{text params1}) and transform it into a 
+  introduction rule (using @{ML "ObjectLogic.rulify"}. 
+  So we can modify the subproof as follows:
+*}
+
+ML{*fun apply_prem_tac i preds rules =
+  SUBPROOF_test (fn {params, prems, context, ...} =>
+  let
+    val (params1, params2) = chop (length params - length preds) params
+    val (prems1, prems2) = chop (length prems - length rules) prems
+  in
+    rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+    THEN print_tac ""
+    THEN no_tac
+  end) *}
+
+text {* and apply it with *}
+
+(*<*)
+lemma fresh_App:
+  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+apply(tactic {* expand_tac @{thms fresh_def} *})
+(*>*)
+apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} *})
+(*<*)oops(*>*)
+
+text {*
+  Since we print out the goal state after the @{ML rtac} we can see
+  the goal state has the two subgoals
+
+  \begin{isabelle}
+  @{text "1."}~@{prop "a \<noteq> b"}\\
+  @{text "2."}~@{prop "fresh a t"}
+  \end{isabelle}
+
+  where the first comes from a non-recursive precondition of the rule
+  and the second comes from a recursive precondition. The first kind
+  can be solved immediately by @{text "prems1"}. The second kind
+  needs more work. It can be solved with the other premise in @{text "prems1"},
+  namely
+
+  @{term [break,display]
+  "\<forall>fresh.
+      (\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>
+      (\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>
+      (\<forall>a t. fresh a (Lam a t)) \<longrightarrow> 
+      (\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}
+
+  but we have to instantiate it appropriately. These instantiations
+  come from @{text "params1"} and @{text "prems2"}. We can determine
+  whether we are in the simple or complicated case by checking whether
+  the topmost connective is @{text "\<forall>"}. The premises in the simple
+  case cannot have such a quantification, since in the first step 
+  of @{ML "expand_tac"} was the ``rulification'' of the lemma. So 
+  we can implement the following function
+*}
+
+ML{*fun prepare_prem params2 prems2 prem =  
+  rtac (case prop_of prem of
            _ $ (Const (@{const_name All}, _) $ _) =>
-             prem' |> all_elims params2 
-                   |> imp_elims prems2
-         | _ => prem';
-   in 
-     rtac prem'' 1 
-   end)*}
+                 prem |> all_elims params2 
+                      |> imp_elims prems2
+         | _ => prem) *}
+
+text {* 
+  which either applies the premise outright or if it had an
+  outermost universial quantification, instantiates it first with 
+  @{text "params1"} and then @{text "prems1"}. The following tactic 
+  will therefore prove the lemma.
+*}
+
+ML{*fun prove_intro_tac i preds rules =
+  SUBPROOF (fn {params, prems, context, ...} =>
+  let
+    val (params1, params2) = chop (length params - length preds) params
+    val (prems1, prems2) = chop (length prems - length rules) prems
+  in
+    rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+    THEN EVERY1 (map (prepare_prem params2 prems2) prems1)
+  end) *}
+
+text {*
+  We can complete the proof of the introduction rule now as follows:
+*}
+
+(*<*)
+lemma fresh_App:
+  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
+apply(tactic {* expand_tac @{thms fresh_def} *})
+(*>*)
+apply(tactic {* prove_intro_tac 3 [fresh_pred] fresh_rules @{context} 1 *})
+done
+
+text {* 
+  Unfortunately, not everything is done yet.
+*}
+
+lemma accpartI:
+  shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+apply(tactic {* expand_tac @{thms accpart_def} *})
+apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *})
+apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *})
+
+txt {*
+  
+  @{subgoals [display]}
+
+  \begin{isabelle}
+  @{text "Params1 from the rule:"}\\
+  @{text "x"}\\
+  @{text "Params2 from the predicate:"}\\
+  @{text "P"}\\
+  @{text "Prems1 from the rule:"}\\
+  @{text "R ?y x \<Longrightarrow> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P ?y"}\\
+  @{text "Prems2 from the predicate:"}\\
+  @{term "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x"}\\
+  \end{isabelle}
+
+*}
+(*<*)oops(*>*)
+
+
+ML{*fun prepare_prem params2 prems2 ctxt prem =  
+  SUBPROOF (fn {prems, ...} =>
+  let
+    val prem' = prems MRS prem
+  in 
+    rtac (case prop_of prem' of
+           _ $ (Const (@{const_name All}, _) $ _) =>
+                 prem' |> all_elims params2 
+                       |> imp_elims prems2
+         | _ => prem') 1
+  end) ctxt *}
+
+ML{*fun prove_intro_tac i preds rules =
+  SUBPROOF (fn {params, prems, context, ...} =>
+  let
+    val (params1, params2) = chop (length params - length preds) params
+    val (prems1, prems2) = chop (length prems - length rules) prems
+  in
+    rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+    THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1)
+  end) *}
+
+lemma accpartI:
+  shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+apply(tactic {* expand_tac @{thms accpart_def} *})
+apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *})
+done
+
+
 
 text {*
 
 *}
 
-
-ML %linenosgray{*fun subproof1 rules preds i = 
- SUBPROOF (fn {params, prems, context = ctxt', ...} =>
-   let
-     val (prems1, prems2) = chop (length prems - length rules) prems
-     val (params1, params2) = chop (length params - length preds) params
-   in
-     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 
-     (* applicateion of the i-ith intro rule *)
-     THEN
-     EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
-   end)*}
-
-text {*
-  @{text "params1"} are the variables of the rules; @{text "params2"} is
-  the variables corresponding to the @{text "preds"}.
-
-  @{text "prems1"} are the assumption corresponding to the rules;
-  @{text "prems2"} are the assumptions coming from the allIs/impIs
-
-  you instantiate the parameters i-th introduction rule with the parameters
-  that come from the rule; and you apply it to the goal
-
-  this now generates subgoals corresponding to the premisses of this
-  intro rule 
-*}
-
 ML{*
 fun intros_tac defs rules preds i ctxt =
   EVERY1 [ObjectLogic.rulify_tac,
           K (rewrite_goals_tac defs),
           REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
-          subproof1 rules preds i ctxt]*}
+          prove_intro_tac i preds rules ctxt]*}
 
 text {*
   A test case
@@ -692,7 +856,7 @@
 apply(tactic {* intros_tac_test @{context} 2 *})
 done
 
-ML{*fun introductions rules preds defs lthy = 
+ML{*fun intros rules preds defs lthy = 
 let
   fun prove_intro (i, goal) =
     Goal.prove lthy [] [] goal
@@ -713,9 +877,9 @@
   val tyss = map (binder_types o fastype_of) preds   
   val (attrs, rules) = split_list rule_specs    
 
-  val (defs, lthy') = definitions rules preds prednames syns tyss lthy      
-  val ind_rules = inductions rules defs preds tyss lthy' 	
-  val intro_rules = introductions rules preds defs lthy'
+  val (defs, lthy') = defns rules preds prednames syns tyss lthy      
+  val ind_rules = inds rules defs preds tyss lthy' 	
+  val intro_rules = intros rules preds defs lthy'
 
   val mut_name = space_implode "_" (map Binding.name_of prednames)
   val case_names = map (Binding.name_of o fst) attrs
@@ -768,6 +932,8 @@
   \item say that the induction principle is weaker (weaker than
   what the standard inductive package generates)
   \item say that no conformity test is done
+  \item exercise about strong induction principles
+  \item exercise about the test for the intro rules
   \end{itemize}
   
 *}