# [isabelle] stuck on proof

```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

```
```theory Simple
imports Main
begin

datatype SExpr = EBool bool
| EInt int
| EGreaterThan SExpr SExpr

datatype SType = TBool
| TInt

inductive STyping :: "SExpr => SType => bool" where
STypingBool:        "STyping (EBool b) TBool"
| STypingInt:         "STyping (EInt n) TInt"
| STypingGreaterThan: "[| STyping lhs TInt;
STyping rhs TInt |]
==> STyping (EGreaterThan lhs rhs) TBool"

fun principalType :: "SExpr => SType option"
where "principalType (EBool b) = Some TBool"
| "principalType (EInt n) = Some TInt"
| "principalType (EGreaterThan lhs rhs)
= (case (principalType lhs, principalType rhs) of
(Some TInt, Some TInt) => Some TBool
| _ => None)"

lemma "(principalType e = Some t) ==> (STyping e t)"
proof (cases e)
case EBool
apply_end simp
from "STypingBool"
show "!!b. STyping (EBool b) TBool"
apply simp .
next
case (EInt n)
fix n
assume "principalType (EInt n) = Some t"
then have x : "principalType (EInt n) = Some TInt" by simp
show ?thesis
assume "t = TInt"
then have "principalType (EInt int) = Some TInt" by simp
show ?thesis

have "t = TInt"

show ?thesis
have x : "principalType e = Some TInt" sorry
have "t = TInt"
with x show ?thesis
fix x
assume x : "principalType e = Some t"
assume y : "e = EInt n"
thus ?thesis by simp
show ?thesis
apply_end simp
fix x
thus ?thesis by simp
from "STypingInt"
show "!!int. STyping (EInt bool) TInt"
apply simp .
next
case EGreaterThan
sorry
qed

```

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