src/HOL/Nat.thy
changeset 47988 e4b69e10b990
parent 47489 04e7d09ade7a
child 48559 686cc7c47589
     1.1 --- a/src/HOL/Nat.thy	Thu May 24 17:05:30 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Thu May 24 17:25:53 2012 +0200
     1.3 @@ -820,12 +820,12 @@
     1.4  
     1.5  lemma Least_Suc:
     1.6       "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
     1.7 -  apply (case_tac "n", auto)
     1.8 +  apply (cases n, auto)
     1.9    apply (frule LeastI)
    1.10    apply (drule_tac P = "%x. P (Suc x) " in LeastI)
    1.11    apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
    1.12    apply (erule_tac [2] Least_le)
    1.13 -  apply (case_tac "LEAST x. P x", auto)
    1.14 +  apply (cases "LEAST x. P x", auto)
    1.15    apply (drule_tac P = "%x. P (Suc x) " in Least_le)
    1.16    apply (blast intro: order_antisym)
    1.17    done
    1.18 @@ -911,7 +911,7 @@
    1.19  text{* A compact version without explicit base case: *}
    1.20  lemma infinite_descent:
    1.21    "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
    1.22 -by (induct n rule: less_induct, auto)
    1.23 +by (induct n rule: less_induct) auto
    1.24  
    1.25  lemma infinite_descent0[case_names 0 smaller]: 
    1.26    "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
    1.27 @@ -1164,7 +1164,7 @@
    1.28  
    1.29  lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
    1.30    apply (safe intro!: mult_less_mono1)
    1.31 -  apply (case_tac k, auto)
    1.32 +  apply (cases k, auto)
    1.33    apply (simp del: le_0_eq add: linorder_not_le [symmetric])
    1.34    apply (blast intro: mult_le_mono1)
    1.35    done