isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:db8e302f44c8
+:d5accbc67e1b
 theory Ind_Code
 imports "../Base" "../FirstSteps" Ind_General_Scheme
 begin
-section {* The Gory Details *}
+section {* The Gory Details\label{sec:code} *}
+text {*
+As mentioned before the code falls roughly into three parts: the definitions,
+the induction principles and the introduction rules. In addition there is an
+administrative function that strings everything together.
+*}
 subsection {* Definitions *}
 text {*
 We first have to produce for each predicate the definition, whose general form is
 end *}
 text {*
 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
+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"}
 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 (the
+The first function, named @{text defn_aux}, constructs the term for one
-argument @{text "pred"} in the code belo). The number of arguments of this predicate is
+particular predicate (the argument @{text "pred"} in the code below). The
-determined by the number of argument types given in @{text "arg_tys"}.
+number of arguments of this predicate is determined by the number of
-The other arguments are all the @{text "preds"} and the @{text "orules"}.
+argument types given in @{text "arg_tys"}. The other arguments of the
+function are the @{text orules} and all the @{text "preds"}.
 *}
 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
 |> fold_rev mk_all preds
 |> fold_rev lambda fresh_args
 end*}
 text {*
-The function in Line 3 is just a helper function for constructing universal
+The function @{text mk_all} in Line 3 is just a helper function for constructing
-quantifications. The code in Lines 5 to 9 produces the fresh @{text
+universal quantifications. The code in Lines 5 to 9 produces the fresh @{text
 "zs"}. For this it pairs every argument type with the string
 @{text [quotes] "z"} (Line 7); then generates variants for all these strings
 so that they are unique w.r.t.~to the predicates and @{text "orules"} (Line 8);
 in Line 9 it generates the corresponding variable terms for the unique
 strings.
-The unique free variables are applied to the predicate (Line 11) using the
+The unique variables are applied to the predicate in 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
 predicate. A testcase for this function is
 *}
 local_setup %gray{* fn lthy =>
 let
-val pred = @{term "even::nat\<Rightarrow>bool"}
+val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
-val arg_tys = [@{typ "nat"}]
-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 defn_aux} for the predicate @{text "even"} and prints
+where we use the shorthands defined in Figure~\ref{fig:shorthands}.
+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
+If we try out the function with the rules for freshness
 *}
 local_setup %gray{* fn lthy =>
 (warning (Syntax.string_of_term lthy
 (defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys)));
 (\<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
+The second function, named @{text defns}, has to just 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 names of the predicates; @{text syns} are the
+"prednames"} is the list of binding names of the predicates; @{text syns}
-syntax annotations for each predicate; @{text "arg_tyss"} is
+are the list of syntax annotations for the predicates; @{text "arg_tyss"} is
-the list of argument-type-lists for each predicate.
+the list of argument-type-lists.
 *}
 ML %linenosgray{*fun defns rules preds prednames syns arg_typss lthy =
 let
 val thy = ProofContext.theory_of lthy
 in
 warning (str_of_thms_no_vars lthy' defs); lthy
 end *}
 text {*
-where we feed into the functions all parameters corresponding to
+where we feed into the function all parameters corresponding to
 the @{text even}-@{text odd} example. The definitions we obtain
 are:
 @{text [display, break]
 "even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))
 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}
 text {*
 This helper function instantiates the @{text "?x"} in the theorem
 @{thm spec} with a given @{ML_type cterm}. We call this helper function
-in the tactic:
+in the next tactic, called @{text inst_spec_tac}.
 *}
 ML{*fun inst_spec_tac ctrms =
 EVERY' (map (dtac o inst_spec) ctrms)*}
 text {*
-This tactic allows us to instantiate in the following proof the
+This tactic expects a list of @{ML_type cterm}s. It allows us in the following
-three quantifiers in the assumption.
+proof to instantiate the three quantifiers in the assumption.
 *}
 lemma
 fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
 shows "\<forall>x y z. P x y z \<Longrightarrow> True"
 @{subgoals}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-Now the complete tactic for proving the induction principles can
+The complete tactic for proving the induction principles can now
 be implemented as follows:
 *}
 ML %linenosgray{*fun ind_tac defs prem insts =
 EVERY1 [ObjectLogic.full_atomize_tac,
 assume_tac]*}
 text {*
 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
+instantiations. Compare this tactic with the manual proof 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:
 *}
 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 {*
-Let us have a closer look at the first proved theorem:
+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.  Therefore let us have a closer look at the first
+proved theorem:
 \begin{isabelle}
 \isacommand{thm}~@{thm [source] automatic_ind_prin_even}\\
 @{text "> "}~@{thm automatic_ind_prin_even}
 \end{isabelle}
 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
+variables are needed so that they can be instantiated by the user.
-on. We have to take care to also generate these schematic variables when
+We have to take care to also generate these schematic variables when
-generating the goals for the induction principles. While the tactic for
+generating the goals for the induction principles.  In general we have
-proving the induction principles is relatively simple, it will be a bit
+to construct for each predicate @{text "pred"} a goal of the form
-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"}
-where the predicates @{text preds} are replaced in the introduction
+where the predicates @{text preds} are replaced in @{text rules} by new
-rules by new distinct variables @{text "?Ps"}.
+distinct variables @{text "?Ps"}. We also need to generate fresh arguments
-We also need to generate fresh arguments @{text "?zs"} for the predicate
+@{text "?zs"} for the predicate  @{text "pred"} and the @{text "?P"} in
-@{text "pred"} and the @{text "?P"} in the conclusion. Note
+the conclusion. The crucial point is that the  @{text "?Ps"} and
-that the  @{text "?Ps"}  and @{text "?zs"} need to be
+@{text "?zs"} need to be schematic variables that can be instantiated
-schematic variables that can be instantiated by the user.
+by the user.
-We generate these goals in two steps. The first function expects that the
+We generate these goals in two steps. The first function, named @{text prove_ind},
-introduction rules are already appropriately substituted. The argument
+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 induction principle;
 @{text "newpred"} is its replacement and @{text "arg_tys"} are the argument
 types of this predicate.
 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 (see Line 4). By exporting this theorem from @{text
+"zs"} are free, but fixed (see Line 4). By exporting this theorem from @{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 newpreds = [@{term "P::nat\<Rightarrow>bool"}, @{term "Q::nat\<Rightarrow>bool"}]
 val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
+val newpred = @{term "P::nat\<Rightarrow>bool"}
 val srules =  map (subst_free (eo_preds ~~ newpreds)) eo_rules
-val newpred = @{term "P::nat\<Rightarrow>bool"}
 val intro =
 prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
 in
 warning (str_of_thm lthy intro); lthy
 end *}
 text {*
 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_ind} over all
-predicates. This is what the second function does:
+predicates. This is what the second function, named @{text inds} does.
 *}
 ML %linenosgray{*fun inds rules defs preds arg_tyss lthy  =
 let
 val Ps = replicate (length preds) "P"
 end*}
 text {*
 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
+@{text "Ps"} fresh and declaring them as free, but fixed, 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 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
 \end{isabelle}
 for freshness of applications. We set up the proof as follows:
 *}
-lemma fresh_App:
+lemma fresh_Lam:
 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
 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
+The first step of ``rulifying'' the lemma will turn out to be important
 later on. Applying this tactic
 *}
 (*<*)
-lemma fresh_App:
+lemma fresh_Lam:
 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 {*
 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
+with @{ML SUBPROOF} is, however, that this tactic always expects us to completely
-discharge with the goal (see Section ???). This is inconvenient for
+discharge the goal (see Section~\ref{sec:simpletacs}). This is inconvenient for
-our gradual explanation of the proof. To circumvent this inconvenience
+our gradual explanation of the proof here. 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.
+all necessary proof steps inside a subproof.
 *}
 text_raw {*
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 |> warning
 end*}
 text_raw{*
 \end{isabelle}
 \end{minipage}
-\caption{FIXME\label{fig:chopprint}}
+\caption{A helper function that prints out the parameters and premises that
+need to be treated differently.\label{fig:chopprint}}
 \end{figure}
 *}
 text {*
 First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
 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.
+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
+case only @{text "1"}) from the lenghts of all parameters. Similarly
-with the @{text "prems"}. The last premises in the goal state must
+with the @{text "prems"}: the last premises in the goal state come from
-come from unfolding of the conclusion. So we can just subtract
+unfolding the definition of the predicate in the conclusion. So we can
-the number of rules from the number of all premises. Applying
+just subtract the number of rules from the number of all premises.
-this tactic in our example
+Applying this tactic in our example
 *}
 (*<*)
