# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1237914380 -3600
# Node ID 0634d42bb69fbad6e06723725ddd04aa42aace5d
# Parent  d3cd633e82404256f92c6bc3ea03dac6cbf65ac8
a bit more work on the simple-inductive package

diff -r d3cd633e8240 -r 0634d42bb69f ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Tue Mar 24 12:09:38 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Tue Mar 24 18:06:20 2009 +0100
@@ -13,8 +13,7 @@
   "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"  
-
+| "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b t"
 
 section {* Code *}
 
@@ -60,15 +59,55 @@
   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 {*
-  First we have to produce for each predicate the definition of the form
+  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"}] *}
+
+
+subsection {* Definitions *}
+
+text {*
+  First we have to produce for each predicate the definition, whose general form is
 
   @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 
-  and then ``register'' the definitions with Isabelle. 
+  and then ``register'' the definition inside a local theory. 
   To do the latter, 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.
@@ -102,8 +141,8 @@
 
 text {*
   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
+  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}:
 
   \begin{isabelle}
@@ -111,18 +150,20 @@
   @{text "> MyTrue \<equiv> True"}
   \end{isabelle}
 
-  The next two functions construct the right-hand sides of the definitions, which
-  are of the form 
+  The next two functions construct the right-hand sides of the definitions, 
+  which are terms of the form
 
   @{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 
-  The variables @{text "zs"} need to be chosen so that they do not occur
-  in the @{text orules} and also be distinct from the @{text "preds"}. 
+  When constructing them, the variables @{text "zs"} need to be chosen so that
+  they do not occur in the @{text orules} and also be distinct from the @{text
+  "preds"}.
+
 
   The first function constructs the term for one particular predicate, say
-  @{text "pred"}; the number of arguments of this predicate is
+  @{text "pred"}. 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 @{text "preds"} and the @{text "orules"}.
+  The other arguments are all the @{text "preds"} and the @{text "orules"}.
 *}
 
 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
@@ -153,26 +194,22 @@
   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 "zs"}, i.e.~the fresh arguments of the
+  over all the @{text "zs"}, i.e., the fresh arguments of the
   predicate. A testcase for this function is
 *}
 
 local_setup %gray{* fn lthy =>
 let
-  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 pred = @{term "even::nat\<Rightarrow>bool"}
   val arg_tys = [@{typ "nat"}]
-  val def = defs_aux lthy orules preds (pred, arg_tys)
+  val def = defs_aux lthy eo_orules eo_preds (pred, arg_tys)
 in
   warning (Syntax.string_of_term lthy def); lthy
 end *}
 
 text {*
-  It calls @{ML defs_aux} for the definition of @{text "even"} and prints
-  out the definition. So we obtain as printout 
+  The testcase  calls @{ML defs_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)) 
@@ -201,7 +238,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 left-hand sides of the
+  to @{ML defs_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 
@@ -209,16 +246,10 @@
 
 local_setup %gray {* fn lthy =>
 let
-  val rules = [@{prop "even 0"},
-               @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
-               @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 
-  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
-  val prednames = [@{binding "even"}, @{binding "odd"}] 
-  val syns = [NoSyn, NoSyn] 
-  val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
-  val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
+  val (defs, lthy') = 
+    definitions eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy
 in
-  warning (str_of_thms_no_vars lthy' defs); lthy'
+  warning (str_of_thms_no_vars lthy' defs); lthy
 end *}
 
 text {*
@@ -227,7 +258,6 @@
   are:
 
   \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,
@@ -235,14 +265,25 @@
 >                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
   \end{isabelle}
 
+  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"} 
+  and @{text "odd"}.
 
   This completes the code for making the definitions. Next we deal with
-  the induction principles. Recall that the proof of the induction principle 
+  the induction principles. 
+*}
+
+subsection {* Introduction Rules *}
+
+text {*
+  Recall that the proof of the induction principle 
   for @{text "even"} was:
 *}
 
-lemma man_ind_principle: 
-assumes prems: "even n"
+lemma manual_ind_prin: 
+assumes prem: "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)
@@ -266,14 +307,15 @@
 
 text {*
   This helper function instantiates the @{text "?x"} in the theorem 
-  @{thm spec} with a given @{ML_type cterm}. Together with the tactic
+  @{thm spec} with a given @{ML_type cterm}. We call this helper function
+  in the tactic:
 *}
 
 ML{*fun inst_spec_tac ctrms = 
   EVERY' (map (dtac o inst_spec) ctrms)*}
 
 text {*
-  we can use @{ML inst_spec_tac} in the following proof to instantiate the 
+  This tactic allows us to instantiate in the following proof the 
   three quantifiers in the assumption. 
 *}
 
@@ -295,37 +337,36 @@
   be implemented as follows:
 *}
 
-ML %linenosgray{*fun induction_tac defs prems insts =
+ML %linenosgray{*fun induction_tac defs prem insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
-          cut_facts_tac prems,
+          cut_facts_tac prem,
           K (rewrite_goals_tac defs),
           inst_spec_tac insts,
           assume_tac]*}
 
 text {*
-  We only have to give it the definitions, the premise (like @{text "even n"})
-  and the instantiations as arguments. Compare this with the manual proof
-  given for the lemma @{thm [source] man_ind_principle}: there is almos a
-  one-to-one correspondence between the \isacommand{apply}-script and the
-  @{ML induction_tac}. A testcase for this tactic is the function
+  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 prems = 
+ML{*fun test_tac prem = 
 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 
+  induction_tac eo_defs prem insts 
 end*}
 
 text {*
   which indeed proves the induction principle: 
 *}
 
-lemma auto_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(tactic {* test_tac @{thms prems} *})
+lemma automatic_ind_prin:
+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
 
 text {*
@@ -335,33 +376,25 @@
   @{text "pred"} a goal of the form
 
   @{text [display] 
-  "pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P$ ?zs"}
+  "pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
 
   where the predicates @{text preds} are replaced in the introduction 
-  rules by new distinct variables written @{text "Ps"}.
-  We also need to generate fresh arguments for the predicate @{text "pred"} in
-  the premise and the @{text "?P"} in the conclusion. Note 
+  rules by new distinct variables @{text "?Ps"}.
+  We also need to generate fresh arguments @{text "?zs"} for the predicate 
+  @{text "pred"} and the @{text "?P"} in the conclusion. Note 
   that the  @{text "?Ps"}  and @{text "?zs"} need to be
-  schematic variables that can be instantiated. This corresponds to what the
-  @{thm [source] auto_ind_principle} looks like:
+  schematic variables that can be instantiated by the user.
 
-  \begin{isabelle}
-  \isacommand{thm}~@{thm [source] auto_ind_principle}\\
-  @{text "> \<lbrakk>even ?n; ?P 0; \<And>m. ?Q m \<Longrightarrow> ?P (Suc m); \<And>m. ?P m \<Longrightarrow> ?Q (Suc m)\<rbrakk> \<Longrightarrow> ?P ?n"}
-  \end{isabelle}
-
-  We achieve
-  that in two steps. 
-
-  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 "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.
+  We generate these goals in two steps. The first function 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 "?Ps"}; @{text
+  "pred"} is the predicate for which we prove the introduction 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_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys) =
 let
   val zs = replicate (length arg_tys) "z"
   val (newargnames, lthy') = Variable.variant_fixes zs lthy;
@@ -380,8 +413,8 @@
   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 just construct the terms corresponding to these variables. 
-  The term variables are applied to the predicate in Line 7 (this corresponds
+  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"} 
   and then add the (substituded) introduction rules as premises. In case that
@@ -389,20 +422,20 @@
   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; in the next line we call the tactic
-  for proving the induction principle. This tactic expects the definitions, the
-  premise and the (certified) predicates with which the introduction rules
-  have been substituted. The code in these two lines will return a theorem. 
-  However, it is a theorem
+  In Line 11 we set up the goal to be proved; in the next line we call the
+  tactic for proving the induction principle. As mentioned before, this tactic
+  expects the definitions, the premise and the (certified) predicates with
+  which the introduction rules have been substituted. The code in these two
+  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. By exporting this theorem from @{text
   "lthy'"} (which contains the @{text "zs"} as free) to @{text
-  "lthy"} (which does not), we obtain the desired schematic variables.
+  "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 defs = [@{thm even_def}, @{thm odd_def}]
   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)"}] 
@@ -411,7 +444,7 @@
   val newpred = @{term "P::nat\<Rightarrow>bool"}
   val arg_tys = [@{typ "nat"}]
   val intro = 
-    prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys)
+    prove_induction lthy eo_defs srules cnewpreds ((pred, newpred), arg_tys)
 in
   warning (str_of_thm lthy intro); lthy
 end *} 
@@ -424,11 +457,12 @@
 
   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 
-  variable @{text "?z"}.
+  variable @{text "?z"}. The @{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
-  predicates. This is what the next function does. 
+  predicates. This is what the second function does: 
 *}
 
 ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy  =
@@ -450,18 +484,18 @@
 end*}
 
 text {*
-  In Line 3 we generate a string @{text [quotes] "P"} for each predicate. 
+  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 "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
+  the new predicates. In Line 8, we construct the types of these new predicates
   using the given argument types. Next we turn them into terms and subsequently
   certify them (Line 9 and 10). We can now produce the substituted introduction rules 
   (Line 11) using the function @{ML subst_free}. 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 "Ps"} to obtain the schematic variables 
+  fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"} 
   (Line 16).
 
   A testcase for this function is
@@ -469,13 +503,7 @@
 
 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
+  val ind_thms = inductions eo_rules eo_defs eo_preds eo_arg_tyss lthy
 in
   warning (str_of_thms lthy ind_thms); lthy
 end *}
@@ -490,21 +518,27 @@
 > 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
+  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.
 
-  This completes the code for the induction principles.  Finally we can prove the 
-  introduction rules. Their proofs are quite a bit more involved. To ease them 
-  somewhat we  use the following two helper function.
+  This completes the code for the induction principles.  
+*}
+
+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
+  functions.
+
 *}
 
 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})*}
 
 text {* 
-  To see what they do, let us suppose whe have the follwoing three
+  To see what these functions do, let us suppose whe have the following three
   theorems. 
 *}
 
