# HG changeset patch
# User hoelzl
# Date 1384280932 -3600
# Node ID f72e58a5a75f50bb87accab7b3d1143a34a5df23
# Parent  0a578fb7fb737bc39b3bb41fa630e8296040dc18
stronger inc_induct and dec_induct

diff -r 0a578fb7fb73 -r f72e58a5a75f src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 12 19:28:51 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 12 19:28:52 2013 +0100
@@ -2336,12 +2336,11 @@
   qed
   {
     fix n m :: nat
-    assume "m \<le> n"
-    then have "{A n..B n} \<subseteq> {A m..B m}"
-    proof (induct rule: inc_induct)
+    assume "m \<le> n" then have "{A n..B n} \<subseteq> {A m..B m}"
+    proof (induction rule: inc_induct)
       case (step i)
       show ?case
-        using AB(4) by (intro order_trans[OF step(2)] subset_interval_imp) auto
+        using AB(4) by (intro order_trans[OF step.IH] subset_interval_imp) auto
     qed simp
   } note ABsubset = this
   have "\<exists>a. \<forall>n. a\<in>{A n..B n}"
diff -r 0a578fb7fb73 -r f72e58a5a75f src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Nov 12 19:28:51 2013 +0100
+++ b/src/HOL/Nat.thy	Tue Nov 12 19:28:52 2013 +0100
@@ -1718,20 +1718,20 @@
 text {* Specialized induction principles that work "backwards": *}
 
 lemma inc_induct[consumes 1, case_names base step]:
-  assumes less: "i <= j"
+  assumes less: "i \<le> j"
   assumes base: "P j"
-  assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i"
+  assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
   shows "P i"
-  using less
-proof (induct d=="j - i" arbitrary: i)
+  using less step
+proof (induct d\<equiv>"j - i" arbitrary: i)
   case (0 i)
   hence "i = j" by simp
   with base show ?case by simp
 next
-  case (Suc d i)
-  hence "i < j" "P (Suc i)"
+  case (Suc d n)
+  hence "n \<le> n" "n < j" "P (Suc n)"
     by simp_all
-  thus "P i" by (rule step)
+  then show "P n" by fact
 qed
 
 lemma strict_inc_induct[consumes 1, case_names base step]:
@@ -1760,9 +1760,8 @@
 text {* Further induction rule similar to @{thm inc_induct} *}
 
 lemma dec_induct[consumes 1, case_names base step]:
-  "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
+  "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
   by (induct j arbitrary: i) (auto simp: le_Suc_eq)
-
  
 subsection {* The divides relation on @{typ nat} *}