theory Ind_Code+ −
imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims+ −
begin+ −
+ −
datatype trm =+ −
Var "string"+ −
| App "trm" "trm"+ −
| Lam "string" "trm"+ −
+ −
simple_inductive + −
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 {*+ −
+ −
@{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}+ −
+ −
@{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}+ −
+ −
@{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}+ −
+ −
@{text [display] "ind ::= \<And>zs. pred zs \<Longrightarrow> rules[preds::=Ps] \<Longrightarrow> P zs"}+ −
+ −
@{text [display] "oind ::= \<forall>zs. pred zs \<longrightarrow> orules[preds::=Ps] \<longrightarrow> P zs"}+ −
+ −
\underline{Induction proof}+ −
+ −
After ``objectivication'' we have + −
@{text "pred zs"} and @{text "orules[preds::=Ps]"}; and have to show+ −
@{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\<forall>preds. orules \<longrightarrow> pred zs"}.+ −
Instantiating the @{text "preds"} with @{text "Ps"} gives+ −
@{text "orules[preds::=Ps] \<longrightarrow> P zs"}. So we can conclude with @{text "P zs"}.+ −
+ −
\underline{Intro proof}+ −
+ −
Assume we want to prove the $i$th intro rule. + −
+ −
We have to show @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"};+ −
expanding the defs, gives + −
+ −
@{text [display]+ −
"\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ts"}+ −
+ −
By applying as many allI and impI as possible, we have+ −
+ −
@{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},+ −
@{text "orules"}; and have to show @{text "pred ts"}+ −
+ −
the $i$th @{text "orule"} is of the + −
form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}.+ −
+ −
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"}.+ −
+ −
*}+ −
+ −
+ −
text {*+ −
First we have to produce for each predicate the definition of the form+ −
+ −
@{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}+ −
+ −
and then ``register'' the definitions with Isabelle. + −
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.+ −
*}+ −
+ −
ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy =+ −
let + −
val arg = ((predname, syn), (Attrib.empty_binding, trm))+ −
val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy+ −
in + −
(thm, lthy') + −
end*}+ −
+ −
text {*+ −
It returns the definition (as a theorem) and the local theory in which this definition has + −
been made. In Line 4, @{ML internalK in Thm} is a flag attached to the + −
theorem (others possibilities are @{ML definitionK in Thm} and @{ML 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. We also+ −
use @{ML empty_binding in Attrib} in Line 3, since the definition does + −
not need to have any theorem attributes. A testcase for this function is+ −
*}+ −
+ −
local_setup %gray {* fn lthy =>+ −
let+ −
val arg = ((@{binding "MyTrue"}, NoSyn), @{term True})+ −
val (def, lthy') = make_defs arg lthy + −
in+ −
warning (str_of_thm 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+ −
changes to the ambient theory, we can query the definition using 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+ −
are 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"}. + −
+ −
The first function constructs the term for one particular predicate, say+ −
@{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"}.+ −
*}+ −
+ −
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+ −
+ −
val fresh_args = + −
arg_tys + −
|> map (pair "z")+ −
|> Variable.variant_frees lthy (preds @ orules) + −
|> map Free+ −
in+ −
list_comb (pred, fresh_args)+ −
|> fold_rev (curry HOLogic.mk_imp) orules+ −
|> 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+ −
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+ −
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 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)+ −
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 + −
+ −
@{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"}+ −
+ −
The second function for the definitions has to just iterate the function+ −
@{ML defs_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 "arg_tyss"} is+ −
the list of argument-type-lists for each predicate.+ −
*}+ −
+ −
ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =+ −
let+ −
val thy = ProofContext.theory_of lthy+ −
val orules = map (ObjectLogic.atomize_term thy) rules+ −
val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) + −
in+ −
fold_map make_defs (prednames ~~ syns ~~ defs) lthy+ −
end*}+ −
+ −
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+ −
@{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+ −
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"},+ −
@{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+ −
in+ −
warning (str_of_thms 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}+ −
+ −
+ −
This completes the code for making the definitions. Next we deal with+ −
the induction principles. Recall that the proof of the induction principle + −
for @{text "even"} was:+ −
*}+ −
+ −
lemma man_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(atomize (full))+ −
apply(cut_tac prems)+ −
apply(unfold even_def)+ −
apply(drule spec[where x=P])+ −
apply(drule spec[where x=Q])+ −
apply(assumption)+ −
done+ −
+ −
text {* + −
The code for automating such induction principles has to accomplish two tasks: + −
constructing the induction principles from the given introduction+ −
rules and then automatically generating proofs for them using a tactic. + −
+ −
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}. Together with 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 + −
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 *})+ −
txt {* + −
We obtain the goal state+ −
+ −
\begin{minipage}{\textwidth}+ −
@{subgoals} + −
\end{minipage}*}+ −
(*<*)oops(*>*)+ −
+ −
text {*+ −
Now the complete tactic for proving the induction principles can + −
be implemented as follows:+ −
*}+ −
+ −
ML %linenosgray{*fun induction_tac defs prems insts =+ −
EVERY1 [ObjectLogic.full_atomize_tac,+ −
cut_facts_tac prems,+ −
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+ −
*}+ −
+ −
ML{*fun test_tac prems = + −
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 + −
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} *})+ −
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"}+ −
+ −
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 + −
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:+ −
+ −
\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.+ −
*}+ −
+ −
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)+ −
+ −
val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))+ −
val goal = Logic.list_implies + −
(srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))+ −
in+ −
Goal.prove lthy' [] [prem] goal+ −
(fn {prems, ...} => induction_tac defs prems cnewpreds)+ −
|> singleton (ProofContext.export lthy' lthy)+ −
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'"}. 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+ −
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+ −
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+ −
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.+ −
*}+ −
+ −
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)+ −
in+ −
warning (str_of_thm_raw lthy intro); lthy+ −
end *} + −
+ −
text {*+ −
This prints out:+ −
+ −
@{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"}.+ −
+ −
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. + −
*}+ −
+ −
ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy =+ −
let+ −
val Ps = replicate (length preds) "P"+ −
val (newprednames, lthy') = Variable.variant_fixes Ps lthy+ −
+ −
val thy = ProofContext.theory_of lthy'+ −
+ −
val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss+ −
val newpreds = map Free (newprednames ~~ tyss')+ −
val cnewpreds = map (cterm_of thy) newpreds+ −
val srules = map (subst_free (preds ~~ newpreds)) rules+ −
+ −
in+ −
map (prove_induction lthy' defs srules cnewpreds) + −
(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 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+ −
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 + −
(Line 16).+ −
+ −
A testcase for this function is+ −
*}+ −
+ −
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+ −
in+ −
warning (str_of_thms_raw lthy ind_thms); lthy+ −
end *}+ −
+ −
+ −
text {*+ −
which prints out+ −
+ −
@{text [display]+ −
"> 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+ −
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.+ −
*}+ −
+ −
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+ −
theorems. + −
*}+ −
+ −
lemma all_elims_test:+ −
fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"+ −
shows "\<forall>x y z. P x y z" sorry+ −
+ −
lemma imp_elims_test:+ −
fixes A B C::"bool"+ −
shows "A \<longrightarrow> B \<longrightarrow> C" sorry+ −
+ −
lemma imp_elims_test':+ −
fixes A::"bool"+ −
shows "A" "B" sorry+ −
+ −
text {*+ −
The function @{ML all_elims} takes a list of (certified) terms and instantiates+ −
theorems of the form @{thm [source] all_elims_test}. For example we can instantiate+ −
the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows+ −
+ −
@{ML_response_fake [display, gray]+ −
"let+ −
val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]+ −
val new_thm = all_elims ctrms @{thm all_elims_test}+ −
in+ −
warning (str_of_thm @{context} new_thm)+ −
end"+ −
"P a b c"}+ −
+ −
Similarly, the function @{ML imp_elims} eliminates preconditions from implications. + −
For example + −
+ −
@{ML_response_fake [display, gray]+ −
"warning (str_of_thm @{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 =+ −
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 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+ −
*}+ −
+ −
+ −
+ −
+ −
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) *})+ −
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;+ −
val prem'' = + −
case prop_of prem' of+ −
_ $ (Const (@{const_name All}, _) $ _) =>+ −
prem' |> all_elims params2 + −
|> imp_elims prems2+ −
| _ => prem';+ −
in + −
rtac prem'' 1 + −
end)*}+ −
+ −
text {*+ −
+ −
*}+ −
+ −
+ −
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;+ −
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)+ −
end)*}+ −
+ −
text {*+ −
@{text "params1"} are the variables of the rules; @{text "params2"} is+ −
the variables corresponding to the @{text "preds"}.+ −
+ −
@{text "prems1"} are the assumption corresponding to the rules;+ −
@{text "prems2"} are the assumptions coming from the allIs/impIs+ −
+ −
you instantiate the parameters i-th introduction rule with the parameters+ −
that come from the rule; and you apply it to the goal+ −
+ −
this now generates subgoals corresponding to the premisses of this+ −
intro rule + −
*}+ −
+ −
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}]),+ −
subproof1 rules preds i ctxt]*}+ −
+ −
text {*+ −
A test case+ −
*}+ −
+ −
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*}+ −
+ −
lemma intro0:+ −
shows "even 0"+ −
apply(tactic {* intros_tac_test @{context} 0 *})+ −
done+ −
+ −
lemma intro1:+ −
shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"+ −
apply(tactic {* intros_tac_test @{context} 1 *})+ −
done+ −
+ −
lemma intro2:+ −
shows "\<And>m. even m \<Longrightarrow> odd (Suc m)"+ −
apply(tactic {* intros_tac_test @{context} 2 *})+ −
done+ −
+ −
ML{*fun introductions rules preds defs lthy = + −
let+ −
fun prove_intro (i, goal) =+ −
Goal.prove lthy [] [] goal+ −
(fn {context, ...} => intros_tac defs rules preds i context)+ −
in+ −
map_index prove_intro rules+ −
end*}+ −
+ −
text {* main internal function *}+ −
+ −
ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy =+ −
let+ −
val syns = map snd pred_specs+ −
val pred_specs' = map fst pred_specs+ −
val prednames = map fst pred_specs'+ −
val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'+ −
+ −
val tyss = map (binder_types o fastype_of) preds + −
val (attrs, rules) = split_list rule_specs + −
+ −
val (defs, lthy') = definitions rules preds prednames syns tyss lthy + −
val ind_rules = inductions rules defs preds tyss lthy' + −
val intro_rules = introductions rules preds defs lthy'+ −
+ −
val mut_name = space_implode "_" (map Binding.name_of prednames)+ −
val case_names = map (Binding.name_of o fst) attrs+ −
in+ −
lthy' + −
|> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>+ −
((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) + −
|-> (fn intross => LocalTheory.note Thm.theoremK+ −
((Binding.qualify false mut_name (@{binding "intros"}), []), maps snd intross)) + −
|>> snd + −
||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>+ −
((Binding.qualify false (Binding.name_of R) (@{binding "induct"}),+ −
[Attrib.internal (K (RuleCases.case_names case_names)),+ −
Attrib.internal (K (RuleCases.consumes 1)),+ −
Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))+ −
(pred_specs ~~ ind_rules)) #>> maps snd) + −
|> snd+ −
end*}+ −
+ −
ML{*fun add_inductive_cmd pred_specs rule_specs lthy =+ −
let+ −
val ((pred_specs', rule_specs'), _) = + −
Specification.read_spec pred_specs rule_specs lthy+ −
in+ −
add_inductive pred_specs' rule_specs' lthy+ −
end*} + −
+ −
ML{*val spec_parser = + −
OuterParse.fixes -- + −
Scan.optional + −
(OuterParse.$$$ "where" |--+ −
OuterParse.!!! + −
(OuterParse.enum1 "|" + −
(SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}+ −
+ −
ML{*val specification =+ −
spec_parser >>+ −
(fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*}+ −
+ −
ML{*val _ = OuterSyntax.local_theory "simple_inductive" + −
"define inductive predicates"+ −
OuterKeyword.thy_decl specification*}+ −
+ −
text {*+ −
Things to include at the end:+ −
+ −
\begin{itemize}+ −
\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+ −
\end{itemize}+ −
+ −
*}+ −
+ −
simple_inductive+ −
Even and Odd+ −
where+ −
Even0: "Even 0"+ −
| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"+ −
| OddS: "Even n \<Longrightarrow> Odd (Suc n)"+ −
+ −
end+ −