# HG changeset patch
# User wenzelm
# Date 1132942184 -3600
# Node ID 2124b24454dd91aef840fca256131e666c8a7f39
# Parent  8de262a22f23cf7bae6615d8b28a2302bf60a7bf
tuned induct proofs;

diff -r 8de262a22f23 -r 2124b24454dd src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/Eta.thy	Fri Nov 25 19:09:44 2005 +0100
@@ -67,16 +67,16 @@
   apply (simp add: diff_Suc subst_Var split: nat.split)
   done
 
-lemma free_eta: "s -e> t ==> (!!i. free t i = free s i)"
-  by (induct set: eta) (simp_all cong: conj_cong)
+lemma free_eta: "s -e> t ==> free t i = free s i"
+  by (induct fixing: i set: eta) (simp_all cong: conj_cong)
 
 lemma not_free_eta:
     "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
   by (simp add: free_eta)
 
 lemma eta_subst [simp]:
-    "s -e> t ==> (!!u i. s[u/i] -e> t[u/i])"
-  by (induct set: eta) (simp_all add: subst_subst [symmetric])
+    "s -e> t ==> s[u/i] -e> t[u/i]"
+  by (induct fixing: u i set: eta) (simp_all add: subst_subst [symmetric])
 
 theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
   by (induct s fixing: i dummy) simp_all
@@ -122,17 +122,17 @@
 subsection "Commutation of beta and eta"
 
 lemma free_beta:
-    "s -> t ==> (!!i. free t i \<Longrightarrow> free s i)"
-  by (induct set: beta) auto
+    "s -> t ==> free t i \<Longrightarrow> free s i"
+  by (induct fixing: i set: beta) auto
 
-lemma beta_subst [intro]: "s -> t ==> (!!u i. s[u/i] -> t[u/i])"
-  by (induct set: beta) (simp_all add: subst_subst [symmetric])
+lemma beta_subst [intro]: "s -> t ==> s[u/i] -> t[u/i]"
+  by (induct fixing: u i set: beta) (simp_all add: subst_subst [symmetric])
 
 lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
   by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
 
-lemma eta_lift [simp]: "s -e> t ==> (!!i. lift s i -e> lift t i)"
-  by (induct set: eta) simp_all
+lemma eta_lift [simp]: "s -e> t ==> lift s i -e> lift t i"
+  by (induct fixing: i set: eta) simp_all
 
 lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
   apply (induct u fixing: s t i)
diff -r 8de262a22f23 -r 2124b24454dd src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Fri Nov 25 19:09:44 2005 +0100
@@ -159,8 +159,8 @@
   Normalization. \medskip *}
 
 theorem subst_preserves_beta [simp]:
-    "r \<rightarrow>\<^sub>\<beta> s ==> (\<And>t i. r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i])"
-  by (induct set: beta) (simp_all add: subst_subst [symmetric])
+    "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
+  by (induct fixing: t i set: beta) (simp_all add: subst_subst [symmetric])
 
 theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
   apply (induct set: rtrancl)
@@ -170,8 +170,8 @@
   done
 
 theorem lift_preserves_beta [simp]:
-    "r \<rightarrow>\<^sub>\<beta> s ==> (\<And>i. lift r i \<rightarrow>\<^sub>\<beta> lift s i)"
-  by (induct set: beta) auto
+    "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
+  by (induct fixing: i set: beta) auto
 
 theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
   apply (induct set: rtrancl)
diff -r 8de262a22f23 -r 2124b24454dd src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/ListApplication.thy	Fri Nov 25 19:09:44 2005 +0100
@@ -53,11 +53,11 @@
   done
 
 lemma Abs_App_neq_Var_apps [iff]:
-    "Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
+    "Abs s \<degree> t \<noteq> Var n \<degree>\<degree> ss"
   by (induct ss fixing: s t rule: rev_induct) auto
 
 lemma Var_apps_neq_Abs_apps [iff]:
-    "Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
+    "Var n \<degree>\<degree> ts \<noteq> Abs r \<degree>\<degree> ss"
   apply (induct ss fixing: ts rule: rev_induct)
    apply simp
   apply (induct_tac ts rule: rev_induct)
