Quelle  StrongNorm.thy

(*  Title:      HOL/Proofs/Lambda/StrongNorm.thy
  Author: Stefan Berghofer
  Copyright 2000 TU Muenchen
*)

section ‹Strong normalization for simply-typed lambda calculus›

theory StrongNorm imports LambdaType InductTermi begin

text ‹
 Formalization by Stefan Berghofer. Partly based on a paper proof by
 Felix Joachimski and Ralph Matthes 🍋‹"Matthes-Joachimski-AML"›.
 ›


subsection ‹Properties of ‹IT›\›

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

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

lemma subst_Var_IT: "IT r ==> IT (r[Var i/j])"
  apply (induct arbitrary: i j set: IT)
    txt ‹Case 🍋‹Var›:›
    apply (simp (no_asm) add: subst_Var)
    apply
    ((rule conjI impI)+,
      rule IT.Var,
      erule listsp.induct,
      simp (no_asm),
      simp (no_asm),
      rule listsp.Cons,
      fast,
      assumption)+
   txt ‹Case 🍋‹Lambda›:›
   apply atomize
   apply simp
   apply (rule IT.Lambda)
   apply fast
  txt ‹Case 🍋‹Beta›:›
  apply atomize
  apply (simp (no_asm_use) add: subst_subst [symmetric])
  apply (rule IT.Beta)
   apply auto
  done

lemma Var_IT: "IT (Var n)"
  apply (subgoal_tac "IT (Var n 🍋🍋 [])")
   apply simp
  apply (rule IT.Var)
  apply (rule listsp.Nil)
  done

