Re: [isabelle] Quickcheck in locale with defines directive
Am 07.09.2014 um 14:55 schrieb Julian Brunner <julianbrunner at gmail.com>:
> Consider the following locale:
> locale test =
> fixes foo :: "nat"
> defines "foo == 0"
> lemma "foo = 0" unfolding foo_def by rule
> 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?
Your analysis appears to be correct. The guilty code is in "src/Tools/quickcheck.ML":
val assms =
if Config.get lthy no_assms then 
(case some_locale of
NONE => Assumption.all_assms_of lthy
| SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy));
If the case distinction in the "else" case were to be replaced by an unconditional
your example would work fine. But then some other examples from "src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy" would fail.
Florian, your change d9549f9da779 introduced the above code. Do you know what could be done to take "defines" into consideration?
This archive was generated by a fusion of
Pipermail (Mailman edition) and