232 lemma "\<forall>x1 x2 x3. P (x1::nat) (x2::nat) (x3::nat) \<Longrightarrow> True"

   232 lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"

   252 ML{*fun induction_tac defs prems insts =

   252 ML %linenosgray{*fun induction_tac defs prems insts =

   283   rules. For this we have to construct

   283   rules. For this we have to construct for each predicate @{text "pred"}

   286   "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$> \<^raw:$zs$>"}

   286   "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$>\<^raw:$zs$>"}

   287 

   287 

   288   where the given predicates are replaced by new ones written

   288   where the given predicates @{text preds} are replaced by new distinct 

   289   as @{text "\<^raw:$Ps$>"}, and also generate new variables 

   289   ones written as @{text "\<^raw:$Ps$>"}, and also need to be applied to

   290   @{text "\<^raw:$zs$>"}.

   290   new variables @{text "\<^raw:$zs$>"}. 

   291 *}

   291 

   292 

   292   The function below expects that the rules are already appropriately

   293 ML %linenosgray{* fun prove_induction lthy defs rules cnewpreds ((pred, newpred), tys)  =

   293   replaced. The argument @{text "mrules"} stands for these modified

   294   introduction rules; @{text cnewpreds} are the certified terms coresponding

   295   to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for

   296   which we prove the introduction principle; @{text "newpred"} is its

   297   replacement and @{text "tys"} are the types of its argument.

   298 *}

   299 

   300 ML %linenosgray{* fun prove_induction lthy defs mrules cnewpreds ((pred, newpred), tys)  =

   301          (rules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))

   308          (mrules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))

   308 text {* *}

   315 text {* 

   316   In Line 3 we produce a list of names @{text "\<^raw:$zs$>"} according to the type 

   317   list. Line 4 makes these names unique and declare them as \emph{free} (but fixed)

   318   variables. These variables are free in the new theory @{text "lthy'"}. In Line 5

   319   we just construct the terms corresponding to the variables. The term variables are

   320   applied to the predicate in Line 7 (this is the first premise 

   321   @{text "pred \<^raw:$zs$>"} of the induction principle). In Line 8 and 9

   322   we first the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} and then add

   323   the (modified) introduction rules as premises.

   324 

   325   In Line 11 we set up the goal to be proved; call the induction tactic in

   326   Line 13. This returns a theorem. However, it is a theorem proved inside

   327   the local theory @{text "lthy'"} where the variables @{text "\<^raw:$zs$>"} are

   328   fixed, but free. By exporting this theorem from @{text "lthy'"} (which does contain

   329   the  @{text "\<^raw:$zs$>"} as free) to @{text "lthy"} (which does not), we

   330   obtain the desired quantifications @{text "\<And>\<^raw:$zs$>"}.

   331 

   332   So it is left to produce the modified rules and 

   333 *}