Theory System_F_Normalization

theory System_F_Normalization
  imports System_F_Erasure
begin

definition f_env_ok :: "(nat ⇒ ulam set) ⇒ bool" where
  "f_env_ok ρ ⟷ (∀k. ucandidate (ρ k))"

definition f_all_sem :: "(ulam set ⇒ ulam set) ⇒ ulam set" where
  "f_all_sem F = {M. ∀C. ucandidate C ⟶ M ∈ F C}"

lemma f_all_candidate:
  assumes H: "∀C. ucandidate C ⟶ ucandidate (F C)"
  shows "ucandidate (f_all_sem F)"
proof (unfold ucandidate_def, intro conjI)
  show "uCR1 (f_all_sem F)"
    unfolding uCR1_def f_all_sem_def
    using H uSN_set_candidate
    unfolding ucandidate_def uCR1_def
    by blast
next
  show "uCR2 (f_all_sem F)"
    unfolding uCR2_def f_all_sem_def
    using H
    unfolding ucandidate_def uCR2_def
    by blast
next
  show "uCR3 (f_all_sem F)"
    unfolding uCR3_def f_all_sem_def
    using H
    unfolding ucandidate_def uCR3_def
    by blast
qed

definition f_env_insert ::
  "nat ⇒ ulam set ⇒ (nat ⇒ ulam set) ⇒
    nat ⇒ ulam set"
where
  "f_env_insert k C ρ n =
    (if n < k then ρ n else
      if n = k then C else ρ (n - 1))"

lemma f_env_insert_zero:
  "f_env_insert 0 C ρ = ty_env_cons C ρ"
proof (rule ext)
  fix x
  show "f_env_insert 0 C ρ x = ty_env_cons C ρ x"
  proof (cases x)
    case 0
    then show ?thesis
      by (simp add: f_env_insert_def ty_env_cons_def)
  next
    case (Suc n)
    then show ?thesis
      by (simp add: f_env_insert_def ty_env_cons_def split: if_splits)
qed
qed

lemma f_env_insert_suc_cons:
  "f_env_insert (Suc k) C (ty_env_cons D ρ) =
    ty_env_cons D (f_env_insert k C ρ)"
proof (rule ext)
  fix x
  show "f_env_insert (Suc k) C (ty_env_cons D ρ) x =
    ty_env_cons D (f_env_insert k C ρ) x"
  proof (induct x)
    case 0
    then show ?case
      by (simp add: f_env_insert_def ty_env_cons_def)
  next
    case (Suc n)
    then show ?case
    proof (cases n)
      case 0
      then show ?thesis
        by (simp add: f_env_insert_def ty_env_cons_def)
    next
      case (Suc m)
      then show ?thesis
        by (simp add: f_env_insert_def ty_env_cons_def
          split: if_splits; arith)
      qed
    qed
qed

lemma f_env_ok_cons:
  assumes "f_env_ok ρ" and "ucandidate C"
  shows "f_env_ok (ty_env_cons C ρ)"
  using assms
  unfolding f_env_ok_def ty_env_cons_def
  by (intro allI; case_tac k; simp_all)

fun f_sem :: "dty ⇒ (nat ⇒ ulam set) ⇒ ulam set" where
  "f_sem (TyVar k) ρ = ρ k"
| "f_sem (TyArr A B) ρ =
    uarr (f_sem A ρ) (f_sem B ρ)"
| "f_sem (TyAll A) ρ =
    f_all_sem (λC. f_sem A (ty_env_cons C ρ))"

lemma f_sem_candidate:
  "f_env_ok ρ ⟶ ucandidate (f_sem A ρ)"
proof (induct A arbitrary: ρ)
  case (TyVar k)
  then show ?case
    unfolding f_sem.simps f_env_ok_def ucandidate_def by blast
next
  case (TyArr A B)
  then show ?case
    by (auto intro: uarr_candidate)
next
  case (TyAll A)
  have body:
    "f_env_ok ρ ⟶
      (∀C. ucandidate C ⟶
        ucandidate (f_sem A (ty_env_cons C ρ)))"
    using TyAll(1)
    by (blast intro: f_env_ok_cons)
  then show ?case
    unfolding f_sem.simps
    by (intro impI; blast intro: f_all_candidate)
