# Re: [isabelle] simple proof question

On Fri, Aug 13, 2010 at 01:37:12PM +0200, Tobias Nipkow wrote:
> My mistake: I didn't run it. Your mistake: you had phrased the theorem
> as "... : STyping" but the rules as "STyping ...". Don't mix the two
> notations, it complicates your life. Either set or predicate.
Aha, thanks!
> Concerning your overall proof strategy, I recommend rule induction on
> STyping:
>
> proof(induct rule: STyping.induct)
>
> That takes care of all the case distinctins you were going to do by hand.
Hmm, that gives me:
1. !!b. principalType e = Some t
which doesn't look provable to me. And there's also:
3. !!guard exprTrue ta exprFalse.
[| STyping (guard, TBool); principalType e = Some t;
STyping (exprTrue, ta); principalType e = Some t;
STyping (exprFalse, ta); principalType e = Some t |]
==> principalType e = Some t
but the t's shouldn't all be the same.
Thanks
Ian

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