lemma app_Var_IT: "IT t ==> IT (t 🍋 Var i)"
  apply (induct set: IT)
    apply (subst app_last)
    apply (rule IT.Var)
    apply simp
    apply (rule listsp.Cons)
     apply (rule Var_IT)
    apply (rule listsp.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. IT t ==> e⟨i:U⟩ ⊨ t : T ==>
    IT u ==> e ⊨ u : U ==> IT (t[u/i])"
  (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 "IT t"
  thus "∧e T' u i. PROP ?Q t e T' u i T"
  proof induct
    fix e T' u i
    assume uIT: "IT u"
    assume uT: "e ⊨ u : T"
    {
      case (Var rs n e1 T'1 u1 i1)
      assume nT: "e⟨i:T⟩ ⊨ Var n 🍋🍋 rs : T'"
      let ?ty = "λt. ∃T'. e⟨i:T⟩ ⊨ t : T'"
      let ?R = "λt. ∀e T' u i.
        e⟨i:T⟩ ⊨ t : T' ⟶ IT u ⟶ e ⊨ u : T ⟶ IT (t[u/i])"
      show "IT ((Var n 🍋🍋 rs)[u/i])"
      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⟩ ⊨ Var n 🍋 a 🍋🍋 as : T'" by simp
          then obtain Ts
              where headT: "e⟨i:T⟩ ⊨ Var n 🍋 a : Ts ⇛ T'"
              and argsT: "e⟨i:T⟩ ⊨!!! as : Ts"
            by (rule list_app_typeE)
          from headT obtain T''
              where varT: "e⟨i:T⟩ ⊨ Var n : T'' ==> Ts ⇛ T'"
              and argT: "e⟨i:T⟩ ⊨ a : T''"
            by cases simp_all
          from varT True have T: "T = T'' ==> Ts ⇛ T'"
            by cases auto
          with uT have uT': "e ⊨ u : T'' ==> Ts ⇛ T'" by simp
          from T have "IT ((Var 0 🍋🍋 map (λt. lift t 0)
            (map (λt. t[u/i]) as))[(u 🍋 a[u/i])/0])"
          proof (rule MI2)
            from T have "IT ((lift u 0 🍋 Var 0)[a[u/i]/0])"
            proof (rule MI1)
              have "IT (lift u 0)" by (rule lift_IT [OF uIT])
              thus "IT (lift u 0 🍋 Var 0)" by (rule app_Var_IT)
              show "e⟨0:T''⟩ ⊨ lift u 0 🍋 Var 0 : Ts ⇛ T'"
              proof (rule typing.App)
                show "e⟨0:T''⟩ ⊨ lift u 0 : T'' ==> Ts ⇛ T'"
                  by (rule lift_type) (rule uT')
                show "e⟨0:T''⟩ ⊨ 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 "IT (a[u/i])" by simp
              from argT uT show "e ⊨ a[u/i] : T''"
                by (rule subst_lemma) simp
            qed
            thus "IT (u 🍋 a[u/i])" by simp
            from Var have "listsp ?R as"
              by cases (simp_all add: Cons)
            moreover from argsT have "listsp ?ty as"
              by (rule lists_typings)
            ultimately have "listsp (λt. ?R t ∧ ?ty t) as"
              by simp
            hence "listsp IT (map (λt. lift t 0) (map (λt. t[u/i]) as))"
              (is "listsp IT (?ls as)")
            proof induct
              case Nil
              show ?case by fastforce
            next
              case (Cons b bs)
              hence I: "?R b" by simp
              from Cons obtain U where "e⟨i:T⟩ ⊨ b : U" by fast
              with uT uIT I have "IT (b[u/i])" by simp
              hence "IT (lift (b[u/i]) 0)" by (rule lift_IT)
              hence "listsp IT (lift (b[u/i]) 0 # ?ls bs)"
                by (rule listsp.Cons) (rule Cons)
              thus ?case by simp
            qed
            thus "IT (Var 0 🍋🍋 ?ls as)" by (rule IT.Var)
            have "e⟨0:Ts ⇛ T'⟩ ⊨ Var 0 : Ts ⇛ T'"
              by (rule typing.Var) simp
            moreover from uT argsT have "e ⊨!!! map (λt. t[u/i]) as : Ts"
              by (rule substs_lemma)
            hence "e⟨0:Ts ⇛ T'⟩ ⊨!!! ?ls as : Ts"
              by (rule lift_types)
            ultimately show "e⟨0:Ts ⇛ T'⟩ ⊨ Var 0 🍋🍋 ?ls as : T'"
              by (rule list_app_typeI)
            from argT uT have "e ⊨ a[u/i] : T''"
              by (rule subst_lemma) (rule refl)
            with uT' show "e ⊨ u 🍋 a[u/i] : Ts ⇛ T'"
              by (rule typing.App)
          qed
          with Cons True show ?thesis
            by (simp add: comp_def)
        qed
      next
        case False
        from Var have "listsp ?R rs" by simp
        moreover from nT obtain Ts where "e⟨i:T⟩ ⊨!!! rs : Ts"
          by (rule list_app_typeE)
        hence "listsp ?ty rs" by (rule lists_typings)
        ultimately have "listsp (λt. ?R t ∧ ?ty t) rs"
          by simp
        hence "listsp IT (map (λx. x[u/i]) rs)"
        proof induct
          case Nil
          show ?case by fastforce
        next
          case (Cons a as)
          hence I: "?R a" by simp
          from Cons obtain U where "e⟨i:T⟩ ⊨ a : U" by fast
          with uT uIT I have "IT (a[u/i])" by simp
          hence "listsp IT (a[u/i] # map (λt. t[u/i]) as)"
            by (rule listsp.Cons) (rule Cons)
          thus ?case by simp
        qed
        with False show ?thesis by (auto simp add: subst_Var)
      qed
    next
      case (Lambda r e1 T'1 u1 i1)
      assume "e⟨i:T⟩ ⊨ Abs r : T'"
        and "∧e T' u i. PROP ?Q r e T' u i T"
      with uIT uT show "IT (Abs r[u/i])"
        by fastforce
    next
      case (Beta r a as e1 T'1 u1 i1)
      assume T: "e⟨i:T⟩ ⊨ 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 "IT (Abs (r[lift u 0/Suc i]) 🍋 a[u/i] 🍋🍋 map (λt. t[u/i]) as)"
      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⟩ ⊨ r[a/0] 🍋🍋 as : T'"
          by (rule subject_reduction)
        hence "IT ((r[a/0] 🍋🍋 as)[u/i])"
          using uIT uT by (rule SI1)
        thus "IT (r[lift u 0/Suc i][a[u/i]/0] 🍋🍋 map (λt. t[u/i]) as)"
          by (simp del: subst_map add: subst_subst subst_map [symmetric])
        from T obtain U where "e⟨i:T⟩ ⊨ Abs r 🍋 a : U"
          by (rule list_app_typeE) fast
        then obtain T'' where "e⟨i:T⟩ ⊨ a : T''" by cases simp_all
        thus "IT (a[u/i])" using uIT uT by (rule SI2)
      qed
      thus "IT ((Abs r 🍋 a 🍋🍋 as)[u/i])" by simp
    }
  qed
qed


subsection ‹Well-typed terms are strongly normalizing›

lemma type_implies_IT:
  assumes "e ⊨ t : T"
  shows "IT t"
  using assms
proof induct
  case Var
  show ?case by (rule Var_IT)
next
  case Abs
  show ?case by (rule IT.Lambda) (rule Abs)
next
  case (App e s T U t)
  have "IT ((Var 0 🍋 lift t 0)[s/0])"
  proof (rule subst_type_IT)
    have "IT (lift t 0)" using ‹IT t› by (rule lift_IT)
    hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil)
    hence "IT (Var 0 🍋🍋 [lift t 0])" 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⟩ ⊨ Var 0 : T ==> U"
      by (rule typing.Var) simp
    moreover have "e⟨0:T ==> U⟩ ⊨ lift t 0 : T"
      by (rule lift_type) (rule App.hyps)
    ultimately show "e⟨0:T ==> U⟩ ⊨ Var 0 🍋 lift t 0 : U"
      by (rule typing.App)
    show "IT s" by fact
    show "e ⊨ s : T ==> U" by fact
  qed
  thus ?case by simp
qed

theorem type_implies_termi: "e ⊨ t : T ==> termip beta t"
proof -
  assume "e ⊨ t : T"
  hence "IT t" by (rule type_implies_IT)
  thus ?thesis by (rule IT_implies_termi)
qed

end