[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.