Email Gateway (Aug 22 2022 at 14:09): Email Gateway (Aug 22 2022 at 14:09):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
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
Barf.thy
Email Gateway (Aug 22 2022 at 14:09):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Nov 21 2024 at 12:39 UTC