Theory System_F

theory System_F
  imports Main
begin

datatype dty =
    TyVar nat
  | TyArr dty dty
  | TyAll dty

datatype dtm =
    TmVar nat
  | TmApp dtm dtm
  | TmLam dty dtm
  | TmTAbs dtm
  | TmTApp dtm dty

fun ty_shift :: "nat ⇒ dty ⇒ dty" where
  "ty_shift k (TyVar n) =
    (if n < k then TyVar n else TyVar (Suc n))"
| "ty_shift k (TyArr A B) = TyArr (ty_shift k A) (ty_shift k B)"
| "ty_shift k (TyAll A) = TyAll (ty_shift (Suc k) A)"

fun ty_subst :: "nat ⇒ dty ⇒ dty ⇒ dty" where
  "ty_subst k S (TyVar n) =
    (if n < k then TyVar n else
      if n = k then S else TyVar (n - 1))"
| "ty_subst k S (TyArr A B) =
    TyArr (ty_subst k S A) (ty_subst k S B)"
| "ty_subst k S (TyAll A) =
    TyAll (ty_subst (Suc k) (ty_shift 0 S) A)"

definition ty_subst0 :: "dty ⇒ dty ⇒ dty"
where
  "ty_subst0 S A = ty_subst 0 S A"

fun tm_shift :: "nat ⇒ dtm ⇒ dtm" where
  "tm_shift k (TmVar n) =
    (if n < k then TmVar n else TmVar (Suc n))"
| "tm_shift k (TmApp M N) = TmApp (tm_shift k M) (tm_shift k N)"
| "tm_shift k (TmLam A M) = TmLam A (tm_shift (Suc k) M)"
| "tm_shift k (TmTAbs M) = TmTAbs (tm_shift k M)"
| "tm_shift k (TmTApp M A) = TmTApp (tm_shift k M) A"

fun tm_ty_shift :: "nat ⇒ dtm ⇒ dtm" where
  "tm_ty_shift k (TmVar n) = TmVar n"
| "tm_ty_shift k (TmApp M P) =
    TmApp (tm_ty_shift k M) (tm_ty_shift k P)"
| "tm_ty_shift k (TmLam A M) =
    TmLam (ty_shift k A) (tm_ty_shift k M)"
| "tm_ty_shift k (TmTAbs M) =
    TmTAbs (tm_ty_shift (Suc k) M)"
| "tm_ty_shift k (TmTApp M A) =
    TmTApp (tm_ty_shift k M) (ty_shift k A)"

fun tm_subst :: "nat ⇒ dtm ⇒ dtm ⇒ dtm" where
  "tm_subst k N (TmVar n) =
    (if n < k then TmVar n else
      if n = k then N else TmVar (n - 1))"
| "tm_subst k N (TmApp M P) =
    TmApp (tm_subst k N M) (tm_subst k N P)"
| "tm_subst k N (TmLam A M) =
    TmLam A (tm_subst (Suc k) (tm_shift 0 N) M)"
| "tm_subst k N (TmTAbs M) =
    TmTAbs (tm_subst k (tm_ty_shift 0 N) M)"
| "tm_subst k N (TmTApp M A) =
    TmTApp (tm_subst k N M) A"

definition tm_subst0 :: "dtm ⇒ dtm ⇒ dtm"
where
  "tm_subst0 N M = tm_subst 0 N M"

fun tm_ty_subst :: "nat ⇒ dty ⇒ dtm ⇒ dtm" where
  "tm_ty_subst k S (TmVar n) = TmVar n"
| "tm_ty_subst k S (TmApp M N) =
    TmApp (tm_ty_subst k S M) (tm_ty_subst k S N)"
| "tm_ty_subst k S (TmLam A M) =
    TmLam (ty_subst k S A) (tm_ty_subst k S M)"
| "tm_ty_subst k S (TmTAbs M) =
    TmTAbs (tm_ty_subst (Suc k) (ty_shift 0 S) M)"
| "tm_ty_subst k S (TmTApp M A) =
    TmTApp (tm_ty_subst k S M) (ty_subst k S A)"

definition tm_ty_subst0 :: "dty ⇒ dtm ⇒ dtm"
where
  "tm_ty_subst0 S M = tm_ty_subst 0 S M"

