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