Hi Eugene,

This problem comes from the internal handling of schematic variable names in Isabelle.

Schematic variables all carry an index number, which is 0 by default, but may take higher

values due to theorem operations (in particular resolution). If this index is 0, the

output omits the index, i.e., ?x.0 is printed as ?x (unless the variable name ends with a

number). Moreover, the dot is omitted in pretty-printing and parsing unless the variable

name ends with a number. I.e., ?x.1 is printed (and parsed) as ?x1 whereas ?x1.0 is

printed as ?x1.0 (and you also have to use [where ?x1.0=foo] to instantiate such variables

with numbers in the end in theorems).

Back to your example: let bindings are handled internally like schematic variables. Hence,

?x0 gets parsed as ?x.0 and ?x1 as ?x.1 and ?x becomes ?x.0 again. That's why your last

let-binding overrides the first.

Best,

Andreas

*Post by Eugene W. Stark*Can somebody explain this mysterious behavior? Thanks.

- Gene Stark

----------------------

theory Barf

imports Main

begin

lemma

shows nothing

proof -

let ?x0 = 100

let ?x1 = 101

let ?y = "\<lambda>i. if i = 0 then ?x0 else ?x1"

have "?y 0 = ?x0" by presburger

let ?x = 102

have "?y 0 = ?x0" oops (* ?x0 is now 102 *)

end