[isabelle] Quickcheck in locale with defines directive



Dear all,

Consider the following locale:

locale test =
  fixes foo :: "nat"
  defines "foo == 0"
begin

  lemma "foo = 0" unfolding foo_def by rule

end

Isabelle2014 then produces this output at the lemma statement:

Auto Quickcheck found a counterexample:

foo = Suc 0

Evaluated terms:
0 = 0

So it looks like quickcheck thinks that it can still define "foo",
when it is actually already defined. Or did I misunderstand what the
defines directive does?




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