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.