*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 13 Nov 2012 11:03:53 +0100*In-reply-to*: <CAE5E_avmHuAou3ktw_AWTssQCiyntYUp54tuD=agSm3i2oO+RQ@mail.gmail.com>*References*: <CAE5E_avmHuAou3ktw_AWTssQCiyntYUp54tuD=agSm3i2oO+RQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:16.0) Gecko/20121026 Thunderbird/16.0.2

The reason for this failure is consistency: when proving P(?x), you delay the point at which you give the actual witness t for ?x. But that is just an operational rearrangement of the proof. Logically it must be possible to construct that t right away. Hence t must not depend on anything that only came into existence while proving P(?x). Otherwise you could prove EX x. ALL y. x=y: apply(rule exI) 1. ALL y. ?x = y apply(rule allI) 1. !!y. ?x = y apply(rule refl) fails because you would need to instantiate ?x with the local y, which Isabelle prevents. (Contrast this with a proof of ALL x. EX y. x=y) Your failed proof attempt was morally correct, but you need to convince the system that the witness could have been constructed up front, usually by rearranging your proof text, eg as Lars suggested. Best Tobias Am 12/11/2012 20:21, schrieb Julian Brunner: > Hello, > > While using Isabelle, I keep running into the problem of not being able to > prove existentially quantified statements using a witness with the show > statement telling me that the "Local statement will fail to refine any > pending goal". > > For instance: > > theorem "EX x. x = (0 :: nat)" > proof > obtain x where x_def: "x = (0 :: nat)" by simp > show "x = 0" using x_def by simp > qed > > This example results in "Local statement will fail to refine any pending > goal" in line 4 of the proof. Furthermore, replacing line 3 with > > def x == "0 :: nat" > > makes everything work just fine. This is a minimal example built from a > bigger proof where the witness used for proving the existential statement > was an expression containing variables that originated in an obtain > statement. From what I've observed so far, it appears that whenever > variables from an obtain statement are part of the witness, the show > statement fails. I've used [[show_types]] to confirm that the types aren't > part of the issue, both x and 0 are of type nat. Also, the output doesn't > give me the usual "Failed attempt to solve goal by exported rule" line > stating why the show statement failed, as is the case with assume > statements that don't match any assumption in the goal. > > Of course I can work around this by invoking proof with the '-' method and > using automation to prove the existentially quantified statement using the > witness, but it'd be nicer if it'd work like this, I feel like this is just > a minor technical issue, but I couldn't figure out what's going on. > > I think I've also run into a similar problem that didn't involve obtain > statements but I can't find the theory where that happened right now, maybe > I'll post again if I run into that issue once more. For now, I'd be happy > with figuring this one out. > > Cheers, > Julian >

**References**:

- Previous by Date: Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails
- Next by Date: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- Previous by Thread: Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails
- Next by Thread: Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails
- Cl-isabelle-users November 2012 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