isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:7b6d81ff9d9a
+:0a8981f52045
 begin
 section {* The Gory Details\label{sec:code} *}
 text {*
-As mentioned before the code falls roughly into three parts: code that deals
+As mentioned before the code falls roughly into three parts: the code that deals
-with the definitions, withe the induction principles and the introduction
+with the definitions, with the induction principles and with the introduction
-rules, respectively. In addition there are some administrative functions
+rules. In addition there are some administrative functions that string everything
-that string everything together.
+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
+It returns the definition (as a theorem) and the local theory in which the
-been made. In Line 4, @{ML internalK in Thm} is a flag attached to the
+definition has been made. In Line 4, @{ML internalK in Thm} is a flag
-theorem (others possibile flags are @{ML definitionK in Thm} and @{ML axiomK in Thm}).
+attached to the theorem (others possibile flags are @{ML definitionK in Thm}
-These flags just classify theorems and have no significant meaning, except
+and @{ML axiomK in Thm}). These flags just classify theorems and have no
-for tools that, for example, find theorems in the theorem database. We also
+significant meaning, except for tools that, for example, find theorems in
-use @{ML empty_binding in Attrib} in Line 3, since for our inductive predicates
+the theorem database.\footnote{FIXME: put in the section about theorems.} We
-the definitions do not need to have any theorem attributes. A testcase for this
+also use @{ML empty_binding in Attrib} in Line 3, since the definitions for
-function is
+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"}\\
+\isacommand{thm}~@{thm [source] "My_True_def"}\\
-@{text "> MyTrue \<equiv> True"}
+@{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
+When constructing these terms, the variables @{text "zs"} need to be chosen so
-they do not occur in the @{text orules} and also be distinct from the @{text
+that they do not occur in the @{text orules} and also be distinct from the
-"preds"}.
+@{text "preds"}.
 The first function, named @{text defn_aux}, constructs the term for one
 particular predicate (the argument @{text "pred"} in the code below). The
 number of arguments of this predicate is determined by the number of
 (\<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, 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
+the list of predicates as @{ML_type term}s; the argument @{text
-"prednames"} is the list of binding names of the predicates; @{text syns}
+"prednames"} is the list of binding names of the predicates; @{text mxs}
-are the list of syntax annotations for the predicates; @{text "arg_tyss"} is
+are the list of syntax, or mixfix, annotations for the predicates;
-the list of argument-type-lists.
+@{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
+meta-quanti\-fications. In Line 4, we transform these introduction rules
-the object logic (since definitions cannot be stated with
+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
+definitions. The actual definitions are then made in Line 7.  The result of
-of the function is a list of theorems and a local theory. A testcase for
+the function is a list of theorems and a local theory (the theorems are
-this function is
+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 *}
 text {*
 [@{cterm "P::string\<Rightarrow>trm\<Rightarrow>bool"}] *})
 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:
 \begin{isabelle}
 \isacommand{thm}~@{thm [source] automatic_ind_prin_even}\\
 and the introduction rules @{text "rule_spec"}.
 *}
 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'
 val tyss = map (binder_types o fastype_of) preds
 val (namesattrs, rules) = split_list rule_specs
-val (defs, lthy') = defns rules preds prednames syns tyss lthy
+val (defs, lthy') = defns rules preds prednames mxs tyss lthy
-val ind_prin = inds rules defs preds 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*}
 text {*
 In Line 3 the function extracts the syntax annotations from the predicates.
 @{text [quotes] "_"}-separated list of predicate names (for example
 @{text "even_odd"}. Also by custom, the case names in intuction
 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
+Lines 18 and 19 now add to @{text "lthy'"} all the introduction rules
-under the name @{text "mut_name.intros"} (see previous paragraph).
+und induction principles under the name @{text "mut_name.intros"} and
-Line 19 add further every introduction rule under its own name
+@{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}
 indicates that the first premise of the induction principle (namely
 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(*>*)

changeset 237	0a8981f52045
parent 224	647cab4a72c2
child 239	b63c72776f03