# Re: [isabelle] Isar syntax question

On 17.07.2014 00:00, Vadim Zaliva wrote:
> 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
Have a look ath the proof state after "proof (rule ccontr)". The
precondition is "~~ something". Your assumption "something" does not
unify with this, so you get an error message as soon as you try to
discharge a proof obligation with show (or thus).
(Actually, it would be nice if the system would actually warn you about
this probable error at the assume statement).
You can either assume "~~something", or -- which is nicer -- do not use
the rule "ccontr" here. You just need "notI" (which is actually the
default rule, so changing line 3 to just "proof" should make everything
go through).
> 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
The important difference is not the split into hence/thus (which is
indeed entirely unnecessary), but "proof (rule ccontr)" vs just "proof"
(which is equivalent here to "proof (rule notI)".
Have a look at both rules by doing "print_statement ccontr notI".
Best regards, Lars

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