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