Eugene W. Stark

2016-09-25 10:49:09 UTC

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

- 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