src/HOL/Lambda/StrongNorm.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 18257 2124b24454dd
child 20503 503ac4c5ef91
permissions -rw-r--r--
simplified code generator setup
     1 (*  Title:      HOL/Lambda/StrongNorm.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer
     4     Copyright   2000 TU Muenchen
     5 *)
     6 
     7 header {* Strong normalization for simply-typed lambda calculus *}
     8 
     9 theory StrongNorm imports Type InductTermi begin
    10 
    11 text {*
    12 Formalization by Stefan Berghofer. Partly based on a paper proof by
    13 Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.
    14 *}
    15 
    16 
    17 subsection {* Properties of @{text IT} *}
    18 
    19 lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> lift t i \<in> IT"
    20   apply (induct fixing: i set: IT)
    21     apply (simp (no_asm))
    22     apply (rule conjI)
    23      apply
    24       (rule impI,
    25        rule IT.Var,
    26        erule lists.induct,
    27        simp (no_asm),
    28        rule lists.Nil,
    29        simp (no_asm),
    30        erule IntE,
    31        rule lists.Cons,
    32        blast,
    33        assumption)+
    34      apply auto
    35    done
    36 
    37 lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
    38   by (induct ts) auto
    39 
    40 lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> r[Var i/j] \<in> IT"
    41   apply (induct fixing: i j set: IT)
    42     txt {* Case @{term Var}: *}
    43     apply (simp (no_asm) add: subst_Var)
    44     apply
    45     ((rule conjI impI)+,
    46       rule IT.Var,
    47       erule lists.induct,
    48       simp (no_asm),
    49       rule lists.Nil,
    50       simp (no_asm),
    51       erule IntE,
    52       erule CollectE,
    53       rule lists.Cons,
    54       fast,
    55       assumption)+
    56    txt {* Case @{term Lambda}: *}
    57    apply atomize
    58    apply simp
    59    apply (rule IT.Lambda)
    60    apply fast
    61   txt {* Case @{term Beta}: *}
    62   apply atomize
    63   apply (simp (no_asm_use) add: subst_subst [symmetric])
    64   apply (rule IT.Beta)
    65    apply auto
    66   done
    67 
    68 lemma Var_IT: "Var n \<in> IT"
    69   apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> IT")
    70    apply simp
    71   apply (rule IT.Var)
    72   apply (rule lists.Nil)
    73   done
    74 
    75 lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<degree> Var i \<in> IT"
    76   apply (induct set: IT)
    77     apply (subst app_last)
    78     apply (rule IT.Var)
    79     apply simp
    80     apply (rule lists.Cons)
    81      apply (rule Var_IT)
    82     apply (rule lists.Nil)
    83    apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
    84     apply (erule subst_Var_IT)
    85    apply (rule Var_IT)
    86   apply (subst app_last)
    87   apply (rule IT.Beta)
    88    apply (subst app_last [symmetric])
    89    apply assumption
    90   apply assumption
    91   done
    92 
    93 
    94 subsection {* Well-typed substitution preserves termination *}
    95 
    96 lemma subst_type_IT:
    97   "\<And>t e T u i. t \<in> IT \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
    98     u \<in> IT \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> t[u/i] \<in> IT"
    99   (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
   100 proof (induct U)
   101   fix T t
   102   assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
   103   assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
   104   assume "t \<in> IT"
   105   thus "\<And>e T' u i. PROP ?Q t e T' u i T"
   106   proof induct
   107     fix e T' u i
   108     assume uIT: "u \<in> IT"
   109     assume uT: "e \<turnstile> u : T"
   110     {
   111       case (Var n rs e_ T'_ u_ i_)
   112       assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
   113       let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
   114       let ?R = "\<lambda>t. \<forall>e T' u i.
   115         e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e \<turnstile> u : T \<longrightarrow> t[u/i] \<in> IT"
   116       show "(Var n \<degree>\<degree> rs)[u/i] \<in> IT"
   117       proof (cases "n = i")
   118         case True
   119         show ?thesis
   120         proof (cases rs)
   121           case Nil
   122           with uIT True show ?thesis by simp
   123         next
   124           case (Cons a as)
   125           with nT have "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a \<degree>\<degree> as : T'" by simp
   126           then obtain Ts
   127               where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a : Ts \<Rrightarrow> T'"
   128               and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts"
   129             by (rule list_app_typeE)
   130           from headT obtain T''
   131               where varT: "e\<langle>i:T\<rangle> \<turnstile> Var n : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
   132               and argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''"
   133             by cases simp_all
   134           from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'"
   135             by cases auto
   136           with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
   137           from T have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
   138             (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0] \<in> IT"
   139           proof (rule MI2)
   140             from T have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<in> IT"
   141             proof (rule MI1)
   142               have "lift u 0 \<in> IT" by (rule lift_IT)
   143               thus "lift u 0 \<degree> Var 0 \<in> IT" by (rule app_Var_IT)
   144               show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
   145               proof (rule typing.App)
   146                 show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
   147                   by (rule lift_type) (rule uT')
   148                 show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''"
   149                   by (rule typing.Var) simp
   150               qed
   151               from Var have "?R a" by cases (simp_all add: Cons)
   152               with argT uIT uT show "a[u/i] \<in> IT" by simp
   153               from argT uT show "e \<turnstile> a[u/i] : T''"
   154                 by (rule subst_lemma) simp
   155             qed
   156             thus "u \<degree> a[u/i] \<in> IT" by simp
   157             from Var have "as \<in> lists {t. ?R t}"
   158               by cases (simp_all add: Cons)
   159             moreover from argsT have "as \<in> lists ?ty"
   160               by (rule lists_typings)
   161             ultimately have "as \<in> lists ({t. ?R t} \<inter> ?ty)"
   162               by (rule lists_IntI)
   163             hence "map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) \<in> lists IT"
   164               (is "(?ls as) \<in> _")
   165             proof induct
   166               case Nil
   167               show ?case by fastsimp
   168             next
   169               case (Cons b bs)
   170               hence I: "?R b" by simp
   171               from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> b : U" by fast
   172               with uT uIT I have "b[u/i] \<in> IT" by simp
   173               hence "lift (b[u/i]) 0 \<in> IT" by (rule lift_IT)
   174               hence "lift (b[u/i]) 0 # ?ls bs \<in> lists IT"
   175                 by (rule lists.Cons) (rule Cons)
   176               thus ?case by simp
   177             qed
   178             thus "Var 0 \<degree>\<degree> ?ls as \<in> IT" by (rule IT.Var)
   179             have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'"
   180               by (rule typing.Var) simp
   181             moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
   182               by (rule substs_lemma)
   183             hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> ?ls as : Ts"
   184               by (rule lift_types)
   185             ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> ?ls as : T'"
   186               by (rule list_app_typeI)
   187             from argT uT have "e \<turnstile> a[u/i] : T''"
   188               by (rule subst_lemma) (rule refl)
   189             with uT' show "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'"
   190               by (rule typing.App)
   191           qed
   192           with Cons True show ?thesis
   193             by (simp add: map_compose [symmetric] o_def)
   194         qed
   195       next
   196         case False
   197         from Var have "rs \<in> lists {t. ?R t}" by simp
   198         moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts"
   199           by (rule list_app_typeE)
   200         hence "rs \<in> lists ?ty" by (rule lists_typings)
   201         ultimately have "rs \<in> lists ({t. ?R t} \<inter> ?ty)"
   202           by (rule lists_IntI)
   203         hence "map (\<lambda>x. x[u/i]) rs \<in> lists IT"
   204         proof induct
   205           case Nil
   206           show ?case by fastsimp
   207         next
   208           case (Cons a as)
   209           hence I: "?R a" by simp
   210           from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> a : U" by fast
   211           with uT uIT I have "a[u/i] \<in> IT" by simp
   212           hence "(a[u/i] # map (\<lambda>t. t[u/i]) as) \<in> lists IT"
   213             by (rule lists.Cons) (rule Cons)
   214           thus ?case by simp
   215         qed
   216         with False show ?thesis by (auto simp add: subst_Var)
   217       qed
   218     next
   219       case (Lambda r e_ T'_ u_ i_)
   220       assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
   221         and "\<And>e T' u i. PROP ?Q r e T' u i T"
   222       with uIT uT show "Abs r[u/i] \<in> IT"
   223         by fastsimp
   224     next
   225       case (Beta r a as e_ T'_ u_ i_)
   226       assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
   227       assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
   228       assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
   229       have "Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
   230       proof (rule IT.Beta)
   231         have "Abs r \<degree> a \<degree>\<degree> as \<rightarrow>\<^sub>\<beta> r[a/0] \<degree>\<degree> as"
   232           by (rule apps_preserves_beta) (rule beta.beta)
   233         with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
   234           by (rule subject_reduction)
   235         hence "(r[a/0] \<degree>\<degree> as)[u/i] \<in> IT"
   236           by (rule SI1)
   237         thus "r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
   238           by (simp del: subst_map add: subst_subst subst_map [symmetric])
   239         from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U"
   240           by (rule list_app_typeE) fast
   241         then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all
   242         thus "a[u/i] \<in> IT" by (rule SI2)
   243       qed
   244       thus "(Abs r \<degree> a \<degree>\<degree> as)[u/i] \<in> IT" by simp
   245     }
   246   qed
   247 qed
   248 
   249 
   250 subsection {* Well-typed terms are strongly normalizing *}
   251 
   252 lemma type_implies_IT:
   253   assumes "e \<turnstile> t : T"
   254   shows "t \<in> IT"
   255   using prems
   256 proof induct
   257   case Var
   258   show ?case by (rule Var_IT)
   259 next
   260   case Abs
   261   show ?case by (rule IT.Lambda)
   262 next
   263   case (App T U e s t)
   264   have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
   265   proof (rule subst_type_IT)
   266     have "lift t 0 \<in> IT" by (rule lift_IT)
   267     hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
   268     hence "Var 0 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
   269     also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
   270     finally show "\<dots> \<in> IT" .
   271     have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
   272       by (rule typing.Var) simp
   273     moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
   274       by (rule lift_type)
   275     ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
   276       by (rule typing.App)
   277   qed
   278   thus ?case by simp
   279 qed
   280 
   281 theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> t \<in> termi beta"
   282 proof -
   283   assume "e \<turnstile> t : T"
   284   hence "t \<in> IT" by (rule type_implies_IT)
   285   thus ?thesis by (rule IT_implies_termi)
   286 qed
   287 
   288 end