From: Martin Desharnais <martin.desharnais@posteo.de>

Dear Isabelle developers,

I just discovered what seems to be a name clash when using "let"

definitions in the following, minimized lemma.

lemma

fixes xs :: "('a × 'b) list" and P :: "'a × 'b ⇒ bool"

shows False

proof -

let ?x0 = "takeWhile P xs"

let ?x = "map fst ?x0"

let ?y = "map snd ?x0"

(*

Type unification failed

Type error in application: incompatible operand type

Operator: map snd :: (??'a × ??'b) list ⇒ ??'b list

Operand: ?x :: 'a list

*)

oops

The name ?x0 seems to be a synonym for ?x. My expectation was that ?x0

and ?x would be two different names for different constants, with

possibly different types).

I confirmed this behaviour with Isabelle/a9aaef9fcf86+ and Isabelle 2020.

Regards,

Martin Desharnais

From: Mathias Fleury <mathias.fleury12@gmail.com>

Hi Martin,

This behaviour is documented and intended that way. From the Isar-ref

document, Section 3.2:

» ?x and ?x0 and ?x.0 all refer to the same unknown, with basename x and

index 0.«

Regards,

Mathias

From: Martin Desharnais <martin.desharnais@posteo.de>

Hi Mathias,

Thanks for the clarification. I should have investigated more thoroughly

before posting.

Sorry for disturbing,

Martin

From: Peter Lammich <lammich@in.tum.de>

If you should need to refer to the variable name "x0" with index 0, you

can always write ?x0.0, e.g.

lemma foo: "x0 + (0::int) = x0" by simp

thm foo[where ?x0.0=2]

Last updated: Sep 25 2021 at 09:17 UTC