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