definition ty_env_cons :: "'a ⇒ (nat ⇒ 'a) ⇒ nat ⇒ 'a"
where
  "ty_env_cons C ρ n = (case n of 0 ⇒ C | Suc k ⇒ ρ k)"

definition tm_env_cons :: "dtm ⇒ (nat ⇒ dtm) ⇒ nat ⇒ dtm"
where
  "tm_env_cons N δ n = (case n of 0 ⇒ N | Suc k ⇒ δ k)"

definition tm_env_shift :: "(nat ⇒ dtm) ⇒ nat ⇒ dtm"
where
  "tm_env_shift δ n =
    (case n of 0 ⇒ TmVar 0 | Suc k ⇒ tm_shift 0 (δ k))"

fun tm_subst_env :: "(nat ⇒ dtm) ⇒ dtm ⇒ dtm" where
  "tm_subst_env δ (TmVar k) = δ k"
| "tm_subst_env δ (TmApp M N) =
    TmApp (tm_subst_env δ M) (tm_subst_env δ N)"
| "tm_subst_env δ (TmLam A M) =
    TmLam A (tm_subst_env (tm_env_shift δ) M)"
| "tm_subst_env δ (TmTAbs M) = TmTAbs (tm_subst_env δ M)"
| "tm_subst_env δ (TmTApp M A) =
    TmTApp (tm_subst_env δ M) A"

inductive wf_ty :: "nat ⇒ dty ⇒ bool" where
  wf_var: "n < k ⟹ wf_ty k (TyVar n)"
| wf_arr: "⟦wf_ty k A; wf_ty k B⟧ ⟹
    wf_ty k (TyArr A B)"
| wf_all: "wf_ty (Suc k) A ⟹ wf_ty k (TyAll A)"

inductive ctx_mem :: "dty list ⇒ nat ⇒ dty ⇒ bool" where
  ctx_zero: "ctx_mem (A # Γ) 0 A"
| ctx_suc: "ctx_mem Γ k A ⟹ ctx_mem (B # Γ) (Suc k) A"

inductive typing :: "nat ⇒ dty list ⇒ dtm ⇒ dty ⇒ bool"
  (‹_ ; _ ⊢ _ : _› [60,60,60,60] 60) where
  ty_var: "ctx_mem Γ n A ⟹ typing k Γ (TmVar n) A"
| ty_app: "⟦typing k Γ M (TyArr A B); typing k Γ N A⟧
    ⟹ typing k Γ (TmApp M N) B"
| ty_lam: "⟦wf_ty k A; typing k (A # Γ) M B⟧
    ⟹ typing k Γ (TmLam A M) (TyArr A B)"
| ty_tabs: "typing (Suc k) (map (ty_shift 0) Γ) M B
    ⟹ typing k Γ (TmTAbs M) (TyAll B)"
| ty_tapp: "⟦typing k Γ M (TyAll B); wf_ty k A⟧
    ⟹ typing k Γ (TmTApp M A) (ty_subst0 A B)"

inductive beta :: "dtm ⇒ dtm ⇒ bool"
  (‹_ ⟶⇩β _› [80,80] 80) where
  beta_appL: "M ⟶⇩β M' ⟹
    TmApp M N ⟶⇩β TmApp M' N"
| beta_appR: "N ⟶⇩β N' ⟹
    TmApp M N ⟶⇩β TmApp M N'"
| beta_lam: "M ⟶⇩β M' ⟹
    TmLam A M ⟶⇩β TmLam A M'"
| beta_tabs: "M ⟶⇩β M' ⟹
    TmTAbs M ⟶⇩β TmTAbs M'"
| beta_tapp: "M ⟶⇩β M' ⟹
    TmTApp M A ⟶⇩β TmTApp M' A"
| beta_term: "TmApp (TmLam A M) N ⟶⇩β tm_subst0 N M"
| beta_type: "TmTApp (TmTAbs M) A ⟶⇩β tm_ty_subst0 A M"

inductive SN :: "dtm ⇒ bool" where
  SN_intro: "(⋀M'. M ⟶⇩β M' ⟹ SN M') ⟹ SN M"

end