--- 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}"
--- 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} *}