Re: [isabelle] Isar syntax question



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).

I do not know what is involved implementation-wiser but it would be nice if Isabelle could deal with 
trivial double negation during unification.

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva





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