
diff -r 7b6d81ff9d9a -r 0a8981f52045 ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Thu Apr 09 18:11:35 2009 +0000
+++ b/ProgTutorial/Package/Ind_Code.thy	Sat Apr 11 19:23:58 2009 +0000
@@ -5,71 +5,73 @@
 section {* The Gory Details\label{sec:code} *} 
 
 text {*
-  As mentioned before the code falls roughly into three parts: code that deals
-  with the definitions, withe the induction principles and the introduction
-  rules, respectively. In addition there are some administrative functions
-  that string everything together.
+  As mentioned before the code falls roughly into three parts: the code that deals
+  with the definitions, with the induction principles and with the introduction
+  rules. In addition there are some administrative functions that string everything 
+  together.
 *}
 
 subsection {* Definitions *}
 
 text {*
-  We first have to produce for each predicate the definition, whose general form is
+  We first have to produce for each predicate the user specifies an appropriate
+  definition, whose general form is
 
   @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 
   and then ``register'' the definition inside a local theory. 
-  To do the latter, we use the following wrapper for 
+  To do the latter, we use the following wrapper for the function
   @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
   annotation and a term representing the right-hand side of the definition.
 *}
 
-ML %linenosgray{*fun make_defn ((predname, syn), trm) lthy =
+ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy =
 let 
-  val arg = ((predname, syn), (Attrib.empty_binding, trm))
+  val arg = ((predname, mx), (Attrib.empty_binding, trm))
   val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
 in 
   (thm, lthy') 
 end*}
 
 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 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 for our inductive predicates 
-  the definitions do not need to have any theorem attributes. A testcase for this 
-  function is
+  It returns the definition (as a theorem) and the local theory in which the
+  definition has been made. In Line 4, @{ML internalK in Thm} is a flag
+  attached to the 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.\footnote{FIXME: put in the section about theorems.} We
+  also use @{ML empty_binding in Attrib} in Line 3, since the definitions for
+  our inductive predicates are not meant to be seen by the user and therefore
+  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 arg = ((@{binding "My_True"}, NoSyn), @{term True})
   val (def, lthy') = make_defn arg lthy 
 in
   warning (str_of_thm_no_vars lthy' def); lthy'
 end *}
 
 text {*
-  which introduces the definition @{prop "MyTrue \<equiv> True"} and then prints it out. 
+  which introduces the definition @{thm My_True_def} and then prints it out. 
   Since we are testing the function inside \isacommand{local\_setup}, i.e., make
   actual changes to the ambient theory, we can query the definition with the usual
   command \isacommand{thm}:
 
   \begin{isabelle}
-  \isacommand{thm}~@{text "MyTrue_def"}\\
-  @{text "> MyTrue \<equiv> True"}
+  \isacommand{thm}~@{thm [source] "My_True_def"}\\
+  @{text ">"}~@{thm "My_True_def"}
   \end{isabelle}
 
   The next two functions construct the right-hand sides of the definitions, 
-  which are terms of the form
+  which are terms whose general form is:
 
   @{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 
-  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"}.
+  When constructing these terms, 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, named @{text defn_aux}, constructs the term for one
@@ -145,40 +147,40 @@
                 (\<forall>a b t. \<not> a = b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh z za"}
 
 
-  The second function, named @{text defns}, has to just iterate the function
+  The second function, named @{text defns}, has to iterate the function
   @{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 binding names of the predicates; @{text syns} 
-  are the list of syntax annotations for the predicates; @{text "arg_tyss"} is
-  the list of argument-type-lists.
+  the list of predicates as @{ML_type term}s; the argument @{text
+  "prednames"} is the list of binding names of the predicates; @{text mxs} 
+  are the list of syntax, or mixfix, annotations for the predicates; 
+  @{text "arg_tyss"} is the list of argument-type-lists.
 *}
 
-ML %linenosgray{*fun defns rules preds prednames syns arg_typss lthy =
+ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy =
 let
   val thy = ProofContext.theory_of lthy
   val orules = map (ObjectLogic.atomize_term thy) rules
   val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) 
 in
-  fold_map make_defn (prednames ~~ syns ~~ defs) lthy
+  fold_map make_defn (prednames ~~ mxs ~~ defs) lthy
 end*}
 
 text {*
   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-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 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 
+  definitions. The actual definitions are then made in Line 7.  The result of
+  the function is a list of theorems and a local theory (the theorems are
+  registered with the local theory). A testcase for this function is
 *}
 
 local_setup %gray {* fn lthy =>
 let
   val (defs, lthy') = 
-    defns eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy
+    defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy
 in
   warning (str_of_thms_no_vars lthy' defs); lthy
 end *}
@@ -301,7 +303,7 @@
 
 text {*
   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
+  it will be a bit more work to construct the goals from the introduction rules
   the user provides.  Therefore let us have a closer look at the first 
   proved theorem:
 
@@ -968,7 +970,7 @@
 
 ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy =
 let
-  val syns = map snd pred_specs
+  val mxs = map snd pred_specs
   val pred_specs' = map fst pred_specs
   val prednames = map fst pred_specs'
   val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'
@@ -976,20 +978,21 @@
 
   val (namesattrs, rules) = split_list rule_specs    
 
-  val (defs, lthy') = defns rules preds prednames syns tyss lthy      
-  val ind_prin = inds rules defs preds tyss lthy' 	
+  val (defs, lthy') = defns rules preds prednames mxs tyss lthy      
+  val ind_prins = 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) namesattrs
 in
   lthy' |> reg_many mut_name ((@{binding "intros"}, []), intro_rules) 
+        ||>> reg_many mut_name ((@{binding "inducts"}, []), ind_prins)
         ||>> fold_map (reg_single1 mut_name) (namesattrs ~~ intro_rules)  
         ||>> fold_map (reg_single2 @{binding "induct"} 
               [Attrib.internal (K (RuleCases.case_names case_names)),
                Attrib.internal (K (RuleCases.consumes 1)),
                Attrib.internal (K (Induct.induct_pred ""))]) 
-             (prednames ~~ ind_prin) 
+             (prednames ~~ ind_prins) 
         |> snd
 end*}
 
@@ -1017,11 +1020,13 @@
   proofs correspond to the names of the introduction rules. These
   are generated in Line 16.
 
-  Line 18 now adds to @{text "lthy'"} all the introduction rules 
-  under the name @{text "mut_name.intros"} (see previous paragraph).
-  Line 19 add further every introduction rule under its own name
+  Lines 18 and 19 now add to @{text "lthy'"} all the introduction rules 
+  und induction principles under the name @{text "mut_name.intros"} and
+  @{text "mut_name.inducts"}, respectively (see previous paragraph).
+  
+  Line 20 add further every introduction rule under its own name
   (given by the user).\footnote{FIXME: what happens if the user did not give
-  any name.} Line 20 registers the induction principles. For this we have
+  any name.} Line 21 registers the induction principles. For this we have
   to use some specific attributes. The first @{ML "case_names" in RuleCases} 
   corresponds to the case names that are used by Isar to reference the proof
   obligations in the induction. The second @{ML "consumes 1" in RuleCases}
@@ -1029,7 +1034,8 @@
   the predicate over which the induction proceeds) is eliminated. 
 
   This completes all the code and fits in with the ``front end'' described
-  in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. Why the mut-name? 
+  in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. 
+  Why the mut-name? 
   What does @{ML Binding.qualify} do?}
 *}
 (*<*)end(*>*)
\ No newline at end of file




