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

```