*To*: Jason Dagit <dagitj at gmail.com>*Subject*: Re: [isabelle] Quickcheck counter example of "3 < 4"?*From*: Makarius <makarius at sketis.net>*Date*: Thu, 2 Jul 2015 23:50:49 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAJ-DSywanf37-avEQMT1X5WM=EMNX7+MaBuWNBY5CVp2a574aA@mail.gmail.com>*References*: <CAJ-DSyzHTYYeHT3DqUotjs10cwwpj3SkskSTmoQoY7aWz63Aow@mail.gmail.com> <5594D6B7.1080109@in.tum.de> <CAJ-DSywanf37-avEQMT1X5WM=EMNX7+MaBuWNBY5CVp2a574aA@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Thu, 2 Jul 2015, Jason Dagit wrote:

On Wed, Jul 1, 2015 at 11:14 PM, Tobias Nipkow <nipkow at in.tum.de> wrote: I think I've been bitten by this several times. Most recently (and where I discovered the above example), I was proving the follow lemma, using the induction lemma described in [1]: lemma "(n::nat) > 1 â nâ2 > n + 1" In the case of n = 2, I had this: case 2 show "2 + 1 < 2â2" by auto This was giving me a message saying: show 2 + 1 < 2â2 Successful attempt to solve goal by exported rule: (1 < 2) â 2 + 1 < 2â2 But also saying: Failed to finish proofâ: goal (1 subgoal): 1. 3 < 2â2 Of course, if I manually simplified the expression in my `show` to match the goal, then I get an error about refining the goal.As you might have already guessed, the solution is rather simple, I haveto add a type annotation somewhere in the `show`. So having an alertabout polymorphic numerals would have been helpful here for thisbeginner. Lesson learned.

Makarius

**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:*Jason Dagit

- Previous by Date: Re: [isabelle] using makeindex in document preparation
- Next by Date: Re: [isabelle] simp vs Simplifier.rewrite
- Previous by Thread: Re: [isabelle] Quickcheck counter example of "3 < 4"?
- Next by Thread: [isabelle] case_names, obtains (par_name), and named local hypotheses
- 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