*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] writing an Isar proof for multiple subgoals*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Tue, 14 Jul 2015 20:09:38 +0200*In-reply-to*: <C32D3449D568C445AB18C60817FABFE10144D5B2577A@ingrid.foiskola.krf>*References*: <C32D3449D568C445AB18C60817FABFE10144D5B25774@ingrid.foiskola.krf> <55A3AF39.40800@in.tum.de> <C32D3449D568C445AB18C60817FABFE10144D5B2577A@ingrid.foiskola.krf>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.7.0

On 14.07.2015 11:19, Buday Gergely wrote: > I have a problem proving the third subgoal: > > lemma "â (P::bool) (x::lam). (â xa. x = xa â P) â P" > proof - > fix P x assume "â xa. x = xa â P" show P by auto > > Isabelle tells me > > show Pâbool > Successful attempt to solve goal by exported rule: > (âxaâ?'aâtype. (?x2â?'aâtype) = xa â ?P2âbool) â ?P2 > proof (state): depth 0 > > this: > Pâbool This tells you that the show statement can discharge one of the subgoals ... > > goal: > No subgoals! > Failed to apply initial proof method: > goal (1 subgoal): > 1. P > variables: > P :: bool ... but auto failed to solve it. Notice the suspicious lack of "!!xa. x = xa" in the second part? That is because you did not feed the assumption into the show statement (which you could do e.g. using "then"). -- Lars

**Follow-Ups**:**Re: [isabelle] writing an Isar proof for multiple subgoals***From:*Gergely Buday

**References**:**[isabelle] writing an Isar proof for multiple subgoals***From:*Buday Gergely

**Re: [isabelle] writing an Isar proof for multiple subgoals***From:*Lars Noschinski

**Re: [isabelle] writing an Isar proof for multiple subgoals***From:*Buday Gergely

- Previous by Date: Re: [isabelle] writing an Isar proof for multiple subgoals
- Next by Date: Re: [isabelle] Destruction rules setup
- Previous by Thread: Re: [isabelle] writing an Isar proof for multiple subgoals
- Next by Thread: Re: [isabelle] writing an Isar proof for multiple subgoals
- 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