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:
>
> 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?

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.

- Brian





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