qed

lemma f_sem_ty_shift:
  "f_sem (ty_shift k A) (f_env_insert k C ρ) =
    f_sem A ρ"
proof (induct A arbitrary: k C ρ)
  case (TyVar n)
  then show ?case
    by (simp add: f_env_insert_def split: if_splits; arith)
next
  case (TyArr A B)
  then show ?case by simp
next
  case (TyAll A)
  have body_eq:
    "∀D. f_sem (ty_shift (Suc k) A)
        (ty_env_cons D (f_env_insert k C ρ)) =
      f_sem A (ty_env_cons D ρ)"
    using TyAll(1)
    by (simp add: f_env_insert_suc_cons[symmetric])
  show ?case
    using body_eq
    by (simp add: f_all_sem_def)
qed

lemma f_sem_ty_subst:
  "f_sem (ty_subst k S A) ρ =
    f_sem A (f_env_insert k (f_sem S ρ) ρ)"
proof (induct A arbitrary: k S ρ)
  case (TyVar n)
  then show ?case
    by (simp add: f_env_insert_def split: if_splits; arith)
next
  case (TyArr A B)
  then show ?case by simp
next
  case (TyAll A)
  have shift0:
    "∀D. f_sem (ty_shift 0 S) (ty_env_cons D ρ) =
      f_sem S ρ"
    using f_sem_ty_shift[of 0 S] f_env_insert_zero by simp
  have body_eq:
    "∀D. f_sem (ty_subst (Suc k) (ty_shift 0 S) A)
        (ty_env_cons D ρ) =
      f_sem A
        (ty_env_cons D (f_env_insert k (f_sem S ρ) ρ))"
    using TyAll(1)
    by (simp add: shift0 f_sem_ty_shift f_env_insert_zero
      f_env_insert_suc_cons)
  show ?case
    using body_eq
    by (simp add: f_all_sem_def)
qed

definition f_tenv_cons :: "ulam ⇒ (nat ⇒ ulam) ⇒
    nat ⇒ ulam"
where
  "f_tenv_cons N η n =
    (case n of 0 ⇒ N | Suc k ⇒ η k)"

definition f_tenv_shift :: "(nat ⇒ ulam) ⇒ nat ⇒ ulam"
where
  "f_tenv_shift η n =
    (case n of 0 ⇒ UVar 0 | Suc k ⇒ u_shift 0 (η k))"

definition f_env_subst ::
  "nat ⇒ ulam ⇒ (nat ⇒ ulam) ⇒
    nat ⇒ ulam"
where
  "f_env_subst k N η n = u_subst k N (η n)"

lemma f_env_subst_shift:
  "f_env_subst (Suc k) (u_shift 0 N) (f_tenv_shift η) =
    f_tenv_shift (f_env_subst k N η)"
proof (rule ext)
  fix n
  show "f_env_subst (Suc k) (u_shift 0 N) (f_tenv_shift η) n =
    f_tenv_shift (f_env_subst k N η) n"
  proof (induct n)
    case 0
    then show ?case
      by (simp add: f_env_subst_def f_tenv_shift_def)
  next
    case (Suc n)
    then show ?case
      by (simp add: f_env_subst_def f_tenv_shift_def
        u_shift_subst_comm)
  qed
qed

lemma f_env_subst_shift0:
  "f_env_subst 0 N (f_tenv_shift η) =
    f_tenv_cons N η"
proof (rule ext)
  fix n
  show "f_env_subst 0 N (f_tenv_shift η) n =
    f_tenv_cons N η n"
  proof (induct n)
    case 0
    then show ?case
      by (simp add: f_env_subst_def f_tenv_shift_def f_tenv_cons_def
        u_subst0_def)
  next
    case (Suc n)
    then show ?case
      by (simp add: f_env_subst_def f_tenv_shift_def f_tenv_cons_def
        u_subst0_def u_subst_shift)
  qed
qed

fun f_interp :: "(nat ⇒ ulam) ⇒ dtm ⇒ ulam" where
  "f_interp η (TmVar n) = η n"
