Re: [isabelle] simple proof question



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. And if
predicate, then it is usually better to curry it.

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.

Tobias


Ian Lynagh schrieb:
> 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.