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


	Makarius





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