@@ -535,7 +569,7 @@
   "P a b c"}
 
   Similarly, the function @{ML imp_elims} eliminates preconditions from implications. 
-  For example 
+  For example: 
 
   @{ML_response_fake [display, gray]
 "warning (str_of_thm_no_vars @{context} 
@@ -548,57 +582,26 @@
 ML {* Logic.strip_assums_hyp *}
 
 ML {*
-fun chop_print_tac m n ctxt thm =
+fun chop_print (params1, params2) (prems1, prems2) ctxt =
 let
-  val [trm] = prems_of thm
-  val params = map fst (Logic.strip_params trm)
-  val prems  = Logic.strip_assums_hyp trm
-  val (prems1, prems2) = chop (length prems - m) prems;
-  val (params1, params2) = chop (length params - n) params;
-  val _ = warning (Syntax.string_of_term ctxt trm)
-  val _ = warning (commas params)
-  val _ = warning (commas (map (Syntax.string_of_term ctxt) prems))
   val _ = warning ((commas params1) ^ " | " ^ (commas params2))
   val _ = warning ((commas (map (Syntax.string_of_term ctxt) prems1)) ^ " | " ^
                    (commas (map (Syntax.string_of_term ctxt) prems2)))
 in
-   Seq.single thm
+   ()
 end
 *}
 
-ML {* METAHYPS *}
 
-ML {*
-fun chop_print_tac2 ctxt prems =
-let
-  val _ = warning (commas (map (str_of_thm_no_vars ctxt) prems))
-in
-   all_tac
-end
-*}
 
 lemma intro1:
   shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
 apply(tactic {* ObjectLogic.rulify_tac 1 *})
 apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *})
 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
