src/HOL/Nat.thy
changeset 15251 bb6f072c8d10
parent 15140 322485b816ac
child 15281 bd4611956c7b
     1.1 --- a/src/HOL/Nat.thy	Mon Oct 18 13:40:45 2004 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Oct 19 18:18:45 2004 +0200
     1.3 @@ -149,7 +149,7 @@
     1.4  theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
     1.5      (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
     1.6    apply (rule_tac x = m in spec)
     1.7 -  apply (induct_tac n)
     1.8 +  apply (induct n)
     1.9    prefer 2
    1.10    apply (rule allI)
    1.11    apply (induct_tac x, rules+)
    1.12 @@ -261,8 +261,8 @@
    1.13  
    1.14  text {* "Less than" is a linear ordering *}
    1.15  lemma less_linear: "m < n | m = n | n < (m::nat)"
    1.16 -  apply (induct_tac m)
    1.17 -  apply (induct_tac n)
    1.18 +  apply (induct m)
    1.19 +  apply (induct n)
    1.20    apply (rule refl [THEN disjI1, THEN disjI2])
    1.21    apply (rule zero_less_Suc [THEN disjI1])
    1.22    apply (blast intro: Suc_mono less_SucI elim: lessE)
    1.23 @@ -614,10 +614,10 @@
    1.24  text {* Difference *}
    1.25  
    1.26  lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
    1.27 -  by (induct_tac n) simp_all
    1.28 +  by (induct n) simp_all
    1.29  
    1.30  lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
    1.31 -  by (induct_tac n) simp_all
    1.32 +  by (induct n) simp_all
    1.33  
    1.34  
    1.35  text {*
    1.36 @@ -730,7 +730,7 @@
    1.37  qed
    1.38  
    1.39  lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
    1.40 -  apply (induct_tac m)
    1.41 +  apply (induct m)
    1.42    apply (induct_tac [2] n, simp_all)
    1.43    done
    1.44  
    1.45 @@ -743,7 +743,7 @@
    1.46  text {* strict, in both arguments *}
    1.47  lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
    1.48    apply (rule add_less_mono1 [THEN less_trans], assumption+)
    1.49 -  apply (induct_tac j, simp_all)
    1.50 +  apply (induct j, simp_all)
    1.51    done
    1.52  
    1.53  text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
    1.54 @@ -999,8 +999,8 @@
    1.55    done
    1.56  
    1.57  lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
    1.58 -  apply (induct_tac m, simp)
    1.59 -  apply (induct_tac n, simp, fastsimp)
    1.60 +  apply (induct m, simp)
    1.61 +  apply (induct n, simp, fastsimp)
    1.62    done
    1.63  
    1.64  lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"