Email Gateway (Aug 19 2022 at 16:00): Email Gateway (Aug 19 2022 at 16:00):From: Julian Brunner <julianbrunner@gmail.com>
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?
Email Gateway (Aug 19 2022 at 16:01):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Julian,
Your analysis appears to be correct. The guilty code is in "src/Tools/quickcheck.ML":
val assms =
if Config.get lthy no_assms then []
else
(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
Assumption.all_assms_of lthy
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?
Jasmin
Email Gateway (Aug 19 2022 at 16:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
Well, the change above made quickcheck operate on the interpretations of
a locale rather than just pulling the locale's context into its search
space. It seems to me that nowadays there are configuration options
»expand« and »interpret« to choose either the naked context or all
interpretations of that particular locale respectively. Have you tried
the option »expand«? Maybe there is some documentation on quickcheck
which gives further hints.
Cheers,
Florian
signature.asc
Last updated: Apr 19 2024 at 01:05 UTC