src/HOL/Nat.thy
 changeset 54411 f72e58a5a75f parent 54223 85705ba18add child 54496 178922b63b58
```     1.1 --- a/src/HOL/Nat.thy	Tue Nov 12 19:28:51 2013 +0100
1.2 +++ b/src/HOL/Nat.thy	Tue Nov 12 19:28:52 2013 +0100
1.3 @@ -1718,20 +1718,20 @@
1.4  text {* Specialized induction principles that work "backwards": *}
1.5
1.6  lemma inc_induct[consumes 1, case_names base step]:
1.7 -  assumes less: "i <= j"
1.8 +  assumes less: "i \<le> j"
1.9    assumes base: "P j"
1.10 -  assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i"
1.11 +  assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
1.12    shows "P i"
1.13 -  using less
1.14 -proof (induct d=="j - i" arbitrary: i)
1.15 +  using less step
1.16 +proof (induct d\<equiv>"j - i" arbitrary: i)
1.17    case (0 i)
1.18    hence "i = j" by simp
1.19    with base show ?case by simp
1.20  next
1.21 -  case (Suc d i)
1.22 -  hence "i < j" "P (Suc i)"
1.23 +  case (Suc d n)
1.24 +  hence "n \<le> n" "n < j" "P (Suc n)"
1.25      by simp_all
1.26 -  thus "P i" by (rule step)
1.27 +  then show "P n" by fact
1.28  qed
1.29
1.30  lemma strict_inc_induct[consumes 1, case_names base step]:
1.31 @@ -1760,9 +1760,8 @@
1.32  text {* Further induction rule similar to @{thm inc_induct} *}
1.33
1.34  lemma dec_induct[consumes 1, case_names base step]:
1.35 -  "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
1.36 +  "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"
1.37    by (induct j arbitrary: i) (auto simp: le_Suc_eq)
1.38 -
1.39
1.40  subsection {* The divides relation on @{typ nat} *}
1.41
```