src/HOL/Nat.thy
changeset 62683 ddd1c864408b
parent 62608 19f87fa0cfcb
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/Nat.thy	Mon Mar 21 20:38:39 2016 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Mar 21 21:18:08 2016 +0100
     1.3 @@ -928,7 +928,7 @@
     1.4    by (rule less_induct) (auto intro: step simp:le_simps)
     1.5  
     1.6  text\<open>An induction rule for estabilishing binary relations\<close>
     1.7 -lemma less_Suc_induct:
     1.8 +lemma less_Suc_induct [consumes 1]:
     1.9    assumes less:  "i < j"
    1.10       and  step:  "!!i. P i (Suc i)"
    1.11       and  trans: "!!i j k. i < j ==> j < k ==>  P i j ==> P j k ==> P i k"
    1.12 @@ -1646,7 +1646,7 @@
    1.13  proof (cases "n < n'")
    1.14    case True
    1.15    then show ?thesis
    1.16 -    by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
    1.17 +    by (induct n n' rule: less_Suc_induct) (auto intro: mono)
    1.18  qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
    1.19  
    1.20  lemma lift_Suc_antimono_le:
    1.21 @@ -1655,14 +1655,14 @@
    1.22  proof (cases "n < n'")
    1.23    case True
    1.24    then show ?thesis
    1.25 -    by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
    1.26 +    by (induct n n' rule: less_Suc_induct) (auto intro: mono)
    1.27  qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
    1.28  
    1.29  lemma lift_Suc_mono_less:
    1.30    assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
    1.31    shows "f n < f n'"
    1.32  using \<open>n < n'\<close>
    1.33 -by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
    1.34 +by (induct n n' rule: less_Suc_induct) (auto intro: mono)
    1.35  
    1.36  lemma lift_Suc_mono_less_iff:
    1.37    "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"