clarified rule structure;
authorwenzelm
Mon Mar 21 21:18:08 2016 +0100 (2016-03-21)
changeset 62683ddd1c864408b
parent 62682 0c9b1857504b
child 62684 cb20e8828196
clarified rule structure;
src/HOL/Hilbert_Choice.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Mar 21 20:38:39 2016 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Mar 21 21:18:08 2016 +0100
     1.3 @@ -762,7 +762,7 @@
     1.4    next
     1.5      fix n m :: nat assume "m < n" "n \<le> N"
     1.6      then show "f m < f n"
     1.7 -    proof (induct rule: less_Suc_induct[consumes 1])
     1.8 +    proof (induct rule: less_Suc_induct)
     1.9        case (1 i)
    1.10        then have "i < N" by simp
    1.11        then have "f i \<noteq> f (Suc i)"
     2.1 --- a/src/HOL/Nat.thy	Mon Mar 21 20:38:39 2016 +0100
     2.2 +++ b/src/HOL/Nat.thy	Mon Mar 21 21:18:08 2016 +0100
     2.3 @@ -928,7 +928,7 @@
     2.4    by (rule less_induct) (auto intro: step simp:le_simps)
     2.5  
     2.6  text\<open>An induction rule for estabilishing binary relations\<close>
     2.7 -lemma less_Suc_induct:
     2.8 +lemma less_Suc_induct [consumes 1]:
     2.9    assumes less:  "i < j"
    2.10       and  step:  "!!i. P i (Suc i)"
    2.11       and  trans: "!!i j k. i < j ==> j < k ==>  P i j ==> P j k ==> P i k"
    2.12 @@ -1646,7 +1646,7 @@
    2.13  proof (cases "n < n'")
    2.14    case True
    2.15    then show ?thesis
    2.16 -    by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
    2.17 +    by (induct n n' rule: less_Suc_induct) (auto intro: mono)
    2.18  qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
    2.19  
    2.20  lemma lift_Suc_antimono_le:
    2.21 @@ -1655,14 +1655,14 @@
    2.22  proof (cases "n < n'")
    2.23    case True
    2.24    then show ?thesis
    2.25 -    by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
    2.26 +    by (induct n n' rule: less_Suc_induct) (auto intro: mono)
    2.27  qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
    2.28  
    2.29  lemma lift_Suc_mono_less:
    2.30    assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
    2.31    shows "f n < f n'"
    2.32  using \<open>n < n'\<close>
    2.33 -by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
    2.34 +by (induct n n' rule: less_Suc_induct) (auto intro: mono)
    2.35  
    2.36  lemma lift_Suc_mono_less_iff:
    2.37    "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"