# HG changeset patch
# User berghofe
# Date 1056443877 -7200
# Node ID 35d36f43ba06f09f7c5336b865cd32a9b1d384c2
# Parent  e61a310cde02614e783a0b474493b840e1886e58
Moved strong normalization proof to StrongNorm.thy

diff -r e61a310cde02 -r 35d36f43ba06 src/HOL/Lambda/StrongNorm.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/StrongNorm.thy	Tue Jun 24 10:37:57 2003 +0200
@@ -0,0 +1,289 @@
+(*  Title:      HOL/Lambda/StrongNorm.thy
+    ID:         $Id$
+    Author:     Stefan Berghofer
+    Copyright   2000 TU Muenchen
+*)
+
+header {* Strong normalization for simply-typed lambda calculus *}
+
+theory StrongNorm = Type + InductTermi:
+
+text {*
+Formalization by Stefan Berghofer. Partly based on a paper proof by
+Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.
+*}
+
+
+subsection {* Properties of @{text IT} *}
+
+lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> (\<And>i. lift t i \<in> IT)"
+  apply (induct set: IT)
+    apply (simp (no_asm))
+    apply (rule conjI)
+     apply
+      (rule impI,
+       rule IT.Var,
+       erule lists.induct,
+       simp (no_asm),
+       rule lists.Nil,
+       simp (no_asm),
+       erule IntE,
+       rule lists.Cons,
+       blast,
+       assumption)+
+     apply auto
+   done
+
+lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
+  by (induct ts) auto
+
+lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> (\<And>i j. r[Var i/j] \<in> IT)"
+  apply (induct set: IT)
+    txt {* Case @{term Var}: *}
+    apply (simp (no_asm) add: subst_Var)
+    apply
+    ((rule conjI impI)+,
+      rule IT.Var,
+      erule lists.induct,
+      simp (no_asm),
+      rule lists.Nil,
+      simp (no_asm),
+      erule IntE,
+      erule CollectE,
+      rule lists.Cons,
+      fast,
+      assumption)+
+   txt {* Case @{term Lambda}: *}
+   apply atomize
+   apply simp
+   apply (rule IT.Lambda)
+   apply fast
+  txt {* Case @{term Beta}: *}
+  apply atomize
+  apply (simp (no_asm_use) add: subst_subst [symmetric])
+  apply (rule IT.Beta)
+   apply auto
+  done
+
+lemma Var_IT: "Var n \<in> IT"
+  apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> IT")
+   apply simp
+  apply (rule IT.Var)
+  apply (rule lists.Nil)
+  done
+
+lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<degree> Var i \<in> IT"
+  apply (induct set: IT)
+    apply (subst app_last)
+    apply (rule IT.Var)
+    apply simp
+    apply (rule lists.Cons)
+     apply (rule Var_IT)
+    apply (rule lists.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:
+  "\<And>t e T u i. t \<in> IT \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
+    u \<in> IT \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> t[u/i] \<in> IT"
+  (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
+proof (induct U)
+  fix T t
+  assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
+  assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
+  assume "t \<in> IT"
+  thus "\<And>e T' u i. PROP ?Q t e T' u i T"
+  proof induct
+    fix e T' u i
+    assume uIT: "u \<in> IT"
+    assume uT: "e \<turnstile> u : T"
+    {
+      case (Var n rs e_ T'_ u_ i_)
+      assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
+      let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
+      let ?R = "\<lambda>t. \<forall>e T' u i.
+        e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e \<turnstile> u : T \<longrightarrow> t[u/i] \<in> IT"
+      show "(Var n \<degree>\<degree> rs)[u/i] \<in> IT"
+      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\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a \<degree>\<degree> as : T'" by simp
+          then obtain Ts
+              where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a : Ts \<Rrightarrow> T'"
+              and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts"
+            by (rule list_app_typeE)
+          from headT obtain T''
+              where varT: "e\<langle>i:T\<rangle> \<turnstile> Var n : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
+              and argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''"
+            by cases simp_all
+          from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'"
+            by cases auto
+          with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
+          from T have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
+            (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0] \<in> IT"
+          proof (rule MI2)
+            from T have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<in> IT"
+            proof (rule MI1)
+              have "lift u 0 \<in> IT" by (rule lift_IT)
+              thus "lift u 0 \<degree> Var 0 \<in> IT" by (rule app_Var_IT)
+              show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
+              proof (rule typing.App)
+                show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
+                  by (rule lift_type) (rule uT')
+                show "e\<langle>0:T''\<rangle> \<turnstile> 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 "a[u/i] \<in> IT" by simp
+              from argT uT show "e \<turnstile> a[u/i] : T''"
+                by (rule subst_lemma) simp
+            qed
+            thus "u \<degree> a[u/i] \<in> IT" by simp
+            from Var have "as \<in> lists {t. ?R t}"
+              by cases (simp_all add: Cons)
+            moreover from argsT have "as \<in> lists ?ty"
+              by (rule lists_typings)
+            ultimately have "as \<in> lists ({t. ?R t} \<inter> ?ty)"
+              by (rule lists_IntI)
+            hence "map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) \<in> lists IT"
+              (is "(?ls as) \<in> _")
+            proof induct
+              case Nil
+              show ?case by fastsimp
+            next
+              case (Cons b bs)
+              hence I: "?R b" by simp
+              from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> b : U" by fast
+              with uT uIT I have "b[u/i] \<in> IT" by simp
+              hence "lift (b[u/i]) 0 \<in> IT" by (rule lift_IT)
+              hence "lift (b[u/i]) 0 # ?ls bs \<in> lists IT"
+                by (rule lists.Cons) (rule Cons)
+              thus ?case by simp
+            qed
+            thus "Var 0 \<degree>\<degree> ?ls as \<in> IT" by (rule IT.Var)
+            have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'"
+              by (rule typing.Var) simp
+            moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
+              by (rule substs_lemma)
+            hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> ?ls as : Ts"
+              by (rule lift_types)
+            ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> ?ls as : T'"
+              by (rule list_app_typeI)
+            from argT uT have "e \<turnstile> a[u/i] : T''"
+              by (rule subst_lemma) (rule refl)
+            with uT' show "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'"
+              by (rule typing.App)
+          qed
+          with Cons True show ?thesis
+            by (simp add: map_compose [symmetric] o_def)
+        qed
+      next
+        case False
+        from Var have "rs \<in> lists {t. ?R t}" by simp
+        moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts"
+          by (rule list_app_typeE)
+        hence "rs \<in> lists ?ty" by (rule lists_typings)
+        ultimately have "rs \<in> lists ({t. ?R t} \<inter> ?ty)"
+          by (rule lists_IntI)
+        hence "map (\<lambda>x. x[u/i]) rs \<in> lists IT"
+        proof induct
+          case Nil
+          show ?case by fastsimp
+        next
+          case (Cons a as)
+          hence I: "?R a" by simp
+          from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> a : U" by fast
+          with uT uIT I have "a[u/i] \<in> IT" by simp
+          hence "(a[u/i] # map (\<lambda>t. t[u/i]) as) \<in> lists IT"
+            by (rule lists.Cons) (rule Cons)
+          thus ?case by simp
+        qed
+        with False show ?thesis by (auto simp add: subst_Var)
+      qed
+    next
+      case (Lambda r e_ T'_ u_ i_)
+      assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
+        and "\<And>e T' u i. PROP ?Q r e T' u i T"
+      with uIT uT show "Abs r[u/i] \<in> IT"
+        by fastsimp
+    next
+      case (Beta r a as e_ T'_ u_ i_)
+      assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
+      assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
+      assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
+      have "Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
+      proof (rule IT.Beta)
+        have "Abs r \<degree> a \<degree>\<degree> as \<rightarrow>\<^sub>\<beta> r[a/0] \<degree>\<degree> as"
+          by (rule apps_preserves_beta) (rule beta.beta)
+        with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
+          by (rule subject_reduction)
+        hence "(r[a/0] \<degree>\<degree> as)[u/i] \<in> IT"
+          by (rule SI1)
+        thus "r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
+          by (simp del: subst_map add: subst_subst subst_map [symmetric])
+        from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U"
+          by (rule list_app_typeE) fast
+        then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all
+        thus "a[u/i] \<in> IT" by (rule SI2)
+      qed
+      thus "(Abs r \<degree> a \<degree>\<degree> as)[u/i] \<in> IT" by simp
+    }
+  qed
+qed
+
+
+subsection {* Well-typed terms are strongly normalizing *}
+
+lemma type_implies_IT: "e \<turnstile> t : T \<Longrightarrow> t \<in> IT"
+proof -
+  assume "e \<turnstile> t : T"
+  thus ?thesis
+  proof induct
+    case Var
+    show ?case by (rule Var_IT)
+  next
+    case Abs
+    show ?case by (rule IT.Lambda)
+  next
+    case (App T U e s t)
+    have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
+    proof (rule subst_type_IT)
+      have "lift t 0 \<in> IT" by (rule lift_IT)
+      hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
+      hence "Var 0 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
+      also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
+      finally show "\<dots> \<in> IT" .
+      have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
+        by (rule typing.Var) simp
+      moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
+        by (rule lift_type)
+      ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
+        by (rule typing.App)
+    qed
+    thus ?case by simp
+  qed
+qed
+
+theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> t \<in> termi beta"
+proof -
+  assume "e \<turnstile> t : T"
+  hence "t \<in> IT" by (rule type_implies_IT)
+  thus ?thesis by (rule IT_implies_termi)
+qed
+
+end
diff -r e61a310cde02 -r 35d36f43ba06 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Tue Jun 24 10:37:12 2003 +0200
+++ b/src/HOL/Lambda/Type.thy	Tue Jun 24 10:37:57 2003 +0200
@@ -4,15 +4,9 @@
     Copyright   2000 TU Muenchen
 *)
 
-header {* Simply-typed lambda terms: subject reduction and strong
-  normalization *}
-
-theory Type = InductTermi:
+header {* Simply-typed lambda terms *}
 
-text_raw {*
-  \footnote{Formalization by Stefan Berghofer.  Partly based on a
-  paper proof by Ralph Matthes.}
-*}
+theory Type = ListApplication:
 
 
 subsection {* Environments *}
@@ -95,6 +89,68 @@
   by force
 
 
+subsection {* Lists of types *}
+
+lemma lists_typings:
+    "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
+  apply (induct ts)
+   apply (case_tac Ts)
+     apply simp
+     apply (rule lists.Nil)
+    apply simp
+  apply (case_tac Ts)
+   apply simp
+  apply simp
+  apply (rule lists.Cons)
+   apply blast
+  apply blast
+  done
+
+lemma types_snoc: "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
+  apply (induct ts)
+  apply simp
+  apply (case_tac Ts)
+  apply simp+
+  done
+
+lemma types_snoc_eq: "\<And>Ts. e \<tturnstile> ts @ [t] : Ts @ [T] =
+  (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)"
+  apply (induct ts)
+  apply (case_tac Ts)
+  apply simp+
+  apply (case_tac Ts)
+  apply (case_tac "list @ [t]")
+  apply simp+
+  done
+
+lemma rev_exhaust2 [case_names Nil snoc, extraction_expand]:
+  "(xs = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>ys y. xs = ys @ [y] \<Longrightarrow> P) \<Longrightarrow> P"
+  -- {* Cannot use @{text rev_exhaust} from the @{text List}
+    theory, since it is not constructive *}
+  apply (subgoal_tac "\<forall>ys. xs = rev ys \<longrightarrow> P")
+  apply (erule_tac x="rev xs" in allE)
+  apply simp
+  apply (rule allI)
+  apply (rule impI)
+  apply (case_tac ys)
+  apply simp
+  apply simp
+  apply atomize
+  apply (erule allE)+
+  apply (erule mp, rule conjI)
+  apply (rule refl)+
+  done
+
+lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow>
+  (\<And>Us U. Ts = Us @ [U] \<Longrightarrow> e \<tturnstile> ts : Us \<Longrightarrow> e \<turnstile> t : U \<Longrightarrow> P) \<Longrightarrow> P"
+  apply (cases Ts rule: rev_exhaust2)
+  apply simp
+  apply (case_tac "ts @ [t]")
+  apply (simp add: types_snoc_eq)+
+  apply rules
+  done
+
+
 subsection {* n-ary function types *}
 
 lemma list_app_typeD:
@@ -135,58 +191,105 @@
   apply blast
   done
 
-lemma lists_typings:
-    "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
-  apply (induct ts)
-   apply (case_tac Ts)
-     apply simp
-     apply (rule lists.Nil)
-    apply simp
-  apply (case_tac Ts)
-   apply simp
+text {*
+For the specific case where the head of the term is a variable,
+the following theorems allow to infer the types of the arguments
+without analyzing the typing derivation. This is crucial
+for program extraction.
+*}
+
+theorem var_app_type_eq:
+  "\<And>T U. e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
+  apply (induct ts rule: rev_induct)
+  apply simp
+  apply (ind_cases "e \<turnstile> Var i : T")
+  apply (ind_cases "e \<turnstile> Var i : T")
+  apply simp
+  apply simp
+  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply atomize
+  apply (erule_tac x="Ta \<Rightarrow> T" in allE)
+  apply (erule_tac x="Tb \<Rightarrow> U" in allE)
+  apply (erule impE)
+  apply assumption
+  apply (erule impE)
+  apply assumption
+  apply simp
+  done
+
+lemma var_app_types: "\<And>ts Ts U. e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
+  e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us"
+  apply (induct us)
+  apply simp
+  apply (erule var_app_type_eq)
+  apply assumption
+  apply simp
+  apply atomize
+  apply (case_tac U)
+  apply (rule FalseE)
+  apply simp
+  apply (erule list_app_typeE)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
+  apply assumption
   apply simp
-  apply (rule lists.Cons)
-   apply blast
-  apply blast
+  apply (erule_tac x="ts @ [a]" in allE)
+  apply (erule_tac x="Ts @ [type1]" in allE)
+  apply (erule_tac x="type2" in allE)
+  apply simp
+  apply (erule impE)
+  apply (rule types_snoc)
+  apply assumption
+  apply (erule list_app_typeE)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
+  apply assumption
+  apply simp
+  apply (erule impE)
+  apply (rule typing.App)
+  apply assumption
+  apply (erule list_app_typeE)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
+  apply assumption
+  apply simp
+  apply (erule exE)
+  apply (rule_tac x="type1 # Us" in exI)
+  apply simp
+  apply (erule list_app_typeE)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T")
+  apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
+  apply assumption
+  apply simp
+  done
+
+lemma var_app_typesE: "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow>
+  (\<And>Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> P) \<Longrightarrow> P"
+  apply (drule var_app_types [of _ _ "[]", simplified])
+  apply (rules intro: typing.Var)+
+  done
+
+lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P"
+  apply (cases T)
+  apply (rule FalseE)
+  apply (erule typing.elims)
+  apply simp_all
+  apply atomize
+  apply (erule_tac x="type1" in allE)
+  apply (erule_tac x="type2" in allE)
+  apply (erule mp)
+  apply (erule typing.elims)
+  apply simp_all
   done
 
 
-subsection {* Lifting preserves termination and well-typedness *}
-
-lemma lift_map [simp]:
-    "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
-  by (induct ts) simp_all
-
-lemma subst_map [simp]:
-    "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
-  by (induct ts) simp_all
-
-lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> (\<And>i. lift t i \<in> IT)"
-  apply (induct set: IT)
-    apply (simp (no_asm))
-    apply (rule conjI)
-     apply
-      (rule impI,
-       rule IT.Var,
-       erule lists.induct,
-       simp (no_asm),
-       rule lists.Nil,
-       simp (no_asm),
-       erule IntE,
-       rule lists.Cons,
-       blast,
-       assumption)+
-     apply auto
-   done
-
-lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
-  by (induct ts) auto
+subsection {* Lifting preserves well-typedness *}
 
 lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> (\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T)"
   by (induct set: typing) auto
 
-
-lemma lift_typings:
+lemma lift_types:
   "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
   apply (induct ts)
    apply simp
@@ -240,64 +343,11 @@
      apply auto
   done
 
-
-subsection {* Additional lemmas *}
-
-lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
-  by simp
+theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T"
+  by (induct set: rtrancl) (rules intro: subject_reduction)+
 
-lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> (\<And>i j. r[Var i/j] \<in> IT)"
-  apply (induct set: IT)
-    txt {* Case @{term Var}: *}
-    apply (simp (no_asm) add: subst_Var)
-    apply
-    ((rule conjI impI)+,
-      rule IT.Var,
-      erule lists.induct,
-      simp (no_asm),
-      rule lists.Nil,
-      simp (no_asm),
-      erule IntE,
-      erule CollectE,
-      rule lists.Cons,
-      fast,
-      assumption)+
-   txt {* Case @{term Lambda}: *}
-   apply atomize
-   apply simp
-   apply (rule IT.Lambda)
-   apply fast
-  txt {* Case @{term Beta}: *}
-  apply atomize
-  apply (simp (no_asm_use) add: subst_subst [symmetric])
-  apply (rule IT.Beta)
-   apply auto
-  done
 
-lemma Var_IT: "Var n \<in> IT"
-  apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> IT")
-   apply simp
-  apply (rule IT.Var)
-  apply (rule lists.Nil)
-  done
-
-lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<degree> Var i \<in> IT"
-  apply (induct set: IT)
-    apply (subst app_last)
-    apply (rule IT.Var)
-    apply simp
-    apply (rule lists.Cons)
-     apply (rule Var_IT)
-    apply (rule lists.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 {* Alternative induction rule for types *}
 
 lemma type_induct [induct type]:
   "(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow>
@@ -314,200 +364,4 @@
   qed
 qed
 
-
-subsection {* Well-typed substitution preserves termination *}
-
-lemma subst_type_IT:
-  "\<And>t e T u i. t \<in> IT \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
-    u \<in> IT \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> t[u/i] \<in> IT"
-  (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
-proof (induct U)
-  fix T t
-  assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
-  assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
-  assume "t \<in> IT"
-  thus "\<And>e T' u i. PROP ?Q t e T' u i T"
-  proof induct
-    fix e T' u i
-    assume uIT: "u \<in> IT"
-    assume uT: "e \<turnstile> u : T"
-    {
-      case (Var n rs e_ T'_ u_ i_)
-      assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
-      let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
-      let ?R = "\<lambda>t. \<forall>e T' u i.
-        e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> IT \<longrightarrow> e \<turnstile> u : T \<longrightarrow> t[u/i] \<in> IT"
-      show "(Var n \<degree>\<degree> rs)[u/i] \<in> IT"
-      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\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a \<degree>\<degree> as : T'" by simp
-          then obtain Ts
-              where headT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree> a : Ts \<Rrightarrow> T'"
-              and argsT: "e\<langle>i:T\<rangle> \<tturnstile> as : Ts"
-            by (rule list_app_typeE)
-          from headT obtain T''
-              where varT: "e\<langle>i:T\<rangle> \<turnstile> Var n : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
-              and argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''"
-            by cases simp_all
-          from varT True have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'"
-            by cases auto
-          with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
-          from T have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
-            (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0] \<in> IT"
-          proof (rule MI2)
-            from T have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<in> IT"
-            proof (rule MI1)
-              have "lift u 0 \<in> IT" by (rule lift_IT)
-              thus "lift u 0 \<degree> Var 0 \<in> IT" by (rule app_Var_IT)
-              show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
-              proof (rule typing.App)
-                show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
-                  by (rule lift_type) (rule uT')
-                show "e\<langle>0:T''\<rangle> \<turnstile> 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 "a[u/i] \<in> IT" by simp
-              from argT uT show "e \<turnstile> a[u/i] : T''"
-                by (rule subst_lemma) simp
-            qed
-            thus "u \<degree> a[u/i] \<in> IT" by simp
-            from Var have "as \<in> lists {t. ?R t}"
-              by cases (simp_all add: Cons)
-            moreover from argsT have "as \<in> lists ?ty"
-              by (rule lists_typings)
-            ultimately have "as \<in> lists ({t. ?R t} \<inter> ?ty)"
-              by (rule lists_IntI)
-            hence "map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) \<in> lists IT"
-              (is "(?ls as) \<in> _")
-            proof induct
-              case Nil
-              show ?case by fastsimp
-            next
-              case (Cons b bs)
-              hence I: "?R b" by simp
-              from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> b : U" by fast
-              with uT uIT I have "b[u/i] \<in> IT" by simp
-              hence "lift (b[u/i]) 0 \<in> IT" by (rule lift_IT)
-              hence "lift (b[u/i]) 0 # ?ls bs \<in> lists IT"
-                by (rule lists.Cons) (rule Cons)
-              thus ?case by simp
-            qed
-            thus "Var 0 \<degree>\<degree> ?ls as \<in> IT" by (rule IT.Var)
-            have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'"
-              by (rule typing.Var) simp
-            moreover from uT argsT have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
-              by (rule substs_lemma)
-            hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> ?ls as : Ts"
-              by (rule lift_typings)
-            ultimately show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> ?ls as : T'"
-              by (rule list_app_typeI)
-            from argT uT have "e \<turnstile> a[u/i] : T''"
-              by (rule subst_lemma) (rule refl)
-            with uT' show "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'"
-              by (rule typing.App)
-          qed
-          with Cons True show ?thesis
-            by (simp add: map_compose [symmetric] o_def)
-        qed
-      next
-        case False
-        from Var have "rs \<in> lists {t. ?R t}" by simp
-        moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts"
-          by (rule list_app_typeE)
-        hence "rs \<in> lists ?ty" by (rule lists_typings)
-        ultimately have "rs \<in> lists ({t. ?R t} \<inter> ?ty)"
-          by (rule lists_IntI)
-        hence "map (\<lambda>x. x[u/i]) rs \<in> lists IT"
-        proof induct
-          case Nil
-          show ?case by fastsimp
-        next
-          case (Cons a as)
-          hence I: "?R a" by simp
-          from Cons obtain U where "e\<langle>i:T\<rangle> \<turnstile> a : U" by fast
-          with uT uIT I have "a[u/i] \<in> IT" by simp
-          hence "(a[u/i] # map (\<lambda>t. t[u/i]) as) \<in> lists IT"
-            by (rule lists.Cons) (rule Cons)
-          thus ?case by simp
-        qed
-        with False show ?thesis by (auto simp add: subst_Var)
-      qed
-    next
-      case (Lambda r e_ T'_ u_ i_)
-      assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
-        and "\<And>e T' u i. PROP ?Q r e T' u i T"
-      with uIT uT show "Abs r[u/i] \<in> IT"
-        by fastsimp
-    next
-      case (Beta r a as e_ T'_ u_ i_)
-      assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
-      assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
-      assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
-      have "Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
-      proof (rule IT.Beta)
-        have "Abs r \<degree> a \<degree>\<degree> as -> r[a/0] \<degree>\<degree> as"
-          by (rule apps_preserves_beta) (rule beta.beta)
-        with T have "e\<langle>i:T\<rangle> \<turnstile> r[a/0] \<degree>\<degree> as : T'"
-          by (rule subject_reduction)
-        hence "(r[a/0] \<degree>\<degree> as)[u/i] \<in> IT"
-          by (rule SI1)
-        thus "r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as \<in> IT"
-          by (simp del: subst_map add: subst_subst subst_map [symmetric])
-        from T obtain U where "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a : U"
-          by (rule list_app_typeE) fast
-        then obtain T'' where "e\<langle>i:T\<rangle> \<turnstile> a : T''" by cases simp_all
-        thus "a[u/i] \<in> IT" by (rule SI2)
-      qed
-      thus "(Abs r \<degree> a \<degree>\<degree> as)[u/i] \<in> IT" by simp
-    }
-  qed
-qed
-
-
-subsection {* Well-typed terms are strongly normalizing *}
-
-lemma type_implies_IT: "e \<turnstile> t : T \<Longrightarrow> t \<in> IT"
-proof -
-  assume "e \<turnstile> t : T"
-  thus ?thesis
-  proof induct
-    case Var
-    show ?case by (rule Var_IT)
-  next
-    case Abs
-    show ?case by (rule IT.Lambda)
-  next
-    case (App T U e s t)
-    have "(Var 0 \<degree> lift t 0)[s/0] \<in> IT"
-    proof (rule subst_type_IT)
-      have "lift t 0 \<in> IT" by (rule lift_IT)
-      hence "[lift t 0] \<in> lists IT" by (rule lists.Cons) (rule lists.Nil)
-      hence "Var 0 \<degree>\<degree> [lift t 0] \<in> IT" by (rule IT.Var)
-      also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
-      finally show "\<dots> \<in> IT" .
-      have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
-        by (rule typing.Var) simp
-      moreover have "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t 0 : T"
-        by (rule lift_type)
-      ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
-        by (rule typing.App)
-    qed
-    thus ?case by simp
-  qed
-qed
-
-theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> t \<in> termi beta"
-proof -
-  assume "e \<turnstile> t : T"
-  hence "t \<in> IT" by (rule type_implies_IT)
-  thus ?thesis by (rule IT_implies_termi)
-qed
-
 end