isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:d5accbc67e1b
+:ac01ddb285f6
 begin
 section {* The Gory Details\label{sec:code} *}
 text {*
-As mentioned before the code falls roughly into three parts: the definitions,
+As mentioned before the code falls roughly into three parts: code that deals
-the induction principles and the introduction rules. In addition there is an
+with the definitions, the induction principles and the introduction rules, respectively.
-administrative function that strings everything together.
+In addition there are some administrative functions that string everything together.
 *}
 subsection {* Definitions *}
 text {*
 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 next tactic, called @{text inst_spec_tac}.
+in the following tactic, called @{text inst_spec_tac}.
 *}
 ML{*fun inst_spec_tac ctrms =
 EVERY' (map (dtac o inst_spec) ctrms)*}
 text {*
-This tactic expects a list of @{ML_type cterm}s. It allows us in the following
+This tactic expects a list of @{ML_type cterm}s. It allows us in the
-proof to instantiate the three quantifiers in the assumption.
+proof below 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"
 apply (tactic {*
-inst_spec_tac  [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
+inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
 txt {*
 We obtain the goal state
 \begin{minipage}{\textwidth}
 @{subgoals}
 \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.
-We have to take care to also generate these schematic variables when
+It will take a bit of work to generate these schematic variables when
-generating the goals for the induction principles.  In general we have
+constructing the goals for the induction principles.  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 @{text 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. The crucial point is that the  @{text "?Ps"} and
+the conclusion. As just mentioned, the crucial point is that the
-@{text "?zs"} need to be schematic variables that can be instantiated
+@{text "?Ps"} and @{text "?zs"} need to be schematic variables that can
-by the user.
+be instantiated by the user.
 We generate these goals in two steps. The first function, named @{text prove_ind},
 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
 end *}
 text {*
 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'"}.
+\emph{free but fixed} variables in the local theory @{text "lthy'"}.
-That means they are not (yet) schematic variables.
+That means they are not schematic variables (yet).
 In 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 (substituted) introduction rules as premises. In case that
+and then add the (substituted) introduction rules as preconditions. In
-no introduction rules are given, the conclusion of this implication needs
+case that no introduction rules are given, the conclusion of this
-to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal
+implication needs to be wrapped inside a @{term Trueprop}, otherwise
-mechanism will fail.
+the Isabelle's goal mechanism will fail.\footnote{FIXME: check with
+Stefan...is this so?}
 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
 *}
 subsection {* Introduction Rules *}
 text {*
-The proofs of the introduction rules are quite a bit
+Constructing the goals for the introduction rules is easy: they
-more involved than the ones for the induction principles.
+are just the rules given by the user. However, their proofs are
-To ease somewhat our work here, we use the following two helper
+quite a bit more involved than the ones for the induction principles.
-functions.
+To explain the general method, our running example will be
+the introduction rule
+\begin{isabelle}
+@{prop "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
+\end{isabelle}
+about freshness for lambdas. In order to ease somewhat
+our work here, 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 these functions do, let us suppose whe have the following three
+To see what these functions do, let us suppose we have the following three
 theorems.
 *}
 lemma all_elims_test:
 fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
 @{ML_response_fake [display, gray]
 "warning (str_of_thm_no_vars @{context}
 (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
 "C"}
-To explain the proof for the introduction rule, our running example will be
+Now we set up the proof for the introduction rule as follows:
-the rule:
-\begin{isabelle}
-@{prop "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
-\end{isabelle}
-for freshness of applications. We set up the proof as follows:
 *}
 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
+The first step in the proof will be to expand the definitions of freshness
 and then introduce quantifiers and implications. For this we
 will use the tactic
 *}
-ML{*fun expand_tac defs =
+ML %linenosgray{*fun expand_tac defs =
 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 to be important
+The function in Line 2 ``rulifies'' the lemma. This will turn out to
-later on. Applying this tactic
+be important later on. Applying this tactic
 *}
 (*<*)
 lemma fresh_Lam:
 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 As you can see, there are parameters (namely @{text "a"}, @{text "b"}
 and @{text "t"}) which come from the introduction rule and parameters
 (in the case above only @{text "fresh"}) which come from the universal
 quantification in the definition @{term "fresh a (App t s)"}.
-Similarly, there are preconditions
+Similarly, there are assumptions
-that come from the premises of the rule and premises from the
+that come from the premises of the rule and assumptions from the
-definition. We need to treat these
+definition of the predicate. We need to treat these
-parameters and preconditions differently. In the code below
+parameters and assumptions differently. In the code below
 we will therefore separate them into @{text "params1"} and @{text params2},
 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
+with the parameters (as list of @{ML_type cterm}s) and the assumptions
-(as list of @{ML_type thm}s). The problem we have to overcome
+(as list of @{ML_type thm}s called @{text prems}). The problem we have
-with @{ML SUBPROOF} is, however, that this tactic always expects us to completely
+to overcome with @{ML SUBPROOF} is, however, that this tactic always
-discharge the goal (see Section~\ref{sec:simpletacs}). This is inconvenient for
+expects us to completely discharge the goal (see Section~\ref{sec:simpletacs}).
-our gradual explanation of the proof here. To circumvent this inconvenience
+This is inconvenient for our gradual explanation of the proof here. To
-we use the following modified tactic:
+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 inside a subproof.
+all necessary proof steps inside a subproof. Once we are finished, we
+just have to replace it with @{ML SUBPROOF}.
 *}
 text_raw {*
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \end{figure}
 *}
 text {*
 First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
-from @{text "params"} and @{text "prems"}, respectively. To see what is
+from @{text "params"} and @{text "prems"}, respectively. To better see what is
-going in our example, we will print out the values using the printing
+going in our example, we will print out these values using the printing
 function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will
 supply us the @{text "params"} and @{text "prems"} as lists, we can
 separate them using the function @{ML chop}.
 *}
 in
 chop_print params1 params2 prems1 prems2 context; no_tac
 end) *}
 text {*
-For the separation we can rely on that Isabelle deterministically
+For the separation we can rely on the fact that Isabelle deterministically
-produces parameter and premises in a goal state. The last parameters
+produces parameters 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
+(see the tactic @{ML expand_tac}).
 Therefore we only have to subtract the number of predicates (in this
 case only @{text "1"}) from the lenghts of all parameters. Similarly
 with the @{text "prems"}: the last premises in the goal state come from
 unfolding the definition of the predicate in the conclusion. So we can
 just subtract the number of rules from the number of all premises.
 We now have to select from @{text prems2} the premise
 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)"}
+@{term [display] "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam a t)"}
 To use this premise with @{ML rtac}, we need to instantiate its
 quantifiers (with @{text params1}) and transform it into rule
 format (using @{ML "ObjectLogic.rulify"}. So we can modify the
 subproof as follows:
 *}
-ML{*fun apply_prem_tac i preds rules =
+ML %linenosgray{*fun apply_prem_tac i preds rules =
 SUBPROOF_test (fn {params, prems, context, ...} =>
 let
 val (params1, params2) = chop (length params - length preds) params
 val (prems1, prems2) = chop (length prems - length rules) prems
 in
 THEN no_tac
 end) *}
 text {*
 The argument @{text i} corresponds to the number of the
-introduction we want to analyse. We will later on lat it range
+introduction we want to prove. We will later on lat it range
-from @{text 0} to the number of introduction rules.
+from @{text 0} to the number of @{text "rules - 1"}.
-Below we applying this function with @{text 3}, since
+Below we apply this function with @{text 3}, since
 we are proving the fourth introduction rule.
 *}
 (*<*)
 lemma fresh_Lam:
 apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} *})
 (*<*)oops(*>*)
 text {*
 Since we print out the goal state just after the application of
-@{ML rtac}, we can see the goal state we obtain: as expected it has
+@{ML rtac} (Line 8), we can see the goal state we obtain:
-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 premise of the rule
+As expected there are two subgoals, where the first comes from a
-and the second comes from a recursive premise. The first goal
+non-recursive premise of the introduction rule and the second comes
-can be solved immediately by @{text "prems1"}. The second
+from a recursive premise. The first goal can be solved immediately
-needs more work. It can be solved with the other premise
+by @{text "prems1"}. The second needs more work. It can be solved
-in @{text "prems1"}, namely
+with the other premise 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>
 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 an @{text "\<forall>"}. The premises in the simple
-case cannot have such a quantification, since in the first step
+case cannot have such a quantification, since the first step
-of @{ML "expand_tac"} was the ``rulification'' of the lemma.
+of @{ML "expand_tac"} was to ``rulify'' 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
 *}
 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
 THEN EVERY1 (map (prepare_prem params2 prems2) prems1)
 end) *}
 text {*
+Note that the tactic is now @{ML SUBPROOF}, not @{ML SUBPROOF_test}.
 The full proof of the introduction rule now as follows:
 *}
 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 {* prove_intro_tac 3 [fresh_pred] fresh_rules @{context} 1 *})
 done
 text {*
-Unfortunately, not everything is done yet. If you look closely
+Phew!  Unfortunately, not everything is done yet. If you look closely
-at the general principle outlined in Section~\ref{sec:nutshell},
+at the general principle outlined for the introduction rules in
-we have  not yet dealt with the case when recursive premises
+Section~\ref{sec:nutshell}, we have  not yet dealt with the case where
-in a rule have preconditions @{text Bs}. The introduction rule
+recursive premises have preconditions. 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"
 *}(*<*)oops(*>*)
 text {*
-In order to make progress as before, we have to use the precondition
+In order to make progress, 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
+since the preconditions will then 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, ...} =>
 | _ => prem') 1
 end) ctxt *}
 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}
