Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Shadowing constants in obtains clause

view this post on Zulip Email Gateway (Aug 19 2022 at 16:49):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Last updated: Apr 26 2024 at 12:28 UTC