Re: [isabelle] Strange variable binding on obtains - long-goal format



On Mon, 23 Apr 2012, Brian Huffman wrote:

Using a type annotation (even a dummy one) seems to make it work:

lemma
 assumes P
 obtains sym :: "_" where "sym = w"

goal (1 subgoal):
1. (!!sym. sym = w ==> thesis) ==> thesis

The behavior in the latest developer version (8b31786fe603) seems to
be the same.

Adding a "fixes sym" to the lemma results in a "duplicate fixed
variable" error.

If this behavior is intended, is there any reason for silently ignoring the variable binding given by the user, not even issuing a warning?

I doubt that the behavior is intended. It seems to me like a classic mistake in context-plumbing: Without the type annotation, the term "sym = w" is parsed in a context where "sym" has not been declared as a variable name.

Perhaps we will be able to fix this in time for the next release.

These things are an order of magnitude for complex than they seem. The 'obtains' element has suffured from some imperfections ever since its introduction some years ago. These are not shallow "bugs", but some deeper problems how the fixes/assumes/obtains format is processed -- it still cannot process the split into disjunctive contexts properly.

It is all going back to the wild times of 2006/2007, when too many people where doing too many too ambitious things at the same time (Wenzel, Haftmann, Ballarin, Krauss). This has resulted in what was called "national debts" in Isabelle jargon, and it has required many years to pay back quite a lot of that, but not all. (When I am finished here, I will ask the German government if they need an expert on that.)

For Isabelle2012, which is due before the end of May, I have again made various refinements of the local theory and context management infrastructure that is relevant here. I've also considered to rework these old 'obtains' points, but did not get that far. So it is again postponed to another release after the coming one.


BTW, in order to get really acquainted with these delicacies of the Isabelle implementation at an expert level, the first step is to overcome the illusion that it is easy to "fix" the system. Most of the easy things have all been done already in the past, mainly the hard and very hard ones are pending.


It might be worth documenting the above workarounds on the new Isabelle community https://isabelle.in.tum.de/community/Main_Page wiki. I am not engaged there myself, but I occasionally look if certain issues being raised there should be put on the current agenda to be refined or reformed.


	Makarius





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