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

On Tue, 17 Feb 2015, Christian Sternagel wrote:

in src/Pure/goal.ML there is the Goal.prove_future variant of Goal.prove. However I couldn't find a "future" variant of Goal.prove_multi.

Is it just an interface-omission that there is no Goal.prove_multi_future or are there technical reasons for not having such a 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. The Goal.prove variants are relatively pragmatic, e.g. legacy things like Goal.prove_global are there, because some packages still need them, and thus their implementation is simplified a bit.

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.

Why isn't Goal.prove implicitly "futurized"? (So that the standard behavior allows for implicit parallelization; I guess that's not always a good thing.)

In Isabelle/ML programming there is often a situation where some tool uses Goal.prove ... handle ERROR _ => to react on a failed attempt, i.e. there is an implicit assumption of strictness of this operation.

There is an ancient Isabelle tradition to change semantics only together with the name of an operation, so I left Goal.prove unchanged and added Goal.prove_future. It should be easy to upgrade tools that cope with forked proofs by searching for Goal.prove and making educated guesses if it can be replaced by Goal.prove_future.


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