--- a/ProgTutorial/Package/Ind_Code.thy	Tue Mar 24 18:06:20 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Mar 25 15:09:04 2009 +0100
@@ -83,7 +83,7 @@
 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"}]] *}
+val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] *}
 
 
 ML{*val fresh_defs = [@{thm fresh_def}]
@@ -103,7 +103,7 @@
 subsection {* Definitions *}
 
 text {*
-  First we have to produce for each predicate the definition, whose general form is
+  We first have to produce for each predicate the definition, whose general form is
 
   @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 
@@ -124,7 +124,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 a flag attached to the 
-  theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}). 
+  theorem (others possibilities are the flags @{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 
@@ -133,7 +133,7 @@
 
 local_setup %gray {* fn lthy =>
 let
-  val arg =  ((@{binding "MyTrue"}, NoSyn), @{term True})
+  val arg = ((@{binding "MyTrue"}, NoSyn), @{term True})
   val (def, lthy') = make_defs arg lthy 
 in
   warning (str_of_thm_no_vars lthy' def); lthy'
@@ -218,7 +218,8 @@
   The second function for the definitions 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
+  "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.
 *}
 
@@ -283,10 +284,10 @@
 *}
 
 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"
+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))
-apply(cut_tac prems)
+apply(cut_tac prem)
 apply(unfold even_def)
 apply(drule spec[where x=P])
 apply(drule spec[where x=Q])
@@ -370,6 +371,13 @@
 done
 
 text {*
+  This gives the theorem:
+
+  \begin{isabelle}
+  \isacommand{thm}~@{thm [source] automatic_ind_prin}\\
+  @{text "> "}~@{thm automatic_ind_prin}
+  \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 
@@ -417,7 +425,7 @@
   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
+  and then add the (substituted) 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. 
@@ -428,7 +436,7 @@
   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
+  "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 does not), we obtain the desired schematic variables @{text "?zs"}.
   A testcase for this function is
@@ -457,7 +465,7 @@
 
   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"}. The @{text "P"} and @{text "Q"} are not yet
+  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
@@ -515,8 +523,8 @@
 @{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"}
+> 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 
@@ -575,41 +583,31 @@
 "warning (str_of_thm_no_vars @{context} 
             (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
   "C"}
-*}
 
-ML {* prems_of *}
-ML {* Logic.strip_params *}
-ML {* Logic.strip_assums_hyp *}
+  We now look closely at the proof for the introduction rule
 
-ML {*
-fun chop_print (params1, params2) (prems1, prems2) ctxt =
-let
-  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
-   ()
-end
+  \begin{isabelle}
+  @{term "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"}
+  \end{isabelle}
+  
 *}
 
 
-
-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) *})
-oops
-
-ML {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}
-
-
 lemma fresh_App:
-  shows "\<And>a t s. \<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
+  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 "" *})
+
+txt {*
+  \begin{isabelle}
+  @{subgoals}
+  \end{isabelle}
+*}
+
+ML_prf {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}
+
 apply(tactic {* SUBPROOF_test (fn {params, prems, ...} =>
    let
      val (prems1, prems2) = chop (length prems - length fresh_rules) prems

--- a/ProgTutorial/Tactical.thy	Tue Mar 24 18:06:20 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Mar 25 15:09:04 2009 +0100
@@ -515,7 +515,8 @@
   theorem in the first.
 
   @{ML_response_fake [display,gray]
-   "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" 
+"map (no_vars @{context}) 
+   ([@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}])" 
 "[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
  \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
  (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
@@ -1067,7 +1068,7 @@
 
 text {*
   If the simplifier cannot make any progress, then it leaves the goal unchanged,
-  i.e.~does not raise any error message. That means if you use it to unfold a 
+  i.e., does not raise any error message. That means if you use it to unfold a 
   definition for a constant and this constant is not present in the goal state, 
   you can still safely apply the simplifier.
 
@@ -1117,11 +1118,11 @@
   \end{readmore}
 
   \begin{readmore}
-  FIXME: Find the right place Discrimination nets are implemented
+  FIXME: Find the right place: Discrimination nets are implemented
   in @{ML_file "Pure/net.ML"}.
   \end{readmore}
 
-  The most common combinators to modify simpsets are
+  The most common combinators to modify simpsets are:
 
   \begin{isabelle}
   \begin{tabular}{ll}
@@ -1170,7 +1171,7 @@
 text {* 
   To see how they work, consider the function in Figure~\ref{fig:printss}, which
   prints out some parts of a simpset. If you use it to print out the components of the
-  empty simpset, i.e.~ @{ML empty_ss}
+  empty simpset, i.e., @{ML empty_ss}
   
   @{ML_response_fake [display,gray]
   "print_ss @{context} empty_ss"
@@ -1351,7 +1352,7 @@
   it would be desirable to add also the lemma @{thm [source] perm_compose} to
   the simplifier for pushing permutations over other permutations. Unfortunately, 
   the right-hand side of this lemma is again an instance of the left-hand side 
-  and so causes an infinite loop. The seems to be no easy way to reformulate 
+  and so causes an infinite loop. There seems to be no easy way to reformulate 
   this rule and so one ends up with clunky proofs like:
 *}
 
@@ -1417,7 +1418,7 @@
 end*}
 
 text {*
-  For all three phases we have to build simpsets addig specific lemmas. As is sufficient
+  For all three phases we have to build simpsets adding specific lemmas. As is sufficient
   for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
   the desired results. Now we can solve the following lemma
 *}
@@ -1430,8 +1431,8 @@
 
 
 text {*
-  in one step. This tactic can deal with most instances of normalising permutations;
-  in order to solve all cases we have to deal with corner-cases such as the
+  in one step. This tactic can deal with most instances of normalising permutations.
+  In order to solve all cases we have to deal with corner-cases such as the
   lemma being an exact instance of the permutation composition lemma. This can
   often be done easier by implementing a simproc or a conversion. Both will be 
   explained in the next two chapters.

--- a/ProgTutorial/antiquote_setup.ML	Tue Mar 24 18:06:20 2009 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Wed Mar 25 15:09:04 2009 +0100
@@ -111,18 +111,17 @@
     | _ => error "No proof state")
 
   val state = proof_state node;
-  val goals = Proof.pretty_goals false state;
+  val goals = Pretty.chunks (Proof.pretty_goals false state);
 
   val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
   val (As, B) = Logic.strip_horn prop;
   val output  = (case (length As) of
-                      0 => goals 
-                    | n => (Pretty.str (subgoals n))::goals)  
+                      0 => [goals] 
+                    | n => [Pretty.str (subgoals n), goals])  
 in 
   ThyOutput.output output
 end
 
-
 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
-   
+ 
 end;

Binary file progtutorial.pdf has changed