Re: [isabelle] stuck on proof



lemma "(principalType e = Some t) ==> (STyping e t)"
apply (induct e arbitrary: t)
apply (auto simp: STyping.intros split:option.splits SType.splits)
done

split: ... instructs auto (or simp) to split case expressions for
certain types automatically.

Tobias

Ian Lynagh schrieb:
> Hi all,
> 
> I'm stuck on a proof of
>     lemma "(principalType e = Some t) ==> (STyping e t)"
> (details in attachment). I've managed to solve the EBool case with
>     apply_end simp
>     from "STypingBool"
>     show "!!b. STyping (EBool b) TBool"
>         apply simp .
> but I don't think this is a good proof: I'm sure using "apply_end simp"
> is bad style, and I don't think I should be copy/pasting
> "!!b. STyping (EBool b) TBool" from the proof state. Even "apply simp"
> I'm not sure is good style.
> 
> I've therefore tried to write a better proof for the EInt case, but got
> nowhere. The attached script shows some of my meanderings.
> 
> Has anyone got any hints, please?
> 
> 
> I'm also not sure what's going to happen when I get to a recursive case.
> I suspect "proof (cases e)" is not sufficient for the recursive case,
> but "proof (induct e)" doesn't look like it's generating the right goal
> for the recursive case (as t doesn't vary), and
> "proof (induct rule: SExpr.induct)" has the same problem. Again, can
> anyone point me in the right direction please?
> 
> 
> Incidentally, in proof general, the "Isabelle/Show me .../Facts" menu
> says "C-c C-a <h> <f>" next to it, but after typing just "ctrl-c ctrl-a h"
> emacs says "C-c C-a h is undefined". Any idea what's wrong?
> 
> 
> Thanks
> Ian
> 
> 





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