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