Re: [isabelle] Mysterious behavior of "let"



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

On 25/09/16 12:43, Eugene W. Stark wrote:
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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.