Re: [isabelle] Strange variable binding on obtains - long-goal format
On Mon, Apr 23, 2012 at 10:48 AM, Peter Lammich <lammich at 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:
> assumes P
> obtains sym where "sym = w"
> thm that
> 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?
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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and