Re: [isabelle] Parallel proofs issue, potentially in subst method
On Wed, 12 Sep 2012, Makarius wrote:
The error should be on the line attempting the subst:
*** exception THM 0 raised (line 758 of "thm.ML"):
*** forall_intr: variable "bs" free in assumptions
*** [| length bs = sz; P (Suc p) sz bs; p # Z = Z |]
*** ==> p # load_list_basic sz (Suc p) = Z
*** At command "apply" (line 30 of "/home/rafalk/t/isa_bug/Loading.thy")
The issue is definitely due to some shadowing/renaming of the variable bs,
but what else is going on is well beyond my current grasp of comprehension.
I've had a quick look at the "subst" method, but it looks very bad. That
code has not been maintained in many years. It simply ignores the
all-important Proof.context when inventing free variables that are expected
to be fresh, but aren't. There is not just one place, but many. One could
probably make a small changeset to get your example working, but it will then
crash in another situation.
See http://isabelle.in.tum.de/repos/isabelle/rev/d1fcb4de8349 and
http://isabelle.in.tum.de/repos/isabelle/rev/25fc6e0da459 for what I've
made in the meantime. You have to see yourself how to apply this to
Isabelle2012 (via "hg import" etc). Isabelle has only a single official
release branch, and it will take a few months until the next one is
I think the main problem with your example was in RWInst.mk_renamings, as
changed in 25fc6e0da459 to get rid of usednames_of_thm in particular.
There are many more situations where "subst" produces free variables on
the spot. They still don't look 100% canonical to me, even after the
change, but for this round of refurbishing tools from the Isabelle library
it should be sufficient.
This archive was generated by a fusion of
Pipermail (Mailman edition) and