[isabelle] simple proof question



Hi all,

I'm trying to write a simple proof in Isabelle, but I'm a little lost. I
wonder if anyone can help me please? I've attached the script I have so
far.

At the point at which I am stuck, I have
    using this:
        (EBool bool_, t) : STyping
and I want to show that "t = TBool", which must be true as
    STypingBool: "forall (b :: bool) ==> STyping (EBool b, TBool)"
is the only constructor matching that pattern. My best guess was
    proof (cases this)
but that says
    *** empty result sequence -- proof command failed
    *** At command "proof".
Can anyone give me a pointer in the right direction please?


I'm also not sure why I can't do
    apply simpl
immediately after
    case EBool
? My goal here was to try to get "principalType (EBool bool)" to reduce.


Finally, I'd also be very interested to know if the general structure
looks sensible, or if there would be a more sensible way to write this
sort of proof.


Thanks
Ian

theory Simple
imports Main
begin

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

datatype SType = TBool
               | TInt

inductive STyping :: "(SExpr * SType) => bool" where
    STypingBool:        "forall (b :: bool) ==> STyping (EBool b, TBool)"
  | STypingInt:         "forall (n :: int) ==> STyping (EInt n, TInt)"
  | STypingIfThenElse:  "[| STyping (guard, TBool);
                            STyping (exprTrue, t);
                            STyping (exprFalse, t) |]
                         ==> STyping (EIfThenElse guard exprTrue exprFalse, t)"
  | STypingGreaterThan: "[| STyping (lhs, TInt);
                            STyping (rhs, TInt) |]
                         ==> STyping (EGreaterThan lhs rhs, TBool)"
  | STypingBoolToInt:   "STyping (b, TBool)
                         ==> STyping (EBoolToInt b, TInt)"

fun principalType :: "SExpr => SType option"
    where "principalType (EBool b) = Some TBool"
        | "principalType (EInt n) = Some TInt"
        | "principalType (EIfThenElse guard exprTrue exprFalse)
               = (case (principalType guard, principalType exprTrue, principalType exprFalse) of
                  (Some TBool, Some t1, Some t2) =>
                      if t1 = t2 then Some t1 else None
                | _ => None)"
        | "principalType (EGreaterThan lhs rhs)
               = (case (principalType lhs, principalType rhs) of
                  (Some TInt, Some TInt) => Some TBool
                | _ => None)"
        | "principalType (EBoolToInt b)
               = (case principalType b of
                  Some TBool => Some TInt
                | _ => None)"

lemma "((e, t) \<in> STyping) ==> (principalType e = Some t)"
proof (induct e)
    case EBool
        from this have "t = TBool"
(*
The next line gives:
*** empty result sequence -- proof command failed
*** At command "proof".
*)
        proof (cases this)


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