Re: [isabelle] Isar syntax question


Am Mittwoch, den 16.07.2014, 15:00 -0700 schrieb Vadim Zaliva:
> I am learning Isar and have another naive question on the syntax:
> I am trying to do something like this in Isar:
> 1: lemma
> 2:   shows "not something"
> 3: proof(rule ccontr)
> 4:  assume "something"
> 5:  thus False proof cases
> 6: 	...
> 7:   qed
> 8: qed
> and get "*** Failed to refine any pending goal" error around line 5
> Why this does not work? Something like this works instead:
> lemma
>   shows "not something"
> proof
>  assume "something" 
>  hence False proof cases
>  	...
>    qed
>   thus False by simp
> qed

it would be very helpful, especially for beginners, but often also for
me, if a "proof" would tell us what rule it applied – similar to how
"also" tells us what the current calculation is.

(And while are are at it: "also" could also tell us what rule it

Such features give great insight into the system and give the users more
confidence in using it.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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