Re: [isabelle] Isar syntax question



I agree. If I remember correctly, a crude form of that is provided by the rule_trace option.

Joachim Breitner <breitner at kit.edu> schrieb:

>Hi,
>
>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
>used...)
>
>Such features give great insight into the system and give the users more
>confidence in using it.
>
>Greetings,
>Joachim
>
>-- 
>Dipl.-Math. Dipl.-Inform. Joachim Breitner
>Wissenschaftlicher Mitarbeiter
>http://pp.ipd.kit.edu/~breitner


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