[isabelle] Mysterious behavior of "let"

Andreas Lochbihler

2016-09-26 06:50:41 UTC

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