| "f_interp η (TmApp M N) =
    UApp (f_interp η M) (f_interp η N)"
| "f_interp η (TmLam A M) =
    ULam (f_interp (f_tenv_shift η) M)"
| "f_interp η (TmTAbs M) = f_interp η M"
| "f_interp η (TmTApp M A) = f_interp η M"

lemma f_interp_subst:
  "u_subst k N (f_interp η M) =
    f_interp (f_env_subst k N η) M"
proof (induct M arbitrary: k N η rule: dtm.induct)
  case (TmVar n)
  then show ?case by (simp add: f_env_subst_def)
next
  case (TmApp M P)
  then show ?case by simp
next
  case (TmLam A M)
  then show ?case
    by (simp add: f_env_subst_shift)
next
  case (TmTAbs M)
  then show ?case by simp
next
  case (TmTApp M A)
  then show ?case by simp
qed

lemma f_tenv_shift_id:
  "f_tenv_shift (λn. UVar n) = (λn. UVar n)"
proof (rule ext)
  fix x :: nat
  show "f_tenv_shift (λn. UVar n) x = UVar x"
  proof (induct x)
    case 0
    then show ?case by (simp add: f_tenv_shift_def)
  next
    case (Suc n)
    then show ?case by (simp add: f_tenv_shift_def)
  qed
qed

lemma f_interp_id:
  "f_interp (λn. UVar n) M = f_erase M"
  by (induct M rule: dtm.induct)
     (simp_all add: f_tenv_shift_id)

lemma f_interp_subst0_shift:
  "u_subst0 N (f_interp (f_tenv_shift η) M) =
    f_interp (f_tenv_cons N η) M"
  using f_interp_subst[of 0 N "f_tenv_shift η" M]
    f_env_subst_shift0
  by (simp add: u_subst0_def)

definition f_tenv_ok ::
  "dty list ⇒ (nat ⇒ ulam) ⇒
    (nat ⇒ ulam set) ⇒ bool"
where
  "f_tenv_ok Γ η ρ ⟷
    (∀n A. ctx_mem Γ n A ⟶
      η n ∈ f_sem A ρ)"

lemma f_ctx_mem_mapE:
  "ctx_mem (map (ty_shift 0) Γ) n B ⟶
    (∃A. ctx_mem Γ n A ∧ B = ty_shift 0 A)"
proof (induct Γ arbitrary: n B)
  case Nil
  then show ?case by (auto elim: ctx_mem.cases)
next
  case (Cons A Γ)
  then show ?case
  proof (intro impI)
    assume h: "ctx_mem (map (ty_shift 0) (A # Γ)) n B"
    have h': "ctx_mem (ty_shift 0 A # map (ty_shift 0) Γ) n B"
      using h by simp
    then show "∃A'. ctx_mem (A # Γ) n A' ∧
      B = ty_shift 0 A'"
    proof (cases rule: ctx_mem.cases)
      case ctx_zero
      then show ?thesis
        by (auto intro: ctx_mem.ctx_zero)
    next
      case ctx_suc
      have h'':
        "ctx_mem (map (ty_shift 0) Γ) (n - 1) B"
        using ctx_suc(1) ctx_suc(2) by simp
      have ex:
        "∃A'. ctx_mem Γ (n - 1) A' ∧
          B = ty_shift 0 A'"
        using Cons(1)[of "n - 1" B] h'' by blast
      have ex':
        "∃A'. ctx_mem (A # Γ) (Suc (n - 1)) A' ∧
          B = ty_shift 0 A'"
        using ex by (blast intro: ctx_mem.ctx_suc)
      from ex' ctx_suc(1) show ?thesis by simp
    qed
  qed
qed

lemma f_tenv_ok_cons:
  assumes hctx: "f_tenv_ok Γ η ρ"
    and hval: "N ∈ f_sem A ρ"
  shows "f_tenv_ok (A # Γ) (f_tenv_cons N η) ρ"
  using assms
  unfolding f_tenv_ok_def
  by (auto simp add: f_tenv_cons_def elim: ctx_mem.cases)

