diff -r 6ceb8d38bc9e -r 35fcab3da1b7 src/HOL/Lambda/StrongNorm.thy
--- a/src/HOL/Lambda/StrongNorm.thy	Tue Sep 07 11:51:53 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,286 +0,0 @@
-(*  Title:      HOL/Lambda/StrongNorm.thy
-    Author:     Stefan Berghofer
-    Copyright   2000 TU Muenchen
-*)
-
-header {* Strong normalization for simply-typed lambda calculus *}
-
-theory StrongNorm imports Type InductTermi begin
-
-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!]: "IT t \<Longrightarrow> IT (lift t i)"
-  apply (induct arbitrary: i set: IT)
-    apply (simp (no_asm))
-    apply (rule conjI)
-     apply
-      (rule impI,
-       rule IT.Var,
-       erule listsp.induct,
-       simp (no_asm),
-       rule listsp.Nil,
-       simp (no_asm),
-       rule listsp.Cons,
-       blast,
-       assumption)+
-     apply auto
-   done
-
-lemma lifts_IT: "listsp IT ts \<Longrightarrow> listsp IT (map (\<lambda>t. lift t 0) ts)"
-  by (induct ts) auto
-
-lemma subst_Var_IT: "IT r \<Longrightarrow> IT (r[Var i/j])"
-  apply (induct arbitrary: i j set: IT)
-    txt {* Case @{term Var}: *}
-    apply (simp (no_asm) add: subst_Var)
-    apply
-    ((rule conjI impI)+,
-      rule IT.Var,
-      erule listsp.induct,
-      simp (no_asm),
-      rule listsp.Nil,
-      simp (no_asm),
-      rule listsp.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: "IT (Var n)"
-  apply (subgoal_tac "IT (Var n \<degree>\<degree> [])")
-   apply simp
-  apply (rule IT.Var)
-  apply (rule listsp.Nil)
-  done
-
-lemma app_Var_IT: "IT t \<Longrightarrow> IT (t \<degree> Var i)"
-  apply (induct set: IT)
-    apply (subst app_last)
-    apply (rule IT.Var)
-    apply simp
-    apply (rule listsp.Cons)
-     apply (rule Var_IT)
-    apply (rule listsp.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. IT t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow>
-    IT u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> IT (t[u/i])"
-  (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 "IT t"
-  thus "\<And>e T' u i. PROP ?Q t e T' u i T"
-  proof induct
-    fix e T' u i
-    assume uIT: "IT u"
-    assume uT: "e \<turnstile> u : T"
-    {
-      case (Var rs n e_ T'_ u_ i_)
-      assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
-      let ?ty = "\<lambda>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> IT u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> IT (t[u/i])"
-      show "IT ((Var n \<degree>\<degree> rs)[u/i])"
-      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 "IT ((Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0)
-            (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0])"
-          proof (rule MI2)
-            from T have "IT ((lift u 0 \<degree> Var 0)[a[u/i]/0])"
-            proof (rule MI1)
-              have "IT (lift u 0)" by (rule lift_IT [OF uIT])
-              thus "IT (lift u 0 \<degree> Var 0)" 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 "IT (a[u/i])" by simp
-              from argT uT show "e \<turnstile> a[u/i] : T''"
-                by (rule subst_lemma) simp
-            qed
-            thus "IT (u \<degree> a[u/i])" by simp
-            from Var have "listsp ?R as"
-              by cases (simp_all add: Cons)
-            moreover from argsT have "listsp ?ty as"
-              by (rule lists_typings)
-            ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) as"
-              by simp
-            hence "listsp IT (map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as))"
-              (is "listsp IT (?ls as)")
-            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 "IT (b[u/i])" by simp
-              hence "IT (lift (b[u/i]) 0)" by (rule lift_IT)
-              hence "listsp IT (lift (b[u/i]) 0 # ?ls bs)"
-                by (rule listsp.Cons) (rule Cons)
-              thus ?case by simp
-            qed
-            thus "IT (Var 0 \<degree>\<degree> ?ls as)" 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: comp_def)
-        qed
-      next
-        case False
-        from Var have "listsp ?R rs" by simp
-        moreover from nT obtain Ts where "e\<langle>i:T\<rangle> \<tturnstile> rs : Ts"
-          by (rule list_app_typeE)
-        hence "listsp ?ty rs" by (rule lists_typings)
-        ultimately have "listsp (\<lambda>t. ?R t \<and> ?ty t) rs"
-          by simp
-        hence "listsp IT (map (\<lambda>x. x[u/i]) rs)"
-        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 "IT (a[u/i])" by simp
-          hence "listsp IT (a[u/i] # map (\<lambda>t. t[u/i]) as)"
-            by (rule listsp.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 "IT (Abs r[u/i])"
-        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 "IT (Abs (r[lift u 0/Suc i]) \<degree> a[u/i] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
-      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 "IT ((r[a/0] \<degree>\<degree> as)[u/i])"
-          using uIT uT by (rule SI1)
-        thus "IT (r[lift u 0/Suc i][a[u/i]/0] \<degree>\<degree> map (\<lambda>t. t[u/i]) as)"
-          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 "IT (a[u/i])" using uIT uT by (rule SI2)
-      qed
-      thus "IT ((Abs r \<degree> a \<degree>\<degree> as)[u/i])" by simp
-    }
-  qed
-qed
-
-
-subsection {* Well-typed terms are strongly normalizing *}
-
-lemma type_implies_IT:
-  assumes "e \<turnstile> t : T"
-  shows "IT t"
-  using assms
-proof induct
-  case Var
-  show ?case by (rule Var_IT)
-next
-  case Abs
-  show ?case by (rule IT.Lambda) (rule Abs)
-next
-  case (App e s T U t)
-  have "IT ((Var 0 \<degree> lift t 0)[s/0])"
-  proof (rule subst_type_IT)
-    have "IT (lift t 0)" using `IT t` by (rule lift_IT)
-    hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil)
-    hence "IT (Var 0 \<degree>\<degree> [lift t 0])" by (rule IT.Var)
-    also have "Var 0 \<degree>\<degree> [lift t 0] = Var 0 \<degree> lift t 0" by simp
-    finally show "IT \<dots>" .
-    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) (rule App.hyps)
-    ultimately show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t 0 : U"
-      by (rule typing.App)
-    show "IT s" by fact
-    show "e \<turnstile> s : T \<Rightarrow> U" by fact
-  qed
-  thus ?case by simp
-qed
-
-theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termip beta t"
-proof -
-  assume "e \<turnstile> t : T"
-  hence "IT t" by (rule type_implies_IT)
-  thus ?thesis by (rule IT_implies_termi)
-qed
-
-end