src/HOL/Nat.thy
changeset 62481 b5d8e57826df
parent 62378 85ed00c1fe7c
child 62502 8857237c3a90
     1.1 --- a/src/HOL/Nat.thy	Tue Mar 01 10:32:55 2016 +0100
     1.2 +++ b/src/HOL/Nat.thy	Tue Mar 01 10:36:19 2016 +0100
     1.3 @@ -8,14 +8,13 @@
     1.4  section \<open>Natural numbers\<close>
     1.5  
     1.6  theory Nat
     1.7 -imports Inductive Typedef Fun Fields
     1.8 +imports Inductive Typedef Fun Rings
     1.9  begin
    1.10  
    1.11  ML_file "~~/src/Tools/rat.ML"
    1.12  
    1.13  named_theorems arith "arith facts -- only ground formulas"
    1.14  ML_file "Tools/arith_data.ML"
    1.15 -ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
    1.16  
    1.17  
    1.18  subsection \<open>Type \<open>ind\<close>\<close>
    1.19 @@ -724,11 +723,16 @@
    1.20    by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
    1.21  
    1.22  text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
    1.23 -lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
    1.24 -apply(auto simp: gr0_conv_Suc)
    1.25 -apply (induct_tac m)
    1.26 -apply (simp_all add: add_less_mono)
    1.27 -done
    1.28 +lemma mult_less_mono2:
    1.29 +  fixes i j :: nat
    1.30 +  assumes "i < j" and "0 < k"
    1.31 +  shows "k * i < k * j"
    1.32 +using \<open>0 < k\<close> proof (induct k)
    1.33 +  case 0 then show ?case by simp
    1.34 +next
    1.35 +  case (Suc k) with \<open>i < j\<close> show ?case
    1.36 +    by (cases k) (simp_all add: add_less_mono)
    1.37 +qed
    1.38  
    1.39  text \<open>Addition is the inverse of subtraction:
    1.40    if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close>
    1.41 @@ -1103,8 +1107,18 @@
    1.42  lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
    1.43  by (induct j k rule: diff_induct) simp_all
    1.44  
    1.45 +lemma add_diff_assoc [simp]:
    1.46 +  fixes i j k :: nat
    1.47 +  shows "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k"
    1.48 +  by (fact diff_add_assoc [symmetric])
    1.49 +
    1.50  lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
    1.51 -by (simp add: add.commute diff_add_assoc)
    1.52 +  by (simp add: ac_simps)
    1.53 +
    1.54 +lemma add_diff_assoc2 [simp]:
    1.55 +  fixes i j k :: nat
    1.56 +  shows "k \<le> j \<Longrightarrow> j - k + i = j + i - k"
    1.57 +  by (fact diff_add_assoc2 [symmetric])
    1.58  
    1.59  lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
    1.60  by auto
    1.61 @@ -1457,6 +1471,14 @@
    1.62  
    1.63  declare of_nat_code [code]
    1.64  
    1.65 +context ring_1
    1.66 +begin
    1.67 +
    1.68 +lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
    1.69 +by (simp add: algebra_simps of_nat_add [symmetric])
    1.70 +
    1.71 +end
    1.72 +
    1.73  text\<open>Class for unital semirings with characteristic zero.
    1.74   Includes non-ordered rings like the complex numbers.\<close>
    1.75  
    1.76 @@ -1485,6 +1507,8 @@
    1.77  
    1.78  end
    1.79  
    1.80 +class ring_char_0 = ring_1 + semiring_char_0
    1.81 +
    1.82  context linordered_semidom
    1.83  begin
    1.84  
    1.85 @@ -1521,14 +1545,6 @@
    1.86  
    1.87  end
    1.88  
    1.89 -context ring_1
    1.90 -begin
    1.91 -
    1.92 -lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
    1.93 -by (simp add: algebra_simps of_nat_add [symmetric])
    1.94 -
    1.95 -end
    1.96 -
    1.97  context linordered_idom
    1.98  begin
    1.99  
   1.100 @@ -1621,21 +1637,6 @@
   1.101    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
   1.102    \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
   1.103  
   1.104 -ML_file "Tools/lin_arith.ML"
   1.105 -setup \<open>Lin_Arith.global_setup\<close>
   1.106 -declaration \<open>K Lin_Arith.setup\<close>
   1.107 -
   1.108 -simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
   1.109 -  \<open>K Lin_Arith.simproc\<close>
   1.110 -(* Because of this simproc, the arithmetic solver is really only
   1.111 -useful to detect inconsistencies among the premises for subgoals which are
   1.112 -*not* themselves (in)equalities, because the latter activate
   1.113 -fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
   1.114 -solver all the time rather than add the additional check. *)
   1.115 -
   1.116 -
   1.117 -lemmas [arith_split] = nat_diff_split split_min split_max
   1.118 -
   1.119  context order
   1.120  begin
   1.121  
   1.122 @@ -1695,62 +1696,95 @@
   1.123  
   1.124  text\<open>Subtraction laws, mostly by Clemens Ballarin\<close>
   1.125  
   1.126 -lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
   1.127 -by arith
   1.128 -
   1.129 -lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
   1.130 -by arith
   1.131 +lemma diff_less_mono:
   1.132 +  fixes a b c :: nat
   1.133 +  assumes "a < b" and "c \<le> a"
   1.134 +  shows "a - c < b - c"
   1.135 +proof -
   1.136 +  from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0"
   1.137 +    by (auto dest!: le_Suc_ex less_imp_Suc_add simp add: ac_simps)
   1.138 +  then show ?thesis by simp
   1.139 +qed
   1.140 +
   1.141 +lemma less_diff_conv:
   1.142 +  fixes i j k :: nat
   1.143 +  shows "i < j - k \<longleftrightarrow> i + k < j" (is "?P \<longleftrightarrow> ?Q")
   1.144 +  by (cases "k \<le> j")
   1.145 +    (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
   1.146  
   1.147  lemma less_diff_conv2:
   1.148    fixes j k i :: nat
   1.149    assumes "k \<le> j"
   1.150 -  shows "j - k < i \<longleftrightarrow> j < i + k"
   1.151 -  using assms by arith
   1.152 -
   1.153 -lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
   1.154 -by arith
   1.155 -
   1.156 -lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
   1.157 -by arith
   1.158 -
   1.159 -(*Replaces the previous diff_less and le_diff_less, which had the stronger
   1.160 -  second premise n\<le>m*)
   1.161 -lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
   1.162 -by arith
   1.163 +  shows "j - k < i \<longleftrightarrow> j < i + k" (is "?P \<longleftrightarrow> ?Q")
   1.164 +  using assms by (auto dest: le_Suc_ex)
   1.165 +
   1.166 +lemma le_diff_conv:
   1.167 +  fixes j k i :: nat
   1.168 +  shows "j - k \<le> i \<longleftrightarrow> j \<le> i + k"
   1.169 +  by (cases "k \<le> j")
   1.170 +    (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
   1.171 +
   1.172 +lemma diff_diff_cancel [simp]:
   1.173 +  fixes i n :: nat
   1.174 +  shows "i \<le> n \<Longrightarrow> n - (n - i) = i"
   1.175 +  by (auto dest: le_Suc_ex)
   1.176 +
   1.177 +lemma diff_less [simp]:
   1.178 +  fixes i n :: nat
   1.179 +  shows "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m"
   1.180 +  by (auto dest: less_imp_Suc_add)
   1.181  
   1.182  text \<open>Simplification of relational expressions involving subtraction\<close>
   1.183  
   1.184 -lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
   1.185 -by (simp split add: nat_diff_split)
   1.186 +lemma diff_diff_eq:
   1.187 +  fixes m n k :: nat
   1.188 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n"
   1.189 +  by (auto dest!: le_Suc_ex)
   1.190  
   1.191  hide_fact (open) diff_diff_eq
   1.192  
   1.193 -lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
   1.194 -by (auto split add: nat_diff_split)
   1.195 -
   1.196 -lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
   1.197 -by (auto split add: nat_diff_split)
   1.198 -
   1.199 -lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
   1.200 -by (auto split add: nat_diff_split)
   1.201 +lemma eq_diff_iff:
   1.202 +  fixes m n k :: nat
   1.203 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n"
   1.204 +  by (auto dest: le_Suc_ex)
   1.205 +
   1.206 +lemma less_diff_iff:
   1.207 +  fixes m n k :: nat
   1.208 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n"
   1.209 +  by (auto dest!: le_Suc_ex)
   1.210 +
   1.211 +lemma le_diff_iff:
   1.212 +  fixes m n k :: nat
   1.213 +  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
   1.214 +  by (auto dest!: le_Suc_ex)
   1.215  
   1.216  text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
   1.217  
   1.218 -(* Monotonicity of subtraction in first argument *)
   1.219 -lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
   1.220 -by (simp split add: nat_diff_split)
   1.221 -
   1.222 -lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
   1.223 -by (simp split add: nat_diff_split)
   1.224 -
   1.225 -lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
   1.226 -by (simp split add: nat_diff_split)
   1.227 -
   1.228 -lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
   1.229 -by (simp split add: nat_diff_split)
   1.230 -
   1.231 -lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
   1.232 -by auto
   1.233 +lemma diff_le_mono:
   1.234 +  fixes m n l :: nat
   1.235 +  shows "m \<le> n \<Longrightarrow> m - l \<le> n - l"
   1.236 +  by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
   1.237 +
   1.238 +lemma diff_le_mono2:
   1.239 +  fixes m n l :: nat
   1.240 +  shows "m \<le> n \<Longrightarrow> l - n \<le> l - m"
   1.241 +  by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
   1.242 +
   1.243 +lemma diff_less_mono2:
   1.244 +  fixes m n l :: nat
   1.245 +  shows "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
   1.246 +  by (auto dest: less_imp_Suc_add split add: nat_diff_split)
   1.247 +
   1.248 +lemma diffs0_imp_equal:
   1.249 +  fixes m n :: nat
   1.250 +  shows "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
   1.251 +  by (simp split add: nat_diff_split)
   1.252 +
   1.253 +lemma min_diff:
   1.254 +  fixes m n i :: nat
   1.255 +  shows "min (m - i) (n - i) = min m n - i" (is "?lhs = ?rhs")
   1.256 +  by (cases m n rule: le_cases)
   1.257 +    (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono)
   1.258  
   1.259  lemma inj_on_diff_nat:
   1.260    assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
   1.261 @@ -1759,78 +1793,130 @@
   1.262    fix x y
   1.263    assume a: "x \<in> N" "y \<in> N" "x - k = y - k"
   1.264    with k_le_n have "x - k + k = y - k + k" by auto
   1.265 -  with a k_le_n show "x = y" by auto
   1.266 +  with a k_le_n show "x = y" by (auto simp add: eq_diff_iff)
   1.267  qed
   1.268  
   1.269  text\<open>Rewriting to pull differences out\<close>
   1.270  
   1.271 -lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
   1.272 -by arith
   1.273 -
   1.274 -lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
   1.275 -by arith
   1.276 -
   1.277 -lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
   1.278 -by arith
   1.279 -
   1.280 -lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
   1.281 -by simp
   1.282 -
   1.283 -(*The others are
   1.284 -      i - j - k = i - (j + k),
   1.285 -      k \<le> j ==> j - k + i = j + i - k,
   1.286 -      k \<le> j ==> i + (j - k) = i + j - k *)
   1.287 -lemmas add_diff_assoc = diff_add_assoc [symmetric]
   1.288 -lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
   1.289 -declare add_diff_assoc [simp] add_diff_assoc2[simp]
   1.290 -
   1.291 -text\<open>At present we prove no analogue of \<open>not_less_Least\<close> or \<open>Least_Suc\<close>, since there appears to be no need.\<close>
   1.292 -
   1.293 -text\<open>Lemmas for ex/Factorization\<close>
   1.294 -
   1.295 -lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
   1.296 -by (cases m) auto
   1.297 -
   1.298 -lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
   1.299 -by (cases m) auto
   1.300 -
   1.301 -lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
   1.302 -by (cases m) auto
   1.303 +lemma diff_diff_right [simp]:
   1.304 +  fixes i j k :: nat
   1.305 +  shows "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j"
   1.306 +  by (fact diff_diff_right)
   1.307 +
   1.308 +lemma diff_Suc_diff_eq1 [simp]:
   1.309 +  assumes "k \<le> j"
   1.310 +  shows "i - Suc (j - k) = i + k - Suc j"
   1.311 +proof -
   1.312 +  from assms have *: "Suc (j - k) = Suc j - k"
   1.313 +    by (simp add: Suc_diff_le)
   1.314 +  from assms have "k \<le> Suc j"
   1.315 +    by (rule order_trans) simp
   1.316 +  with diff_diff_right [of k "Suc j" i] * show ?thesis
   1.317 +    by simp
   1.318 +qed
   1.319 +
   1.320 +lemma diff_Suc_diff_eq2 [simp]:
   1.321 +  assumes "k \<le> j"
   1.322 +  shows "Suc (j - k) - i = Suc j - (k + i)"
   1.323 +proof -
   1.324 +  from assms obtain n where "j = k + n"
   1.325 +    by (auto dest: le_Suc_ex)
   1.326 +  moreover have "Suc n - i = (k + Suc n) - (k + i)"
   1.327 +    using add_diff_cancel_left [of k "Suc n" i] by simp
   1.328 +  ultimately show ?thesis by simp
   1.329 +qed
   1.330 +
   1.331 +lemma Suc_diff_Suc:
   1.332 +  assumes "n < m"
   1.333 +  shows "Suc (m - Suc n) = m - n"
   1.334 +proof -
   1.335 +  from assms obtain q where "m = n + Suc q"
   1.336 +    by (auto dest: less_imp_Suc_add)
   1.337 +  moreover def r \<equiv> "Suc q"
   1.338 +  ultimately have "Suc (m - Suc n) = r" and "m = n + r"
   1.339 +    by simp_all
   1.340 +  then show ?thesis by simp
   1.341 +qed
   1.342 +
   1.343 +lemma one_less_mult:
   1.344 +  "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
   1.345 +  using less_1_mult [of n m] by (simp add: ac_simps)
   1.346 +
   1.347 +lemma n_less_m_mult_n:
   1.348 +  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
   1.349 +  using mult_strict_right_mono [of 1 m n] by simp
   1.350 +
   1.351 +lemma n_less_n_mult_m:
   1.352 +  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
   1.353 +  using mult_strict_left_mono [of 1 m n] by simp
   1.354  
   1.355  text \<open>Specialized induction principles that work "backwards":\<close>
   1.356  
   1.357 -lemma inc_induct[consumes 1, case_names base step]:
   1.358 +lemma inc_induct [consumes 1, case_names base step]:
   1.359    assumes less: "i \<le> j"
   1.360    assumes base: "P j"
   1.361    assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
   1.362    shows "P i"
   1.363    using less step
   1.364 -proof (induct d\<equiv>"j - i" arbitrary: i)
   1.365 +proof (induct "j - i" arbitrary: i)
   1.366    case (0 i)
   1.367 -  hence "i = j" by simp
   1.368 +  then have "i = j" by simp
   1.369    with base show ?case by simp
   1.370  next
   1.371    case (Suc d n)
   1.372 -  hence "n \<le> n" "n < j" "P (Suc n)"
   1.373 -    by simp_all
   1.374 -  then show "P n" by fact
   1.375 +  from Suc.hyps have "n \<noteq> j" by auto
   1.376 +  with Suc have "n < j" by (simp add: less_le)
   1.377 +  from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp
   1.378 +  then have "d + 1 - 1 = j - n - 1" by simp
   1.379 +  then have "d = j - n - 1" by simp
   1.380 +  then have "d = j - (n + 1)" 
   1.381 +    by (simp add: diff_diff_eq)
   1.382 +  then have "d = j - Suc n"
   1.383 +    by simp
   1.384 +  moreover from \<open>n < j\<close> have "Suc n \<le> j"
   1.385 +    by (simp add: Suc_le_eq)
   1.386 +  ultimately have "P (Suc n)"
   1.387 +  thm Suc.hyps TrueI Suc.prems
   1.388 +  proof (rule Suc.hyps)
   1.389 +    fix q
   1.390 +    assume "Suc n \<le> q"
   1.391 +    then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le)
   1.392 +    moreover assume "q < j"
   1.393 +    moreover assume "P (Suc q)"
   1.394 +    ultimately show "P q"
   1.395 +      by (rule Suc.prems)
   1.396 +  qed
   1.397 +  with order_refl \<open>n < j\<close> show "P n"
   1.398 +    by (rule Suc.prems)
   1.399  qed
   1.400 -
   1.401 -lemma strict_inc_induct[consumes 1, case_names base step]:
   1.402 +    
   1.403 +lemma strict_inc_induct [consumes 1, case_names base step]:
   1.404    assumes less: "i < j"
   1.405 -  assumes base: "!!i. j = Suc i ==> P i"
   1.406 -  assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i"
   1.407 +  assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i"
   1.408 +  assumes step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
   1.409    shows "P i"
   1.410 -  using less
   1.411 -proof (induct d=="j - i - 1" arbitrary: i)
   1.412 +using less proof (induct "j - i - 1" arbitrary: i)
   1.413    case (0 i)
   1.414 -  with \<open>i < j\<close> have "j = Suc i" by simp
   1.415 +  from \<open>i < j\<close> obtain n where "j = i + n" and "n > 0"
   1.416 +    by (auto dest!: less_imp_Suc_add)
   1.417 +  with 0 have "j = Suc i"
   1.418 +    by (auto intro: order_antisym simp add: Suc_le_eq)
   1.419    with base show ?case by simp
   1.420  next
   1.421    case (Suc d i)
   1.422 -  hence "i < j" "P (Suc i)"
   1.423 -    by simp_all
   1.424 -  thus "P i" by (rule step)
   1.425 +  from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i"
   1.426 +    by (simp add: diff_diff_add)
   1.427 +  then have "Suc d - 1 = j - Suc i - 1"
   1.428 +    by simp
   1.429 +  then have "d = j - Suc i - 1"
   1.430 +    by simp
   1.431 +  moreover from * have "j - Suc i \<noteq> 0"
   1.432 +    by auto
   1.433 +  then have "Suc i < j"
   1.434 +    by (simp add: not_le)
   1.435 +  ultimately have "P (Suc i)"
   1.436 +    by (rule Suc.hyps)
   1.437 +  with \<open>i < j\<close> show "P i" by (rule step)
   1.438  qed
   1.439  
   1.440  lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
   1.441 @@ -1841,9 +1927,35 @@
   1.442  
   1.443  text \<open>Further induction rule similar to @{thm inc_induct}\<close>
   1.444  
   1.445 -lemma dec_induct[consumes 1, case_names base step]:
   1.446 +lemma dec_induct [consumes 1, case_names base step]:
   1.447    "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
   1.448 -  by (induct j arbitrary: i) (auto simp: le_Suc_eq)
   1.449 +proof (induct j arbitrary: i)
   1.450 +  case 0 then show ?case by simp
   1.451 +next
   1.452 +  case (Suc j)
   1.453 +  from Suc.prems have "i \<le> j \<or> i = Suc j"
   1.454 +    by (simp add: le_Suc_eq)
   1.455 +  then show ?case proof
   1.456 +    assume "i \<le> j"
   1.457 +    moreover have "j < Suc j" by simp
   1.458 +    moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close>
   1.459 +    proof (rule Suc.hyps)
   1.460 +      fix q
   1.461 +      assume "i \<le> q"
   1.462 +      moreover assume "q < j" then have "q < Suc j"
   1.463 +        by (simp add: less_Suc_eq)
   1.464 +      moreover assume "P q"
   1.465 +      ultimately show "P (Suc q)"
   1.466 +        by (rule Suc.prems)
   1.467 +    qed
   1.468 +    ultimately show "P (Suc j)"
   1.469 +      by (rule Suc.prems)
   1.470 +  next
   1.471 +    assume "i = Suc j"
   1.472 +    with \<open>P i\<close> show "P (Suc j)" by simp
   1.473 +  qed
   1.474 +qed
   1.475 +
   1.476  
   1.477  subsection \<open> Monotonicity of funpow \<close>
   1.478  
   1.479 @@ -1912,7 +2024,7 @@
   1.480  proof -
   1.481    from assms(1) obtain q where "k * n = (k * m) * q" ..
   1.482    then have "k * n = k * (m * q)" by (simp add: ac_simps)
   1.483 -  with \<open>0 < k\<close> have "n = m * q" by simp
   1.484 +  with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel)
   1.485    then show ?thesis ..
   1.486  qed
   1.487    
   1.488 @@ -1949,7 +2061,7 @@
   1.489  lemma dvd_minus_self:
   1.490    fixes m n :: nat
   1.491    shows "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
   1.492 -  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add)
   1.493 +  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le)
   1.494  
   1.495  lemma dvd_minus_add:
   1.496    fixes m n q r :: nat