-lemma fresh_App:
+lemma fresh_Lam:
 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(*>*)
 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
+quantifiers (with @{text params1}) and transform it into rule
-introduction rule (using @{ML "ObjectLogic.rulify"}.
+format (using @{ML "ObjectLogic.rulify"}. So we can modify the
-So we can modify the subproof as follows:
+subproof as follows:
 *}
 ML{*fun apply_prem_tac i preds rules =
 SUBPROOF_test (fn {params, prems, context, ...} =>
 let
 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
 THEN print_tac ""
 THEN no_tac
 end) *}
-text {* and apply it with *}
+text {*
+The argument @{text i} corresponds to the number of the
+introduction we want to analyse. We will later on lat it range
+from @{text 0} to the number of introduction rules.
+Below we applying this function with @{text 3}, since
+we are proving the fourth introduction rule.
+*}
 (*<*)
-lemma fresh_App:
+lemma fresh_Lam:
 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
+Since we print out the goal state just after the application of
-the goal state has the two subgoals
+@{ML rtac}, we can see the goal state we obtain: as expected it 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
+where the first comes from a non-recursive premise of the rule
-and the second comes from a recursive precondition. The first kind
+and the second comes from a recursive premise. The first goal
-can be solved immediately by @{text "prems1"}. The second kind
+can be solved immediately by @{text "prems1"}. The second
-needs more work. It can be solved with the other premise in @{text "prems1"},
+needs more work. It can be solved with the other premise
-namely
+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 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
+the topmost connective is an @{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
+of @{ML "expand_tac"} was the ``rulification'' of the lemma.
+The premise of the complicated case must have at least one  @{text "\<forall>"}
+coming from the quantification over the @{text preds}. So
 we can implement the following function
 *}
 ML{*fun prepare_prem params2 prems2 prem =
 rtac (case prop_of prem of
 prem |> all_elims params2
 |> imp_elims prems2
 | _ => prem) *}
 text {*
-which either applies the premise outright or if it had an
+which either applies the premise outright (the default case) or if
-outermost universial quantification, instantiates it first with
+it has an outermost universial quantification, instantiates it first
-@{text "params1"} and then @{text "prems1"}. The following tactic
+with  @{text "params1"} and then @{text "prems1"}. The following
-will therefore prove the lemma.
+tactic will therefore prove the lemma completely.
 *}
 ML{*fun prove_intro_tac i preds rules =
-SUBPROOF (fn {params, prems, context, ...} =>
+SUBPROOF (fn {params, prems, ...} =>
 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:
+The full proof of the introduction rule now as follows:
 *}
-(*<*)
+lemma fresh_Lam:
-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.
+Unfortunately, not everything is done yet. If you look closely
+at the general principle outlined in Section~\ref{sec:nutshell},
+we have  not yet dealt with the case when recursive premises
+in a rule have preconditions @{text Bs}. The introduction rule
+of the accessible part is such a rule.
 *}
 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 {*
+Here @{ML chop_test_tac} prints out the following
-@{subgoals [display]}
+values for @{text "params1/2"} and @{text "prems1/2"}
 \begin{isabelle}
 @{text "Params1 from the rule:"}\\
 @{text "x"}\\
 @{text "Params2 from the predicate:"}\\
 @{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}
-*}
+and after application of the introduction rule
-(*<*)oops(*>*)
+using @{ML apply_prem_tac}, we are in the goal state
+\begin{isabelle}
-ML{*fun prepare_prem params2 prems2 ctxt prem =
+@{text "1."}~@{term "\<And>y. R y x \<Longrightarrow> P y"}
+\end{isabelle}
+*}(*<*)oops(*>*)
+text {*
+In order to make progress as before, we have to use the precondition
+@{text "R y x"} (in general there can be many of them). The best way
+to get a handle on these preconditions is to open up another subproof,
+since the preconditions will be bound to @{text prems}. Therfore we
+modify the function @{ML prepare_prem} as follows
+*}
+ML %linenosgray{*fun prepare_prem params2 prems2 ctxt prem =
 SUBPROOF (fn {prems, ...} =>
 let
 val prem' = prems MRS prem
 in
 rtac (case prop_of prem' of
 prem' |> all_elims params2
 |> imp_elims prems2
 | _ => prem') 1
 end) ctxt *}
-ML{*fun prove_intro_tac i preds rules =
+text {*
+In Line 4 we use the @{text prems} from the @{ML SUBPROOF} and resolve
+them with @{text prem}. In the simple case, that is where the @{text prem}
+comes from a non-recursive premise of the rule, @{text prems} will be
+just the empty list and the @{ML MRS} does nothing. Similarly, in the
+cases where the recursive premises of the rule do not have preconditions.
+The function @{ML prove_intro_tac} only needs to give the context to
+@{ML prepare_prem} (Line 8) and is as follows.
+*}
+ML %linenosgray{*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) *}
+text {*
+With these extended function we can also prove the introduction
+rule for the accessible part.
+*}
 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 {*
+Finally we need two functions that string everything together. The first
-text {*
+function is the tactic that performs the proofs.
+*}
-*}
+ML %linenosgray{*fun intro_tac defs rules preds i ctxt =
-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}]),
 prove_intro_tac i preds rules ctxt]*}
 text {*
-A test case
+Lines 2 to 4 correspond to the function @{ML expand_tac}. Some testcases
-*}
+dor this tactic are:
+*}
-ML{*fun intros_tac_test ctxt i =
-intros_tac eo_defs eo_rules eo_preds i ctxt *}
+lemma even0_intro:
-lemma intro0:
 shows "even 0"
