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