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)