Re: [isabelle] Goal.prove_future variant of Goal.prove_multi



> 
> Yes, as far as I can say on the spot, there could be Goal.prove_multi_future, but it was never used so far. 
> 
> In most situations, a plain "map" of Goal.prove should do the same job. You mainly need Goal.prove_multi for simultaneous induction.
> 
> If you do have a convincing application, I can nonetheless add the missing variant for the next release.

That would indeed be nice. The application we have in mind are the datatype order/show/... generators.
We just recently got a request from Dmitriy to use the Goal.prove_..._future variants, since the invocation
of the generator on some particular datatype took over 3 minutes which was blocking the further proceeding
of the theory file. This is now fixed for the current generators which work on the (old) datatypes and do not require
Goal.prove_multi. However, we are in the process of also providing these generators for the BNF-based (new) datatypes, where the usage
of Goal.prove_multi is essential since the first step is an simultaneous induction. 

To summarize, without Goal.prove_multi_future we have to wait over a minute for the new generators on Dmitriys datatype,
but with it(*) the generator returns immediately. 

Best regards,
RenÃ



(*): Here is our diff in Pure/goal.ML:

(in signature)

val prove_multi_future: Proof.context -> string list -> term list -> term list ->
    ({prems: thm list, context: Proof.context} -> tactic) -> thm list


(in implementation)
val prove_multi_future = prove_common false ~1;



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.