Re: [isabelle] simple proof question



Hi Tobias,

On Fri, Aug 13, 2010 at 09:42:23AM +0200, Tobias Nipkow wrote:
> 
> outermost universal quantifiers can and should
> be dropped. Just write "STyping (EBool b, TBool)".

Aha, thanks!

> inductive_cases STypingE[elim!]:
>   "STyping (EBool b, t)"
> 
> The resulting lemma STypingE is what you need. The magic "[elim!]" tells
> auto and blast and friends to apply this rule eagerly. Now your proof
> should just be
> 
> from this have "t = TBool" by auto

Do you mean like this?:

lemma "((e, t) \<in> STyping) ==> (principalType e = Some t)"
proof (induct e)
    case EBool
        from this have "t = TBool" by auto

If so, the "by auto" fails with:

    *** Failed to finish proof
    *** At command "by".


Thanks
Ian






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