# Theory StrongNorm

Up to index of Isabelle/HOL/Lambda

theory StrongNorm
imports Type InductTermi
begin

    (*  Title:      HOL/Lambda/StrongNorm.thy
        ID:         $Id: StrongNorm.thy,v 1.2 2005/06/17 14:13:08 haftmann Exp $
        Author:     Stefan Berghofer
        Copyright   2000 TU Muenchen
    *)

    header {* Strong normalization for simply-typed lambda calculus *}

    theory StrongNorm imports Type InductTermi begin

    text {*
    Formalization by Stefan Berghofer. Partly based on a paper proof by
    Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.
    *}

    subsection {* Properties of @{text IT} *}

    lemma lift_IT [intro!]: "t ∈ IT ==> (!!i. lift t i ∈ IT)"
      apply (induct set: IT)
        apply (simp (no_asm))
        apply (rule conjI)
         apply
          (rule impI,
           rule IT.Var,
           erule lists.induct,
           simp (no_asm),
           rule lists.Nil,
           simp (no_asm),
           erule IntE,
           rule lists.Cons,
           blast,
           assumption)+
         apply auto
       done

    lemma lifts_IT: "ts ∈ lists IT ==> map (λt. lift t 0) ts ∈ lists IT"
      by (induct ts) auto

    lemma subst_Var_IT: "r ∈ IT ==> (!!i j. r[Var i/j] ∈ IT)"
      apply (induct set: IT)
        txt {* Case @{term Var}: *}
        apply (simp (no_asm) add: subst_Var)
        apply
        ((rule conjI impI)+,
          rule IT.Var,
          erule lists.induct,
          simp (no_asm),
          rule lists.Nil,
          simp (no_asm),
          erule IntE,
          erule CollectE,
          rule lists.Cons,
          fast,
          assumption)+
       txt {* Case @{term Lambda}: *}
       apply atomize
       apply simp
       apply (rule IT.Lambda)
       apply fast
      txt {* Case @{term Beta}: *}
      apply atomize
      apply (simp (no_asm_use) add: subst_subst [symmetric])
      apply (rule IT.Beta)
       apply auto
      done

    lemma Var_IT: "Var n ∈ IT"
      apply (subgoal_tac "Var n °° [] ∈ IT")
       apply simp
      apply (rule IT.Var)
      apply (rule lists.Nil)
      done

    lemma app_Var_IT: "t ∈ IT ==> t ° Var i ∈ IT"
      apply (induct set: IT)
        apply (subst app_last)
        apply (rule IT.Var)
        apply simp
        apply (rule lists.Cons)
         apply (rule Var_IT)
        apply (rule lists.Nil)
       apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
        apply (erule subst_Var_IT)
       apply (rule Var_IT)
      apply (subst app_last)
      apply (rule IT.Beta)
       apply (subst app_last [symmetric])
       apply assumption
      apply assumption
      done

    subsection {* Well-typed substitution preserves termination *}

    lemma subst_type_IT:
      "!!t e T u i. t ∈ IT ==> e⟨i:U⟩ \<turnstile> t : T ==>
        u ∈ IT ==> e \<turnstile> u : U ==> t[u/i] ∈ IT"
      (is "PROP ?P U" is "!!t e T u i. _ ==> PROP ?Q t e T u i U")
    proof (induct U)
      fix T t
      assume MI1: "!!T1 T2. T = T1 => T2 ==> PROP ?P T1"
      assume MI2: "!!T1 T2. T = T1 => T2 ==> PROP ?P T2"
      assume "t ∈ IT"
      thus "!!e T' u i. PROP ?Q t e T' u i T"
      proof induct
        fix e T' u i
        assume uIT: "u ∈ IT"
        assume uT: "e \<turnstile> u : T"
        {
          case (Var n rs e_ T'_ u_ i_)
          assume nT: "e⟨i:T⟩ \<turnstile> Var n °° rs : T'"
          let ?ty = "{t. ∃T'. e⟨i:T⟩ \<turnstile> t : T'}"
          let ?R = "λt. ∀e T' u i.
            e⟨i:T⟩ \<turnstile> t : T' --> u ∈ IT --> e \<turnstile> u : T --> t[u/i] ∈ IT"
          show "(Var n °° rs)[u/i] ∈ IT"
          proof (cases "n = i")
            case True
            show ?thesis
            proof (cases rs)
              case Nil
              with uIT True show ?thesis by simp
            next
              case (Cons a as)
              with nT have "e⟨i:T⟩ \<turnstile> Var n ° a °° as : T'" by simp
              then obtain Ts
                  where headT: "e⟨i:T⟩ \<turnstile> Var n ° a : Ts \<Rrightarrow> T'"
                  and argsT: "e⟨i:T⟩ \<tturnstile> as : Ts"
                by (rule list_app_typeE)
              from headT obtain T''
                  where varT: "e⟨i:T⟩ \<turnstile> Var n : T'' => Ts \<Rrightarrow> T'"
                  and argT: "e⟨i:T⟩ \<turnstile> a : T''"
                by cases simp_all
              from varT True have T: "T = T'' => Ts \<Rrightarrow> T'"
                by cases auto
              with uT have uT': "e \<turnstile> u : T'' => Ts \<Rrightarrow> T'" by simp
              from T have "(Var 0 °° map (λt. lift t 0)
                (map (λt. t[u/i]) as))[(u ° a[u/i])/0] ∈ IT"
              proof (rule MI2)
                from T have "(lift u 0 ° Var 0)[a[u/i]/0] ∈ IT"
                proof (rule MI1)
                  have "lift u 0 ∈ IT" by (rule lift_IT)
                  thus "lift u 0 ° Var 0 ∈ IT" by (rule app_Var_IT)
                  show "e⟨0:T''⟩ \<turnstile> lift u 0 ° Var 0 : Ts \<Rrightarrow> T'"
                  proof (rule typing.App)
                    show "e⟨0:T''⟩ \<turnstile> lift u 0 : T'' => Ts \<Rrightarrow> T'"
                      by (rule lift_type) (rule uT')
                    show "e⟨0:T''⟩ \<turnstile> Var 0 : T''"
                      by (rule typing.Var) simp
                  qed
                  from Var have "?R a" by cases (simp_all add: Cons)
                  with argT uIT uT show "a[u/i] ∈ IT" by simp
                  from argT uT show "e \<turnstile> a[u/i] : T''"
                    by (rule subst_lemma) simp
                qed
                thus "u ° a[u/i] ∈ IT" by simp
                from Var have "as ∈ lists {t. ?R t}"
                  by cases (simp_all add: Cons)
                moreover from argsT have "as ∈ lists ?ty"
                  by (rule lists_typings)
                ultimately have "as ∈ lists ({t. ?R t} ∩ ?ty)"
                  by (rule lists_IntI)
                hence "map (λt. lift t 0) (map (λt. t[u/i]) as) ∈ lists IT"
                  (is "(?ls as) ∈ _")
                proof induct
                  case Nil
                  show ?case by fastsimp
                next
                  case (Cons b bs)
                  hence I: "?R b" by simp
                  from Cons obtain U where "e⟨i:T⟩ \<turnstile> b : U" by fast
                  with uT uIT I have "b[u/i] ∈ IT" by simp
                  hence "lift (b[u/i]) 0 ∈ IT" by (rule lift_IT)
                  hence "lift (b[u/i]) 0 # ?ls bs ∈ lists IT"
                    by (rule lists.Cons) (rule Cons)
                  thus ?case by simp
                qed
                thus "Var 0 °° ?ls as ∈ IT" by (rule IT.Var)
                have "e⟨0:Ts \<Rrightarrow> T'⟩ \<turnstile> Var 0 : Ts \<Rrightarrow> T'"
                  by (rule typing.Var) simp
                moreover from uT argsT have "e \<tturnstile> map (λt. t[u/i]) as : Ts"
                  by (rule substs_lemma)
                hence "e⟨0:Ts \<Rrightarrow> T'⟩ \<tturnstile> ?ls as : Ts"
                  by (rule lift_types)
                ultimately show "e⟨0:Ts \<Rrightarrow> T'⟩ \<turnstile> Var 0 °° ?ls as : T'"
                  by (rule list_app_typeI)
                from argT uT have "e \<turnstile> a[u/i] : T''"
                  by (rule subst_lemma) (rule refl)
                with uT' show "e \<turnstile> u ° a[u/i] : Ts \<Rrightarrow> T'"
                  by (rule typing.App)
              qed
              with Cons True show ?thesis
                by (simp add: map_compose [symmetric] o_def)
            qed
          next
            case False
            from Var have "rs ∈ lists {t. ?R t}" by simp
            moreover from nT obtain Ts where "e⟨i:T⟩ \<tturnstile> rs : Ts"
              by (rule list_app_typeE)
            hence "rs ∈ lists ?ty" by (rule lists_typings)
            ultimately have "rs ∈ lists ({t. ?R t} ∩ ?ty)"
              by (rule lists_IntI)
            hence "map (λx. x[u/i]) rs ∈ lists IT"
            proof induct
              case Nil
              show ?case by fastsimp
            next
              case (Cons a as)
              hence I: "?R a" by simp
              from Cons obtain U where "e⟨i:T⟩ \<turnstile> a : U" by fast
              with uT uIT I have "a[u/i] ∈ IT" by simp
              hence "(a[u/i] # map (λt. t[u/i]) as) ∈ lists IT"
                by (rule lists.Cons) (rule Cons)
              thus ?case by simp
            qed
            with False show ?thesis by (auto simp add: subst_Var)
          qed
        next
          case (Lambda r e_ T'_ u_ i_)
          assume "e⟨i:T⟩ \<turnstile> Abs r : T'"
            and "!!e T' u i. PROP ?Q r e T' u i T"
          with uIT uT show "Abs r[u/i] ∈ IT"
            by fastsimp
        next
          case (Beta r a as e_ T'_ u_ i_)
          assume T: "e⟨i:T⟩ \<turnstile> Abs r ° a °° as : T'"
          assume SI1: "!!e T' u i. PROP ?Q (r[a/0] °° as) e T' u i T"
          assume SI2: "!!e T' u i. PROP ?Q a e T' u i T"
          have "Abs (r[lift u 0/Suc i]) ° a[u/i] °° map (λt. t[u/i]) as ∈ IT"
          proof (rule IT.Beta)
            have "Abs r ° a °° as ->β r[a/0] °° as"
              by (rule apps_preserves_beta) (rule beta.beta)
            with T have "e⟨i:T⟩ \<turnstile> r[a/0] °° as : T'"
              by (rule subject_reduction)
            hence "(r[a/0] °° as)[u/i] ∈ IT"
              by (rule SI1)
            thus "r[lift u 0/Suc i][a[u/i]/0] °° map (λt. t[u/i]) as ∈ IT"
              by (simp del: subst_map add: subst_subst subst_map [symmetric])
            from T obtain U where "e⟨i:T⟩ \<turnstile> Abs r ° a : U"
              by (rule list_app_typeE) fast
            then obtain T'' where "e⟨i:T⟩ \<turnstile> a : T''" by cases simp_all
            thus "a[u/i] ∈ IT" by (rule SI2)
          qed
          thus "(Abs r ° a °° as)[u/i] ∈ IT" by simp
        }
      qed
    qed

    subsection {* Well-typed terms are strongly normalizing *}

    lemma type_implies_IT: "e \<turnstile> t : T ==> t ∈ IT"
    proof -
      assume "e \<turnstile> t : T"
      thus ?thesis
      proof induct
        case Var
        show ?case by (rule Var_IT)
      next
        case Abs
        show ?case by (rule IT.Lambda)
      next
        case (App T U e s t)
        have "(Var 0 ° lift t 0)[s/0] ∈ IT"
        proof (rule subst_type_IT)
          have "lift t 0 ∈ IT" by (rule lift_IT)
          hence "[lift t 0] ∈ lists IT" by (rule lists.Cons) (rule lists.Nil)
          hence "Var 0 °° [lift t 0] ∈ IT" by (rule IT.Var)
          also have "Var 0 °° [lift t 0] = Var 0 ° lift t 0" by simp
          finally show "… ∈ IT" .
          have "e⟨0:T => U⟩ \<turnstile> Var 0 : T => U"
            by (rule typing.Var) simp
          moreover have "e⟨0:T => U⟩ \<turnstile> lift t 0 : T"
            by (rule lift_type)
          ultimately show "e⟨0:T => U⟩ \<turnstile> Var 0 ° lift t 0 : U"
            by (rule typing.App)
        qed
        thus ?case by simp
      qed
    qed

    theorem type_implies_termi: "e \<turnstile> t : T ==> t ∈ termi beta"
    proof -
      assume "e \<turnstile> t : T"
      hence "t ∈ IT" by (rule type_implies_IT)
      thus ?thesis by (rule IT_implies_termi)
    qed

    end

### Properties of @{text IT}

lemma lift_IT:

      t ∈ IT ==> lift t i ∈ IT

lemma lifts_IT:

      ts ∈ lists IT ==> map (%t. lift t 0) ts ∈ lists IT

lemma subst_Var_IT:

      r ∈ IT ==> r[Var i/j] ∈ IT

lemma Var_IT:

      Var n ∈ IT

lemma app_Var_IT:

      t ∈ IT ==> t ° Var i ∈ IT

### Well-typed substitution preserves termination

lemma subst_type_IT:

      [| t ∈ IT; e⟨i:U⟩ |- t : T; u ∈ IT; e |- u : U |] ==> t[u/i] ∈ IT

### Well-typed terms are strongly normalizing

lemma type_implies_IT:

      e |- t : T ==> t ∈ IT

theorem type_implies_termi:

      e |- t : T ==> t ∈ termi beta