# HG changeset patch
# User wenzelm
# Date 1004488002 -3600
# Node ID 319cc9aba0cf099c9c7a105cdc60d475e687ffa8
# Parent  d20e653fc64fd4bcbf41628a894132cc1dfee8d8
(induct set: ...);

diff -r d20e653fc64f -r 319cc9aba0cf src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Wed Oct 31 01:22:27 2001 +0100
+++ b/src/HOL/Lambda/Type.thy	Wed Oct 31 01:26:42 2001 +0100
@@ -159,10 +159,8 @@
     "\<And>t. subst (t \<^sub>\<degree>\<^sub>\<degree> ts) u i = subst t u i \<^sub>\<degree>\<^sub>\<degree> map (\<lambda>t. subst t u i) ts"
   by (induct ts) simp_all
 
-lemma lift_IT [rule_format, intro!]:
-    "t \<in> IT \<Longrightarrow> \<forall>i. lift t i \<in> IT"
-  apply (erule IT.induct)
-    apply (rule allI)
+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
@@ -200,10 +198,9 @@
 
 subsection {* Substitution lemmas *}
 
-lemma subst_lemma [rule_format]:
-  "e \<turnstile> t : T \<Longrightarrow> \<forall>e' i U u. e' \<turnstile> u : U \<longrightarrow> e = e'\<langle>i:U\<rangle> \<longrightarrow> e' \<turnstile> t[u/i] : T"
-  apply (erule typing.induct)
-    apply (intro strip)
+lemma subst_lemma:
+    "e \<turnstile> t : T \<Longrightarrow> (\<And>e' i U u. e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T)"
+  apply (induct set: typing)
     apply (rule_tac x = x and y = i in linorder_cases)
       apply auto
   apply blast
@@ -227,15 +224,32 @@
   apply (rule refl)
   done
 
+lemma substs_lemma [rule_format]:
+  "e \<turnstile> u : T \<Longrightarrow> \<forall>Ts. e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<longrightarrow>
+     e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
+  apply (induct_tac ts)
+   apply (intro strip)
+   apply (case_tac Ts)
+    apply simp
+   apply simp
+  apply (intro strip)
+  apply (case_tac Ts)
+   apply simp
+  apply simp
+  apply (erule conjE)
+  apply (erule subst_lemma)
+   apply assumption
+  apply (rule refl)
+  done
+
 
 subsection {* Subject reduction *}
 
-lemma subject_reduction [rule_format]:
-    "e \<turnstile> t : T \<Longrightarrow> \<forall>t'. t -> t' \<longrightarrow> e \<turnstile> t' : T"
-  apply (erule typing.induct)
+lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> (\<And>t'. t -> t' \<Longrightarrow> e \<turnstile> t' : T)"
+  apply (induct set: typing)
     apply blast
    apply blast
-  apply (intro strip)
+  apply atomize
   apply (ind_cases "s \<^sub>\<degree> t -> t'")
     apply hypsubst
     apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U")
@@ -253,10 +267,10 @@
 lemma app_last: "(t \<^sub>\<degree>\<^sub>\<degree> ts) \<^sub>\<degree> u = t \<^sub>\<degree>\<^sub>\<degree> (ts @ [u])"
   by simp
 
-lemma subst_Var_IT [rule_format]: "r \<in> IT \<Longrightarrow> \<forall>i j. r[Var i/j] \<in> IT"
-  apply (erule IT.induct)
+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 (intro strip)
+    apply atomize
     apply (simp (no_asm) add: subst_Var)
     apply
     ((rule conjI impI)+,
@@ -271,12 +285,12 @@
       fast,
       assumption)+
    txt {* Case @{term Lambda}: *}
-   apply (intro strip)
+   apply atomize
    apply simp
    apply (rule IT.Lambda)
    apply fast
   txt {* Case @{term Beta}: *}
-  apply (intro strip)
+  apply atomize
   apply (simp (no_asm_use) add: subst_subst [symmetric])
   apply (rule IT.Beta)
    apply auto
@@ -290,7 +304,7 @@
   done
 
 lemma app_Var_IT: "t \<in> IT \<Longrightarrow> t \<^sub>\<degree> Var i \<in> IT"
-  apply (erule IT.induct)
+  apply (induct set: IT)
     apply (subst app_last)
     apply (rule IT.Var)
     apply simp