# Re: [isabelle] Isar syntax question

On 17.07.2014 00:49, Vadim Zaliva wrote:
> On Jul 16, 2014, at 15:12 , Lars Noschinski <noschinl at in.tum.de> wrote:
>
>> 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).
> Thanks! That helps. The reason I used "something" instead of "~~something"
> in the assumption is to be able to use simpler cases syntax as my "something"
> is inductive definition:
>
> inductive something :: .... where
> C1: ... |
> C2: ...
>
> If I am proving "something" I can write "proof cases". If I proving ~~something
> I have to write proof (cases something).
As a side remark, if you are doing "unstructured" case analysis (i.e.,
there is not directly a rule matching your goal/assumptions and the
desired analysis), one way to write this is the following:
{ assume P1
have Q ... }
moreover
{ assume P2
have Q ...}
moreover
{ assume P3
have Q ...}
ultimately
have Q ...
Usually, blast or metis is then a good method to discharge the final
obligation.

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