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"
```