-apply(tactic {* chop_print_tac 3 2 @{context} *})
 oops
 
-ML {*
-fun SUBPROOF_test tac ctxt =
-  SUBPROOF (fn {params, prems, context,...} =>
-    let
-      val thy = ProofContext.theory_of context
-    in 
-      tac (params, prems, context) 
-      THEN  Method.insert_tac prems 1
-      THEN  print_tac "SUBPROOF Test"
-      THEN  SkipProof.cheat_tac thy
-    end) ctxt 1
-*}
-
-
+ML {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}
 
 
 lemma fresh_App:
@@ -606,17 +609,16 @@
 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 "" *})
+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
-(*
-apply(tactic {* SUBPROOF_test 
-  (fn (params, prems, ctxt) =>
-   let 
-     val (prems1, prems2) = chop (length prems - 4) prems;
-     val (params1, params2) = chop (length params - 1) params;
-   in
-     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 2))) 1
-   end) @{context} *})
-*)
+
 
 ML{*fun subproof2 prem params2 prems2 =  
  SUBPROOF (fn {prems, ...} =>
@@ -640,8 +642,8 @@
 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;
+     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 *)
@@ -675,15 +677,7 @@
 *}
 
 ML{*fun intros_tac_test ctxt i =
-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"}]
-in
-  intros_tac defs rules preds i ctxt
-end*}
+  intros_tac eo_defs eo_rules eo_preds i ctxt *}
 
 lemma intro0:
   shows "even 0"
diff -r d3cd633e8240 -r 0634d42bb69f ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Tue Mar 24 12:09:38 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Mar 24 18:06:20 2009 +0100
@@ -347,7 +347,7 @@
 (*<*)oops(*>*)
 
 text {*
-  A simple tactic making theorem proving particularly simple is 
+  A simple tactic for ``easily'' discharging proof obligations is 
   @{ML SkipProof.cheat_tac}. This tactic corresponds to
   the Isabelle command \isacommand{sorry} and is sometimes useful  
   during the development of tactics.
diff -r d3cd633e8240 -r 0634d42bb69f progtutorial.pdf
Binary file progtutorial.pdf has changed