*To*: Manuel Eberl <eberlm at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Quickcheck counter example of "3 < 4"?*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 2 Jul 2015 08:51:12 +0200*In-reply-to*: <5594D879.6050905@in.tum.de>*References*: <CAJ-DSyzHTYYeHT3DqUotjs10cwwpj3SkskSTmoQoY7aWz63Aow@mail.gmail.com> <5594D6B7.1080109@in.tum.de> <5594D879.6050905@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Andreas On 02/07/15 08:21, Manuel Eberl wrote:

Should it not at least show the interpretation of the free type variable? Manuel On 02/07/15 08:14, Tobias Nipkow wrote:On 02/07/2015 07:48, Jason Dagit wrote:I forgot to add a type annotation and ended up with the following (Isabelle 2015 on Windows 7): lemma "3 < 4" quickcheckNo type constraints. Because 3, 4 and < are polymorphic, quickcheck is free to build a type/model with an interpretation for < where 3 < 4 does not hold. There used to be a time when the interface alerted you to polymorphic numerals, which are almost always not what one wants. But we have moved on from that. The fact that you are not shown the model is because only the interpretation of the free variables is shown, but there are none. TobiasQuickchecking... For instantiation with default_type Enum.finite_1: Enum.finite_1 to be substituted for variable 'a does not have sort {numeral,ord} Testing conjecture with Quickcheck-exhaustive... Quickcheck found a counterexample: Compared with the type annotation: lemma "(3::nat) < 4" quickcheck Quickchecking... Testing conjecture with Quickcheck-exhaustive... Quickcheck found no counterexample. Note: in the first case it says there is a counter example but that is the end of the output in the "Output" tab of jEdit. Is this to be expected when no types are given? As a new Isabelle user it quite surprised me. Thanks, Jason

**Follow-Ups**:**Re: [isabelle] Quickcheck counter example of "3 < 4"?***From:*Matthew Fernandez

**References**:**[isabelle] Quickcheck counter example of "3 < 4"?***From:*Jason Dagit

**Re: [isabelle] Quickcheck counter example of "3 < 4"?***From:*Tobias Nipkow

**Re: [isabelle] Quickcheck counter example of "3 < 4"?***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Next by Date: [isabelle] case_names, obtains (par_name), and named local hypotheses
- Previous by Thread: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Next by Thread: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list