--- a/ProgTutorial/Package/Ind_Code.thy Tue Mar 24 12:09:38 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy Tue Mar 24 18:06:20 2009 +0100
@@ -13,8 +13,7 @@
"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"
-
+| "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b t"
section {* Code *}
@@ -60,15 +59,55 @@
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}
+ ****************************
+ \end{center}
*}
text {*
- First we have to produce for each predicate the definition of the form
+ 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.
@@ -102,8 +141,8 @@
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
- changes to the ambient theory, we can query the definition using the usual
+ 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
command \isacommand{thm}:
\begin{isabelle}
@@ -111,18 +150,20 @@
@{text "> MyTrue \<equiv> True"}
\end{isabelle}
- The next two functions construct the right-hand sides of the definitions, which
- are of the form
+ The next two functions construct the right-hand sides of the definitions,
+ 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
- in the @{text orules} and also be distinct from the @{text "preds"}.
+ 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, 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) =
@@ -153,26 +194,22 @@
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
- out the definition. So we obtain as printout
+ The testcase calls @{ML defs_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))
@@ -201,7 +238,7 @@
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
@@ -209,16 +246,10 @@
local_setup %gray {* fn lthy =>
let
- val rules = [@{prop "even 0"},
- @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
- @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
- val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
- 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
+ val (defs, lthy') =
+ definitions eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy
in
- warning (str_of_thms_no_vars lthy' defs); lthy'
+ warning (str_of_thms_no_vars lthy' defs); lthy
end *}
text {*
@@ -227,7 +258,6 @@
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,
@@ -235,14 +265,25 @@
> \<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:
-assumes prems: "even n"
+lemma manual_ind_prin:
+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)
@@ -266,14 +307,15 @@
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.
*}
@@ -295,37 +337,36 @@
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"})
- and the instantiations as arguments. Compare this with the manual proof
- given for the lemma @{thm [source] man_ind_principle}: there is almos a
- one-to-one correspondence between the \isacommand{apply}-script and the
- @{ML induction_tac}. A testcase for this tactic is the function
+ We have to give it as arguments the definitions, the premise
+ (for example @{text "even n"}) and the instantiations. Compare this with the
+ manual proof given for the lemma @{thm [source] manual_ind_prin}:
+ as you can see there is almost a one-to-one correspondence between the \isacommand{apply}-script
+ 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:
-assumes prems: "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(tactic {* test_tac @{thms prems} *})
+lemma automatic_ind_prin:
+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"
+apply(tactic {* test_tac @{thms prem} *})
done
text {*
@@ -335,33 +376,25 @@
@{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"}.
- We also need to generate fresh arguments for the predicate @{text "pred"} in
- the premise and the @{text "?P"} in the conclusion. Note
+ 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. Note
that the @{text "?Ps"} and @{text "?zs"} need to be
- schematic variables that can be instantiated. This corresponds to what the
- @{thm [source] auto_ind_principle} looks like:
+ schematic variables that can be instantiated by the user.
- \begin{isabelle}
- \isacommand{thm}~@{thm [source] auto_ind_principle}\\
- @{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"}
- \end{isabelle}
-
- We achieve
- that in two steps.
-
- The function below 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 introduction principle; @{text "newpred"} is its
- replacement and @{text "tys"} are the argument types of this predicate.
+ We generate these goals in two steps. The first function 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 introduction principle;
+ @{text "newpred"} is its replacement and @{text "arg_tys"} are the argument
+ types of this predicate.
*}
-ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys) =
+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;
@@ -380,8 +413,8 @@
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.
- The term variables are applied to the predicate in Line 7 (this corresponds
+ 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 (substituded) introduction rules as premises. In case that
@@ -389,20 +422,20 @@
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
- for proving the induction principle. 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
+ 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
+ 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)"}]
@@ -411,7 +444,7 @@
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 *}
@@ -424,11 +457,12 @@
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 =
@@ -450,18 +484,18 @@
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
@@ -469,13 +503,7 @@
local_setup %gray {* fn lthy =>
let
- 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"}]
- val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
- val ind_thms = inductions rules defs preds tyss lthy
+ val ind_thms = inductions eo_rules eo_defs eo_preds eo_arg_tyss lthy
in
warning (str_of_thms lthy ind_thms); lthy
end *}
@@ -490,21 +518,27 @@
> 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
- introduction rules. Their proofs are quite a bit more involved. To ease them
- somewhat we use the following two helper function.
+ This completes the code for the induction principles.
+*}
+
+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.
*}
@@ -535,7 +569,7 @@
"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}
@@ -548,57 +582,26 @@
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 {*
-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
-*}
-
-
+ML {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}
lemma fresh_App:
@@ -606,17 +609,16 @@
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, ...} =>
@@ -640,8 +642,8 @@
ML %linenosgray{*fun subproof1 rules preds i =
SUBPROOF (fn {params, prems, context = ctxt', ...} =>
let
- val (prems1, prems2) = chop (length prems - length rules) prems;
- val (params1, params2) = chop (length params - length preds) params;
+ val (prems1, prems2) = chop (length prems - length rules) prems
+ 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 *)
@@ -675,15 +677,7 @@
*}
ML{*fun intros_tac_test ctxt i =
-let
- 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*}
+ intros_tac eo_defs eo_rules eo_preds i ctxt *}
lemma intro0:
shows "even 0"