Theory InterTypeSystem

section "Declarative semantics as a type system"

theory InterTypeSystem
  imports Lambda
begin

datatype ty = TNat nat | TFun funty
    and funty = TArrow ty ty (infix "" 55) | TInt funty funty (infix "" 56) | TTop ("")

inductive subtype :: "ty  ty  bool" (infix "<:" 52) 
  and fsubtype :: "funty  funty  bool" (infix "<::" 52) where
  sub_refl: "A <: A" |
  sub_funty[intro!]: "f1 <:: f2  TFun f1 <: TFun f2" | 
  sub_fun[intro!]: " T1 <: T1'; T1' <: T1; T2 <: T2'; T2' <: T2   (T1T2) <:: (T1'T2')" |
  sub_inter_l1[intro!]: "T1  T2 <:: T1" |
  sub_inter_l2[intro!]: "T1  T2 <:: T2" |
  sub_inter_r[intro!]: " T3 <:: T1; T3 <:: T2   T3 <:: T1  T2" |
  sub_fun_top[intro!]: "T1  T2 <:: " |
  sub_top_top[intro!]: " <:: " |
  fsub_refl[intro!]: "T <:: T" |
  sub_trans[trans]: " T1 <:: T2; T2 <:: T3   T1 <:: T3"

definition ty_eq  :: "ty  ty  bool" (infix "" 50) where
  "A  B  A <: B  B <: A"
definition fty_eq :: "funty  funty  bool" (infix "" 50) where
  "F1  F2  F1 <:: F2  F2 <:: F1"
  
type_synonym tyenv = "(name × ty) list"

inductive wt :: "tyenv  exp  ty  bool" ("_  _ : _" [51,51,51] 51) where
  wt_var[intro!]: "lookup Γ x = Some T  Γ  EVar x : T" |
  wt_nat[intro!]: "Γ  ENat n : TNat n" |
  wt_lam[intro!]: " (x,A)#Γ  e : B   Γ  ELam x e : TFun (A  B)" |
  wt_app[intro!]: " Γ  e1 : TFun (A  B); Γ  e2 : A   Γ  EApp e1 e2 : B" |
  wt_top[intro!]: "Γ  ELam x e : TFun " |
  wt_inter[intro!]: " Γ  ELam x e : TFun A; Γ  ELam x e : TFun B  
        Γ  ELam x e : TFun (A  B)" |
  wt_sub[intro!]: " Γ  e : A; A <: B   Γ  e : B" |
  wt_prim[intro!]: " Γ  e1 : TNat n1; Γ  e2 : TNat n2 
        Γ  EPrim f e1 e2 : TNat (f n1 n2)" |
  wt_ifz[intro!]: " Γ  e1 : TNat 0; Γ  e3 : B  
        Γ  EIf e1 e2 e3 : B" |
  wt_ifnz[intro!]: " Γ  e1 : TNat n; n  0; Γ  e2 : B 
      Γ  EIf e1 e2 e3 : B"

end