*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails*From*: Julian Brunner <julianbrunner at gmail.com>*Date*: Mon, 12 Nov 2012 20:21:01 +0100

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

**Follow-Ups**:**Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails***From:*Lars Noschinski

**Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails***From:*Tobias Nipkow

**Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails***From:*Florian Haftmann

- Previous by Date: [isabelle] CFP : 2nd International Workshop on Engineering Safety and Security Systems (ESSS)
- Next by Date: [isabelle] Follow-up [Re: Isabelle operator precedence]
- Previous by Thread: [isabelle] CFP : 2nd International Workshop on Engineering Safety and Security Systems (ESSS)
- 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