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 and 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 published.

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 MHonArc.