[isabelle] Proof state in Isar proof style are difficult to follow



Hi

I was used to ML proof style and now I am trying to learn the isar mode.
But I found it very hard to follow. I am not sure whether this is normal
or I am missing something:

Let me explain this with this example taken from the ?Structured Proofs in
Isar/HOL? document:

lemma assumes ex: "EX x. ALL y. P x y" shows "ALL y. EX x. P x y"
proof
  fix a
  from ex obtain x where "ALL y. P x y" ..
  hence "P x a" ..
  thus "EX x. P x a" ..
qed

Proof starts with a nice display of the proof state (with every thing I
need):

proof (state): step 1
fixed variables: P
prems:
  EX x. ALL y. P x y
goal (lemma, 1 subgoal):
 1. !!y. EX x. P x y

But things go differently
1. When I do ?fix a? for  the variable ?y? in the goal,
I get the equality a = a in the ?fixed variables? section.

proof (state): step 2

fixed variables: P, a = a
prems:
  EX x. ALL y. P x y

goal (lemma, 1 subgoal):
 1. !!y. EX x. P x y

However I was expecting ?y = a? instead.

2. At the second step (from ex obtain ?) the display becomes difficult to
follow:
a) execution of ?from ex? gives:

proof (chain): step 3

picking this:
  EX x. ALL y. P x y

(no thing shown about the rest of the state)

b) execution of all the 'from' step returns
have (!!x. ALL y. P x y ==> ?thesis) ==> ?thesis
Every thing is hided.

The same thing happens with proof steps starting ?have?.

How one can see what goals remain to be proved?

This kind of displays confuses me.

Best regards







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