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.