(* :encoding=utf-8: *)

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 \<Longrightarrow> STyping rhs TInt \<Longrightarrow>
        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"
  by (induct e arbitrary: t)
    (auto simp: STyping.intros split: option.splits SType.splits)

lemma "principalType e = Some t ==> STyping e t"
proof (induct e arbitrary: t)
  case (EBool b)
  then show ?case
    by (simp add: STyping.intros)
next
  case (EInt n)
  then show ?case
    by (simp add: STyping.intros)
next
  case (EGreaterThan lhs rhs)
  then show ?case
    by (auto simp: STyping.intros split: option.splits SType.splits)
qed

lemma "principalType e = Some t ==> STyping e t"
proof (induct e arbitrary: t)
  case (EBool b)
  then have "t = TBool" by simp
  also have "STyping (EBool b) TBool" ..
  finally show "STyping (EBool b) t" .
next
  case (EInt n)
  then have "t = TInt" by simp
  also have "STyping (EInt n) TInt" ..
  finally show "STyping (EInt n) t" .
next
  case (EGreaterThan lhs rhs)
  have *: "principalType (EGreaterThan lhs rhs) = Some t" by fact
  show "STyping (EGreaterThan lhs rhs) t"
  proof (cases t)
    case TBool
    have "STyping lhs TInt"
    proof (rule EGreaterThan.hyps)
      from TBool and * show "principalType lhs = Some TInt"
        by (simp split: option.splits SType.splits)
    qed
    moreover
    have "STyping rhs TInt"
    proof (rule EGreaterThan.hyps)
      from TBool and * show "principalType rhs = Some TInt"
        by (simp split: option.splits SType.splits)
    qed
    ultimately have "STyping (EGreaterThan lhs rhs) TBool" ..
    then show ?thesis by (simp only: TBool)
  next
    case TInt
    with * have False by (simp split: option.splits SType.splits)
    then show ?thesis ..
  qed
qed

end