isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:d3cd633e8240
+:0634d42bb69f
 fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" ("_ \<sharp> _" [100,100] 100)
 where
 "a\<noteq>b \<Longrightarrow> a\<sharp>Var b"
 | "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
 | "a\<sharp>Lam a t"
 | "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b t"
 section {* Code *}
 text {*
 So we apply the $i$th @{text "orule"}, but we have to show the @{text "As"} (by assumption)
 and all @{text "(\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>*"}. For the latter we use the assumptions
 @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"} and @{text "orules"}.
-*}
+\begin{center}
+****************************
-text {*
+\end{center}
-First we have to produce for each predicate the definition of the form
+*}
+text {*
+For building testcases let us give some shorthands for the definitions of @{text "even/odd"} and
+@{text "fresh"}. (FIXME put in a figure)
+*}
+ML{*val eo_defs = [@{thm even_def}, @{thm odd_def}]
+val eo_rules =
+[@{prop "even 0"},
+@{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"},
+@{prop "\<And>n. even n \<Longrightarrow> odd (Suc n)"}]
+val eo_orules =
+[@{prop "even 0"},
+@{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"},
+@{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}]
+val eo_preds =  [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+val eo_prednames = [@{binding "even"}, @{binding "odd"}]
+val eo_syns = [NoSyn, NoSyn]
+val eo_arg_tyss = [[@{typ "nat"}],[@{typ "nat"}]] *}
+ML{*val fresh_defs = [@{thm fresh_def}]
+val fresh_rules =
+[@{prop "\<And>a b. a\<noteq>b \<Longrightarrow> a\<sharp>Var b"},
+@{prop "\<And>a s t. a\<sharp>t \<Longrightarrow> a\<sharp>s \<Longrightarrow> a\<sharp>App t s"},
+@{prop "\<And>a t. a\<sharp>Lam a t"},
+@{prop "\<And>a b t. a\<noteq>b \<Longrightarrow> a\<sharp>t \<Longrightarrow> a\<sharp>Lam b t"}]
+val fresh_orules =
+[@{prop "\<forall>a b. a\<noteq>b \<longrightarrow> a\<sharp>Var b"},
+@{prop "\<forall>a s t. a\<sharp>t \<longrightarrow> a\<sharp>s \<longrightarrow> a\<sharp>App t s"},
+@{prop "\<forall>a t. a\<sharp>Lam a t"},
+@{prop "\<forall>a b t. a\<noteq>b \<longrightarrow> a\<sharp>t \<longrightarrow> a\<sharp>Lam b t"}]
+val fresh_preds =  [@{term "fresh::string\<Rightarrow>trm\<Rightarrow>bool"}] *}
+subsection {* Definitions *}
+text {*
+First we have to produce for each predicate the definition, whose general form is
 @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
-and then ``register'' the definitions with Isabelle.
+and then ``register'' the definition inside a local theory.
 To do the latter, we use the following wrapper for
 @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
 annotation and a term representing the right-hand side of the definition.
 *}
 warning (str_of_thm_no_vars lthy' def); lthy'
 end *}
 text {*
 which makes the definition @{prop "MyTrue \<equiv> True"} and then prints it out.
-Since we are testing the function inside \isacommand{local\_setup}, i.e.~make
+Since we are testing the function inside \isacommand{local\_setup}, i.e., make
-changes to the ambient theory, we can query the definition using the usual
+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"}
 \end{isabelle}
-The next two functions construct the right-hand sides of the definitions, which
+The next two functions construct the right-hand sides of the definitions,
-are of the form
+which are terms of the form
 @{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
-The variables @{text "zs"} need to be chosen so that they do not occur
+When constructing them, the variables @{text "zs"} need to be chosen so that
-in the @{text orules} and also be distinct from the @{text "preds"}.
+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, say
-@{text "pred"}; the number of arguments of this predicate is
+@{text "pred"}. The number of arguments of this predicate is
 determined by the number of argument types given in @{text "arg_tys"}.
-The other arguments are all @{text "preds"} and the @{text "orules"}.
+The other arguments are all the @{text "preds"} and the @{text "orules"}.
 *}
 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =
 let
 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
 strings.
 The unique free variables are applied to the predicate (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
+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 orules = [@{prop "even 0"},
-@{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},
-@{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}]
-val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
 val pred = @{term "even::nat\<Rightarrow>bool"}
 val arg_tys = [@{typ "nat"}]
-val def = defs_aux lthy orules preds (pred, arg_tys)
+val def = defs_aux lthy eo_orules eo_preds (pred, arg_tys)
 in
 warning (Syntax.string_of_term lthy def); lthy
 end *}
 text {*
-It calls @{ML defs_aux} for the definition of @{text "even"} and prints
+The testcase  calls @{ML defs_aux} for the predicate @{text "even"} and prints
-out the definition. So we obtain as printout
+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"}
 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 defs_aux} in Line 5 produces all left-hand sides of the
+to @{ML defs_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
 *}
 local_setup %gray {* fn lthy =>
 let
-val rules = [@{prop "even 0"},
+val (defs, lthy') =
-@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+definitions eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy
-@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
+in
-val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+warning (str_of_thms_no_vars lthy' defs); lthy
-val prednames = [@{binding "even"}, @{binding "odd"}]
-val syns = [NoSyn, NoSyn]
-val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
-val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
-in
-warning (str_of_thms_no_vars lthy' defs); lthy'
 end *}
 text {*
 where we feed into the functions all parameters corresponding to
 the @{text even}-@{text odd} example. The definitions we obtain
 are:
 \begin{isabelle}
-\isacommand{thm}~@{text "even_def odd_def"}\\
 @{text [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,
 > odd \<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> odd z"}
 \end{isabelle}
+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 make again the
+definition, we pollute the name space with two versions of @{text "even"}
+and @{text "odd"}.
 This completes the code for making the definitions. Next we deal with
-the induction principles. Recall that the proof of the induction principle
+the induction principles.
+*}
+subsection {* Introduction Rules *}
+text {*
+Recall that the proof of the induction principle
 for @{text "even"} was:
 *}
-lemma man_ind_principle:
+lemma manual_ind_prin:
-assumes prems: "even n"
+assumes prem: "even n"
 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
 apply(atomize (full))
 apply(cut_tac prems)
 apply(unfold even_def)
 apply(drule spec[where x=P])
 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}. Together with the tactic
+@{thm spec} with a given @{ML_type cterm}. We call this helper function
+in the tactic:
 *}
 ML{*fun inst_spec_tac ctrms =
 EVERY' (map (dtac o inst_spec) ctrms)*}
 text {*
-we can use @{ML inst_spec_tac} in the following proof to instantiate the
+This tactic allows us to instantiate in the following proof the
 three quantifiers in the assumption.
 *}
 lemma
 fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
 text {*
 Now the complete tactic for proving the induction principles can
 be implemented as follows:
 *}
-ML %linenosgray{*fun induction_tac defs prems insts =
+ML %linenosgray{*fun induction_tac defs prem insts =
 EVERY1 [ObjectLogic.full_atomize_tac,
-cut_facts_tac prems,
+cut_facts_tac prem,
 K (rewrite_goals_tac defs),
 inst_spec_tac insts,
 assume_tac]*}
 text {*
-We only have to give it the definitions, the premise (like @{text "even n"})
+We have to give it as arguments the definitions, the premise
-and the instantiations as arguments. Compare this with the manual proof
+(for example @{text "even n"}) and the instantiations. Compare this with the
-given for the lemma @{thm [source] man_ind_principle}: there is almos a
+manual proof given for the lemma @{thm [source] manual_ind_prin}:
-one-to-one correspondence between the \isacommand{apply}-script and the
+as you can see there is almost a one-to-one correspondence between the \isacommand{apply}-script
-@{ML induction_tac}. A testcase for this tactic is the function
+and the @{ML induction_tac}. A testcase for this tactic is the function
 *}
-ML{*fun test_tac prems =
+ML{*fun test_tac prem =
 let
-val defs = [@{thm even_def}, @{thm odd_def}]
 val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
 in
-induction_tac defs prems insts
+induction_tac eo_defs prem insts
 end*}
 text {*
 which indeed proves the induction principle:
 *}
-lemma auto_ind_principle:
+lemma automatic_ind_prin:
-assumes prems: "even n"
+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 n"
+shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"
-apply(tactic {* test_tac @{thms prems} *})
+apply(tactic {* test_tac @{thms prem} *})
 done
 text {*
 While the tactic for the induction principle is relatively simple,
 it is a bit harder 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"}
+"pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}
 where the predicates @{text preds} are replaced in the introduction
-rules by new distinct variables written @{text "Ps"}.
+rules by new distinct variables @{text "?Ps"}.
-We also need to generate fresh arguments for the predicate @{text "pred"} in
+We also need to generate fresh arguments @{text "?zs"} for the predicate
-the premise and the @{text "?P"} in the conclusion. Note
+@{text "pred"} and the @{text "?P"} in the conclusion. Note
 that the  @{text "?Ps"}  and @{text "?zs"} need to be
-schematic variables that can be instantiated. This corresponds to what the
+schematic variables that can be instantiated by the user.
-@{thm [source] auto_ind_principle} looks like:
+We generate these goals in two steps. The first function expects that the
-\begin{isabelle}
+introduction rules are already appropriately substituted. The argument
-\isacommand{thm}~@{thm [source] auto_ind_principle}\\
+@{text "srules"} stands for these substituted rules; @{text cnewpreds} are
-@{text "> \<lbrakk>even ?n; ?P 0; \<And>m. ?Q m \<Longrightarrow> ?P (Suc m); \<And>m. ?P m \<Longrightarrow> ?Q (Suc m)\<rbrakk> \<Longrightarrow> ?P ?n"}
+the certified terms coresponding to the variables @{text "?Ps"}; @{text
-\end{isabelle}
+"pred"} is the predicate for which we prove the introduction principle;
+@{text "newpred"} is its replacement and @{text "arg_tys"} are the argument
-We achieve
+types of this predicate.
-that in two steps.
+*}
-The function below expects that the introduction rules are already appropriately
+ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys) =
-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 introduction principle; @{text "newpred"} is its
-replacement and @{text "tys"} are the argument types of this predicate.
-*}
-ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys)  =
 let
 val zs = replicate (length arg_tys) "z"
 val (newargnames, lthy') = Variable.variant_fixes zs lthy;
 val newargs = map Free (newargnames ~~ arg_tys)
 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'"}. In
-Line 5 we just construct the terms corresponding to these variables.
+Line 5 we construct the terms corresponding to these variables.
-The term variables are applied to the predicate in Line 7 (this corresponds
+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 (substituded) introduction rules as premises. In 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.
-In Line 11 we set up the goal to be proved; in the next line we call the tactic
+In Line 11 we set up the goal to be proved; in the next line we call the
-for proving the induction principle. This tactic expects the definitions, the
+tactic for proving the induction principle. As mentioned before, this tactic
-premise and the (certified) predicates with which the introduction rules
+expects the definitions, the premise and the (certified) predicates with
-have been substituted. The code in these two lines will return a theorem.
+which the introduction rules have been substituted. The code in these two
-However, it is a theorem
+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. By exporting this theorem from @{text
 "lthy'"} (which contains the @{text "zs"} as free) to @{text
-"lthy"} (which does not), we obtain the desired schematic variables.
+"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 defs = [@{thm even_def}, @{thm odd_def}]
 val srules = [@{prop "P (0::nat)"},
 @{prop "\<And>n::nat. Q n \<Longrightarrow> P (Suc n)"},
 @{prop "\<And>n::nat. P n \<Longrightarrow> Q (Suc n)"}]
 val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
 val pred = @{term "even::nat\<Rightarrow>bool"}
 val newpred = @{term "P::nat\<Rightarrow>bool"}
 val arg_tys = [@{typ "nat"}]
 val intro =
-prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys)
+prove_induction lthy eo_defs srules cnewpreds ((pred, newpred), arg_tys)
 in
 warning (str_of_thm lthy intro); lthy
 end *}
 text {*
 @{text [display]
 " \<lbrakk>even ?z; P 0; \<And>n. Q n \<Longrightarrow> P (Suc n); \<And>n. P n \<Longrightarrow> Q (Suc n)\<rbrakk> \<Longrightarrow> P ?z"}
 Note that the export from @{text lthy'} to @{text lthy} in Line 13 above
 has turned the free, but fixed, @{text "z"} into a schematic
-variable @{text "?z"}.
+variable @{text "?z"}. The @{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_induction} over all
-predicates. This is what the next function does.
+predicates. This is what the second function does:
 *}
 ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy  =
 let
 val Ps = replicate (length preds) "P"
 (preds ~~ newpreds ~~ arg_tyss)
 |> ProofContext.export lthy' lthy
 end*}
 text {*
-In Line 3 we generate a string @{text [quotes] "P"} for each predicate.
+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
 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 calculate the types of these new predicates
+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
 (Line 11) using the function @{ML subst_free}. Line 14 and 15 just iterate
 the proofs for all predicates.
 From this we obtain a list of theorems. Finally we need to export the
-fixed variables @{text "Ps"} to obtain the schematic variables
+fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"}
 (Line 16).
 A testcase for this function is
 *}
 local_setup %gray {* fn lthy =>
 let
-val rules = [@{prop "even (0::nat)"},
+val ind_thms = inductions eo_rules eo_defs eo_preds eo_arg_tyss lthy
-@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
-@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
-val defs = [@{thm even_def}, @{thm odd_def}]
-val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
-val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
-val ind_thms = inductions rules defs preds tyss lthy
 in
 warning (str_of_thms lthy ind_thms); lthy
 end *}
 "> even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>
 > (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,
 > odd ?z \<Longrightarrow> ?P1 0
 > \<Longrightarrow> (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}
+Note that now both, the @{text "?Ps"} and the @{text "?zs"}, are schematic
-Note that now both, the @{text "Ps"} and the @{text "zs"}, are schematic
 variables. The numbers have been introduced by the pretty-printer and are
 not significant.
-This completes the code for the induction principles.  Finally we can prove the
+This completes the code for the induction principles.
-introduction rules. Their proofs are quite a bit more involved. To ease them
+*}
-somewhat we  use the following two helper function.
+subsection {* Introduction Rules *}
+text {*
+Finally we can prove the introduction rules. Their proofs are quite a bit
+more involved. To ease these proofs somewhat 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 they do, let us suppose whe have the follwoing three
+To see what these functions do, let us suppose whe have the following three
 theorems.
 *}
 lemma all_elims_test:
 fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
 warning (str_of_thm_no_vars @{context} new_thm)
 end"
 "P a b c"}
 Similarly, the function @{ML imp_elims} eliminates preconditions from implications.
-For example
+For example:
 @{ML_response_fake [display, gray]
 "warning (str_of_thm_no_vars @{context}
 (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
 "C"}
 ML {* prems_of *}
 ML {* Logic.strip_params *}
 ML {* Logic.strip_assums_hyp *}
 ML {*
-fun chop_print_tac m n ctxt thm =
+fun chop_print (params1, params2) (prems1, prems2) ctxt =
 let
-val [trm] = prems_of thm
-val params = map fst (Logic.strip_params trm)
-val prems  = Logic.strip_assums_hyp trm
-val (prems1, prems2) = chop (length prems - m) prems;
-val (params1, params2) = chop (length params - n) params;
-val _ = warning (Syntax.string_of_term ctxt trm)
-val _ = warning (commas params)
-val _ = warning (commas (map (Syntax.string_of_term ctxt) prems))
 val _ = warning ((commas params1) ^ " | " ^ (commas params2))
 val _ = warning ((commas (map (Syntax.string_of_term ctxt) prems1)) ^ " | " ^
 (commas (map (Syntax.string_of_term ctxt) prems2)))
 in
-Seq.single thm
+()
 end
 *}
-ML {* METAHYPS *}
-ML {*
-fun chop_print_tac2 ctxt prems =
-let
-val _ = warning (commas (map (str_of_thm_no_vars ctxt) prems))
-in
-all_tac
-end
-*}
 lemma intro1:
 shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
 apply(tactic {* ObjectLogic.rulify_tac 1 *})
 apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *})
 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
-apply(tactic {* chop_print_tac 3 2 @{context} *})
 oops
-ML {*
+ML {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}
-fun SUBPROOF_test tac ctxt =
-SUBPROOF (fn {params, prems, context,...} =>
-let
-val thy = ProofContext.theory_of context
-in
-tac (params, prems, context)
-THEN  Method.insert_tac prems 1
-THEN  print_tac "SUBPROOF Test"
-THEN  SkipProof.cheat_tac thy
-end) ctxt 1
-*}
 lemma fresh_App:
 shows "\<And>a t s. \<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
 apply(tactic {* ObjectLogic.rulify_tac 1 *})
 apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *})
 apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
+apply(tactic {* print_tac "" *})
+apply(tactic {* SUBPROOF_test (fn {params, prems, ...} =>
+let
+val (prems1, prems2) = chop (length prems - length fresh_rules) prems
+val (params1, params2) = chop (length params - length fresh_preds) params
+in
+no_tac
+end) @{context} *})
 oops
-(*
-apply(tactic {* SUBPROOF_test
-(fn (params, prems, ctxt) =>
-let
-val (prems1, prems2) = chop (length prems - 4) prems;
-val (params1, params2) = chop (length params - 1) params;
-in
-rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 2))) 1
-end) @{context} *})
-*)
 ML{*fun subproof2 prem params2 prems2 =
 SUBPROOF (fn {prems, ...} =>
 let
 val prem' = prems MRS prem;
 ML %linenosgray{*fun subproof1 rules preds i =
 SUBPROOF (fn {params, prems, context = ctxt', ...} =>
 let
-val (prems1, prems2) = chop (length prems - length rules) prems;
+val (prems1, prems2) = chop (length prems - length rules) prems
-val (params1, params2) = chop (length params - length preds) params;
+val (params1, params2) = chop (length params - length preds) params
 in
 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
 (* applicateion of the i-ith intro rule *)
 THEN
 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
 text {*
 A test case
 *}
 ML{*fun intros_tac_test ctxt i =
-let
+intros_tac eo_defs eo_rules eo_preds i ctxt *}
-val rules = [@{prop "even (0::nat)"},
-@{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
-@{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
-val defs = [@{thm even_def}, @{thm odd_def}]
-val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
-in
-intros_tac defs rules preds i ctxt
-end*}
 lemma intro0:
 shows "even 0"
 apply(tactic {* intros_tac_test @{context} 0 *})
 done

changeset 208	0634d42bb69f
parent 194	8cd51a25a7ca
child 209	17b1512f51af