lemma f_tenv_ok_ty_shift:
  assumes hctx: "f_tenv_ok Γ η ρ"
    and henv: "f_env_ok ρ"
    and hcan: "ucandidate C"
  shows "f_tenv_ok (map (ty_shift 0) Γ) η
    (ty_env_cons C ρ)"
proof (unfold f_tenv_ok_def, intro allI allI impI)
  fix n B
  assume memB: "ctx_mem (map (ty_shift 0) Γ) n B"
  have ex:
    "∃A. ctx_mem Γ n A ∧ B = ty_shift 0 A"
    using f_ctx_mem_mapE[of Γ n B] memB by blast
  have sh:
    "∀A. f_sem (ty_shift 0 A) (ty_env_cons C ρ) =
      f_sem A ρ"
    using f_sem_ty_shift[of 0] f_env_insert_zero by simp
  have sem:
    "∀A. ctx_mem Γ n A ⟶
      η n ∈ f_sem (ty_shift 0 A) (ty_env_cons C ρ)"
    using hctx sh unfolding f_tenv_ok_def by blast
  from ex sem show "η n ∈ f_sem B (ty_env_cons C ρ)"
    by blast
qed

definition f_prop ::
  "dty list ⇒ dtm ⇒ dty ⇒ bool"
where
  "f_prop Γ M A ⟷
    (∀ρ η.
      f_env_ok ρ ⟶
      f_tenv_ok Γ η ρ ⟶
      f_interp η M ∈ f_sem A ρ)"

lemma f_fundamental:
  "typing k Γ M A ⟹ f_prop Γ M A"
proof (induct rule: typing.induct)
  case ty_var
  then show ?case
    unfolding f_prop_def f_interp.simps f_sem.simps f_tenv_ok_def
    by blast
next
  case ty_app
  then show ?case
    unfolding f_prop_def f_interp.simps f_sem.simps uarr_def
    by blast
next
  case (ty_lam k0 A0 G0 M0 B0)
  show ?case
    unfolding f_prop_def f_interp.simps f_sem.simps
  proof (intro allI allI impI impI)
    fix ρ η
    assume env: "f_env_ok ρ"
    assume ctx: "f_tenv_ok G0 η ρ"
    have Ccan: "ucandidate (f_sem A0 ρ)"
      using f_sem_candidate[of ρ A0] env by blast
    have Dcan: "ucandidate (f_sem B0 ρ)"
      using f_sem_candidate[of ρ B0] env by blast
    have body:
      "∀s. s ∈ f_sem A0 ρ ⟶
        u_subst0 s (f_interp (f_tenv_shift η) M0) ∈ f_sem B0 ρ"
    proof (intro allI impI)
      fix s
      assume sA: "s ∈ f_sem A0 ρ"
      have ctxs:
        "f_tenv_ok (A0 # G0) (f_tenv_cons s η) ρ"
        using f_tenv_ok_cons[OF ctx sA] .
      have ih:
        "f_interp (f_tenv_cons s η) M0 ∈ f_sem B0 ρ"
        using ty_lam(3) env ctxs
        unfolding f_prop_def by blast
      have eq:
        "u_subst0 s (f_interp (f_tenv_shift η) M0) =
          f_interp (f_tenv_cons s η) M0"
        using f_interp_subst0_shift by blast
      from ih show
        "u_subst0 s (f_interp (f_tenv_shift η) M0) ∈ f_sem B0 ρ"
        using eq by simp
    qed
    have abs:
      "ULam (f_interp (f_tenv_shift η) M0) ∈
        uarr (f_sem A0 ρ) (f_sem B0 ρ)"
      using Ccan Dcan body by (rule uabs_RED)
    then show "ULam (f_interp (f_tenv_shift η) M0) ∈
      uarr (f_sem A0 ρ) (f_sem B0 ρ)" .
  qed
