Re: [isabelle] simple proof question
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)".
> 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)
from this have "t = TBool" by auto
If so, the "by auto" fails with:
*** Failed to finish proof
*** At command "by".
This archive was generated by a fusion of
Pipermail (Mailman edition) and