+them with @{text prem}. In the simple cases, 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
+just the empty list and the function @{ML MRS} does nothing. Similarly, in the
 cases where the recursive premises of the rule do not have preconditions.
+In case there are preconditions, then Line 4 discharges them. After
+that we can proceed as before, i.e., check whether the outermost
+connective is @{text "\<forall>"}.
-The function @{ML prove_intro_tac} only needs to give the context to
+The function @{ML prove_intro_tac} only needs to be changed so that it
-@{ML prepare_prem} (Line 8) and is as follows.
+gives the context to @{ML prepare_prem} (Line 8). The modified version
+is below.
 *}
 ML %linenosgray{*fun prove_intro_tac i preds rules =
 SUBPROOF (fn {params, prems, context, ...} =>
 let
 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
+With these two functions we can now 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"
 REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
 prove_intro_tac i preds rules ctxt]*}
 text {*
 Lines 2 to 4 correspond to the function @{ML expand_tac}. Some testcases
-dor this tactic are:
+for this tactic are:
 *}
 lemma even0_intro:
 shows "even 0"
 by (tactic {* intro_tac eo_defs eo_rules eo_preds 0 @{context} *})
 lemma evenS_intro:
 shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
 by (tactic {* intro_tac eo_defs eo_rules eo_preds 1 @{context} *})
 shows "\<And>a t s. \<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
 by (tactic {*
 intro_tac @{thms fresh_def} fresh_rules [fresh_pred] 1 @{context} *})
 text {*
-The second function sets up in Line 4 the goals (in this case this is easy
+The second function sets up in Line 4 the goals (this is easy
-since they are exactly the introduction rules the user gives)
+for the introduction rules since they are exactly the rules
-and iterates @{ML intro_tac} over all introduction rules.
+given by the user) and iterates @{ML intro_tac} over all
+introduction rules.
 *}
 ML %linenosgray{*fun intros rules preds defs lthy =
 let
 fun intros_aux (i, goal) =
 Goal.prove lthy [] [] goal
 (fn {context, ...} => intro_tac defs rules preds i context)
 in
 map_index intros_aux rules
 end*}
+text {*
+The iteration is done with the function @{ML map_index} since we
+need the introduction rule together with its number (counted from
+@{text 0}). This completes the code for the functions deriving the
+reasoning infrastructure. It remains to implement some administrative
+code that strings everything together.
+*}
 subsection {* Main Function *}
 text {* main internal function *}

changeset 212	ac01ddb285f6
parent 211	d5accbc67e1b
child 215	8d1a344a621e