isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:ee9d53fbb56b
+:24c68350d059
 end*}
 text {*
 It returns the definition (as a theorem) and the local theory in which the
 definition has been made. In Line 4, @{ML [index] internalK in Thm} is a flag
-attached to the theorem (others possibile flags are @{ML [index] definitionK in Thm}
+attached to the theorem (other possibile flags are @{ML [index] definitionK in Thm}
 and @{ML [index] 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 [index] 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
 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 =>
+local_setup %gray {* fn lthy =>
 let
 val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)
 in
 writeln (Syntax.string_of_term lthy def); lthy
 end *}
 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"}
 If we try out the function with the rules for freshness
 *}
-local_setup %gray{* fn lthy =>
+local_setup %gray {* fn lthy =>
-(writeln (Syntax.string_of_term lthy
+let
-(defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys)));
+val def = defn_aux lthy fresh_orules
-lthy) *}
+[fresh_pred] (fresh_pred, fresh_arg_tys)
+in
+writeln (Syntax.string_of_term lthy def); lthy
+end *}
 text {*
 we obtain
 @{term [display]
 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-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
+behind the local theory using the function @{ML [index] theory_of in ProofContext}
+(Line 3); with this theory we can use the function
 @{ML [index] atomize_term in ObjectLogic} 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 (the theorems are
 registered with the local theory). A testcase for this function is
 writeln (string_of_thms_no_vars lthy' defs); lthy
 end *}
 text {*
 where we feed into the function all parameters corresponding to
-the @{text even}-@{text odd} example. The definitions we obtain
+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))
 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,
 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}
 Note that in the testcase we return the local theory @{text lthy}
 (not the modified @{text lthy'}). As a result the test case has no effect
 on the ambient theory. The reason is that if we introduce the
-definition again, we pollute the name space with two versions of @{text "even"}
+definition again, we pollute the name space with two versions of
-and @{text "odd"}.
+@{text "even"} and @{text "odd"}. We want to avoid this here.
 This completes the code for introducing the definitions. Next we deal with
 the induction principles.
 *}
 The tactic will use the following helper function for instantiating universal
 quantifiers.
 *}
 ML{*fun inst_spec ctrm =
 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 following tactic, called @{text inst_spec_tac}\label{fun:instspectac}.
+in the following tactic.\label{fun:instspectac}.
 *}
 ML{*fun inst_spec_tac ctrms =
 EVERY' (map (dtac o inst_spec) ctrms)*}
 assume_tac]*}
 text {*
 We have to give it as arguments the definitions, the premise (a list of
 formulae) and the instantiations. The premise is @{text "even n"} in lemma
-@{thm [source] manual_ind_prin_even}; in our code it will always be a list
+@{thm [source] manual_ind_prin_even} shown above; in our code it will always be a list
 consisting of a single formula. 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:
+the @{ML ind_tac}. We first rewrite the goal to use only object connectives (Line 2),
+"cut in" the premise (Line 3), unfold the definitions (Line 4), instantiate
+the assumptions of the goal (Line 5) and then conclude with @{ML assume_tac}.
+Two testcases for this tactic are:
 *}
 lemma automatic_ind_prin_even:
 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"
 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.\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