-apply(tactic {* intros_tac_test @{context} 0 *})
+by (tactic {* intro_tac eo_defs eo_rules eo_preds 0 @{context} *})
-done
-lemma intro1:
+lemma evenS_intro:
 shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
-apply(tactic {* intros_tac_test @{context} 1 *})
+by (tactic {* intro_tac eo_defs eo_rules eo_preds 1 @{context} *})
-done
+lemma fresh_App:
-lemma intro2:
+shows "\<And>a t s. \<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
-shows "\<And>m. even m \<Longrightarrow> odd (Suc m)"
+by (tactic {*
-apply(tactic {* intros_tac_test @{context} 2 *})
+intro_tac @{thms fresh_def} fresh_rules [fresh_pred] 1 @{context} *})
-done
+text {*
-ML{*fun intros rules preds defs lthy =
+The second function sets up in Line 4 the goals (in this case this is easy
+since they are exactly the introduction rules the user gives)
+and iterates @{ML intro_tac} over all introduction rules.
+*}
+ML %linenosgray{*fun intros rules preds defs lthy =
 let
-fun prove_intro (i, goal) =
+fun intros_aux (i, goal) =
 Goal.prove lthy [] [] goal
-(fn {context, ...} => intros_tac defs rules preds i context)
+(fn {context, ...} => intro_tac defs rules preds i context)
 in
-map_index prove_intro rules
+map_index intros_aux rules
 end*}
+subsection {* Main Function *}
 text {* main internal function *}
+ML {* LocalTheory.notes *}
 ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy =
 let
 val syns = map snd pred_specs
 val pred_specs' = map fst pred_specs
 text {*
 Things to include at the end:
 \begin{itemize}
+\item include the code for the parameters
 \item say something about add-inductive-i to return
 the rules
 \item say that the induction principle is weaker (weaker than
 what the standard inductive package generates)
 \item say that no conformity test is done

changeset 211	d5accbc67e1b
parent 210	db8e302f44c8
child 212	ac01ddb285f6