[isabelle] Shadowing constants in obtains clause



Dear Isar experts,

How can I name a variable in an obtains clause whose name clashes with an existing constant name in scope? Here is an minmal example:

consts P :: "nat => bool"

lemma
  assumes "?map. P map"
  obtains map where "P map"

Here, the map in the where clause gets resolved to List.map rather than the variable map bound by the obtains. When I write the lemma as explicit elimination rule, this works as expected:

lemma
  assumes "?map. P map"
  and that[intro?]: "!!map. P map ==> thesis"
  shows "thesis"

Is there any way to use the nicer obtains format without changing the name of map? I tried

lemma
  fixes map
  assumes "?map. P map"
  obtains map where "P map"

but this yields the error of map being fixed twice.

Andreas




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