Ian Lynagh

2010-08-17 07:22:03 UTC

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

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