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