Re: [isabelle] Quickcheck in locale with defines directive



Hi Julian,

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"
> 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?

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





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