next
  case (ty_tabs k0 G0 M0 B0)
  show ?case
    unfolding f_prop_def
  proof (intro allI allI impI impI)
    fix ρ η
    assume env: "f_env_ok ρ"
    assume ctx: "f_tenv_ok G0 η ρ"
    have all:
      "∀C. ucandidate C ⟶
        f_interp η M0 ∈ f_sem B0 (ty_env_cons C ρ)"
    proof (intro allI impI)
      fix C
      assume Ccan: "ucandidate C"
      have envC: "f_env_ok (ty_env_cons C ρ)"
        using f_env_ok_cons[OF env Ccan] .
      have ctxC:
          "f_tenv_ok (map (ty_shift 0) G0) η
          (ty_env_cons C ρ)"
        using f_tenv_ok_ty_shift[OF ctx env Ccan] .
      have ih:
        "f_interp η M0 ∈ f_sem B0 (ty_env_cons C ρ)"
        using ty_tabs(2) envC ctxC
        unfolding f_prop_def by blast
      from ih show "f_interp η M0 ∈ f_sem B0 (ty_env_cons C ρ)"
        by assumption
    qed
    show "f_interp η (TmTAbs M0) ∈ f_sem (TyAll B0) ρ"
      using all unfolding f_interp.simps f_sem.simps f_all_sem_def by blast
  qed
next
  case (ty_tapp k0 G0 M0 B0 A0)
  show ?case
    unfolding f_prop_def
  proof (intro allI allI impI impI)
    fix ρ η
    assume env: "f_env_ok ρ"
    assume ctx: "f_tenv_ok G0 η ρ"
    have ih:
      "f_interp η M0 ∈ f_sem (TyAll B0) ρ"
      using ty_tapp(2) env ctx
      unfolding f_prop_def by blast
    have Acan: "ucandidate (f_sem A0 ρ)"
      using f_sem_candidate[of ρ A0] env by blast
    have body:
      "f_interp η M0 ∈
        f_sem B0 (ty_env_cons (f_sem A0 ρ) ρ)"
      using ih Acan unfolding f_sem.simps f_all_sem_def by blast
    have sem_eq:
      "f_sem (ty_subst0 A0 B0) ρ =
        f_sem B0 (ty_env_cons (f_sem A0 ρ) ρ)"
      using f_sem_ty_subst[of 0 A0 B0 ρ] f_env_insert_zero
      by (simp add: ty_subst0_def)
    show "f_interp η (TmTApp M0 A0) ∈
      f_sem (ty_subst0 A0 B0) ρ"
      using body sem_eq by simp
  qed
qed

lemma f_identity_tenv_ok:
  "f_tenv_ok Γ (λn. UVar n) (λ_. uSN_set)"
proof (unfold f_tenv_ok_def, intro allI allI impI)
  fix n A
  assume "ctx_mem Γ n A"
  have can:
    "ucandidate (f_sem A (λ_. uSN_set))"
    using f_sem_candidate[of "(λ_. uSN_set)" A]
    by (simp add: f_env_ok_def uSN_set_candidate)
  from uvar_mem_candidate[OF can]
  show "UVar n ∈ f_sem A (λ_. uSN_set)" .
qed

lemma f_welltyped_fundamental:
  assumes "typing k Γ M A"
  shows "uSN (f_erase M)"
proof -
  have env: "f_env_ok (λ_. uSN_set)"
    unfolding f_env_ok_def
    by (simp add: uSN_set_candidate)
  have ctx:
    "f_tenv_ok Γ (λn. UVar n) (λ_. uSN_set)"
    using f_identity_tenv_ok .
  have sem:
    "f_interp (λn. UVar n) M ∈
      f_sem A (λ_. uSN_set)"
    using f_fundamental[OF assms] env ctx
    unfolding f_prop_def by blast
  have semM:
    "f_erase M ∈ f_sem A (λ_. uSN_set)"
    using sem f_interp_id by simp
  have can:
    "ucandidate (f_sem A (λ_. uSN_set))"
    using f_sem_candidate[of "(λ_. uSN_set)" A] env by blast
  from can semM show "uSN (f_erase M)"
    unfolding ucandidate_def uCR1_def by blast
qed

theorem strong_normalization:
  assumes "typing k Γ M A"
  shows "SN M"
  using fSN_reflect[OF f_welltyped_fundamental[OF assms]] .

end