+In Line 11 we set up the goal to be proved using the function @{ML [index]
-tactic for proving the induction principle. As mentioned before, this tactic
+prove in Goal}; in the next line we call the tactic for proving the
-expects the definitions, the premise and the (certified) predicates with
+induction principle. As mentioned before, this tactic expects the
-which the introduction rules have been substituted. The code in these two
+definitions, the premise and the (certified) predicates with which the
-lines will return a theorem. However, it is a theorem
+introduction rules have been substituted. The code in these two lines will
-proved inside the local theory @{text "lthy'"}, where the variables @{text
+return a theorem. However, it is a theorem proved inside the local theory
-"zs"} are free, but fixed (see Line 4). By exporting this theorem from @{text
+@{text "lthy'"}, where the variables @{text "zs"} are free, but fixed (see
-"lthy'"} (which contains the @{text "zs"} as free variables) to @{text
+Line 4). By exporting this theorem from @{text "lthy'"} (which contains the
-"lthy"} (which does not), we obtain the desired schematic variables @{text "?zs"}.
+@{text "zs"} as free variables) to @{text "lthy"} (which does not), we
-A testcase for this function is
+obtain the desired schematic variables @{text "?zs"}.  A testcase for this
-*}
+function is
+*}
-local_setup %gray{* fn lthy =>
+local_setup %gray {* fn lthy =>
 let
-val newpreds = [@{term "P::nat\<Rightarrow>bool"}, @{term "Q::nat\<Rightarrow>bool"}]
+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 cnewpreds = [@{cterm "P::nat \<Rightarrow> bool"}, @{cterm "Q::nat \<Rightarrow> bool"}]
-val newpred = @{term "P::nat\<Rightarrow>bool"}
+val newpred = @{term "P::nat \<Rightarrow> bool"}
 val srules =  map (subst_free (eo_preds ~~ newpreds)) eo_rules
 val intro =
 prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)
 in
 writeln (string_of_thm lthy intro); lthy
 Similarly, the function @{ML imp_elims} eliminates preconditions from implications.
 For example we can eliminate the preconditions @{text "A"} and @{text "B"} from
 @{thm [source] imp_elims_test}:
 @{ML_response_fake [display, gray]
-"writeln (string_of_thm_no_vars @{context}
+"let
-(imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
+val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
+in
+writeln (string_of_thm_no_vars @{context} res)
+end"
 "C"}
 Now we set up the proof for the introduction rule as follows:
 *}
 ObjectLogic.rulify_tac 1
 THEN rewrite_goals_tac defs
 THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
 text {*
-The function in Line 2 ``rulifies'' the lemma. This will turn out to
+The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better}
+This will turn out to
 be important later on. Applying this tactic in our proof of @{text "fresh_Lem"}
 *}
 (*<*)
 lemma fresh_Lam:
 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 [index] SUBPROOF}, since this tactic provides us 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 with @{ML SUBPROOF}
+The problem with @{ML SUBPROOF}, however, is that it always expects us to
-is, however, that this tactic always expects us to completely discharge the
+completely discharge the goal (see Section~\ref{sec:simpletacs}). This is
-goal (see Section~\ref{sec:simpletacs}). This is inconvenient for our
+a bit inconvenient for our gradual explanation of the proof here. Therefore
-gradual explanation of the proof here. To circumvent this inconvenience we
+we use first the function @{ML [index] FOCUS}, which does same as @{ML SUBPROOF}
-use the following modified tactic:
+but does not require us to completely discharge the goal.
 *}
 (*<*)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. Once we are finished, we
-just have to replace it with @{ML SUBPROOF}.
-*}
 text_raw {*
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
 @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1)
 @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2)
 in
 s |> separate "\n"
 |> implode
-|> writeln
+|> tracing
 end*}
 text_raw{*
 \end{isabelle}
 \end{minipage}
 \caption{A helper function that prints out the parameters and premises that
 text {*
 First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
 from @{text "params"} and @{text "prems"}, respectively. To better see what is
 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
+function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS} will
 supply us the @{text "params"} and @{text "prems"} as lists, we can
 separate them using the function @{ML [index] chop}.
 *}
-ML{*fun chop_test_tac preds rules =
+ML %linenosgray{*fun chop_test_tac preds rules =
-SUBPROOF_test (fn {params, prems, context, ...} =>
+FOCUS (fn {params, prems, context, ...} =>
 let
-val (params1, params2) = chop (length params - length preds) (map snd params)
+val cparams = map snd params
+val (params1, params2) = chop (length cparams - length preds) cparams
 val (prems1, prems2) = chop (length prems - length rules) prems
 in
-chop_print params1 params2 prems1 prems2 context; no_tac
+chop_print params1 params2 prems1 prems2 context; all_tac
 end) *}
 text {*
 For the separation we can rely on the fact that Isabelle deterministically
 produces parameters and premises in a goal state. The last parameters
 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
+Therefore we only have to subtract in Line 5 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
+with the @{text "prems"} in line 6: 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.
-Applying this tactic in our example
+To check our calculations we print them out in Line 8 using the
+function @{ML chop_print} from Figure~\ref{fig:chopprint} and then
+just do nothing, that is @{ML all_tac}. Applying this tactic in our example
 *}
 (*<*)
 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} *})
+apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} 1 *})
 (*<*)oops(*>*)
 text {*
 gives
 @{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 [index] rulify in ObjectLogic}. So we can modify the
+format (using @{ML [index] rulify in ObjectLogic}). So we can modify the
-subproof as follows:
+code as follows:
 *}
 ML %linenosgray{*fun apply_prem_tac i preds rules =
-SUBPROOF_test (fn {params, prems, context, ...} =>
+FOCUS (fn {params, prems, context, ...} =>
 let
-val (params1, params2) = chop (length params - length preds) (map snd params)
+val cparams = map snd params
+val (params1, params2) = chop (length cparams - length preds) cparams
 val (prems1, prems2) = chop (length prems - length rules) prems
 in
 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
-THEN print_tac ""
-THEN no_tac
 end) *}
 text {*
 The argument @{text i} corresponds to the number of the
 introduction we want to prove. We will later on let it range
 (*<*)
 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} *})
+apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} 1 *})
 (*<*)oops(*>*)
 text {*
-Since we print out the goal state just after the application of
+The goal state we obtain is:
-@{ML rtac} (Line 8), we can see the goal state we obtain:
 \begin{isabelle}
-@{text "1."}~@{prop "a \<noteq> b"}\\
+@{text "1."}~@{text "\<dots> \<Longrightarrow> "}~@{prop "a \<noteq> b"}\\
-@{text "2."}~@{prop "fresh a t"}
+@{text "2."}~@{text "\<dots> \<Longrightarrow> "}~@{prop "fresh a t"}
 \end{isabelle}
 As expected there are two subgoals, where the first comes from the
 non-recursive premise of the introduction rule and the second comes
 from the recursive one. The first goal can be solved immediately
 *}
 ML{*fun prove_intro_tac i preds rules =
 SUBPROOF (fn {params, prems, ...} =>
 let
-val (params1, params2) = chop (length params - length preds) (map snd params)
+val cparams = map snd params
+val (params1, params2) = chop (length cparams - length preds) cparams
 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 {*
-Note that the tactic is now @{ML SUBPROOF}, not @{ML SUBPROOF_test}.
+Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS} anymore.
 The full proof of the introduction rule is 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 {*
-Phew!  ...Unfortunately, not everything is done yet. If you look closely
+Phew!\ldots
+Unfortunately, not everything is done yet. If you look closely
 at the general principle outlined for the introduction rules in
 Section~\ref{sec:nutshell}, we have  not yet dealt with the case where
 recursive premises have preconditions. The introduction rule
 of the accessible part is such a rule.
 *}
 lemma accpartI:
 shows "\<And>R 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 {* chop_test_tac [acc_pred] acc_rules @{context} 1 *})
-apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *})
+apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} 1 *})
 txt {*
 Here @{ML chop_test_tac} prints out the following
 values for @{text "params1/2"} and @{text "prems1/2"}
 *}
 ML %linenosgray{*fun prove_intro_tac i preds rules =
 SUBPROOF (fn {params, prems, context, ...} =>
 let
-val (params1, params2) = chop (length params - length preds) (map snd params)
+val cparams = map snd params
+val (params1, params2) = chop (length cparams - length preds) cparams
 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) *}
 For convenience, we use the following
 three wrappers this function:
 *}
-ML{*fun reg_many qname ((name, attrs), thms) =
+ML{*fun note_many qname ((name, attrs), thms) =
 LocalTheory.note Thm.theoremK
 ((Binding.qualify false qname name, attrs), thms)
-fun reg_single1 qname ((name, attrs), thm) =
+fun note_single1 qname ((name, attrs), thm) =
-reg_many qname ((name, attrs), [thm])
+note_many qname ((name, attrs), [thm])
-fun reg_single2 name attrs (qname, thm) =
+fun note_single2 name attrs (qname, thm) =
-reg_many (Binding.name_of qname) ((name, attrs), [thm]) *}
+note_many (Binding.name_of qname) ((name, attrs), [thm]) *}
 text {*
 The function that ``holds everything together'' is @{text "add_inductive"}.
 Its arguments are the specification of the predicates @{text "pred_specs"}
 and the introduction rules @{text "rule_spec"}.
 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)
+lthy' |> note_many mut_name ((@{binding "intros"}, []), intro_rules)
-||>> reg_many mut_name ((@{binding "inducts"}, []), ind_prins)
+||>> note_many mut_name ((@{binding "inducts"}, []), ind_prins)
-||>> fold_map (reg_single1 mut_name) (namesattrs ~~ intro_rules)
+||>> fold_map (note_single1 mut_name) (namesattrs ~~ intro_rules)
-||>> fold_map (reg_single2 @{binding "induct"}
+||>> fold_map (note_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_prins)
 |> snd

changeset 295	24c68350d059
parent 294	ee9d53fbb56b
child 299	d0b81d6e1b28