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 ⟧ ⟹ (T1→T2) <:: (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