*To*: Buday Gergely <gbuday at karolyrobert.hu>*Subject*: Re: [isabelle] writing an Isar proof for multiple subgoals*From*: Jason Dagit <dagitj at gmail.com>*Date*: Tue, 14 Jul 2015 10:30:53 -0700*Cc*: Lars Noschinski <noschinl at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <C32D3449D568C445AB18C60817FABFE10144D5B2577A@ingrid.foiskola.krf>*References*: <C32D3449D568C445AB18C60817FABFE10144D5B25774@ingrid.foiskola.krf> <55A3AF39.40800@in.tum.de> <C32D3449D568C445AB18C60817FABFE10144D5B2577A@ingrid.foiskola.krf>

On Tue, Jul 14, 2015 at 2:19 AM, Buday Gergely <gbuday at karolyrobert.hu> wrote: > 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 > > -- > How did you get isabelle to show you the types? I've been searching for a way to get this information while using jEdit (without having to C-hover). The problems I have with C-hover are: * it's slow to popup * if you need to see the types of multiple terms it's flaky (once it disappears it can be hard to make it appear again) * it's hard for me to hold down a control key while also positioning the mouse just right. You can't position the mouse ahead of time because the control has to be down when the mouse moves for the hover to begin. * if you are trying to compare two complicated types for a small difference it's frustrating that you can't see them on the screen at the same time. I end up copying and pasting both types from the popup windows into my buffer to look a them.

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

**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] Auto has to be invoked twice to succeed
- Next by Date: Re: [isabelle] writing an Isar proof for multiple subgoals
- 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