diff -r 8de262a22f23 -r 2124b24454dd src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/ListOrder.thy	Fri Nov 25 19:09:44 2005 +0100
@@ -64,12 +64,13 @@
   apply (blast intro: append_eq_appendI)
   done
 
-lemma Cons_step1E [rule_format, elim!]:
-  "[| (ys, x # xs) \<in> step1 r;
-    \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
-    \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
-   |] ==> R"
-  apply (case_tac ys)
+lemma Cons_step1E [elim!]:
+  assumes "(ys, x # xs) \<in> step1 r"
+    and "!!y. ys = y # xs \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> R"
+    and "!!zs. ys = x # zs \<Longrightarrow> (zs, xs) \<in> step1 r \<Longrightarrow> R"
+  shows R
+  using prems
+  apply (cases ys)
    apply (simp add: step1_def)
   apply blast
   done
@@ -88,8 +89,8 @@
   done
 
 lemma Cons_acc_step1I [intro!]:
-    "x \<in> acc r ==> (!!xs. xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r))"
-  apply (induct set: acc)
+    "x \<in> acc r ==> xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r)"
+  apply (induct fixing: xs set: acc)
   apply (erule thin_rl)
   apply (erule acc_induct)
   apply (rule accI)
diff -r 8de262a22f23 -r 2124b24454dd src/HOL/Lambda/StrongNorm.thy
--- a/src/HOL/Lambda/StrongNorm.thy	Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/StrongNorm.thy	Fri Nov 25 19:09:44 2005 +0100
@@ -16,8 +16,8 @@
 
 subsection {* Properties of @{text IT} *}
 
-lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> (\<And>i. lift t i \<in> IT)"
-  apply (induct set: IT)
+lemma lift_IT [intro!]: "t \<in> IT \<Longrightarrow> lift t i \<in> IT"
+  apply (induct fixing: i set: IT)
     apply (simp (no_asm))
     apply (rule conjI)
      apply
@@ -37,8 +37,8 @@
 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)
+lemma subst_Var_IT: "r \<in> IT \<Longrightarrow> r[Var i/j] \<in> IT"
+  apply (induct fixing: i j set: IT)
     txt {* Case @{term Var}: *}
     apply (simp (no_asm) add: subst_Var)
     apply
@@ -249,34 +249,33 @@
 
 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
+lemma type_implies_IT:
+  assumes "e \<turnstile> t : T"
+  shows "t \<in> IT"
+  using prems
+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
 
 theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> t \<in> termi beta"
diff -r 8de262a22f23 -r 2124b24454dd src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/Type.thy	Fri Nov 25 19:09:44 2005 +0100
@@ -288,8 +288,8 @@
 
 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_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
+  by (induct fixing: i U set: typing) auto
 
 lemma lift_types:
   "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
@@ -303,8 +303,8 @@
 subsection {* Substitution lemmas *}
 
 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)
+    "e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T"
+  apply (induct fixing: e' i U u set: typing)
     apply (rule_tac x = x and y = i in linorder_cases)
       apply auto
   apply blast
@@ -329,8 +329,8 @@
 
 subsection {* Subject reduction *}
 
-lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> (\<And>t'. t -> t' \<Longrightarrow> e \<turnstile> t' : T)"
-  apply (induct set: typing)
+lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t -> t' \<Longrightarrow> e \<turnstile> t' : T"
+  apply (induct fixing: t' set: typing)
     apply blast
    apply blast
   apply atomize
diff -r 8de262a22f23 -r 2124b24454dd src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Nov 25 19:09:44 2005 +0100
@@ -113,8 +113,8 @@
   listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"
   by (induct ts) simp+
 
-lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> (\<And>i j. t[Var i/j] \<in> NF)"
-  apply (induct set: NF)
+lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"
+  apply (induct fixing: i j set: NF)
   apply simp
   apply (frule listall_conj1)
   apply (drule listall_conj2)
@@ -153,10 +153,10 @@
 lemma lift_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>
   listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>
   listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"
-  by (induct ts) simp+
+  by (induct ts) simp_all
 
-lemma lift_NF: "t \<in> NF \<Longrightarrow> (\<And>i. lift t i \<in> NF)"
-  apply (induct set: NF)
+lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"
+  apply (induct fixing: i set: NF)
   apply (frule listall_conj1)
   apply (drule listall_conj2)
   apply (drule_tac i=i in lift_terms_NF)