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



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







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