*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] writing an Isar proof for multiple subgoals*From*: Gergely Buday <gbuday at gmail.com>*Date*: Fri, 17 Jul 2015 10:56:19 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <55A55062.2030307@in.tum.de>*References*: <C32D3449D568C445AB18C60817FABFE10144D5B25774@ingrid.foiskola.krf> <55A3AF39.40800@in.tum.de> <C32D3449D568C445AB18C60817FABFE10144D5B2577A@ingrid.foiskola.krf> <55A55062.2030307@in.tum.de>

On 14 July 2015 at 20:09, Lars Noschinski <noschinl at in.tum.de> wrote: > 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 >> ... >> 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"). nominal_function simple5 :: "lam â lam" where "simple5 x = x" proof - show "eqvt simple5_graph_aux" by (simp add: eqvt_def simple5_graph_aux_def) next fix x y assume "simple5_graph x y" show True by auto next fix P x assume "â xa . x = xa â P" then show P by simp next fix x xa assume "x = xa" from this show "x = xa" by assumption qed proves the lemma. One thing is not clear: I get exclamation marks aside on the last two assumption: after assume "â xa . x = xa â P" Introduced fixed type variable(s): 'a in "x__" and after assume "x = xa" Introduced fixed type variable(s): 'a in "x__" or "xa__" I guess I can ignore these for now but when could this be significant? - Gergely

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

**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

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

- Previous by Date: Re: [isabelle] writing an Isar proof for multiple subgoals
- Next by Date: [isabelle] AVoCS 2015: Joint Call for Research Idea Papers & Participation
- 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