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:
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
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
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and