# HG changeset patch
# User wenzelm
# Date 1005686283 -3600
# Node ID dc87f33db4477d33d09a3d2003228e38a3088685
# Parent  1433a9cdb55cad4218942f2163b84cb36cc02eea
tuned inductions;

diff -r 1433a9cdb55c -r dc87f33db447 src/HOL/Induct/ABexp.thy
--- a/src/HOL/Induct/ABexp.thy	Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Induct/ABexp.thy	Tue Nov 13 22:18:03 2001 +0100
@@ -55,20 +55,17 @@
   "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
   "substb f (Neg b) = Neg (substb f b)"
 
-lemma subst1_aexp_bexp:
-  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a \<and>
-  evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
+lemma subst1_aexp:
+  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
+and subst1_bexp:
+  "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
     --  {* one variable *}
-  apply (induct a and b)
-         apply simp_all
-  done
+  by (induct a and b) simp_all
 
-lemma subst_all_aexp_bexp:
-  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a \<and>
-  evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
-    -- {* all variables *}
-  apply (induct a and b)
-         apply auto
-  done
+lemma subst_all_aexp:
+  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
+and subst_all_bexp:
+  "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
+  by (induct a and b) auto
 
 end
diff -r 1433a9cdb55c -r dc87f33db447 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Induct/Mutil.thy	Tue Nov 13 22:18:03 2001 +0100
@@ -101,7 +101,7 @@
 text {* \medskip Tilings of dominoes *}
 
 lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
-  apply (erule tiling.induct)
+  apply (induct set: tiling)
    apply auto
   done
 
@@ -111,7 +111,7 @@
 
 lemma tiling_domino_0_1:
   "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured (Suc 0) \<inter> t)"
-  apply (erule tiling.induct)
+  apply (induct set: tiling)
    apply (drule_tac [2] domino_singletons)
    apply auto
   apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
diff -r 1433a9cdb55c -r dc87f33db447 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Induct/Term.thy	Tue Nov 13 22:18:03 2001 +0100
@@ -32,31 +32,25 @@
 text {* \medskip A simple theorem about composition of substitutions *}
 
 lemma subst_comp:
-  "(subst_term ((subst_term f1) \<circ> f2) t) =
-    (subst_term f1 (subst_term f2 t)) \<and>
-  (subst_term_list ((subst_term f1) \<circ> f2) ts) =
-    (subst_term_list f1 (subst_term_list f2 ts))"
-  apply (induct t and ts)
-     apply simp_all
-  done
+  "subst_term (subst_term f1 \<circ> f2) t =
+    subst_term f1 (subst_term f2 t)"
+and "subst_term_list (subst_term f1 \<circ> f2) ts =
+    subst_term_list f1 (subst_term_list f2 ts)"
+  by (induct t and ts) simp_all
 
 
 text {* \medskip Alternative induction rule *}
 
-lemma term_induct2:
-  "(!!v. P (Var v)) ==>
-    (!!f ts. list_all P ts ==> P (App f ts))
-  ==> P t"
-proof -
-  case rule_context
-  have "P t \<and> list_all P ts"
-    apply (induct t and ts)
-       apply (rule rule_context)
-      apply (rule rule_context)
-      apply assumption
-     apply simp_all
-    done
-  thus ?thesis ..
-qed
+lemma
+  (assumes var: "!!v. P (Var v)"
+    and app: "!!f ts. list_all P ts ==> P (App f ts)")
+  term_induct2: "P t"
+and "list_all P ts"
+  apply (induct t and ts)
+     apply (rule var)
+    apply (rule app)
+    apply assumption
+   apply simp_all
+  done
 
 end
diff -r 1433a9cdb55c -r dc87f33db447 src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Induct/Tree.thy	Tue Nov 13 22:18:03 2001 +0100
@@ -19,9 +19,7 @@
   "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
 
 lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
-  apply (induct t)
-   apply simp_all
-  done
+  by (induct t) simp_all
 
 consts
   exists_tree :: "('a => bool) => 'a tree => bool"
@@ -32,9 +30,6 @@
 lemma exists_map:
   "(!!x. P x ==> Q (f x)) ==>
     exists_tree P ts ==> exists_tree Q (map_tree f ts)"
-  apply (induct ts)
-   apply simp_all
-  apply blast
-  done
+  by (induct ts) auto
 
 end
diff -r 1433a9cdb55c -r dc87f33db447 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Lambda/Type.thy	Tue Nov 13 22:18:03 2001 +0100
@@ -182,12 +182,9 @@
 lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
   by (induct ts) auto
 
-lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
-proof -
-  assume "e \<turnstile> t : T"
-  thus "\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
-    by induct auto
-qed
+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:
   "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
@@ -473,6 +470,7 @@
   qed
 qed
 
+
 subsection {* Well-typed terms are strongly normalizing *}
 
 lemma type_implies_IT: "e \<turnstile> t : T \<Longrightarrow> t \<in> IT"