src/HOL/Nat.thy
changeset 63588 d0e2bad67bd4
parent 63561 fba08009ff3e
child 63648 f9f3006a5579
     1.1 --- a/src/HOL/Nat.thy	Tue Aug 02 21:04:52 2016 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Aug 02 21:05:34 2016 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (*  Title:      HOL/Nat.thy
     1.5 -    Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Author:     Lawrence C Paulson
     1.8 +    Author:     Markus Wenzel
     1.9  
    1.10  Type "nat" is a linear order, and a datatype; arithmetic operators + -
    1.11  and * (for div and mod, see theory Divides).
    1.12 @@ -8,7 +10,7 @@
    1.13  section \<open>Natural numbers\<close>
    1.14  
    1.15  theory Nat
    1.16 -imports Inductive Typedef Fun Rings
    1.17 +  imports Inductive Typedef Fun Rings
    1.18  begin
    1.19  
    1.20  named_theorems arith "arith facts -- only ground formulas"
    1.21 @@ -21,75 +23,70 @@
    1.22  
    1.23  axiomatization Zero_Rep :: ind and Suc_Rep :: "ind \<Rightarrow> ind"
    1.24    \<comment> \<open>The axiom of infinity in 2 parts:\<close>
    1.25 -where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y"
    1.26 -  and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    1.27 +  where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y"
    1.28 +    and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    1.29 +
    1.30  
    1.31  subsection \<open>Type nat\<close>
    1.32  
    1.33  text \<open>Type definition\<close>
    1.34  
    1.35 -inductive Nat :: "ind \<Rightarrow> bool" where
    1.36 -  Zero_RepI: "Nat Zero_Rep"
    1.37 -| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
    1.38 +inductive Nat :: "ind \<Rightarrow> bool"
    1.39 +  where
    1.40 +    Zero_RepI: "Nat Zero_Rep"
    1.41 +  | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
    1.42  
    1.43  typedef nat = "{n. Nat n}"
    1.44    morphisms Rep_Nat Abs_Nat
    1.45    using Nat.Zero_RepI by auto
    1.46  
    1.47 -lemma Nat_Rep_Nat:
    1.48 -  "Nat (Rep_Nat n)"
    1.49 +lemma Nat_Rep_Nat: "Nat (Rep_Nat n)"
    1.50    using Rep_Nat by simp
    1.51  
    1.52 -lemma Nat_Abs_Nat_inverse:
    1.53 -  "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n"
    1.54 +lemma Nat_Abs_Nat_inverse: "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n"
    1.55    using Abs_Nat_inverse by simp
    1.56  
    1.57 -lemma Nat_Abs_Nat_inject:
    1.58 -  "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m"
    1.59 +lemma Nat_Abs_Nat_inject: "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m"
    1.60    using Abs_Nat_inject by simp
    1.61  
    1.62  instantiation nat :: zero
    1.63  begin
    1.64  
    1.65 -definition Zero_nat_def:
    1.66 -  "0 = Abs_Nat Zero_Rep"
    1.67 +definition Zero_nat_def: "0 = Abs_Nat Zero_Rep"
    1.68  
    1.69  instance ..
    1.70  
    1.71  end
    1.72  
    1.73 -definition Suc :: "nat \<Rightarrow> nat" where
    1.74 -  "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
    1.75 +definition Suc :: "nat \<Rightarrow> nat"
    1.76 +  where "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
    1.77  
    1.78  lemma Suc_not_Zero: "Suc m \<noteq> 0"
    1.79 -  by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat)
    1.80 +  by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI
    1.81 +      Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat)
    1.82  
    1.83  lemma Zero_not_Suc: "0 \<noteq> Suc m"
    1.84 -  by (rule not_sym, rule Suc_not_Zero not_sym)
    1.85 +  by (rule not_sym) (rule Suc_not_Zero)
    1.86  
    1.87  lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y"
    1.88    by (rule iffI, rule Suc_Rep_inject) simp_all
    1.89  
    1.90  lemma nat_induct0:
    1.91 -  fixes n
    1.92 -  assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    1.93 +  assumes "P 0"
    1.94 +    and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    1.95    shows "P n"
    1.96 -using assms
    1.97 -apply (unfold Zero_nat_def Suc_def)
    1.98 -apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<close>
    1.99 -apply (erule Nat_Rep_Nat [THEN Nat.induct])
   1.100 -apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
   1.101 -done
   1.102 -
   1.103 -free_constructors case_nat for
   1.104 -    "0 :: nat"
   1.105 -  | Suc pred
   1.106 -where
   1.107 -  "pred (0 :: nat) = (0 :: nat)"
   1.108 +  using assms
   1.109 +  apply (unfold Zero_nat_def Suc_def)
   1.110 +  apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<close>
   1.111 +  apply (erule Nat_Rep_Nat [THEN Nat.induct])
   1.112 +  apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
   1.113 +  done
   1.114 +
   1.115 +free_constructors case_nat for "0 :: nat" | Suc pred
   1.116 +  where "pred (0 :: nat) = (0 :: nat)"
   1.117      apply atomize_elim
   1.118      apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
   1.119 -   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject'
   1.120 -     Rep_Nat_inject)
   1.121 +   apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject' Rep_Nat_inject)
   1.122    apply (simp only: Suc_not_Zero)
   1.123    done
   1.124  
   1.125 @@ -97,19 +94,19 @@
   1.126  setup \<open>Sign.mandatory_path "old"\<close>
   1.127  
   1.128  old_rep_datatype "0 :: nat" Suc
   1.129 -  apply (erule nat_induct0, assumption)
   1.130 - apply (rule nat.inject)
   1.131 -apply (rule nat.distinct(1))
   1.132 -done
   1.133 +    apply (erule nat_induct0)
   1.134 +    apply assumption
   1.135 +   apply (rule nat.inject)
   1.136 +  apply (rule nat.distinct(1))
   1.137 +  done
   1.138  
   1.139  setup \<open>Sign.parent_path\<close>
   1.140  
   1.141  \<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
   1.142  setup \<open>Sign.mandatory_path "nat"\<close>
   1.143  
   1.144 -declare
   1.145 -  old.nat.inject[iff del]
   1.146 -  old.nat.distinct(1)[simp del, induct_simp del]
   1.147 +declare old.nat.inject[iff del]
   1.148 +  and old.nat.distinct(1)[simp del, induct_simp del]
   1.149  
   1.150  lemmas induct = old.nat.induct
   1.151  lemmas inducts = old.nat.inducts
   1.152 @@ -134,16 +131,16 @@
   1.153    nat.split_sel_asm
   1.154  
   1.155  lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
   1.156 +  "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
   1.157    \<comment> \<open>for backward compatibility -- names of variables differ\<close>
   1.158 -  "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
   1.159 -by (rule old.nat.exhaust)
   1.160 +  by (rule old.nat.exhaust)
   1.161  
   1.162  lemma nat_induct [case_names 0 Suc, induct type: nat]:
   1.163 -  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
   1.164    fixes n
   1.165    assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
   1.166    shows "P n"
   1.167 -using assms by (rule nat.induct)
   1.168 +  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
   1.169 +  using assms by (rule nat.induct)
   1.170  
   1.171  hide_fact
   1.172    nat_exhaust
   1.173 @@ -180,35 +177,40 @@
   1.174    by (simp add: inj_on_def)
   1.175  
   1.176  lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
   1.177 -by (rule notE, rule Suc_not_Zero)
   1.178 +  by (rule notE) (rule Suc_not_Zero)
   1.179  
   1.180  lemma Zero_neq_Suc: "0 = Suc m \<Longrightarrow> R"
   1.181 -by (rule Suc_neq_Zero, erule sym)
   1.182 +  by (rule Suc_neq_Zero) (erule sym)
   1.183  
   1.184  lemma Suc_inject: "Suc x = Suc y \<Longrightarrow> x = y"
   1.185 -by (rule inj_Suc [THEN injD])
   1.186 +  by (rule inj_Suc [THEN injD])
   1.187  
   1.188  lemma n_not_Suc_n: "n \<noteq> Suc n"
   1.189 -by (induct n) simp_all
   1.190 +  by (induct n) simp_all
   1.191  
   1.192  lemma Suc_n_not_n: "Suc n \<noteq> n"
   1.193 -by (rule not_sym, rule n_not_Suc_n)
   1.194 -
   1.195 -text \<open>A special form of induction for reasoning
   1.196 -  about @{term "m < n"} and @{term "m - n"}\<close>
   1.197 -
   1.198 +  by (rule not_sym) (rule n_not_Suc_n)
   1.199 +
   1.200 +text \<open>A special form of induction for reasoning about @{term "m < n"} and @{term "m - n"}.\<close>
   1.201  lemma diff_induct:
   1.202    assumes "\<And>x. P x 0"
   1.203      and "\<And>y. P 0 (Suc y)"
   1.204      and "\<And>x y. P x y \<Longrightarrow> P (Suc x) (Suc y)"
   1.205    shows "P m n"
   1.206 -  using assms
   1.207 -  apply (rule_tac x = m in spec)
   1.208 -  apply (induct n)
   1.209 -  prefer 2
   1.210 -  apply (rule allI)
   1.211 -  apply (induct_tac x, iprover+)
   1.212 -  done
   1.213 +proof (induct n arbitrary: m)
   1.214 +  case 0
   1.215 +  show ?case by (rule assms(1))
   1.216 +next
   1.217 +  case (Suc n)
   1.218 +  show ?case
   1.219 +  proof (induct m)
   1.220 +    case 0
   1.221 +    show ?case by (rule assms(2))
   1.222 +  next
   1.223 +    case (Suc m)
   1.224 +    from \<open>P m n\<close> show ?case by (rule assms(3))
   1.225 +  qed
   1.226 +qed
   1.227  
   1.228  
   1.229  subsection \<open>Arithmetic operators\<close>
   1.230 @@ -216,11 +218,13 @@
   1.231  instantiation nat :: comm_monoid_diff
   1.232  begin
   1.233  
   1.234 -primrec plus_nat where
   1.235 -  add_0: "0 + n = (n::nat)"
   1.236 -| add_Suc: "Suc m + n = Suc (m + n)"
   1.237 -
   1.238 -lemma add_0_right [simp]: "m + 0 = m" for m :: nat
   1.239 +primrec plus_nat
   1.240 +  where
   1.241 +    add_0: "0 + n = (n::nat)"
   1.242 +  | add_Suc: "Suc m + n = Suc (m + n)"
   1.243 +
   1.244 +lemma add_0_right [simp]: "m + 0 = m"
   1.245 +  for m :: nat
   1.246    by (induct m) simp_all
   1.247  
   1.248  lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   1.249 @@ -231,13 +235,15 @@
   1.250  lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
   1.251    by simp
   1.252  
   1.253 -primrec minus_nat where
   1.254 -  diff_0 [code]: "m - 0 = (m::nat)"
   1.255 -| diff_Suc: "m - Suc n = (case m - n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k)"
   1.256 +primrec minus_nat
   1.257 +  where
   1.258 +    diff_0 [code]: "m - 0 = (m::nat)"
   1.259 +  | diff_Suc: "m - Suc n = (case m - n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k)"
   1.260  
   1.261  declare diff_Suc [simp del]
   1.262  
   1.263 -lemma diff_0_eq_0 [simp, code]: "0 - n = 0" for n :: nat
   1.264 +lemma diff_0_eq_0 [simp, code]: "0 - n = 0"
   1.265 +  for n :: nat
   1.266    by (induct n) (simp_all add: diff_Suc)
   1.267  
   1.268  lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n"
   1.269 @@ -261,30 +267,37 @@
   1.270  instantiation nat :: comm_semiring_1_cancel
   1.271  begin
   1.272  
   1.273 -definition
   1.274 -  One_nat_def [simp]: "1 = Suc 0"
   1.275 -
   1.276 -primrec times_nat where
   1.277 -  mult_0: "0 * n = (0::nat)"
   1.278 -| mult_Suc: "Suc m * n = n + (m * n)"
   1.279 -
   1.280 -lemma mult_0_right [simp]: "m * 0 = 0" for m :: nat
   1.281 +definition One_nat_def [simp]: "1 = Suc 0"
   1.282 +
   1.283 +primrec times_nat
   1.284 +  where
   1.285 +    mult_0: "0 * n = (0::nat)"
   1.286 +  | mult_Suc: "Suc m * n = n + (m * n)"
   1.287 +
   1.288 +lemma mult_0_right [simp]: "m * 0 = 0"
   1.289 +  for m :: nat
   1.290    by (induct m) simp_all
   1.291  
   1.292  lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
   1.293    by (induct m) (simp_all add: add.left_commute)
   1.294  
   1.295 -lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)" for m n k :: nat
   1.296 +lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)"
   1.297 +  for m n k :: nat
   1.298    by (induct m) (simp_all add: add.assoc)
   1.299  
   1.300  instance
   1.301  proof
   1.302    fix k n m q :: nat
   1.303 -  show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp
   1.304 -  show "1 * n = n" unfolding One_nat_def by simp
   1.305 -  show "n * m = m * n" by (induct n) simp_all
   1.306 -  show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
   1.307 -  show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
   1.308 +  show "0 \<noteq> (1::nat)"
   1.309 +    by simp
   1.310 +  show "1 * n = n"
   1.311 +    by simp
   1.312 +  show "n * m = m * n"
   1.313 +    by (induct n) simp_all
   1.314 +  show "(n * m) * q = n * (m * q)"
   1.315 +    by (induct n) (simp_all add: add_mult_distrib)
   1.316 +  show "(n + m) * q = n * q + m * q"
   1.317 +    by (rule add_mult_distrib)
   1.318    show "k * (m - n) = (k * m) - (k * n)"
   1.319      by (induct m n rule: diff_induct) simp_all
   1.320  qed
   1.321 @@ -296,7 +309,8 @@
   1.322  
   1.323  text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close>
   1.324  
   1.325 -lemma add_is_0 [iff]: "(m + n = 0) = (m = 0 \<and> n = 0)" for m n :: nat
   1.326 +lemma add_is_0 [iff]: "m + n = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   1.327 +  for m n :: nat
   1.328    by (cases m) simp_all
   1.329  
   1.330  lemma add_is_1: "m + n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
   1.331 @@ -305,21 +319,26 @@
   1.332  lemma one_is_add: "Suc 0 = m + n \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
   1.333    by (rule trans, rule eq_commute, rule add_is_1)
   1.334  
   1.335 -lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0" for m n :: nat
   1.336 +lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0"
   1.337 +  for m n :: nat
   1.338    by (induct m) simp_all
   1.339  
   1.340 -lemma inj_on_add_nat[simp]: "inj_on (\<lambda>n. n + k) N" for k :: nat
   1.341 -  apply (induct k)
   1.342 -   apply simp
   1.343 -  apply (drule comp_inj_on[OF _ inj_Suc])
   1.344 -  apply (simp add: o_def)
   1.345 -  done
   1.346 +lemma inj_on_add_nat [simp]: "inj_on (\<lambda>n. n + k) N"
   1.347 +  for k :: nat
   1.348 +proof (induct k)
   1.349 +  case 0
   1.350 +  then show ?case by simp
   1.351 +next
   1.352 +  case (Suc k)
   1.353 +  show ?case
   1.354 +    using comp_inj_on [OF Suc inj_Suc] by (simp add: o_def)
   1.355 +qed
   1.356  
   1.357  lemma Suc_eq_plus1: "Suc n = n + 1"
   1.358 -  unfolding One_nat_def by simp
   1.359 +  by simp
   1.360  
   1.361  lemma Suc_eq_plus1_left: "Suc n = 1 + n"
   1.362 -  unfolding One_nat_def by simp
   1.363 +  by simp
   1.364  
   1.365  
   1.366  subsubsection \<open>Difference\<close>
   1.367 @@ -328,7 +347,8 @@
   1.368    by (simp add: diff_diff_add)
   1.369  
   1.370  lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
   1.371 -  unfolding One_nat_def by simp
   1.372 +  by simp
   1.373 +
   1.374  
   1.375  subsubsection \<open>Multiplication\<close>
   1.376  
   1.377 @@ -336,24 +356,30 @@
   1.378    by (induct m) auto
   1.379  
   1.380  lemma mult_eq_1_iff [simp]: "m * n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
   1.381 -  apply (induct m)
   1.382 -   apply simp
   1.383 -  apply (induct n)
   1.384 -   apply auto
   1.385 -  done
   1.386 +proof (induct m)
   1.387 +  case 0
   1.388 +  then show ?case by simp
   1.389 +next
   1.390 +  case (Suc m)
   1.391 +  then show ?case by (induct n) auto
   1.392 +qed
   1.393  
   1.394  lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
   1.395    apply (rule trans)
   1.396 -  apply (rule_tac [2] mult_eq_1_iff, fastforce)
   1.397 +   apply (rule_tac [2] mult_eq_1_iff)
   1.398 +  apply fastforce
   1.399    done
   1.400  
   1.401 -lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
   1.402 +lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1"
   1.403 +  for m n :: nat
   1.404    unfolding One_nat_def by (rule mult_eq_1_iff)
   1.405  
   1.406 -lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
   1.407 +lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
   1.408 +  for m n :: nat
   1.409    unfolding One_nat_def by (rule one_eq_mult_iff)
   1.410  
   1.411 -lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0" for k m n :: nat
   1.412 +lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0"
   1.413 +  for k m n :: nat
   1.414  proof -
   1.415    have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
   1.416    proof (induct n arbitrary: m)
   1.417 @@ -367,7 +393,8 @@
   1.418    then show ?thesis by auto
   1.419  qed
   1.420  
   1.421 -lemma mult_cancel2 [simp]: "m * k = n * k \<longleftrightarrow> m = n \<or> k = 0" for k m n :: nat
   1.422 +lemma mult_cancel2 [simp]: "m * k = n * k \<longleftrightarrow> m = n \<or> k = 0"
   1.423 +  for k m n :: nat
   1.424    by (simp add: mult.commute)
   1.425  
   1.426  lemma Suc_mult_cancel1: "Suc k * m = Suc k * n \<longleftrightarrow> m = n"
   1.427 @@ -381,20 +408,23 @@
   1.428  instantiation nat :: linorder
   1.429  begin
   1.430  
   1.431 -primrec less_eq_nat where
   1.432 -  "(0::nat) \<le> n \<longleftrightarrow> True"
   1.433 -| "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
   1.434 +primrec less_eq_nat
   1.435 +  where
   1.436 +    "(0::nat) \<le> n \<longleftrightarrow> True"
   1.437 +  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
   1.438  
   1.439  declare less_eq_nat.simps [simp del]
   1.440  
   1.441 -lemma le0 [iff]: "0 \<le> n" for n :: nat
   1.442 +lemma le0 [iff]: "0 \<le> n" for
   1.443 +  n :: nat
   1.444    by (simp add: less_eq_nat.simps)
   1.445  
   1.446 -lemma [code]: "0 \<le> n \<longleftrightarrow> True" for n :: nat
   1.447 +lemma [code]: "0 \<le> n \<longleftrightarrow> True"
   1.448 +  for n :: nat
   1.449    by simp
   1.450  
   1.451 -definition less_nat where
   1.452 -  less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
   1.453 +definition less_nat
   1.454 +  where less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
   1.455  
   1.456  lemma Suc_le_mono [iff]: "Suc n \<le> Suc m \<longleftrightarrow> n \<le> m"
   1.457    by (simp add: less_eq_nat.simps(2))
   1.458 @@ -402,13 +432,16 @@
   1.459  lemma Suc_le_eq [code]: "Suc m \<le> n \<longleftrightarrow> m < n"
   1.460    unfolding less_eq_Suc_le ..
   1.461  
   1.462 -lemma le_0_eq [iff]: "n \<le> 0 \<longleftrightarrow> n = 0" for n :: nat
   1.463 +lemma le_0_eq [iff]: "n \<le> 0 \<longleftrightarrow> n = 0"
   1.464 +  for n :: nat
   1.465    by (induct n) (simp_all add: less_eq_nat.simps(2))
   1.466  
   1.467 -lemma not_less0 [iff]: "\<not> n < 0" for n :: nat
   1.468 +lemma not_less0 [iff]: "\<not> n < 0"
   1.469 +  for n :: nat
   1.470    by (simp add: less_eq_Suc_le)
   1.471  
   1.472 -lemma less_nat_zero_code [code]: "n < 0 \<longleftrightarrow> False" for n :: nat
   1.473 +lemma less_nat_zero_code [code]: "n < 0 \<longleftrightarrow> False"
   1.474 +  for n :: nat
   1.475    by simp
   1.476  
   1.477  lemma Suc_less_eq [iff]: "Suc m < Suc n \<longleftrightarrow> m < n"
   1.478 @@ -438,12 +471,15 @@
   1.479    show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
   1.480    proof (induct n arbitrary: m)
   1.481      case 0
   1.482 -    then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   1.483 +    then show ?case
   1.484 +      by (cases m) (simp_all add: less_eq_Suc_le)
   1.485    next
   1.486      case (Suc n)
   1.487 -    then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   1.488 +    then show ?case
   1.489 +      by (cases m) (simp_all add: less_eq_Suc_le)
   1.490    qed
   1.491 -  show "n \<le> n" by (induct n) simp_all
   1.492 +  show "n \<le> n"
   1.493 +    by (induct n) simp_all
   1.494    then show "n = m" if "n \<le> m" and "m \<le> n"
   1.495      using that by (induct n arbitrary: m)
   1.496        (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   1.497 @@ -469,9 +505,11 @@
   1.498  instantiation nat :: order_bot
   1.499  begin
   1.500  
   1.501 -definition bot_nat :: nat where "bot_nat = 0"
   1.502 -
   1.503 -instance by standard (simp add: bot_nat_def)
   1.504 +definition bot_nat :: nat
   1.505 +  where "bot_nat = 0"
   1.506 +
   1.507 +instance
   1.508 +  by standard (simp add: bot_nat_def)
   1.509  
   1.510  end
   1.511  
   1.512 @@ -490,19 +528,24 @@
   1.513  
   1.514  subsubsection \<open>Elimination properties\<close>
   1.515  
   1.516 -lemma less_not_refl: "\<not> n < n" for n :: nat
   1.517 +lemma less_not_refl: "\<not> n < n"
   1.518 +  for n :: nat
   1.519    by (rule order_less_irrefl)
   1.520  
   1.521 -lemma less_not_refl2: "n < m \<Longrightarrow> m \<noteq> n" for m n :: nat
   1.522 +lemma less_not_refl2: "n < m \<Longrightarrow> m \<noteq> n"
   1.523 +  for m n :: nat
   1.524    by (rule not_sym) (rule less_imp_neq)
   1.525  
   1.526 -lemma less_not_refl3: "s < t \<Longrightarrow> s \<noteq> t" for s t :: nat
   1.527 +lemma less_not_refl3: "s < t \<Longrightarrow> s \<noteq> t"
   1.528 +  for s t :: nat
   1.529    by (rule less_imp_neq)
   1.530  
   1.531 -lemma less_irrefl_nat: "n < n \<Longrightarrow> R" for n :: nat
   1.532 +lemma less_irrefl_nat: "n < n \<Longrightarrow> R"
   1.533 +  for n :: nat
   1.534    by (rule notE, rule less_not_refl)
   1.535  
   1.536 -lemma less_zeroE: "n < 0 \<Longrightarrow> R" for n :: nat
   1.537 +lemma less_zeroE: "n < 0 \<Longrightarrow> R"
   1.538 +  for n :: nat
   1.539    by (rule notE) (rule not_less0)
   1.540  
   1.541  lemma less_Suc_eq: "m < Suc n \<longleftrightarrow> m < n \<or> m = n"
   1.542 @@ -511,17 +554,19 @@
   1.543  lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   1.544    by (simp add: less_Suc_eq)
   1.545  
   1.546 -lemma less_one [iff]: "n < 1 \<longleftrightarrow> n = 0" for n :: nat
   1.547 +lemma less_one [iff]: "n < 1 \<longleftrightarrow> n = 0"
   1.548 +  for n :: nat
   1.549    unfolding One_nat_def by (rule less_Suc0)
   1.550  
   1.551  lemma Suc_mono: "m < n \<Longrightarrow> Suc m < Suc n"
   1.552    by simp
   1.553  
   1.554 -text \<open>"Less than" is antisymmetric, sort of\<close>
   1.555 -lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
   1.556 +text \<open>"Less than" is antisymmetric, sort of.\<close>
   1.557 +lemma less_antisym: "\<not> n < m \<Longrightarrow> n < Suc m \<Longrightarrow> m = n"
   1.558    unfolding not_less less_Suc_eq_le by (rule antisym)
   1.559  
   1.560 -lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat
   1.561 +lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m"
   1.562 +  for m n :: nat
   1.563    by (rule linorder_neq_iff)
   1.564  
   1.565  
   1.566 @@ -549,8 +594,10 @@
   1.567      and eq: "m = n \<Longrightarrow> P"
   1.568    shows P
   1.569    apply (rule major [THEN lessE])
   1.570 -  apply (rule eq, blast)
   1.571 -  apply (rule less, blast)
   1.572 +   apply (rule eq)
   1.573 +   apply blast
   1.574 +  apply (rule less)
   1.575 +  apply blast
   1.576    done
   1.577  
   1.578  lemma Suc_lessE:
   1.579 @@ -558,8 +605,9 @@
   1.580      and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
   1.581    shows P
   1.582    apply (rule major [THEN lessE])
   1.583 -  apply (erule lessI [THEN minor])
   1.584 -  apply (erule Suc_lessD [THEN minor], assumption)
   1.585 +   apply (erule lessI [THEN minor])
   1.586 +  apply (erule Suc_lessD [THEN minor])
   1.587 +  apply assumption
   1.588    done
   1.589  
   1.590  lemma Suc_less_SucD: "Suc m < Suc n \<Longrightarrow> m < n"
   1.591 @@ -568,39 +616,42 @@
   1.592  lemma less_trans_Suc:
   1.593    assumes le: "i < j"
   1.594    shows "j < k \<Longrightarrow> Suc i < k"
   1.595 -  apply (induct k, simp_all)
   1.596 -  using le
   1.597 -  apply (simp add: less_Suc_eq)
   1.598 -  apply (blast dest: Suc_lessD)
   1.599 -  done
   1.600 -
   1.601 -text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{prop "n = m \<or> n < m"}\<close>
   1.602 +proof (induct k)
   1.603 +  case 0
   1.604 +  then show ?case by simp
   1.605 +next
   1.606 +  case (Suc k)
   1.607 +  with le show ?case
   1.608 +    by simp (auto simp add: less_Suc_eq dest: Suc_lessD)
   1.609 +qed
   1.610 +
   1.611 +text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{prop "n = m \<or> n < m"}.\<close>
   1.612  lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m"
   1.613 -  unfolding not_less less_Suc_eq_le ..
   1.614 +  by (simp only: not_less less_Suc_eq_le)
   1.615  
   1.616  lemma not_less_eq_eq: "\<not> m \<le> n \<longleftrightarrow> Suc n \<le> m"
   1.617 -  unfolding not_le Suc_le_eq ..
   1.618 -
   1.619 -text \<open>Properties of "less than or equal"\<close>
   1.620 +  by (simp only: not_le Suc_le_eq)
   1.621 +
   1.622 +text \<open>Properties of "less than or equal".\<close>
   1.623  
   1.624  lemma le_imp_less_Suc: "m \<le> n \<Longrightarrow> m < Suc n"
   1.625 -  unfolding less_Suc_eq_le .
   1.626 +  by (simp only: less_Suc_eq_le)
   1.627  
   1.628  lemma Suc_n_not_le_n: "\<not> Suc n \<le> n"
   1.629 -  unfolding not_le less_Suc_eq_le ..
   1.630 -
   1.631 -lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
   1.632 +  by (simp add: not_le less_Suc_eq_le)
   1.633 +
   1.634 +lemma le_Suc_eq: "m \<le> Suc n \<longleftrightarrow> m \<le> n \<or> m = Suc n"
   1.635    by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq)
   1.636  
   1.637  lemma le_SucE: "m \<le> Suc n \<Longrightarrow> (m \<le> n \<Longrightarrow> R) \<Longrightarrow> (m = Suc n \<Longrightarrow> R) \<Longrightarrow> R"
   1.638    by (drule le_Suc_eq [THEN iffD1], iprover+)
   1.639  
   1.640 -lemma Suc_leI: "m < n \<Longrightarrow> Suc(m) \<le> n"
   1.641 -  unfolding Suc_le_eq .
   1.642 -
   1.643 -text \<open>Stronger version of \<open>Suc_leD\<close>\<close>
   1.644 +lemma Suc_leI: "m < n \<Longrightarrow> Suc m \<le> n"
   1.645 +  by (simp only: Suc_le_eq)
   1.646 +
   1.647 +text \<open>Stronger version of \<open>Suc_leD\<close>.\<close>
   1.648  lemma Suc_le_lessD: "Suc m \<le> n \<Longrightarrow> m < n"
   1.649 -  unfolding Suc_le_eq .
   1.650 +  by (simp only: Suc_le_eq)
   1.651  
   1.652  lemma less_imp_le_nat: "m < n \<Longrightarrow> m \<le> n" for m n :: nat
   1.653    unfolding less_eq_Suc_le by (rule Suc_leD)
   1.654 @@ -611,32 +662,41 @@
   1.655  
   1.656  text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close>
   1.657  
   1.658 -lemma less_or_eq_imp_le: "m < n \<or> m = n \<Longrightarrow> m \<le> n" for m n :: nat
   1.659 +lemma less_or_eq_imp_le: "m < n \<or> m = n \<Longrightarrow> m \<le> n"
   1.660 +  for m n :: nat
   1.661    unfolding le_less .
   1.662  
   1.663 -lemma le_eq_less_or_eq: "m \<le> n \<longleftrightarrow> m < n \<or> m = n" for m n :: nat
   1.664 +lemma le_eq_less_or_eq: "m \<le> n \<longleftrightarrow> m < n \<or> m = n"
   1.665 +  for m n :: nat
   1.666    by (rule le_less)
   1.667  
   1.668  text \<open>Useful with \<open>blast\<close>.\<close>
   1.669 -lemma eq_imp_le: "m = n \<Longrightarrow> m \<le> n" for m n :: nat
   1.670 +lemma eq_imp_le: "m = n \<Longrightarrow> m \<le> n"
   1.671 +  for m n :: nat
   1.672    by auto
   1.673  
   1.674 -lemma le_refl: "n \<le> n" for n :: nat
   1.675 +lemma le_refl: "n \<le> n"
   1.676 +  for n :: nat
   1.677    by simp
   1.678  
   1.679 -lemma le_trans: "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" for i j k :: nat
   1.680 +lemma le_trans: "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
   1.681 +  for i j k :: nat
   1.682    by (rule order_trans)
   1.683  
   1.684 -lemma le_antisym: "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n" for m n :: nat
   1.685 +lemma le_antisym: "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n"
   1.686 +  for m n :: nat
   1.687    by (rule antisym)
   1.688  
   1.689 -lemma nat_less_le: "m < n \<longleftrightarrow> m \<le> n \<and> m \<noteq> n" for m n :: nat
   1.690 +lemma nat_less_le: "m < n \<longleftrightarrow> m \<le> n \<and> m \<noteq> n"
   1.691 +  for m n :: nat
   1.692    by (rule less_le)
   1.693  
   1.694 -lemma le_neq_implies_less: "m \<le> n \<Longrightarrow> m \<noteq> n \<Longrightarrow> m < n" for m n :: nat
   1.695 +lemma le_neq_implies_less: "m \<le> n \<Longrightarrow> m \<noteq> n \<Longrightarrow> m < n"
   1.696 +  for m n :: nat
   1.697    unfolding less_le ..
   1.698  
   1.699 -lemma nat_le_linear: "m \<le> n | n \<le> m" for m n :: nat
   1.700 +lemma nat_le_linear: "m \<le> n | n \<le> m"
   1.701 +  for m n :: nat
   1.702    by (rule linear)
   1.703  
   1.704  lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
   1.705 @@ -655,20 +715,24 @@
   1.706  lemma gr0_implies_Suc: "n > 0 \<Longrightarrow> \<exists>m. n = Suc m"
   1.707    by (cases n) simp_all
   1.708  
   1.709 -lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0" for m n :: nat
   1.710 +lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0"
   1.711 +  for m n :: nat
   1.712    by (cases n) simp_all
   1.713  
   1.714 -lemma neq0_conv[iff]: "n \<noteq> 0 \<longleftrightarrow> 0 < n" for n :: nat
   1.715 +lemma neq0_conv[iff]: "n \<noteq> 0 \<longleftrightarrow> 0 < n"
   1.716 +  for n :: nat
   1.717    by (cases n) simp_all
   1.718  
   1.719  text \<open>This theorem is useful with \<open>blast\<close>\<close>
   1.720 -lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n" for n :: nat
   1.721 -  by (rule neq0_conv[THEN iffD1], iprover)
   1.722 +lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
   1.723 +  for n :: nat
   1.724 +  by (rule neq0_conv[THEN iffD1]) iprover
   1.725  
   1.726  lemma gr0_conv_Suc: "0 < n \<longleftrightarrow> (\<exists>m. n = Suc m)"
   1.727    by (fast intro: not0_implies_Suc)
   1.728  
   1.729 -lemma not_gr0 [iff]: "\<not> 0 < n \<longleftrightarrow> n = 0" for n :: nat
   1.730 +lemma not_gr0 [iff]: "\<not> 0 < n \<longleftrightarrow> n = 0"
   1.731 +  for n :: nat
   1.732    using neq0_conv by blast
   1.733  
   1.734  lemma Suc_le_D: "Suc n \<le> m' \<Longrightarrow> \<exists>m. m' = Suc m"
   1.735 @@ -687,34 +751,45 @@
   1.736  lemma Suc_diff_1 [simp]: "0 < n \<Longrightarrow> Suc (n - 1) = n"
   1.737    unfolding One_nat_def by (rule Suc_pred)
   1.738  
   1.739 -lemma nat_add_left_cancel_le [simp]: "k + m \<le> k + n \<longleftrightarrow> m \<le> n" for k m n :: nat
   1.740 +lemma nat_add_left_cancel_le [simp]: "k + m \<le> k + n \<longleftrightarrow> m \<le> n"
   1.741 +  for k m n :: nat
   1.742    by (induct k) simp_all
   1.743  
   1.744 -lemma nat_add_left_cancel_less [simp]: "k + m < k + n \<longleftrightarrow> m < n" for k m n :: nat
   1.745 +lemma nat_add_left_cancel_less [simp]: "k + m < k + n \<longleftrightarrow> m < n"
   1.746 +  for k m n :: nat
   1.747    by (induct k) simp_all
   1.748  
   1.749 -lemma add_gr_0 [iff]: "m + n > 0 \<longleftrightarrow> m > 0 \<or> n > 0" for m n :: nat
   1.750 +lemma add_gr_0 [iff]: "m + n > 0 \<longleftrightarrow> m > 0 \<or> n > 0"
   1.751 +  for m n :: nat
   1.752    by (auto dest: gr0_implies_Suc)
   1.753  
   1.754  text \<open>strict, in 1st argument\<close>
   1.755 -lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k" for i j k :: nat
   1.756 +lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k"
   1.757 +  for i j k :: nat
   1.758    by (induct k) simp_all
   1.759  
   1.760  text \<open>strict, in both arguments\<close>
   1.761 -lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l" for i j k l :: nat
   1.762 +lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l"
   1.763 +  for i j k l :: nat
   1.764    apply (rule add_less_mono1 [THEN less_trans], assumption+)
   1.765 -  apply (induct j, simp_all)
   1.766 +  apply (induct j)
   1.767 +   apply simp_all
   1.768    done
   1.769  
   1.770  text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close>
   1.771  lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)"
   1.772 -  apply (induct n)
   1.773 -  apply (simp_all add: order_le_less)
   1.774 -  apply (blast elim!: less_SucE
   1.775 -               intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
   1.776 -  done
   1.777 -
   1.778 -lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)" for k l :: nat
   1.779 +proof (induct n)
   1.780 +  case 0
   1.781 +  then show ?case by simp
   1.782 +next
   1.783 +  case Suc
   1.784 +  then show ?case
   1.785 +    by (simp add: order_le_less)
   1.786 +      (blast elim!: less_SucE intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
   1.787 +qed
   1.788 +
   1.789 +lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)"
   1.790 +  for k l :: nat
   1.791    by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
   1.792  
   1.793  text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
   1.794 @@ -734,27 +809,34 @@
   1.795  
   1.796  text \<open>Addition is the inverse of subtraction:
   1.797    if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close>
   1.798 -lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m - n) = m" for m n :: nat
   1.799 +lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m - n) = m"
   1.800 +  for m n :: nat
   1.801    by (induct m n rule: diff_induct) simp_all
   1.802  
   1.803 -lemma nat_le_iff_add: "m \<le> n \<longleftrightarrow> (\<exists>k. n = m + k)" for m n :: nat
   1.804 +lemma nat_le_iff_add: "m \<le> n \<longleftrightarrow> (\<exists>k. n = m + k)"
   1.805 +  for m n :: nat
   1.806    using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)
   1.807  
   1.808 -text\<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>\<close>
   1.809 +text \<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>.\<close>
   1.810  
   1.811  instance nat :: linordered_semidom
   1.812  proof
   1.813    fix m n q :: nat
   1.814 -  show "0 < (1::nat)" by simp
   1.815 -  show "m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
   1.816 -  show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
   1.817 -  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
   1.818 +  show "0 < (1::nat)"
   1.819 +    by simp
   1.820 +  show "m \<le> n \<Longrightarrow> q + m \<le> q + n"
   1.821 +    by simp
   1.822 +  show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n"
   1.823 +    by (simp add: mult_less_mono2)
   1.824 +  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0"
   1.825 +    by simp
   1.826    show "n \<le> m \<Longrightarrow> (m - n) + n = m"
   1.827      by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
   1.828  qed
   1.829  
   1.830  instance nat :: dioid
   1.831    by standard (rule nat_le_iff_add)
   1.832 +
   1.833  declare le0[simp del] \<comment> \<open>This is now @{thm zero_le}\<close>
   1.834  declare le_0_eq[simp del] \<comment> \<open>This is now @{thm le_zero_eq}\<close>
   1.835  declare not_less0[simp del] \<comment> \<open>This is now @{thm not_less_zero}\<close>
   1.836 @@ -769,10 +851,12 @@
   1.837  lemma mono_Suc: "mono Suc"
   1.838    by (rule monoI) simp
   1.839  
   1.840 -lemma min_0L [simp]: "min 0 n = 0" for n :: nat
   1.841 +lemma min_0L [simp]: "min 0 n = 0"
   1.842 +  for n :: nat
   1.843    by (rule min_absorb1) simp
   1.844  
   1.845 -lemma min_0R [simp]: "min n 0 = 0" for n :: nat
   1.846 +lemma min_0R [simp]: "min n 0 = 0"
   1.847 +  for n :: nat
   1.848    by (rule min_absorb2) simp
   1.849  
   1.850  lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
   1.851 @@ -784,10 +868,12 @@
   1.852  lemma min_Suc2: "min m (Suc n) = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min m' n))"
   1.853    by (simp split: nat.split)
   1.854  
   1.855 -lemma max_0L [simp]: "max 0 n = n" for n :: nat
   1.856 +lemma max_0L [simp]: "max 0 n = n"
   1.857 +  for n :: nat
   1.858    by (rule max_absorb2) simp
   1.859  
   1.860 -lemma max_0R [simp]: "max n 0 = n" for n :: nat
   1.861 +lemma max_0R [simp]: "max n 0 = n"
   1.862 +  for n :: nat
   1.863    by (rule max_absorb1) simp
   1.864  
   1.865  lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)"
   1.866 @@ -799,25 +885,31 @@
   1.867  lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
   1.868    by (simp split: nat.split)
   1.869  
   1.870 -lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)" for m n q :: nat
   1.871 +lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
   1.872 +  for m n q :: nat
   1.873    by (simp add: min_def not_le)
   1.874      (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   1.875  
   1.876 -lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)" for m n q :: nat
   1.877 +lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)"
   1.878 +  for m n q :: nat
   1.879    by (simp add: min_def not_le)
   1.880      (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   1.881  
   1.882 -lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)" for m n q :: nat
   1.883 +lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)"
   1.884 +  for m n q :: nat
   1.885    by (simp add: max_def)
   1.886  
   1.887 -lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)" for m n q :: nat
   1.888 +lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)"
   1.889 +  for m n q :: nat
   1.890    by (simp add: max_def)
   1.891  
   1.892 -lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)" for m n q :: nat
   1.893 +lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)"
   1.894 +  for m n q :: nat
   1.895    by (simp add: max_def not_le)
   1.896      (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   1.897  
   1.898 -lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)" for m n q :: nat
   1.899 +lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)"
   1.900 +  for m n q :: nat
   1.901    by (simp add: max_def not_le)
   1.902      (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   1.903  
   1.904 @@ -834,10 +926,11 @@
   1.905    proof (induct n)
   1.906      case (0 n)
   1.907      have "P 0" by (rule step) auto
   1.908 -    then show ?case using 0 by auto
   1.909 +    with 0 show ?case by auto
   1.910    next
   1.911      case (Suc m n)
   1.912 -    then have "n \<le> m \<or> n = Suc m" by (simp add: le_Suc_eq)
   1.913 +    then have "n \<le> m \<or> n = Suc m"
   1.914 +      by (simp add: le_Suc_eq)
   1.915      then show ?case
   1.916      proof
   1.917        assume "n \<le> m"
   1.918 @@ -851,34 +944,36 @@
   1.919  qed
   1.920  
   1.921  
   1.922 -lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0" for P :: "nat \<Rightarrow> bool"
   1.923 +lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0"
   1.924 +  for P :: "nat \<Rightarrow> bool"
   1.925    by (rule Least_equality[OF _ le0])
   1.926  
   1.927  lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
   1.928 -  apply (cases n, auto)
   1.929 +  apply (cases n)
   1.930 +   apply auto
   1.931    apply (frule LeastI)
   1.932 -  apply (drule_tac P = "\<lambda>x. P (Suc x) " in LeastI)
   1.933 +  apply (drule_tac P = "\<lambda>x. P (Suc x)" in LeastI)
   1.934    apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
   1.935 -  apply (erule_tac [2] Least_le)
   1.936 -  apply (cases "LEAST x. P x", auto)
   1.937 -  apply (drule_tac P = "\<lambda>x. P (Suc x) " in Least_le)
   1.938 +   apply (erule_tac [2] Least_le)
   1.939 +  apply (cases "LEAST x. P x")
   1.940 +   apply auto
   1.941 +  apply (drule_tac P = "\<lambda>x. P (Suc x)" in Least_le)
   1.942    apply (blast intro: order_antisym)
   1.943    done
   1.944  
   1.945  lemma Least_Suc2: "P n \<Longrightarrow> Q m \<Longrightarrow> \<not> P 0 \<Longrightarrow> \<forall>k. P (Suc k) = Q k \<Longrightarrow> Least P = Suc (Least Q)"
   1.946 -  apply (erule (1) Least_Suc [THEN ssubst])
   1.947 -  apply simp
   1.948 -  done
   1.949 -
   1.950 -lemma ex_least_nat_le: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k" for P :: "nat \<Rightarrow> bool"
   1.951 +  by (erule (1) Least_Suc [THEN ssubst]) simp
   1.952 +
   1.953 +lemma ex_least_nat_le: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k"
   1.954 +  for P :: "nat \<Rightarrow> bool"
   1.955    apply (cases n)
   1.956     apply blast
   1.957    apply (rule_tac x="LEAST k. P k" in exI)
   1.958    apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
   1.959    done
   1.960  
   1.961 -lemma ex_least_nat_less: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (k + 1)" for P :: "nat \<Rightarrow> bool"
   1.962 -  unfolding One_nat_def
   1.963 +lemma ex_least_nat_less: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (k + 1)"
   1.964 +  for P :: "nat \<Rightarrow> bool"
   1.965    apply (cases n)
   1.966     apply blast
   1.967    apply (frule (1) ex_least_nat_le)
   1.968 @@ -957,7 +1052,7 @@
   1.969    apply (rule infinite_descent)
   1.970    using assms
   1.971    apply (case_tac "n > 0")
   1.972 -  apply auto
   1.973 +   apply auto
   1.974    done
   1.975  
   1.976  text \<open>
   1.977 @@ -988,7 +1083,7 @@
   1.978    ultimately show "P x" by auto
   1.979  qed
   1.980  
   1.981 -text\<open>Again, without explicit base case:\<close>
   1.982 +text \<open>Again, without explicit base case:\<close>
   1.983  lemma infinite_descent_measure:
   1.984    fixes V :: "'a \<Rightarrow> nat"
   1.985    assumes "\<And>x. \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y"
   1.986 @@ -1014,17 +1109,21 @@
   1.987  
   1.988  
   1.989  text \<open>non-strict, in 1st argument\<close>
   1.990 -lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k" for i j k :: nat
   1.991 +lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k"
   1.992 +  for i j k :: nat
   1.993    by (rule add_right_mono)
   1.994  
   1.995  text \<open>non-strict, in both arguments\<close>
   1.996 -lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l" for i j k l :: nat
   1.997 +lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l"
   1.998 +  for i j k l :: nat
   1.999    by (rule add_mono)
  1.1000  
  1.1001 -lemma le_add2: "n \<le> m + n" for m n :: nat
  1.1002 +lemma le_add2: "n \<le> m + n"
  1.1003 +  for m n :: nat
  1.1004    by simp
  1.1005  
  1.1006 -lemma le_add1: "n \<le> n + m" for m n :: nat
  1.1007 +lemma le_add1: "n \<le> n + m"
  1.1008 +  for m n :: nat
  1.1009    by simp
  1.1010  
  1.1011  lemma less_add_Suc1: "i < Suc (i + m)"
  1.1012 @@ -1036,43 +1135,54 @@
  1.1013  lemma less_iff_Suc_add: "m < n \<longleftrightarrow> (\<exists>k. n = Suc (m + k))"
  1.1014    by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
  1.1015  
  1.1016 -lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m" for i j m :: nat
  1.1017 +lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m"
  1.1018 +  for i j m :: nat
  1.1019    by (rule le_trans, assumption, rule le_add1)
  1.1020  
  1.1021 -lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j" for i j m :: nat
  1.1022 +lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j"
  1.1023 +  for i j m :: nat
  1.1024    by (rule le_trans, assumption, rule le_add2)
  1.1025  
  1.1026 -lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m" for i j m :: nat
  1.1027 +lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m"
  1.1028 +  for i j m :: nat
  1.1029    by (rule less_le_trans, assumption, rule le_add1)
  1.1030  
  1.1031 -lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j" for i j m :: nat
  1.1032 +lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j"
  1.1033 +  for i j m :: nat
  1.1034    by (rule less_le_trans, assumption, rule le_add2)
  1.1035  
  1.1036 -lemma add_lessD1: "i + j < k \<Longrightarrow> i < k" for i j k :: nat
  1.1037 +lemma add_lessD1: "i + j < k \<Longrightarrow> i < k"
  1.1038 +  for i j k :: nat
  1.1039    by (rule le_less_trans [of _ "i+j"]) (simp_all add: le_add1)
  1.1040  
  1.1041 -lemma not_add_less1 [iff]: "\<not> i + j < i" for i j :: nat
  1.1042 +lemma not_add_less1 [iff]: "\<not> i + j < i"
  1.1043 +  for i j :: nat
  1.1044    apply (rule notI)
  1.1045    apply (drule add_lessD1)
  1.1046    apply (erule less_irrefl [THEN notE])
  1.1047    done
  1.1048  
  1.1049 -lemma not_add_less2 [iff]: "\<not> j + i < i" for i j :: nat
  1.1050 +lemma not_add_less2 [iff]: "\<not> j + i < i"
  1.1051 +  for i j :: nat
  1.1052    by (simp add: add.commute)
  1.1053  
  1.1054 -lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n" for k m n :: nat
  1.1055 -  by (rule order_trans [of _ "m+k"]) (simp_all add: le_add1)
  1.1056 -
  1.1057 -lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n" for k m n :: nat
  1.1058 +lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n"
  1.1059 +  for k m n :: nat
  1.1060 +  by (rule order_trans [of _ "m + k"]) (simp_all add: le_add1)
  1.1061 +
  1.1062 +lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n"
  1.1063 +  for k m n :: nat
  1.1064    apply (simp add: add.commute)
  1.1065    apply (erule add_leD1)
  1.1066    done
  1.1067  
  1.1068 -lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R" for k m n :: nat
  1.1069 +lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R"
  1.1070 +  for k m n :: nat
  1.1071    by (blast dest: add_leD1 add_leD2)
  1.1072  
  1.1073  text \<open>needs \<open>\<And>k\<close> for \<open>ac_simps\<close> to work\<close>
  1.1074 -lemma less_add_eq_less: "\<And>k::nat. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n"
  1.1075 +lemma less_add_eq_less: "\<And>k. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n"
  1.1076 +  for l m n :: nat
  1.1077    by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
  1.1078  
  1.1079  
  1.1080 @@ -1082,42 +1192,52 @@
  1.1081    by (induct m n rule: diff_induct) simp_all
  1.1082  
  1.1083  lemma diff_less_Suc: "m - n < Suc m"
  1.1084 -apply (induct m n rule: diff_induct)
  1.1085 -apply (erule_tac [3] less_SucE)
  1.1086 -apply (simp_all add: less_Suc_eq)
  1.1087 -done
  1.1088 -
  1.1089 -lemma diff_le_self [simp]: "m - n \<le> m" for m n :: nat
  1.1090 +  apply (induct m n rule: diff_induct)
  1.1091 +    apply (erule_tac [3] less_SucE)
  1.1092 +     apply (simp_all add: less_Suc_eq)
  1.1093 +  done
  1.1094 +
  1.1095 +lemma diff_le_self [simp]: "m - n \<le> m"
  1.1096 +  for m n :: nat
  1.1097    by (induct m n rule: diff_induct) (simp_all add: le_SucI)
  1.1098  
  1.1099 -lemma less_imp_diff_less: "j < k \<Longrightarrow> j - n < k" for j k n :: nat
  1.1100 +lemma less_imp_diff_less: "j < k \<Longrightarrow> j - n < k"
  1.1101 +  for j k n :: nat
  1.1102    by (rule le_less_trans, rule diff_le_self)
  1.1103  
  1.1104  lemma diff_Suc_less [simp]: "0 < n \<Longrightarrow> n - Suc i < n"
  1.1105    by (cases n) (auto simp add: le_simps)
  1.1106  
  1.1107 -lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j) - k = i + (j - k)" for i j k :: nat
  1.1108 +lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j) - k = i + (j - k)"
  1.1109 +  for i j k :: nat
  1.1110    by (induct j k rule: diff_induct) simp_all
  1.1111  
  1.1112 -lemma add_diff_assoc [simp]: "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k" for i j k :: nat
  1.1113 +lemma add_diff_assoc [simp]: "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k"
  1.1114 +  for i j k :: nat
  1.1115    by (fact diff_add_assoc [symmetric])
  1.1116  
  1.1117 -lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i) - k = (j - k) + i" for i j k :: nat
  1.1118 +lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i) - k = (j - k) + i"
  1.1119 +  for i j k :: nat
  1.1120    by (simp add: ac_simps)
  1.1121  
  1.1122 -lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j - k + i = j + i - k" for i j k :: nat
  1.1123 +lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j - k + i = j + i - k"
  1.1124 +  for i j k :: nat
  1.1125    by (fact diff_add_assoc2 [symmetric])
  1.1126  
  1.1127 -lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j - i = k) = (j = k + i)" for i j k :: nat
  1.1128 +lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j - i = k) = (j = k + i)"
  1.1129 +  for i j k :: nat
  1.1130    by auto
  1.1131  
  1.1132 -lemma diff_is_0_eq [simp]: "m - n = 0 \<longleftrightarrow> m \<le> n" for m n :: nat
  1.1133 +lemma diff_is_0_eq [simp]: "m - n = 0 \<longleftrightarrow> m \<le> n"
  1.1134 +  for m n :: nat
  1.1135    by (induct m n rule: diff_induct) simp_all
  1.1136  
  1.1137 -lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0" for m n :: nat
  1.1138 +lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0"
  1.1139 +  for m n :: nat
  1.1140    by (rule iffD2, rule diff_is_0_eq)
  1.1141  
  1.1142 -lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n" for m n :: nat
  1.1143 +lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n"
  1.1144 +  for m n :: nat
  1.1145    by (induct m n rule: diff_induct) simp_all
  1.1146  
  1.1147  lemma less_imp_add_positive:
  1.1148 @@ -1129,18 +1249,18 @@
  1.1149  qed
  1.1150  
  1.1151  text \<open>a nice rewrite for bounded subtraction\<close>
  1.1152 -lemma nat_minus_add_max: "n - m + m = max n m" for m n :: nat
  1.1153 -    by (simp add: max_def not_le order_less_imp_le)
  1.1154 +lemma nat_minus_add_max: "n - m + m = max n m"
  1.1155 +  for m n :: nat
  1.1156 +  by (simp add: max_def not_le order_less_imp_le)
  1.1157  
  1.1158  lemma nat_diff_split: "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)"
  1.1159    for a b :: nat
  1.1160 -    \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
  1.1161 -  by (cases "a < b")
  1.1162 -    (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym])
  1.1163 +  \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
  1.1164 +  by (cases "a < b") (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym])
  1.1165  
  1.1166  lemma nat_diff_split_asm: "P (a - b) \<longleftrightarrow> \<not> (a < b \<and> \<not> P 0 \<or> (\<exists>d. a = b + d \<and> \<not> P d))"
  1.1167    for a b :: nat
  1.1168 -    \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
  1.1169 +  \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
  1.1170    by (auto split: nat_diff_split)
  1.1171  
  1.1172  lemma Suc_pred': "0 < n \<Longrightarrow> n = Suc(n - 1)"
  1.1173 @@ -1149,64 +1269,78 @@
  1.1174  lemma add_eq_if: "m + n = (if m = 0 then n else Suc ((m - 1) + n))"
  1.1175    unfolding One_nat_def by (cases m) simp_all
  1.1176  
  1.1177 -lemma mult_eq_if: "m * n = (if m = 0 then 0 else n + ((m - 1) * n))" for m n :: nat
  1.1178 -  unfolding One_nat_def by (cases m) simp_all
  1.1179 +lemma mult_eq_if: "m * n = (if m = 0 then 0 else n + ((m - 1) * n))"
  1.1180 +  for m n :: nat
  1.1181 +  by (cases m) simp_all
  1.1182  
  1.1183  lemma Suc_diff_eq_diff_pred: "0 < n \<Longrightarrow> Suc m - n = m - (n - 1)"
  1.1184 -  unfolding One_nat_def by (cases n) simp_all
  1.1185 +  by (cases n) simp_all
  1.1186  
  1.1187  lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
  1.1188 -  unfolding One_nat_def by (cases m) simp_all
  1.1189 -
  1.1190 -lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
  1.1191 +  by (cases m) simp_all
  1.1192 +
  1.1193 +lemma Let_Suc [simp]: "Let (Suc n) f \<equiv> f (Suc n)"
  1.1194    by (fact Let_def)
  1.1195  
  1.1196  
  1.1197  subsubsection \<open>Monotonicity of multiplication\<close>
  1.1198  
  1.1199 -lemma mult_le_mono1: "i \<le> j \<Longrightarrow> i * k \<le> j * k" for i j k :: nat
  1.1200 +lemma mult_le_mono1: "i \<le> j \<Longrightarrow> i * k \<le> j * k"
  1.1201 +  for i j k :: nat
  1.1202    by (simp add: mult_right_mono)
  1.1203  
  1.1204 -lemma mult_le_mono2: "i \<le> j \<Longrightarrow> k * i \<le> k * j" for i j k :: nat
  1.1205 +lemma mult_le_mono2: "i \<le> j \<Longrightarrow> k * i \<le> k * j"
  1.1206 +  for i j k :: nat
  1.1207    by (simp add: mult_left_mono)
  1.1208  
  1.1209  text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close>
  1.1210 -lemma mult_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i * k \<le> j * l" for i j k l :: nat
  1.1211 +lemma mult_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i * k \<le> j * l"
  1.1212 +  for i j k l :: nat
  1.1213    by (simp add: mult_mono)
  1.1214  
  1.1215 -lemma mult_less_mono1: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> i * k < j * k" for i j k :: nat
  1.1216 +lemma mult_less_mono1: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> i * k < j * k"
  1.1217 +  for i j k :: nat
  1.1218    by (simp add: mult_strict_right_mono)
  1.1219  
  1.1220 -text\<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that
  1.1221 -      there are no negative numbers.\<close>
  1.1222 -lemma nat_0_less_mult_iff [simp]: "0 < m * n \<longleftrightarrow> 0 < m \<and> 0 < n" for m n :: nat
  1.1223 -  apply (induct m)
  1.1224 -   apply simp
  1.1225 -  apply (case_tac n)
  1.1226 -   apply simp_all
  1.1227 -  done
  1.1228 +text \<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that there are no negative numbers.\<close>
  1.1229 +lemma nat_0_less_mult_iff [simp]: "0 < m * n \<longleftrightarrow> 0 < m \<and> 0 < n"
  1.1230 +  for m n :: nat
  1.1231 +proof (induct m)
  1.1232 +  case 0
  1.1233 +  then show ?case by simp
  1.1234 +next
  1.1235 +  case (Suc m)
  1.1236 +  then show ?case by (cases n) simp_all
  1.1237 +qed
  1.1238  
  1.1239  lemma one_le_mult_iff [simp]: "Suc 0 \<le> m * n \<longleftrightarrow> Suc 0 \<le> m \<and> Suc 0 \<le> n"
  1.1240 -  apply (induct m)
  1.1241 -   apply simp
  1.1242 -  apply (case_tac n)
  1.1243 -   apply simp_all
  1.1244 -  done
  1.1245 -
  1.1246 -lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat
  1.1247 +proof (induct m)
  1.1248 +  case 0
  1.1249 +  then show ?case by simp
  1.1250 +next
  1.1251 +  case (Suc m)
  1.1252 +  then show ?case by (cases n) simp_all
  1.1253 +qed
  1.1254 +
  1.1255 +lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n"
  1.1256 +  for k m n :: nat
  1.1257    apply (safe intro!: mult_less_mono1)
  1.1258 -  apply (cases k, auto)
  1.1259 +   apply (cases k)
  1.1260 +    apply auto
  1.1261    apply (simp add: linorder_not_le [symmetric])
  1.1262    apply (blast intro: mult_le_mono1)
  1.1263    done
  1.1264  
  1.1265 -lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat
  1.1266 +lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n"
  1.1267 +  for k m n :: nat
  1.1268    by (simp add: mult.commute [of k])
  1.1269  
  1.1270 -lemma mult_le_cancel1 [simp]: "k * m \<le> k * n \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat
  1.1271 +lemma mult_le_cancel1 [simp]: "k * m \<le> k * n \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)"
  1.1272 +  for k m n :: nat
  1.1273    by (simp add: linorder_not_less [symmetric], auto)
  1.1274  
  1.1275 -lemma mult_le_cancel2 [simp]: "m * k \<le> n * k \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat
  1.1276 +lemma mult_le_cancel2 [simp]: "m * k \<le> n * k \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)"
  1.1277 +  for k m n :: nat
  1.1278    by (simp add: linorder_not_less [symmetric], auto)
  1.1279  
  1.1280  lemma Suc_mult_less_cancel1: "Suc k * m < Suc k * n \<longleftrightarrow> m < n"
  1.1281 @@ -1215,19 +1349,24 @@
  1.1282  lemma Suc_mult_le_cancel1: "Suc k * m \<le> Suc k * n \<longleftrightarrow> m \<le> n"
  1.1283    by (subst mult_le_cancel1) simp
  1.1284  
  1.1285 -lemma le_square: "m \<le> m * m" for m :: nat
  1.1286 +lemma le_square: "m \<le> m * m"
  1.1287 +  for m :: nat
  1.1288    by (cases m) (auto intro: le_add1)
  1.1289  
  1.1290 -lemma le_cube: "m \<le> m * (m * m)" for m :: nat
  1.1291 +lemma le_cube: "m \<le> m * (m * m)"
  1.1292 +  for m :: nat
  1.1293    by (cases m) (auto intro: le_add1)
  1.1294  
  1.1295  text \<open>Lemma for \<open>gcd\<close>\<close>
  1.1296 -lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat
  1.1297 +lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0"
  1.1298 +  for m n :: nat
  1.1299    apply (drule sym)
  1.1300    apply (rule disjCI)
  1.1301 -  apply (rule linorder_cases, erule_tac [2] _)
  1.1302 -   apply (drule_tac [2] mult_less_mono2)
  1.1303 -    apply (auto)
  1.1304 +  apply (rule linorder_cases)
  1.1305 +    defer
  1.1306 +    apply assumption
  1.1307 +   apply (drule mult_less_mono2)
  1.1308 +    apply auto
  1.1309    done
  1.1310  
  1.1311  lemma mono_times_nat:
  1.1312 @@ -1240,7 +1379,7 @@
  1.1313    with assms show "n * m \<le> n * q" by simp
  1.1314  qed
  1.1315  
  1.1316 -text \<open>the lattice order on @{typ nat}\<close>
  1.1317 +text \<open>The lattice order on @{typ nat}.\<close>
  1.1318  
  1.1319  instantiation nat :: distrib_lattice
  1.1320  begin
  1.1321 @@ -1272,15 +1411,16 @@
  1.1322  notation (latex output)
  1.1323    compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
  1.1324  
  1.1325 -text \<open>\<open>f ^^ n = f o ... o f\<close>, the n-fold composition of \<open>f\<close>\<close>
  1.1326 +text \<open>\<open>f ^^ n = f \<circ> \<dots> \<circ> f\<close>, the \<open>n\<close>-fold composition of \<open>f\<close>\<close>
  1.1327  
  1.1328  overloading
  1.1329    funpow \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
  1.1330  begin
  1.1331  
  1.1332 -primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
  1.1333 -  "funpow 0 f = id"
  1.1334 -| "funpow (Suc n) f = f o funpow n f"
  1.1335 +primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
  1.1336 +  where
  1.1337 +    "funpow 0 f = id"
  1.1338 +  | "funpow (Suc n) f = f \<circ> funpow n f"
  1.1339  
  1.1340  end
  1.1341  
  1.1342 @@ -1300,7 +1440,7 @@
  1.1343  
  1.1344  lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right
  1.1345  
  1.1346 -text \<open>for code generation\<close>
  1.1347 +text \<open>For code generation.\<close>
  1.1348  
  1.1349  definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
  1.1350    where funpow_code_def [code_abbrev]: "funpow = compow"
  1.1351 @@ -1315,18 +1455,20 @@
  1.1352  lemma funpow_add: "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
  1.1353    by (induct m) simp_all
  1.1354  
  1.1355 -lemma funpow_mult: "(f ^^ m) ^^ n = f ^^ (m * n)" for f :: "'a \<Rightarrow> 'a"
  1.1356 +lemma funpow_mult: "(f ^^ m) ^^ n = f ^^ (m * n)"
  1.1357 +  for f :: "'a \<Rightarrow> 'a"
  1.1358    by (induct n) (simp_all add: funpow_add)
  1.1359  
  1.1360  lemma funpow_swap1: "f ((f ^^ n) x) = (f ^^ n) (f x)"
  1.1361  proof -
  1.1362    have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp
  1.1363 -  also have "\<dots>  = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
  1.1364 +  also have "\<dots>  = (f ^^ n \<circ> f ^^ 1) x" by (simp only: funpow_add)
  1.1365    also have "\<dots> = (f ^^ n) (f x)" by simp
  1.1366    finally show ?thesis .
  1.1367  qed
  1.1368  
  1.1369 -lemma comp_funpow: "comp f ^^ n = comp (f ^^ n)" for f :: "'a \<Rightarrow> 'a"
  1.1370 +lemma comp_funpow: "comp f ^^ n = comp (f ^^ n)"
  1.1371 +  for f :: "'a \<Rightarrow> 'a"
  1.1372    by (induct n) simp_all
  1.1373  
  1.1374  lemma Suc_funpow[simp]: "Suc ^^ n = (op + n)"
  1.1375 @@ -1342,12 +1484,15 @@
  1.1376  
  1.1377  lemma funpow_mono2:
  1.1378    assumes "mono f"
  1.1379 -  assumes "i \<le> j"
  1.1380 -  assumes "x \<le> y"
  1.1381 -  assumes "x \<le> f x"
  1.1382 +    and "i \<le> j"
  1.1383 +    and "x \<le> y"
  1.1384 +    and "x \<le> f x"
  1.1385    shows "(f ^^ i) x \<le> (f ^^ j) y"
  1.1386 -using assms(2,3)
  1.1387 -proof(induct j arbitrary: y)
  1.1388 +  using assms(2,3)
  1.1389 +proof (induct j arbitrary: y)
  1.1390 +  case 0
  1.1391 +  then show ?case by simp
  1.1392 +next
  1.1393    case (Suc j)
  1.1394    show ?case
  1.1395    proof(cases "i = Suc j")
  1.1396 @@ -1358,40 +1503,43 @@
  1.1397      case False
  1.1398      with assms(1,4) Suc show ?thesis
  1.1399        by (simp del: funpow.simps add: funpow_simps_right le_eq_less_or_eq less_Suc_eq_le)
  1.1400 -         (simp add: Suc.hyps monoD order_subst1)
  1.1401 +        (simp add: Suc.hyps monoD order_subst1)
  1.1402    qed
  1.1403 -qed simp
  1.1404 +qed
  1.1405  
  1.1406  
  1.1407  subsection \<open>Kleene iteration\<close>
  1.1408  
  1.1409  lemma Kleene_iter_lpfp:
  1.1410 +  fixes f :: "'a::order_bot \<Rightarrow> 'a"
  1.1411    assumes "mono f"
  1.1412      and "f p \<le> p"
  1.1413 -  shows "(f^^k) (bot::'a::order_bot) \<le> p"
  1.1414 -proof(induction k)
  1.1415 +  shows "(f ^^ k) bot \<le> p"
  1.1416 +proof (induct k)
  1.1417    case 0
  1.1418    show ?case by simp
  1.1419  next
  1.1420    case Suc
  1.1421 -  from monoD[OF assms(1) Suc] assms(2) show ?case by simp
  1.1422 +  show ?case
  1.1423 +    using monoD[OF assms(1) Suc] assms(2) by simp
  1.1424  qed
  1.1425  
  1.1426  lemma lfp_Kleene_iter:
  1.1427    assumes "mono f"
  1.1428 -    and "(f^^Suc k) bot = (f^^k) bot"
  1.1429 -  shows "lfp f = (f^^k) bot"
  1.1430 +    and "(f ^^ Suc k) bot = (f ^^ k) bot"
  1.1431 +  shows "lfp f = (f ^^ k) bot"
  1.1432  proof (rule antisym)
  1.1433 -  show "lfp f \<le> (f^^k) bot"
  1.1434 +  show "lfp f \<le> (f ^^ k) bot"
  1.1435    proof (rule lfp_lowerbound)
  1.1436 -    show "f ((f^^k) bot) \<le> (f^^k) bot"
  1.1437 +    show "f ((f ^^ k) bot) \<le> (f ^^ k) bot"
  1.1438        using assms(2) by simp
  1.1439    qed
  1.1440 -  show "(f^^k) bot \<le> lfp f"
  1.1441 +  show "(f ^^ k) bot \<le> lfp f"
  1.1442      using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
  1.1443  qed
  1.1444  
  1.1445 -lemma mono_pow: "mono f \<Longrightarrow> mono (f ^^ n)" for f :: "'a \<Rightarrow> 'a::complete_lattice"
  1.1446 +lemma mono_pow: "mono f \<Longrightarrow> mono (f ^^ n)"
  1.1447 +  for f :: "'a \<Rightarrow> 'a::complete_lattice"
  1.1448    by (induct n) (auto simp: mono_def)
  1.1449  
  1.1450  lemma lfp_funpow:
  1.1451 @@ -1405,9 +1553,9 @@
  1.1452      then show "f (lfp (f ^^ Suc n)) \<le> lfp (f ^^ Suc n)"
  1.1453        by (simp add: comp_def)
  1.1454    qed
  1.1455 -  have "(f^^n) (lfp f) = lfp f" for n
  1.1456 +  have "(f ^^ n) (lfp f) = lfp f" for n
  1.1457      by (induct n) (auto intro: f lfp_unfold[symmetric])
  1.1458 -  then show "lfp (f^^Suc n) \<le> lfp f"
  1.1459 +  then show "lfp (f ^^ Suc n) \<le> lfp f"
  1.1460      by (intro lfp_lowerbound) (simp del: funpow.simps)
  1.1461  qed
  1.1462  
  1.1463 @@ -1422,32 +1570,36 @@
  1.1464      then show "f (gfp (f ^^ Suc n)) \<ge> gfp (f ^^ Suc n)"
  1.1465        by (simp add: comp_def)
  1.1466    qed
  1.1467 -  have "(f^^n) (gfp f) = gfp f" for n
  1.1468 +  have "(f ^^ n) (gfp f) = gfp f" for n
  1.1469      by (induct n) (auto intro: f gfp_unfold[symmetric])
  1.1470 -  then show "gfp (f^^Suc n) \<ge> gfp f"
  1.1471 +  then show "gfp (f ^^ Suc n) \<ge> gfp f"
  1.1472      by (intro gfp_upperbound) (simp del: funpow.simps)
  1.1473  qed
  1.1474  
  1.1475  lemma Kleene_iter_gpfp:
  1.1476 +  fixes f :: "'a::order_top \<Rightarrow> 'a"
  1.1477    assumes "mono f"
  1.1478 -  and "p \<le> f p"
  1.1479 -  shows "p \<le> (f ^^ k) (top::'a::order_top)"
  1.1480 -proof(induction k)
  1.1481 -  case 0 show ?case by simp
  1.1482 +    and "p \<le> f p"
  1.1483 +  shows "p \<le> (f ^^ k) top"
  1.1484 +proof (induct k)
  1.1485 +  case 0
  1.1486 +  show ?case by simp
  1.1487  next
  1.1488    case Suc
  1.1489 -  from monoD[OF assms(1) Suc] assms(2)
  1.1490 -  show ?case by simp
  1.1491 +  show ?case
  1.1492 +    using monoD[OF assms(1) Suc] assms(2) by simp
  1.1493  qed
  1.1494  
  1.1495  lemma gfp_Kleene_iter:
  1.1496    assumes "mono f"
  1.1497 -  and "(f ^^ Suc k) top = (f ^^ k) top"
  1.1498 -  shows "gfp f = (f ^^ k) top" (is "?lhs = ?rhs")
  1.1499 -proof(rule antisym)
  1.1500 -  have "?rhs \<le> f ?rhs" using assms(2) by simp
  1.1501 -  then show "?rhs \<le> ?lhs" by(rule gfp_upperbound)
  1.1502 -
  1.1503 +    and "(f ^^ Suc k) top = (f ^^ k) top"
  1.1504 +  shows "gfp f = (f ^^ k) top"
  1.1505 +    (is "?lhs = ?rhs")
  1.1506 +proof (rule antisym)
  1.1507 +  have "?rhs \<le> f ?rhs"
  1.1508 +    using assms(2) by simp
  1.1509 +  then show "?rhs \<le> ?lhs"
  1.1510 +    by (rule gfp_upperbound)
  1.1511    show "?lhs \<le> ?rhs"
  1.1512      using Kleene_iter_gpfp[OF assms(1)] gfp_unfold[OF assms(1)] by simp
  1.1513  qed
  1.1514 @@ -1478,9 +1630,10 @@
  1.1515  lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
  1.1516    by (induct x) (simp_all add: algebra_simps)
  1.1517  
  1.1518 -primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
  1.1519 -  "of_nat_aux inc 0 i = i"
  1.1520 -| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close>
  1.1521 +primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
  1.1522 +  where
  1.1523 +    "of_nat_aux inc 0 i = i"
  1.1524 +  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close>
  1.1525  
  1.1526  lemma of_nat_code: "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
  1.1527  proof (induct n)
  1.1528 @@ -1492,7 +1645,8 @@
  1.1529      by (induct n) simp_all
  1.1530    from this [of 0] have "of_nat_aux (\<lambda>i. i + 1) n 1 = of_nat_aux (\<lambda>i. i + 1) n 0 + 1"
  1.1531      by simp
  1.1532 -  with Suc show ?case by (simp add: add.commute)
  1.1533 +  with Suc show ?case
  1.1534 +    by (simp add: add.commute)
  1.1535  qed
  1.1536  
  1.1537  end
  1.1538 @@ -1525,12 +1679,10 @@
  1.1539  lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
  1.1540    by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
  1.1541  
  1.1542 -lemma of_nat_neq_0 [simp]:
  1.1543 -  "of_nat (Suc n) \<noteq> 0"
  1.1544 +lemma of_nat_neq_0 [simp]: "of_nat (Suc n) \<noteq> 0"
  1.1545    unfolding of_nat_eq_0_iff by simp
  1.1546  
  1.1547 -lemma of_nat_0_neq [simp]:
  1.1548 -  "0 \<noteq> of_nat (Suc n)"
  1.1549 +lemma of_nat_0_neq [simp]: "0 \<noteq> of_nat (Suc n)"
  1.1550    unfolding of_nat_0_eq_iff by simp
  1.1551  
  1.1552  end
  1.1553 @@ -1600,28 +1752,28 @@
  1.1554    by (simp add: Nats_def)
  1.1555  
  1.1556  lemma Nats_0 [simp]: "0 \<in> \<nat>"
  1.1557 -apply (simp add: Nats_def)
  1.1558 -apply (rule range_eqI)
  1.1559 -apply (rule of_nat_0 [symmetric])
  1.1560 -done
  1.1561 +  apply (simp add: Nats_def)
  1.1562 +  apply (rule range_eqI)
  1.1563 +  apply (rule of_nat_0 [symmetric])
  1.1564 +  done
  1.1565  
  1.1566  lemma Nats_1 [simp]: "1 \<in> \<nat>"
  1.1567 -apply (simp add: Nats_def)
  1.1568 -apply (rule range_eqI)
  1.1569 -apply (rule of_nat_1 [symmetric])
  1.1570 -done
  1.1571 +  apply (simp add: Nats_def)
  1.1572 +  apply (rule range_eqI)
  1.1573 +  apply (rule of_nat_1 [symmetric])
  1.1574 +  done
  1.1575  
  1.1576  lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
  1.1577 -apply (auto simp add: Nats_def)
  1.1578 -apply (rule range_eqI)
  1.1579 -apply (rule of_nat_add [symmetric])
  1.1580 -done
  1.1581 +  apply (auto simp add: Nats_def)
  1.1582 +  apply (rule range_eqI)
  1.1583 +  apply (rule of_nat_add [symmetric])
  1.1584 +  done
  1.1585  
  1.1586  lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
  1.1587 -apply (auto simp add: Nats_def)
  1.1588 -apply (rule range_eqI)
  1.1589 -apply (rule of_nat_mult [symmetric])
  1.1590 -done
  1.1591 +  apply (auto simp add: Nats_def)
  1.1592 +  apply (rule range_eqI)
  1.1593 +  apply (rule of_nat_mult [symmetric])
  1.1594 +  done
  1.1595  
  1.1596  lemma Nats_cases [cases set: Nats]:
  1.1597    assumes "x \<in> \<nat>"
  1.1598 @@ -1633,8 +1785,7 @@
  1.1599    then show thesis ..
  1.1600  qed
  1.1601  
  1.1602 -lemma Nats_induct [case_names of_nat, induct set: Nats]:
  1.1603 -  "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x"
  1.1604 +lemma Nats_induct [case_names of_nat, induct set: Nats]: "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x"
  1.1605    by (rule Nats_cases) auto
  1.1606  
  1.1607  end
  1.1608 @@ -1669,7 +1820,8 @@
  1.1609  begin
  1.1610  
  1.1611  lemma lift_Suc_mono_le:
  1.1612 -  assumes mono: "\<And>n. f n \<le> f (Suc n)" and "n \<le> n'"
  1.1613 +  assumes mono: "\<And>n. f n \<le> f (Suc n)"
  1.1614 +    and "n \<le> n'"
  1.1615    shows "f n \<le> f n'"
  1.1616  proof (cases "n < n'")
  1.1617    case True
  1.1618 @@ -1681,7 +1833,8 @@
  1.1619  qed
  1.1620  
  1.1621  lemma lift_Suc_antimono_le:
  1.1622 -  assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
  1.1623 +  assumes mono: "\<And>n. f n \<ge> f (Suc n)"
  1.1624 +    and "n \<le> n'"
  1.1625    shows "f n \<ge> f n'"
  1.1626  proof (cases "n < n'")
  1.1627    case True
  1.1628 @@ -1693,7 +1846,8 @@
  1.1629  qed
  1.1630  
  1.1631  lemma lift_Suc_mono_less:
  1.1632 -  assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
  1.1633 +  assumes mono: "\<And>n. f n < f (Suc n)"
  1.1634 +    and "n < n'"
  1.1635    shows "f n < f n'"
  1.1636    using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono)
  1.1637  
  1.1638 @@ -1737,56 +1891,71 @@
  1.1639    then show ?thesis by simp
  1.1640  qed
  1.1641  
  1.1642 -lemma less_diff_conv: "i < j - k \<longleftrightarrow> i + k < j" for i j k :: nat
  1.1643 +lemma less_diff_conv: "i < j - k \<longleftrightarrow> i + k < j"
  1.1644 +  for i j k :: nat
  1.1645    by (cases "k \<le> j") (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
  1.1646  
  1.1647 -lemma less_diff_conv2: "k \<le> j \<Longrightarrow> j - k < i \<longleftrightarrow> j < i + k" for j k i :: nat
  1.1648 +lemma less_diff_conv2: "k \<le> j \<Longrightarrow> j - k < i \<longleftrightarrow> j < i + k"
  1.1649 +  for j k i :: nat
  1.1650    by (auto dest: le_Suc_ex)
  1.1651  
  1.1652 -lemma le_diff_conv: "j - k \<le> i \<longleftrightarrow> j \<le> i + k" for j k i :: nat
  1.1653 +lemma le_diff_conv: "j - k \<le> i \<longleftrightarrow> j \<le> i + k"
  1.1654 +  for j k i :: nat
  1.1655    by (cases "k \<le> j") (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
  1.1656  
  1.1657 -lemma diff_diff_cancel [simp]: "i \<le> n \<Longrightarrow> n - (n - i) = i" for i n :: nat
  1.1658 +lemma diff_diff_cancel [simp]: "i \<le> n \<Longrightarrow> n - (n - i) = i"
  1.1659 +  for i n :: nat
  1.1660    by (auto dest: le_Suc_ex)
  1.1661  
  1.1662 -lemma diff_less [simp]: "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m" for i n :: nat
  1.1663 +lemma diff_less [simp]: "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m"
  1.1664 +  for i n :: nat
  1.1665    by (auto dest: less_imp_Suc_add)
  1.1666  
  1.1667  text \<open>Simplification of relational expressions involving subtraction\<close>
  1.1668  
  1.1669 -lemma diff_diff_eq: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n" for m n k :: nat
  1.1670 +lemma diff_diff_eq: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n"
  1.1671 +  for m n k :: nat
  1.1672    by (auto dest!: le_Suc_ex)
  1.1673  
  1.1674  hide_fact (open) diff_diff_eq
  1.1675  
  1.1676 -lemma eq_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n" for m n k :: nat
  1.1677 +lemma eq_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n"
  1.1678 +  for m n k :: nat
  1.1679    by (auto dest: le_Suc_ex)
  1.1680  
  1.1681 -lemma less_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n" for m n k :: nat
  1.1682 +lemma less_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n"
  1.1683 +  for m n k :: nat
  1.1684    by (auto dest!: le_Suc_ex)
  1.1685  
  1.1686 -lemma le_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n" for m n k :: nat
  1.1687 +lemma le_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
  1.1688 +  for m n k :: nat
  1.1689    by (auto dest!: le_Suc_ex)
  1.1690  
  1.1691 -lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> a" for a b c :: nat
  1.1692 +lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> a"
  1.1693 +  for a b c :: nat
  1.1694    by (force dest: le_Suc_ex)
  1.1695  
  1.1696  
  1.1697  text \<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
  1.1698  
  1.1699 -lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l" for m n l :: nat
  1.1700 +lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l"
  1.1701 +  for m n l :: nat
  1.1702    by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
  1.1703  
  1.1704 -lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m" for m n l :: nat
  1.1705 +lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m"
  1.1706 +  for m n l :: nat
  1.1707    by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
  1.1708  
  1.1709 -lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m" for m n l :: nat
  1.1710 +lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
  1.1711 +  for m n l :: nat
  1.1712    by (auto dest: less_imp_Suc_add split add: nat_diff_split)
  1.1713  
  1.1714 -lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n" for m n :: nat
  1.1715 +lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
  1.1716 +  for m n :: nat
  1.1717    by (simp split add: nat_diff_split)
  1.1718  
  1.1719 -lemma min_diff: "min (m - i) (n - i) = min m n - i" for m n i :: nat
  1.1720 +lemma min_diff: "min (m - i) (n - i) = min m n - i"
  1.1721 +  for m n i :: nat
  1.1722    by (cases m n rule: le_cases)
  1.1723      (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono)
  1.1724  
  1.1725 @@ -1803,7 +1972,8 @@
  1.1726  
  1.1727  text \<open>Rewriting to pull differences out\<close>
  1.1728  
  1.1729 -lemma diff_diff_right [simp]: "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j" for i j k :: nat
  1.1730 +lemma diff_diff_right [simp]: "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j"
  1.1731 +  for i j k :: nat
  1.1732    by (fact diff_diff_right)
  1.1733  
  1.1734  lemma diff_Suc_diff_eq1 [simp]:
  1.1735 @@ -1870,12 +2040,9 @@
  1.1736    from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp
  1.1737    then have "d + 1 - 1 = j - n - 1" by simp
  1.1738    then have "d = j - n - 1" by simp
  1.1739 -  then have "d = j - (n + 1)"
  1.1740 -    by (simp add: diff_diff_eq)
  1.1741 -  then have "d = j - Suc n"
  1.1742 -    by simp
  1.1743 -  moreover from \<open>n < j\<close> have "Suc n \<le> j"
  1.1744 -    by (simp add: Suc_le_eq)
  1.1745 +  then have "d = j - (n + 1)" by (simp add: diff_diff_eq)
  1.1746 +  then have "d = j - Suc n" by simp
  1.1747 +  moreover from \<open>n < j\<close> have "Suc n \<le> j" by (simp add: Suc_le_eq)
  1.1748    ultimately have "P (Suc n)"
  1.1749    proof (rule Suc.hyps)
  1.1750      fix q
  1.1751 @@ -1883,11 +2050,9 @@
  1.1752      then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le)
  1.1753      moreover assume "q < j"
  1.1754      moreover assume "P (Suc q)"
  1.1755 -    ultimately show "P q"
  1.1756 -      by (rule Suc.prems)
  1.1757 +    ultimately show "P q" by (rule Suc.prems)
  1.1758    qed
  1.1759 -  with order_refl \<open>n < j\<close> show "P n"
  1.1760 -    by (rule Suc.prems)
  1.1761 +  with order_refl \<open>n < j\<close> show "P n" by (rule Suc.prems)
  1.1762  qed
  1.1763  
  1.1764  lemma strict_inc_induct [consumes 1, case_names base step]:
  1.1765 @@ -1906,16 +2071,11 @@
  1.1766    case (Suc d i)
  1.1767    from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i"
  1.1768      by (simp add: diff_diff_add)
  1.1769 -  then have "Suc d - 1 = j - Suc i - 1"
  1.1770 -    by simp
  1.1771 -  then have "d = j - Suc i - 1"
  1.1772 -    by simp
  1.1773 -  moreover from * have "j - Suc i \<noteq> 0"
  1.1774 -    by auto
  1.1775 -  then have "Suc i < j"
  1.1776 -    by (simp add: not_le)
  1.1777 -  ultimately have "P (Suc i)"
  1.1778 -    by (rule Suc.hyps)
  1.1779 +  then have "Suc d - 1 = j - Suc i - 1" by simp
  1.1780 +  then have "d = j - Suc i - 1" by simp
  1.1781 +  moreover from * have "j - Suc i \<noteq> 0" by auto
  1.1782 +  then have "Suc i < j" by (simp add: not_le)
  1.1783 +  ultimately have "P (Suc i)" by (rule Suc.hyps)
  1.1784    with \<open>i < j\<close> show "P i" by (rule step)
  1.1785  qed
  1.1786  
  1.1787 @@ -1925,7 +2085,7 @@
  1.1788  lemma zero_induct: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P 0"
  1.1789    using inc_induct[of 0 k P] by blast
  1.1790  
  1.1791 -text \<open>Further induction rule similar to @{thm inc_induct}\<close>
  1.1792 +text \<open>Further induction rule similar to @{thm inc_induct}.\<close>
  1.1793  
  1.1794  lemma dec_induct [consumes 1, case_names base step]:
  1.1795    "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.1796 @@ -1947,11 +2107,9 @@
  1.1797        moreover assume "q < j" then have "q < Suc j"
  1.1798          by (simp add: less_Suc_eq)
  1.1799        moreover assume "P q"
  1.1800 -      ultimately show "P (Suc q)"
  1.1801 -        by (rule Suc.prems)
  1.1802 +      ultimately show "P (Suc q)" by (rule Suc.prems)
  1.1803      qed
  1.1804 -    ultimately show "P (Suc j)"
  1.1805 -      by (rule Suc.prems)
  1.1806 +    ultimately show "P (Suc j)" by (rule Suc.prems)
  1.1807    next
  1.1808      case 2
  1.1809      with \<open>P i\<close> show "P (Suc j)" by simp
  1.1810 @@ -1961,28 +2119,24 @@
  1.1811  
  1.1812  subsection \<open>Monotonicity of \<open>funpow\<close>\<close>
  1.1813  
  1.1814 -lemma funpow_increasing:
  1.1815 -  fixes f :: "'a \<Rightarrow> 'a::{lattice,order_top}"
  1.1816 -  shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>"
  1.1817 +lemma funpow_increasing: "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>"
  1.1818 +  for f :: "'a::{lattice,order_top} \<Rightarrow> 'a"
  1.1819    by (induct rule: inc_induct)
  1.1820 -     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
  1.1821 -           intro: order_trans[OF _ funpow_mono])
  1.1822 -
  1.1823 -lemma funpow_decreasing:
  1.1824 -  fixes f :: "'a \<Rightarrow> 'a::{lattice,order_bot}"
  1.1825 -  shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>"
  1.1826 +    (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
  1.1827 +      intro: order_trans[OF _ funpow_mono])
  1.1828 +
  1.1829 +lemma funpow_decreasing: "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>"
  1.1830 +  for f :: "'a::{lattice,order_bot} \<Rightarrow> 'a"
  1.1831    by (induct rule: dec_induct)
  1.1832 -     (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
  1.1833 -           intro: order_trans[OF _ funpow_mono])
  1.1834 -
  1.1835 -lemma mono_funpow:
  1.1836 -  fixes Q :: "'a::{lattice,order_bot} \<Rightarrow> 'a"
  1.1837 -  shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
  1.1838 +    (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
  1.1839 +      intro: order_trans[OF _ funpow_mono])
  1.1840 +
  1.1841 +lemma mono_funpow: "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
  1.1842 +  for Q :: "'a::{lattice,order_bot} \<Rightarrow> 'a"
  1.1843    by (auto intro!: funpow_decreasing simp: mono_def)
  1.1844  
  1.1845 -lemma antimono_funpow:
  1.1846 -  fixes Q :: "'a::{lattice,order_top} \<Rightarrow> 'a"
  1.1847 -  shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
  1.1848 +lemma antimono_funpow: "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
  1.1849 +  for Q :: "'a::{lattice,order_top} \<Rightarrow> 'a"
  1.1850    by (auto intro!: funpow_increasing simp: antimono_def)
  1.1851  
  1.1852  
  1.1853 @@ -1994,21 +2148,26 @@
  1.1854  lemma dvd_1_iff_1 [simp]: "m dvd Suc 0 \<longleftrightarrow> m = Suc 0"
  1.1855    by (simp add: dvd_def)
  1.1856  
  1.1857 -lemma nat_dvd_1_iff_1 [simp]: "m dvd 1 \<longleftrightarrow> m = 1" for m :: nat
  1.1858 +lemma nat_dvd_1_iff_1 [simp]: "m dvd 1 \<longleftrightarrow> m = 1"
  1.1859 +  for m :: nat
  1.1860    by (simp add: dvd_def)
  1.1861  
  1.1862 -lemma dvd_antisym: "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n" for m n :: nat
  1.1863 +lemma dvd_antisym: "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n"
  1.1864 +  for m n :: nat
  1.1865    unfolding dvd_def by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
  1.1866  
  1.1867 -lemma dvd_diff_nat [simp]: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)" for k m n :: nat
  1.1868 +lemma dvd_diff_nat [simp]: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)"
  1.1869 +  for k m n :: nat
  1.1870    unfolding dvd_def by (blast intro: right_diff_distrib' [symmetric])
  1.1871  
  1.1872 -lemma dvd_diffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd m" for k m n :: nat
  1.1873 +lemma dvd_diffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd m"
  1.1874 +  for k m n :: nat
  1.1875    apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
  1.1876    apply (blast intro: dvd_add)
  1.1877    done
  1.1878  
  1.1879 -lemma dvd_diffD1: "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd n" for k m n :: nat
  1.1880 +lemma dvd_diffD1: "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd n"
  1.1881 +  for k m n :: nat
  1.1882    by (drule_tac m = m in dvd_diff_nat) auto
  1.1883  
  1.1884  lemma dvd_mult_cancel:
  1.1885 @@ -2022,19 +2181,24 @@
  1.1886    then show ?thesis ..
  1.1887  qed
  1.1888  
  1.1889 -lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1" for m n :: nat
  1.1890 +lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1"
  1.1891 +  for m n :: nat
  1.1892    apply auto
  1.1893 -   apply (subgoal_tac "m * n dvd m * 1")
  1.1894 -   apply (drule dvd_mult_cancel, auto)
  1.1895 +  apply (subgoal_tac "m * n dvd m * 1")
  1.1896 +   apply (drule dvd_mult_cancel)
  1.1897 +    apply auto
  1.1898    done
  1.1899  
  1.1900 -lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1" for m n :: nat
  1.1901 +lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1"
  1.1902 +  for m n :: nat
  1.1903    using dvd_mult_cancel1 [of m n] by (simp add: ac_simps)
  1.1904  
  1.1905 -lemma dvd_imp_le: "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> n" for k n :: nat
  1.1906 +lemma dvd_imp_le: "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> n"
  1.1907 +  for k n :: nat
  1.1908    by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
  1.1909  
  1.1910 -lemma nat_dvd_not_less: "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m" for m n :: nat
  1.1911 +lemma nat_dvd_not_less: "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
  1.1912 +  for m n :: nat
  1.1913    by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
  1.1914  
  1.1915  lemma less_eq_dvd_minus:
  1.1916 @@ -2047,7 +2211,8 @@
  1.1917    then show ?thesis by (simp add: add.commute [of m])
  1.1918  qed
  1.1919  
  1.1920 -lemma dvd_minus_self: "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n" for m n :: nat
  1.1921 +lemma dvd_minus_self: "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
  1.1922 +  for m n :: nat
  1.1923    by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le)
  1.1924  
  1.1925  lemma dvd_minus_add:
  1.1926 @@ -2066,55 +2231,72 @@
  1.1927  
  1.1928  subsection \<open>Aliasses\<close>
  1.1929  
  1.1930 -lemma nat_mult_1: "1 * n = n" for n :: nat
  1.1931 +lemma nat_mult_1: "1 * n = n"
  1.1932 +  for n :: nat
  1.1933    by (fact mult_1_left)
  1.1934  
  1.1935 -lemma nat_mult_1_right: "n * 1 = n" for n :: nat
  1.1936 +lemma nat_mult_1_right: "n * 1 = n"
  1.1937 +  for n :: nat
  1.1938    by (fact mult_1_right)
  1.1939  
  1.1940 -lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n" for k m n :: nat
  1.1941 +lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n"
  1.1942 +  for k m n :: nat
  1.1943    by (fact add_left_cancel)
  1.1944  
  1.1945 -lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n" for k m n :: nat
  1.1946 +lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n"
  1.1947 +  for k m n :: nat
  1.1948    by (fact add_right_cancel)
  1.1949  
  1.1950 -lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)" for k m n :: nat
  1.1951 +lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)"
  1.1952 +  for k m n :: nat
  1.1953    by (fact left_diff_distrib')
  1.1954  
  1.1955 -lemma diff_mult_distrib2: "k * (m - n) = (k * m) - (k * n)" for k m n :: nat
  1.1956 +lemma diff_mult_distrib2: "k * (m - n) = (k * m) - (k * n)"
  1.1957 +  for k m n :: nat
  1.1958    by (fact right_diff_distrib')
  1.1959  
  1.1960 -lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k" for k m n :: nat
  1.1961 +lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k"
  1.1962 +  for k m n :: nat
  1.1963    by (fact le_add_diff)  (* FIXME delete *)
  1.1964  
  1.1965 -lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)" for i j k :: nat
  1.1966 +lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)"
  1.1967 +  for i j k :: nat
  1.1968    by (fact le_diff_conv2) (* FIXME delete *)
  1.1969  
  1.1970 -lemma diff_self_eq_0 [simp]: "m - m = 0" for m :: nat
  1.1971 +lemma diff_self_eq_0 [simp]: "m - m = 0"
  1.1972 +  for m :: nat
  1.1973    by (fact diff_cancel)
  1.1974  
  1.1975 -lemma diff_diff_left [simp]: "i - j - k = i - (j + k)" for i j k :: nat
  1.1976 +lemma diff_diff_left [simp]: "i - j - k = i - (j + k)"
  1.1977 +  for i j k :: nat
  1.1978    by (fact diff_diff_add)
  1.1979  
  1.1980 -lemma diff_commute: "i - j - k = i - k - j" for i j k :: nat
  1.1981 +lemma diff_commute: "i - j - k = i - k - j"
  1.1982 +  for i j k :: nat
  1.1983    by (fact diff_right_commute)
  1.1984  
  1.1985 -lemma diff_add_inverse: "(n + m) - n = m" for m n :: nat
  1.1986 +lemma diff_add_inverse: "(n + m) - n = m"
  1.1987 +  for m n :: nat
  1.1988    by (fact add_diff_cancel_left')
  1.1989  
  1.1990 -lemma diff_add_inverse2: "(m + n) - n = m" for m n :: nat
  1.1991 +lemma diff_add_inverse2: "(m + n) - n = m"
  1.1992 +  for m n :: nat
  1.1993    by (fact add_diff_cancel_right')
  1.1994  
  1.1995 -lemma diff_cancel: "(k + m) - (k + n) = m - n" for k m n :: nat
  1.1996 +lemma diff_cancel: "(k + m) - (k + n) = m - n"
  1.1997 +  for k m n :: nat
  1.1998    by (fact add_diff_cancel_left)
  1.1999  
  1.2000 -lemma diff_cancel2: "(m + k) - (n + k) = m - n" for k m n :: nat
  1.2001 +lemma diff_cancel2: "(m + k) - (n + k) = m - n"
  1.2002 +  for k m n :: nat
  1.2003    by (fact add_diff_cancel_right)
  1.2004  
  1.2005 -lemma diff_add_0: "n - (n + m) = 0" for m n :: nat
  1.2006 +lemma diff_add_0: "n - (n + m) = 0"
  1.2007 +  for m n :: nat
  1.2008    by (fact diff_add_zero)
  1.2009  
  1.2010 -lemma add_mult_distrib2: "k * (m + n) = (k * m) + (k * n)" for k m n :: nat
  1.2011 +lemma add_mult_distrib2: "k * (m + n) = (k * m) + (k * n)"
  1.2012 +  for k m n :: nat
  1.2013    by (fact distrib_left)
  1.2014  
  1.2015  lemmas nat_distrib =