Re: [isabelle] writing an Isar proof for multiple subgoals

On Tue, Jul 14, 2015 at 2:19 AM, Buday Gergely <gbuday at>

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.