*To*: Lars Noschinski <noschinl at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] writing an Isar proof for multiple subgoals*From*: Buday Gergely <gbuday at karolyrobert.hu>*Date*: Tue, 14 Jul 2015 11:19:34 +0200*Accept-language*: en-US, hu-HU*Acceptlanguage*: en-US, hu-HU*In-reply-to*: <55A3AF39.40800@in.tum.de>*References*: <C32D3449D568C445AB18C60817FABFE10144D5B25774@ingrid.foiskola.krf> <55A3AF39.40800@in.tum.de>*Thread-index*: AdC9aAVJRnPKERO3TtSOQk/HPN+bngArQfYw*Thread-topic*: [isabelle] writing an Isar proof for multiple subgoals

Lars Noschinski wrote: > show "eqvt simple4_graph_aux" ... > next > fix x y assume "simple4_graph x y" show True ... > next > fix P y assume "!!x. y = x ==> P" show P ... > ... I know this is trivial with automatic methods but I need to learn Isar. 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 goal: No subgoals! Failed to apply initial proof method: goal (1 subgoal): 1. P variables: P :: bool -- Why is this an error when it says No subgoals! ? Isabelle/jEdit does not let me finish the proof with qed. - Gergely

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

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

- Previous by Date: Re: [isabelle] Reflexive rewriting
- Next by Date: [isabelle] Auto has to be invoked twice to succeed
- 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