Email Gateway (Aug 18 2022 at 19:35): Email Gateway (Aug 18 2022 at 19:35):From: Peter Lammich <lammich@in.tum.de>
Hi all,
referring to Isaballe 2011-1
I just encountered some (in my opinion strange) behavior of the obtains
long-goal format:
lemma
assumes P
obtains sym where "sym = w"
thm that
Outputs:
sym = (w\<Colon>('a \<times> 'a \<Rightarrow> bool) \<Rightarrow>
bool) \<Longrightarrow> thesis\<Colon>bool
That is, sym is recognized as a constant (Relation.sym) here, instead of
a bound variable, as I would expect.
Is there a workaround, i.e., can I use a name declared as a constant
somewhere in an obtains-goal?
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?
Regards,
Peter
Email Gateway (Aug 18 2022 at 19:36):From: Brian Huffman <huffman@in.tum.de>
On Mon, Apr 23, 2012 at 10:48 AM, Peter Lammich <lammich@in.tum.de> wrote:
Hi all,
referring to Isaballe 2011-1
I just encountered some (in my opinion strange) behavior of the obtains
long-goal format:lemma
assumes P
obtains sym where "sym = w"
thm thatOutputs:
sym = (w\<Colon>('a \<times> 'a \<Rightarrow> bool) \<Rightarrow>
bool) \<Longrightarrow> thesis\<Colon>boolThat is, sym is recognized as a constant (Relation.sym) here, instead of
a bound variable, as I would expect.
Is there a workaround, i.e., can I use a name declared as a constant
somewhere in an obtains-goal?
Using a type annotation (even a dummy one) seems to make it work:
lemma
assumes P
obtains sym :: "_" where "sym = w"
goal (1 subgoal):
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.
Email Gateway (Aug 18 2022 at 19:36):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 16 2024 at 16:19 UTC