misc tuning and modernization;
authorwenzelm
Mon May 23 14:43:14 2016 +0200 (2016-05-23)
changeset 63110ccbdce905fca
parent 63109 87a4283537e4
child 63111 caa0c513bbca
misc tuning and modernization;
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Mon May 23 12:48:24 2016 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon May 23 14:43:14 2016 +0200
     1.3 @@ -21,10 +21,10 @@
     1.4  
     1.5  typedecl ind
     1.6  
     1.7 -axiomatization Zero_Rep :: ind and Suc_Rep :: "ind => ind" where
     1.8 -  \<comment> \<open>the axiom of infinity in 2 parts\<close>
     1.9 -  Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
    1.10 -  Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    1.11 +axiomatization Zero_Rep :: ind and Suc_Rep :: "ind \<Rightarrow> ind"
    1.12 +  \<comment> \<open>The axiom of infinity in 2 parts:\<close>
    1.13 +where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y"
    1.14 +  and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    1.15  
    1.16  subsection \<open>Type nat\<close>
    1.17  
    1.18 @@ -120,8 +120,8 @@
    1.19  
    1.20  setup \<open>Sign.parent_path\<close>
    1.21  
    1.22 -abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where
    1.23 -  "rec_nat \<equiv> old.rec_nat"
    1.24 +abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
    1.25 +  where "rec_nat \<equiv> old.rec_nat"
    1.26  
    1.27  declare nat.sel[code del]
    1.28  
    1.29 @@ -199,8 +199,12 @@
    1.30  text \<open>A special form of induction for reasoning
    1.31    about @{term "m < n"} and @{term "m - n"}\<close>
    1.32  
    1.33 -lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    1.34 -    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
    1.35 +lemma diff_induct:
    1.36 +  assumes "\<And>x. P x 0"
    1.37 +    and "\<And>y. P 0 (Suc y)"
    1.38 +    and "\<And>x y. P x y \<Longrightarrow> P (Suc x) (Suc y)"
    1.39 +  shows "P m n"
    1.40 +  using assms
    1.41    apply (rule_tac x = m in spec)
    1.42    apply (induct n)
    1.43    prefer 2
    1.44 @@ -215,10 +219,10 @@
    1.45  begin
    1.46  
    1.47  primrec plus_nat where
    1.48 -  add_0:      "0 + n = (n::nat)"
    1.49 -| add_Suc:  "Suc m + n = Suc (m + n)"
    1.50 -
    1.51 -lemma add_0_right [simp]: "m + 0 = (m::nat)"
    1.52 +  add_0: "0 + n = (n::nat)"
    1.53 +| add_Suc: "Suc m + n = Suc (m + n)"
    1.54 +
    1.55 +lemma add_0_right [simp]: "m + 0 = m" for m :: nat
    1.56    by (induct m) simp_all
    1.57  
    1.58  lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
    1.59 @@ -231,17 +235,18 @@
    1.60  
    1.61  primrec minus_nat where
    1.62    diff_0 [code]: "m - 0 = (m::nat)"
    1.63 -| diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    1.64 +| diff_Suc: "m - Suc n = (case m - n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k)"
    1.65  
    1.66  declare diff_Suc [simp del]
    1.67  
    1.68 -lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
    1.69 +lemma diff_0_eq_0 [simp, code]: "0 - n = 0" for n :: nat
    1.70    by (induct n) (simp_all add: diff_Suc)
    1.71  
    1.72  lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n"
    1.73    by (induct n) (simp_all add: diff_Suc)
    1.74  
    1.75 -instance proof
    1.76 +instance
    1.77 +proof
    1.78    fix n m q :: nat
    1.79    show "(n + m) + q = n + (m + q)" by (induct n) simp_all
    1.80    show "n + m = m + n" by (induct n) simp_all
    1.81 @@ -265,25 +270,24 @@
    1.82    mult_0: "0 * n = (0::nat)"
    1.83  | mult_Suc: "Suc m * n = n + (m * n)"
    1.84  
    1.85 -lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
    1.86 +lemma mult_0_right [simp]: "m * 0 = 0" for m :: nat
    1.87    by (induct m) simp_all
    1.88  
    1.89  lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
    1.90    by (induct m) (simp_all add: add.left_commute)
    1.91  
    1.92 -lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
    1.93 +lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)" for m n k :: nat
    1.94    by (induct m) (simp_all add: add.assoc)
    1.95  
    1.96 -instance proof
    1.97 -  fix n m q :: nat
    1.98 +instance
    1.99 +proof
   1.100 +  fix k n m q :: nat
   1.101    show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp
   1.102    show "1 * n = n" unfolding One_nat_def by simp
   1.103    show "n * m = m * n" by (induct n) simp_all
   1.104    show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
   1.105    show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
   1.106 -next
   1.107 -  fix k m n :: nat
   1.108 -  show "k * ((m::nat) - n) = (k * m) - (k * n)"
   1.109 +  show "k * (m - n) = (k * m) - (k * n)"
   1.110      by (induct m n rule: diff_induct) simp_all
   1.111  qed
   1.112  
   1.113 @@ -294,29 +298,23 @@
   1.114  
   1.115  text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close>
   1.116  
   1.117 -lemma add_is_0 [iff]:
   1.118 -  fixes m n :: nat
   1.119 -  shows "(m + n = 0) = (m = 0 & n = 0)"
   1.120 +lemma add_is_0 [iff]: "(m + n = 0) = (m = 0 \<and> n = 0)" for m n :: nat
   1.121    by (cases m) simp_all
   1.122  
   1.123 -lemma add_is_1:
   1.124 -  "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)"
   1.125 +lemma add_is_1: "m + n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
   1.126    by (cases m) simp_all
   1.127  
   1.128 -lemma one_is_add:
   1.129 -  "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
   1.130 +lemma one_is_add: "Suc 0 = m + n \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
   1.131    by (rule trans, rule eq_commute, rule add_is_1)
   1.132  
   1.133 -lemma add_eq_self_zero:
   1.134 -  fixes m n :: nat
   1.135 -  shows "m + n = m \<Longrightarrow> n = 0"
   1.136 +lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0" for m n :: nat
   1.137    by (induct m) simp_all
   1.138  
   1.139 -lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N"
   1.140 +lemma inj_on_add_nat[simp]: "inj_on (\<lambda>n. n + k) N" for k :: nat
   1.141    apply (induct k)
   1.142     apply simp
   1.143 -  apply(drule comp_inj_on[OF _ inj_Suc])
   1.144 -  apply (simp add:o_def)
   1.145 +  apply (drule comp_inj_on[OF _ inj_Suc])
   1.146 +  apply (simp add: o_def)
   1.147    done
   1.148  
   1.149  lemma Suc_eq_plus1: "Suc n = n + 1"
   1.150 @@ -336,43 +334,45 @@
   1.151  
   1.152  subsubsection \<open>Multiplication\<close>
   1.153  
   1.154 -lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   1.155 +lemma mult_is_0 [simp]: "m * n = 0 \<longleftrightarrow> m = 0 \<or> n = 0" for m n :: nat
   1.156    by (induct m) auto
   1.157  
   1.158 -lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"
   1.159 +lemma mult_eq_1_iff [simp]: "m * n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
   1.160    apply (induct m)
   1.161     apply simp
   1.162    apply (induct n)
   1.163     apply auto
   1.164    done
   1.165  
   1.166 -lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
   1.167 +lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
   1.168    apply (rule trans)
   1.169    apply (rule_tac [2] mult_eq_1_iff, fastforce)
   1.170    done
   1.171  
   1.172 -lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"
   1.173 +lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
   1.174    unfolding One_nat_def by (rule mult_eq_1_iff)
   1.175  
   1.176 -lemma nat_1_eq_mult_iff [simp]: "(1::nat) = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
   1.177 +lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
   1.178    unfolding One_nat_def by (rule one_eq_mult_iff)
   1.179  
   1.180 -lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
   1.181 +lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0" for k m n :: nat
   1.182  proof -
   1.183    have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
   1.184    proof (induct n arbitrary: m)
   1.185 -    case 0 then show "m = 0" by simp
   1.186 +    case 0
   1.187 +    then show "m = 0" by simp
   1.188    next
   1.189 -    case (Suc n) then show "m = Suc n"
   1.190 -      by (cases m) (simp_all add: eq_commute [of "0"])
   1.191 +    case (Suc n)
   1.192 +    then show "m = Suc n"
   1.193 +      by (cases m) (simp_all add: eq_commute [of 0])
   1.194    qed
   1.195    then show ?thesis by auto
   1.196  qed
   1.197  
   1.198 -lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   1.199 +lemma mult_cancel2 [simp]: "m * k = n * k \<longleftrightarrow> m = n \<or> k = 0" for k m n :: nat
   1.200    by (simp add: mult.commute)
   1.201  
   1.202 -lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
   1.203 +lemma Suc_mult_cancel1: "Suc k * m = Suc k * n \<longleftrightarrow> m = n"
   1.204    by (subst mult_cancel1) simp
   1.205  
   1.206  
   1.207 @@ -388,8 +388,12 @@
   1.208  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
   1.209  
   1.210  declare less_eq_nat.simps [simp del]
   1.211 -lemma le0 [iff]: "0 \<le> (n::nat)" by (simp add: less_eq_nat.simps)
   1.212 -lemma [code]: "(0::nat) \<le> n \<longleftrightarrow> True" by simp
   1.213 +
   1.214 +lemma le0 [iff]: "0 \<le> n" for n :: nat
   1.215 +  by (simp add: less_eq_nat.simps)
   1.216 +
   1.217 +lemma [code]: "0 \<le> n \<longleftrightarrow> True" for n :: nat
   1.218 +  by simp
   1.219  
   1.220  definition less_nat where
   1.221    less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
   1.222 @@ -400,13 +404,13 @@
   1.223  lemma Suc_le_eq [code]: "Suc m \<le> n \<longleftrightarrow> m < n"
   1.224    unfolding less_eq_Suc_le ..
   1.225  
   1.226 -lemma le_0_eq [iff]: "(n::nat) \<le> 0 \<longleftrightarrow> n = 0"
   1.227 +lemma le_0_eq [iff]: "n \<le> 0 \<longleftrightarrow> n = 0" for n :: nat
   1.228    by (induct n) (simp_all add: less_eq_nat.simps(2))
   1.229  
   1.230 -lemma not_less0 [iff]: "\<not> n < (0::nat)"
   1.231 +lemma not_less0 [iff]: "\<not> n < 0" for n :: nat
   1.232    by (simp add: less_eq_Suc_le)
   1.233  
   1.234 -lemma less_nat_zero_code [code]: "n < (0::nat) \<longleftrightarrow> False"
   1.235 +lemma less_nat_zero_code [code]: "n < 0 \<longleftrightarrow> False" for n :: nat
   1.236    by simp
   1.237  
   1.238  lemma Suc_less_eq [iff]: "Suc m < Suc n \<longleftrightarrow> m < n"
   1.239 @@ -419,8 +423,7 @@
   1.240    by (cases m) auto
   1.241  
   1.242  lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n"
   1.243 -  by (induct m arbitrary: n)
   1.244 -    (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   1.245 +  by (induct m arbitrary: n) (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   1.246  
   1.247  lemma Suc_leD: "Suc m \<le> n \<Longrightarrow> m \<le> n"
   1.248    by (cases n) (auto intro: le_SucI)
   1.249 @@ -433,33 +436,32 @@
   1.250  
   1.251  instance
   1.252  proof
   1.253 -  fix n m :: nat
   1.254 +  fix n m q :: nat
   1.255    show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
   1.256    proof (induct n arbitrary: m)
   1.257 -    case 0 then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   1.258 +    case 0
   1.259 +    then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   1.260    next
   1.261 -    case (Suc n) then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   1.262 +    case (Suc n)
   1.263 +    then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   1.264    qed
   1.265 -next
   1.266 -  fix n :: nat show "n \<le> n" by (induct n) simp_all
   1.267 -next
   1.268 -  fix n m :: nat assume "n \<le> m" and "m \<le> n"
   1.269 -  then show "n = m"
   1.270 -    by (induct n arbitrary: m)
   1.271 +  show "n \<le> n" by (induct n) simp_all
   1.272 +  then show "n = m" if "n \<le> m" and "m \<le> n"
   1.273 +    using that by (induct n arbitrary: m)
   1.274        (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   1.275 -next
   1.276 -  fix n m q :: nat assume "n \<le> m" and "m \<le> q"
   1.277 -  then show "n \<le> q"
   1.278 +  show "n \<le> q" if "n \<le> m" and "m \<le> q"
   1.279 +    using that
   1.280    proof (induct n arbitrary: m q)
   1.281 -    case 0 show ?case by simp
   1.282 +    case 0
   1.283 +    show ?case by simp
   1.284    next
   1.285 -    case (Suc n) then show ?case
   1.286 +    case (Suc n)
   1.287 +    then show ?case
   1.288        by (simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
   1.289          simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
   1.290          simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits)
   1.291    qed
   1.292 -next
   1.293 -  fix n m :: nat show "n \<le> m \<or> m \<le> n"
   1.294 +  show "n \<le> m \<or> m \<le> n"
   1.295      by (induct n arbitrary: m)
   1.296        (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   1.297  qed
   1.298 @@ -469,11 +471,9 @@
   1.299  instantiation nat :: order_bot
   1.300  begin
   1.301  
   1.302 -definition bot_nat :: nat where
   1.303 -  "bot_nat = 0"
   1.304 -
   1.305 -instance proof
   1.306 -qed (simp add: bot_nat_def)
   1.307 +definition bot_nat :: nat where "bot_nat = 0"
   1.308 +
   1.309 +instance by standard (simp add: bot_nat_def)
   1.310  
   1.311  end
   1.312  
   1.313 @@ -492,94 +492,104 @@
   1.314  
   1.315  subsubsection \<open>Elimination properties\<close>
   1.316  
   1.317 -lemma less_not_refl: "~ n < (n::nat)"
   1.318 +lemma less_not_refl: "\<not> n < n" for n :: nat
   1.319    by (rule order_less_irrefl)
   1.320  
   1.321 -lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
   1.322 +lemma less_not_refl2: "n < m \<Longrightarrow> m \<noteq> n" for m n :: nat
   1.323    by (rule not_sym) (rule less_imp_neq)
   1.324  
   1.325 -lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
   1.326 +lemma less_not_refl3: "s < t \<Longrightarrow> s \<noteq> t" for s t :: nat
   1.327    by (rule less_imp_neq)
   1.328  
   1.329 -lemma less_irrefl_nat: "(n::nat) < n ==> R"
   1.330 +lemma less_irrefl_nat: "n < n \<Longrightarrow> R" for n :: nat
   1.331    by (rule notE, rule less_not_refl)
   1.332  
   1.333 -lemma less_zeroE: "(n::nat) < 0 ==> R"
   1.334 +lemma less_zeroE: "n < 0 \<Longrightarrow> R" for n :: nat
   1.335    by (rule notE) (rule not_less0)
   1.336  
   1.337 -lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
   1.338 +lemma less_Suc_eq: "m < Suc n \<longleftrightarrow> m < n \<or> m = n"
   1.339    unfolding less_Suc_eq_le le_less ..
   1.340  
   1.341  lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   1.342    by (simp add: less_Suc_eq)
   1.343  
   1.344 -lemma less_one [iff]: "(n < (1::nat)) = (n = 0)"
   1.345 +lemma less_one [iff]: "n < 1 \<longleftrightarrow> n = 0" for n :: nat
   1.346    unfolding One_nat_def by (rule less_Suc0)
   1.347  
   1.348 -lemma Suc_mono: "m < n ==> Suc m < Suc n"
   1.349 +lemma Suc_mono: "m < n \<Longrightarrow> Suc m < Suc n"
   1.350    by simp
   1.351  
   1.352  text \<open>"Less than" is antisymmetric, sort of\<close>
   1.353  lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
   1.354    unfolding not_less less_Suc_eq_le by (rule antisym)
   1.355  
   1.356 -lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
   1.357 +lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat
   1.358    by (rule linorder_neq_iff)
   1.359  
   1.360 -lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m"
   1.361 -  and eqCase: "m = n ==> P n m" and lessCase: "n<m ==> P n m"
   1.362 +lemma nat_less_cases:
   1.363 +  fixes m n :: nat
   1.364 +  assumes major: "m < n \<Longrightarrow> P n m"
   1.365 +    and eq: "m = n \<Longrightarrow> P n m"
   1.366 +    and less: "n < m \<Longrightarrow> P n m"
   1.367    shows "P n m"
   1.368    apply (rule less_linear [THEN disjE])
   1.369    apply (erule_tac [2] disjE)
   1.370 -  apply (erule lessCase)
   1.371 -  apply (erule sym [THEN eqCase])
   1.372 +  apply (erule less)
   1.373 +  apply (erule sym [THEN eq])
   1.374    apply (erule major)
   1.375    done
   1.376  
   1.377  
   1.378  subsubsection \<open>Inductive (?) properties\<close>
   1.379  
   1.380 -lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
   1.381 +lemma Suc_lessI: "m < n \<Longrightarrow> Suc m \<noteq> n \<Longrightarrow> Suc m < n"
   1.382    unfolding less_eq_Suc_le [of m] le_less by simp
   1.383  
   1.384  lemma lessE:
   1.385    assumes major: "i < k"
   1.386 -  and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P"
   1.387 +    and 1: "k = Suc i \<Longrightarrow> P"
   1.388 +    and 2: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
   1.389    shows P
   1.390  proof -
   1.391    from major have "\<exists>j. i \<le> j \<and> k = Suc j"
   1.392      unfolding less_eq_Suc_le by (induct k) simp_all
   1.393    then have "(\<exists>j. i < j \<and> k = Suc j) \<or> k = Suc i"
   1.394 -    by (clarsimp simp add: less_le)
   1.395 -  with p1 p2 show P by auto
   1.396 +    by (auto simp add: less_le)
   1.397 +  with 1 2 show P by auto
   1.398  qed
   1.399  
   1.400 -lemma less_SucE: assumes major: "m < Suc n"
   1.401 -  and less: "m < n ==> P" and eq: "m = n ==> P" shows P
   1.402 +lemma less_SucE:
   1.403 +  assumes major: "m < Suc n"
   1.404 +    and less: "m < n \<Longrightarrow> P"
   1.405 +    and eq: "m = n \<Longrightarrow> P"
   1.406 +  shows P
   1.407    apply (rule major [THEN lessE])
   1.408    apply (rule eq, blast)
   1.409    apply (rule less, blast)
   1.410    done
   1.411  
   1.412 -lemma Suc_lessE: assumes major: "Suc i < k"
   1.413 -  and minor: "!!j. i < j ==> k = Suc j ==> P" shows P
   1.414 +lemma Suc_lessE:
   1.415 +  assumes major: "Suc i < k"
   1.416 +    and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
   1.417 +  shows P
   1.418    apply (rule major [THEN lessE])
   1.419    apply (erule lessI [THEN minor])
   1.420    apply (erule Suc_lessD [THEN minor], assumption)
   1.421    done
   1.422  
   1.423 -lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
   1.424 +lemma Suc_less_SucD: "Suc m < Suc n \<Longrightarrow> m < n"
   1.425    by simp
   1.426  
   1.427  lemma less_trans_Suc:
   1.428 -  assumes le: "i < j" shows "j < k ==> Suc i < k"
   1.429 +  assumes le: "i < j"
   1.430 +  shows "j < k \<Longrightarrow> Suc i < k"
   1.431    apply (induct k, simp_all)
   1.432 -  apply (insert le)
   1.433 +  using le
   1.434    apply (simp add: less_Suc_eq)
   1.435    apply (blast dest: Suc_lessD)
   1.436    done
   1.437  
   1.438 -text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{term "n = m | n < m"}\<close>
   1.439 +text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{prop "n = m \<or> n < m"}\<close>
   1.440  lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m"
   1.441    unfolding not_less less_Suc_eq_le ..
   1.442  
   1.443 @@ -588,138 +598,138 @@
   1.444  
   1.445  text \<open>Properties of "less than or equal"\<close>
   1.446  
   1.447 -lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
   1.448 +lemma le_imp_less_Suc: "m \<le> n \<Longrightarrow> m < Suc n"
   1.449    unfolding less_Suc_eq_le .
   1.450  
   1.451 -lemma Suc_n_not_le_n: "~ Suc n \<le> n"
   1.452 +lemma Suc_n_not_le_n: "\<not> Suc n \<le> n"
   1.453    unfolding not_le less_Suc_eq_le ..
   1.454  
   1.455  lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
   1.456    by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq)
   1.457  
   1.458 -lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
   1.459 +lemma le_SucE: "m \<le> Suc n \<Longrightarrow> (m \<le> n \<Longrightarrow> R) \<Longrightarrow> (m = Suc n \<Longrightarrow> R) \<Longrightarrow> R"
   1.460    by (drule le_Suc_eq [THEN iffD1], iprover+)
   1.461  
   1.462 -lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   1.463 +lemma Suc_leI: "m < n \<Longrightarrow> Suc(m) \<le> n"
   1.464    unfolding Suc_le_eq .
   1.465  
   1.466  text \<open>Stronger version of \<open>Suc_leD\<close>\<close>
   1.467 -lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
   1.468 +lemma Suc_le_lessD: "Suc m \<le> n \<Longrightarrow> m < n"
   1.469    unfolding Suc_le_eq .
   1.470  
   1.471 -lemma less_imp_le_nat: "m < n ==> m \<le> (n::nat)"
   1.472 +lemma less_imp_le_nat: "m < n \<Longrightarrow> m \<le> n" for m n :: nat
   1.473    unfolding less_eq_Suc_le by (rule Suc_leD)
   1.474  
   1.475  text \<open>For instance, \<open>(Suc m < Suc n) = (Suc m \<le> n) = (m < n)\<close>\<close>
   1.476  lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
   1.477  
   1.478  
   1.479 -text \<open>Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"}\<close>
   1.480 -
   1.481 -lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
   1.482 +text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close>
   1.483 +
   1.484 +lemma less_or_eq_imp_le: "m < n \<or> m = n \<Longrightarrow> m \<le> n" for m n :: nat
   1.485    unfolding le_less .
   1.486  
   1.487 -lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
   1.488 +lemma le_eq_less_or_eq: "m \<le> n \<longleftrightarrow> m < n \<or> m = n" for m n :: nat
   1.489    by (rule le_less)
   1.490  
   1.491  text \<open>Useful with \<open>blast\<close>.\<close>
   1.492 -lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
   1.493 +lemma eq_imp_le: "m = n \<Longrightarrow> m \<le> n" for m n :: nat
   1.494    by auto
   1.495  
   1.496 -lemma le_refl: "n \<le> (n::nat)"
   1.497 +lemma le_refl: "n \<le> n" for n :: nat
   1.498    by simp
   1.499  
   1.500 -lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
   1.501 +lemma le_trans: "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" for i j k :: nat
   1.502    by (rule order_trans)
   1.503  
   1.504 -lemma le_antisym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
   1.505 +lemma le_antisym: "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n" for m n :: nat
   1.506    by (rule antisym)
   1.507  
   1.508 -lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
   1.509 +lemma nat_less_le: "m < n \<longleftrightarrow> m \<le> n \<and> m \<noteq> n" for m n :: nat
   1.510    by (rule less_le)
   1.511  
   1.512 -lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
   1.513 +lemma le_neq_implies_less: "m \<le> n \<Longrightarrow> m \<noteq> n \<Longrightarrow> m < n" for m n :: nat
   1.514    unfolding less_le ..
   1.515  
   1.516 -lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
   1.517 +lemma nat_le_linear: "m \<le> n | n \<le> m" for m n :: nat
   1.518    by (rule linear)
   1.519  
   1.520  lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
   1.521  
   1.522 -lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
   1.523 +lemma le_less_Suc_eq: "m \<le> n \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m"
   1.524    unfolding less_Suc_eq_le by auto
   1.525  
   1.526 -lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   1.527 +lemma not_less_less_Suc_eq: "\<not> n < m \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m"
   1.528    unfolding not_less by (rule le_less_Suc_eq)
   1.529  
   1.530  lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
   1.531  
   1.532 -lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
   1.533 -by (cases n) simp_all
   1.534 -
   1.535 -lemma gr0_implies_Suc: "n > 0 ==> \<exists>m. n = Suc m"
   1.536 -by (cases n) simp_all
   1.537 -
   1.538 -lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0"
   1.539 -by (cases n) simp_all
   1.540 -
   1.541 -lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
   1.542 -by (cases n) simp_all
   1.543 +lemma not0_implies_Suc: "n \<noteq> 0 \<Longrightarrow> \<exists>m. n = Suc m"
   1.544 +  by (cases n) simp_all
   1.545 +
   1.546 +lemma gr0_implies_Suc: "n > 0 \<Longrightarrow> \<exists>m. n = Suc m"
   1.547 +  by (cases n) simp_all
   1.548 +
   1.549 +lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0" for m n :: nat
   1.550 +  by (cases n) simp_all
   1.551 +
   1.552 +lemma neq0_conv[iff]: "n \<noteq> 0 \<longleftrightarrow> 0 < n" for n :: nat
   1.553 +  by (cases n) simp_all
   1.554  
   1.555  text \<open>This theorem is useful with \<open>blast\<close>\<close>
   1.556 -lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   1.557 -by (rule neq0_conv[THEN iffD1], iprover)
   1.558 -
   1.559 -lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   1.560 -by (fast intro: not0_implies_Suc)
   1.561 -
   1.562 -lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   1.563 -using neq0_conv by blast
   1.564 -
   1.565 -lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   1.566 -by (induct m') simp_all
   1.567 +lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n" for n :: nat
   1.568 +  by (rule neq0_conv[THEN iffD1], iprover)
   1.569 +
   1.570 +lemma gr0_conv_Suc: "0 < n \<longleftrightarrow> (\<exists>m. n = Suc m)"
   1.571 +  by (fast intro: not0_implies_Suc)
   1.572 +
   1.573 +lemma not_gr0 [iff]: "\<not> 0 < n \<longleftrightarrow> n = 0" for n :: nat
   1.574 +  using neq0_conv by blast
   1.575 +
   1.576 +lemma Suc_le_D: "Suc n \<le> m' \<Longrightarrow> \<exists>m. m' = Suc m"
   1.577 +  by (induct m') simp_all
   1.578  
   1.579  text \<open>Useful in certain inductive arguments\<close>
   1.580 -lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
   1.581 -by (cases m) simp_all
   1.582 +lemma less_Suc_eq_0_disj: "m < Suc n \<longleftrightarrow> m = 0 \<or> (\<exists>j. m = Suc j \<and> j < n)"
   1.583 +  by (cases m) simp_all
   1.584  
   1.585  
   1.586  subsubsection \<open>Monotonicity of Addition\<close>
   1.587  
   1.588 -lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
   1.589 -by (simp add: diff_Suc split: nat.split)
   1.590 -
   1.591 -lemma Suc_diff_1 [simp]: "0 < n ==> Suc (n - 1) = n"
   1.592 -unfolding One_nat_def by (rule Suc_pred)
   1.593 -
   1.594 -lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
   1.595 -by (induct k) simp_all
   1.596 -
   1.597 -lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
   1.598 -by (induct k) simp_all
   1.599 -
   1.600 -lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)"
   1.601 -by(auto dest:gr0_implies_Suc)
   1.602 +lemma Suc_pred [simp]: "n > 0 \<Longrightarrow> Suc (n - Suc 0) = n"
   1.603 +  by (simp add: diff_Suc split: nat.split)
   1.604 +
   1.605 +lemma Suc_diff_1 [simp]: "0 < n \<Longrightarrow> Suc (n - 1) = n"
   1.606 +  unfolding One_nat_def by (rule Suc_pred)
   1.607 +
   1.608 +lemma nat_add_left_cancel_le [simp]: "k + m \<le> k + n \<longleftrightarrow> m \<le> n" for k m n :: nat
   1.609 +  by (induct k) simp_all
   1.610 +
   1.611 +lemma nat_add_left_cancel_less [simp]: "k + m < k + n \<longleftrightarrow> m < n" for k m n :: nat
   1.612 +  by (induct k) simp_all
   1.613 +
   1.614 +lemma add_gr_0 [iff]: "m + n > 0 \<longleftrightarrow> m > 0 \<or> n > 0" for m n :: nat
   1.615 +  by (auto dest: gr0_implies_Suc)
   1.616  
   1.617  text \<open>strict, in 1st argument\<close>
   1.618 -lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   1.619 -by (induct k) simp_all
   1.620 +lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k" for i j k :: nat
   1.621 +  by (induct k) simp_all
   1.622  
   1.623  text \<open>strict, in both arguments\<close>
   1.624 -lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   1.625 +lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l" for i j k l :: nat
   1.626    apply (rule add_less_mono1 [THEN less_trans], assumption+)
   1.627    apply (induct j, simp_all)
   1.628    done
   1.629  
   1.630  text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close>
   1.631 -lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
   1.632 +lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)"
   1.633    apply (induct n)
   1.634    apply (simp_all add: order_le_less)
   1.635    apply (blast elim!: less_SucE
   1.636                 intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
   1.637    done
   1.638  
   1.639 -lemma le_Suc_ex: "(k::nat) \<le> l \<Longrightarrow> (\<exists>n. l = k + n)"
   1.640 +lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)" for k l :: nat
   1.641    by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
   1.642  
   1.643  text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
   1.644 @@ -727,173 +737,162 @@
   1.645    fixes i j :: nat
   1.646    assumes "i < j" and "0 < k"
   1.647    shows "k * i < k * j"
   1.648 -using \<open>0 < k\<close> proof (induct k)
   1.649 -  case 0 then show ?case by simp
   1.650 +  using \<open>0 < k\<close>
   1.651 +proof (induct k)
   1.652 +  case 0
   1.653 +  then show ?case by simp
   1.654  next
   1.655 -  case (Suc k) with \<open>i < j\<close> show ?case
   1.656 +  case (Suc k)
   1.657 +  with \<open>i < j\<close> show ?case
   1.658      by (cases k) (simp_all add: add_less_mono)
   1.659  qed
   1.660  
   1.661  text \<open>Addition is the inverse of subtraction:
   1.662    if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close>
   1.663 -lemma add_diff_inverse_nat: "~  m < n ==> n + (m - n) = (m::nat)"
   1.664 -by (induct m n rule: diff_induct) simp_all
   1.665 -
   1.666 -lemma nat_le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
   1.667 -using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)
   1.668 +lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m - n) = m" for m n :: nat
   1.669 +  by (induct m n rule: diff_induct) simp_all
   1.670 +
   1.671 +lemma nat_le_iff_add: "m \<le> n \<longleftrightarrow> (\<exists>k. n = m + k)" for m n :: nat
   1.672 +  using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)
   1.673  
   1.674  text\<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>\<close>
   1.675  
   1.676  instance nat :: linordered_semidom
   1.677  proof
   1.678 +  fix m n q :: nat
   1.679    show "0 < (1::nat)" by simp
   1.680 -  show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
   1.681 -  show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
   1.682 -  show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
   1.683 -  show "\<And>m n :: nat. n \<le> m ==> (m - n) + n = (m::nat)"
   1.684 +  show "m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
   1.685 +  show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
   1.686 +  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
   1.687 +  show "n \<le> m \<Longrightarrow> (m - n) + n = m"
   1.688      by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
   1.689  qed
   1.690  
   1.691  instance nat :: dioid
   1.692 -  proof qed (rule nat_le_iff_add)
   1.693 +  by standard (rule nat_le_iff_add)
   1.694  declare le0[simp del] -- \<open>This is now @{thm zero_le}\<close>
   1.695  declare le_0_eq[simp del] -- \<open>This is now @{thm le_zero_eq}\<close>
   1.696  declare not_less0[simp del] -- \<open>This is now @{thm not_less_zero}\<close>
   1.697  declare not_gr0[simp del] -- \<open>This is now @{thm not_gr_zero}\<close>
   1.698  
   1.699 -instance nat :: ordered_cancel_comm_monoid_add
   1.700 -  proof qed
   1.701 -
   1.702 -instance nat :: ordered_cancel_comm_monoid_diff
   1.703 -  proof qed
   1.704 +instance nat :: ordered_cancel_comm_monoid_add ..
   1.705 +instance nat :: ordered_cancel_comm_monoid_diff ..
   1.706 +
   1.707  
   1.708  subsubsection \<open>@{term min} and @{term max}\<close>
   1.709  
   1.710  lemma mono_Suc: "mono Suc"
   1.711 -by (rule monoI) simp
   1.712 -
   1.713 -lemma min_0L [simp]: "min 0 n = (0::nat)"
   1.714 -by (rule min_absorb1) simp
   1.715 -
   1.716 -lemma min_0R [simp]: "min n 0 = (0::nat)"
   1.717 -by (rule min_absorb2) simp
   1.718 +  by (rule monoI) simp
   1.719 +
   1.720 +lemma min_0L [simp]: "min 0 n = 0" for n :: nat
   1.721 +  by (rule min_absorb1) simp
   1.722 +
   1.723 +lemma min_0R [simp]: "min n 0 = 0" for n :: nat
   1.724 +  by (rule min_absorb2) simp
   1.725  
   1.726  lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
   1.727 -by (simp add: mono_Suc min_of_mono)
   1.728 -
   1.729 -lemma min_Suc1:
   1.730 -   "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
   1.731 -by (simp split: nat.split)
   1.732 -
   1.733 -lemma min_Suc2:
   1.734 -   "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
   1.735 -by (simp split: nat.split)
   1.736 -
   1.737 -lemma max_0L [simp]: "max 0 n = (n::nat)"
   1.738 -by (rule max_absorb2) simp
   1.739 -
   1.740 -lemma max_0R [simp]: "max n 0 = (n::nat)"
   1.741 -by (rule max_absorb1) simp
   1.742 -
   1.743 -lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
   1.744 -by (simp add: mono_Suc max_of_mono)
   1.745 -
   1.746 -lemma max_Suc1:
   1.747 -   "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
   1.748 -by (simp split: nat.split)
   1.749 -
   1.750 -lemma max_Suc2:
   1.751 -   "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
   1.752 -by (simp split: nat.split)
   1.753 -
   1.754 -lemma nat_mult_min_left:
   1.755 -  fixes m n q :: nat
   1.756 -  shows "min m n * q = min (m * q) (n * q)"
   1.757 -  by (simp add: min_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   1.758 -
   1.759 -lemma nat_mult_min_right:
   1.760 -  fixes m n q :: nat
   1.761 -  shows "m * min n q = min (m * n) (m * q)"
   1.762 -  by (simp add: min_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   1.763 -
   1.764 -lemma nat_add_max_left:
   1.765 -  fixes m n q :: nat
   1.766 -  shows "max m n + q = max (m + q) (n + q)"
   1.767 +  by (simp add: mono_Suc min_of_mono)
   1.768 +
   1.769 +lemma min_Suc1: "min (Suc n) m = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min n m'))"
   1.770 +  by (simp split: nat.split)
   1.771 +
   1.772 +lemma min_Suc2: "min m (Suc n) = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min m' n))"
   1.773 +  by (simp split: nat.split)
   1.774 +
   1.775 +lemma max_0L [simp]: "max 0 n = n" for n :: nat
   1.776 +  by (rule max_absorb2) simp
   1.777 +
   1.778 +lemma max_0R [simp]: "max n 0 = n" for n :: nat
   1.779 +  by (rule max_absorb1) simp
   1.780 +
   1.781 +lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)"
   1.782 +  by (simp add: mono_Suc max_of_mono)
   1.783 +
   1.784 +lemma max_Suc1: "max (Suc n) m = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max n m'))"
   1.785 +  by (simp split: nat.split)
   1.786 +
   1.787 +lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
   1.788 +  by (simp split: nat.split)
   1.789 +
   1.790 +lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)" for m n q :: nat
   1.791 +  by (simp add: min_def not_le)
   1.792 +    (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   1.793 +
   1.794 +lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)" for m n q :: nat
   1.795 +  by (simp add: min_def not_le)
   1.796 +    (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   1.797 +
   1.798 +lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)" for m n q :: nat
   1.799    by (simp add: max_def)
   1.800  
   1.801 -lemma nat_add_max_right:
   1.802 -  fixes m n q :: nat
   1.803 -  shows "m + max n q = max (m + n) (m + q)"
   1.804 +lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)" for m n q :: nat
   1.805    by (simp add: max_def)
   1.806  
   1.807 -lemma nat_mult_max_left:
   1.808 -  fixes m n q :: nat
   1.809 -  shows "max m n * q = max (m * q) (n * q)"
   1.810 -  by (simp add: max_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   1.811 -
   1.812 -lemma nat_mult_max_right:
   1.813 -  fixes m n q :: nat
   1.814 -  shows "m * max n q = max (m * n) (m * q)"
   1.815 -  by (simp add: max_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   1.816 +lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)" for m n q :: nat
   1.817 +  by (simp add: max_def not_le)
   1.818 +    (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   1.819 +
   1.820 +lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)" for m n q :: nat
   1.821 +  by (simp add: max_def not_le)
   1.822 +    (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   1.823  
   1.824  
   1.825  subsubsection \<open>Additional theorems about @{term "op \<le>"}\<close>
   1.826  
   1.827  text \<open>Complete induction, aka course-of-values induction\<close>
   1.828  
   1.829 -instance nat :: wellorder proof
   1.830 +instance nat :: wellorder
   1.831 +proof
   1.832    fix P and n :: nat
   1.833 -  assume step: "\<And>n::nat. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n"
   1.834 +  assume step: "(\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n" for n :: nat
   1.835    have "\<And>q. q \<le> n \<Longrightarrow> P q"
   1.836    proof (induct n)
   1.837      case (0 n)
   1.838      have "P 0" by (rule step) auto
   1.839 -    thus ?case using 0 by auto
   1.840 +    then show ?case using 0 by auto
   1.841    next
   1.842      case (Suc m n)
   1.843      then have "n \<le> m \<or> n = Suc m" by (simp add: le_Suc_eq)
   1.844 -    thus ?case
   1.845 +    then show ?case
   1.846      proof
   1.847 -      assume "n \<le> m" thus "P n" by (rule Suc(1))
   1.848 +      assume "n \<le> m"
   1.849 +      then show "P n" by (rule Suc(1))
   1.850      next
   1.851        assume n: "n = Suc m"
   1.852 -      show "P n"
   1.853 -        by (rule step) (rule Suc(1), simp add: n le_simps)
   1.854 +      show "P n" by (rule step) (rule Suc(1), simp add: n le_simps)
   1.855      qed
   1.856    qed
   1.857    then show "P n" by auto
   1.858  qed
   1.859  
   1.860  
   1.861 -lemma Least_eq_0[simp]: "P(0::nat) \<Longrightarrow> Least P = 0"
   1.862 -by (rule Least_equality[OF _ le0])
   1.863 -
   1.864 -lemma Least_Suc:
   1.865 -     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   1.866 +lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0" for P :: "nat \<Rightarrow> bool"
   1.867 +  by (rule Least_equality[OF _ le0])
   1.868 +
   1.869 +lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
   1.870    apply (cases n, auto)
   1.871    apply (frule LeastI)
   1.872 -  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
   1.873 +  apply (drule_tac P = "\<lambda>x. P (Suc x) " in LeastI)
   1.874    apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
   1.875    apply (erule_tac [2] Least_le)
   1.876    apply (cases "LEAST x. P x", auto)
   1.877 -  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   1.878 +  apply (drule_tac P = "\<lambda>x. P (Suc x) " in Least_le)
   1.879    apply (blast intro: order_antisym)
   1.880    done
   1.881  
   1.882 -lemma Least_Suc2:
   1.883 -   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   1.884 +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.885    apply (erule (1) Least_Suc [THEN ssubst])
   1.886    apply simp
   1.887    done
   1.888  
   1.889 -lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
   1.890 +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.891    apply (cases n)
   1.892     apply blast
   1.893 -  apply (rule_tac x="LEAST k. P(k)" in exI)
   1.894 +  apply (rule_tac x="LEAST k. P k" in exI)
   1.895    apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
   1.896    done
   1.897  
   1.898 -lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
   1.899 +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.900    unfolding One_nat_def
   1.901    apply (cases n)
   1.902     apply blast
   1.903 @@ -907,14 +906,16 @@
   1.904    done
   1.905  
   1.906  lemma nat_less_induct:
   1.907 -  assumes "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
   1.908 +  fixes P :: "nat \<Rightarrow> bool"
   1.909 +  assumes "\<And>n. \<forall>m. m < n \<longrightarrow> P m \<Longrightarrow> P n"
   1.910 +  shows "P n"
   1.911    using assms less_induct by blast
   1.912  
   1.913  lemma measure_induct_rule [case_names less]:
   1.914    fixes f :: "'a \<Rightarrow> nat"
   1.915    assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
   1.916    shows "P a"
   1.917 -by (induct m\<equiv>"f a" arbitrary: a rule: less_induct) (auto intro: step)
   1.918 +  by (induct m \<equiv> "f a" arbitrary: a rule: less_induct) (auto intro: step)
   1.919  
   1.920  text \<open>old style induction rules:\<close>
   1.921  lemma measure_induct:
   1.922 @@ -923,18 +924,19 @@
   1.923    by (rule measure_induct_rule [of f P a]) iprover
   1.924  
   1.925  lemma full_nat_induct:
   1.926 -  assumes step: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
   1.927 +  assumes step: "\<And>n. (\<forall>m. Suc m \<le> n \<longrightarrow> P m) \<Longrightarrow> P n"
   1.928    shows "P n"
   1.929    by (rule less_induct) (auto intro: step simp:le_simps)
   1.930  
   1.931 -text\<open>An induction rule for estabilishing binary relations\<close>
   1.932 +text\<open>An induction rule for establishing binary relations\<close>
   1.933  lemma less_Suc_induct [consumes 1]:
   1.934 -  assumes less:  "i < j"
   1.935 -     and  step:  "!!i. P i (Suc i)"
   1.936 -     and  trans: "!!i j k. i < j ==> j < k ==>  P i j ==> P j k ==> P i k"
   1.937 +  assumes less: "i < j"
   1.938 +    and step: "\<And>i. P i (Suc i)"
   1.939 +    and trans: "\<And>i j k. i < j \<Longrightarrow> j < k \<Longrightarrow> P i j \<Longrightarrow> P j k \<Longrightarrow> P i k"
   1.940    shows "P i j"
   1.941  proof -
   1.942 -  from less obtain k where j: "j = Suc (i + k)" by (auto dest: less_imp_Suc_add)
   1.943 +  from less obtain k where j: "j = Suc (i + k)"
   1.944 +    by (auto dest: less_imp_Suc_add)
   1.945    have "P i (Suc (i + k))"
   1.946    proof (induct k)
   1.947      case 0
   1.948 @@ -942,11 +944,11 @@
   1.949    next
   1.950      case (Suc k)
   1.951      have "0 + i < Suc k + i" by (rule add_less_mono1) simp
   1.952 -    hence "i < Suc (i + k)" by (simp add: add.commute)
   1.953 +    then have "i < Suc (i + k)" by (simp add: add.commute)
   1.954      from trans[OF this lessI Suc step]
   1.955      show ?case by simp
   1.956    qed
   1.957 -  thus "P i j" by (simp add: j)
   1.958 +  then show "P i j" by (simp add: j)
   1.959  qed
   1.960  
   1.961  text \<open>The method of infinite descent, frequently used in number theory.
   1.962 @@ -959,13 +961,18 @@
   1.963  \end{itemize}\<close>
   1.964  
   1.965  text\<open>A compact version without explicit base case:\<close>
   1.966 -lemma infinite_descent:
   1.967 -  "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
   1.968 -by (induct n rule: less_induct) auto
   1.969 +lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool"
   1.970 +  by (induct n rule: less_induct) auto
   1.971  
   1.972  lemma infinite_descent0[case_names 0 smaller]:
   1.973 -  "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
   1.974 -by (rule infinite_descent) (case_tac "n>0", auto)
   1.975 +  fixes P :: "nat \<Rightarrow> bool"
   1.976 +  assumes "P 0" and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m. m < n \<and> \<not> P m)"
   1.977 +  shows "P n"
   1.978 +  apply (rule infinite_descent)
   1.979 +  using assms
   1.980 +  apply (case_tac "n > 0")
   1.981 +  apply auto
   1.982 +  done
   1.983  
   1.984  text \<open>
   1.985  Infinite descent using a mapping to $\mathbb{N}$:
   1.986 @@ -977,20 +984,21 @@
   1.987  NB: the proof also shows how to use the previous lemma.\<close>
   1.988  
   1.989  corollary infinite_descent0_measure [case_names 0 smaller]:
   1.990 -  assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
   1.991 -    and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
   1.992 +  fixes V :: "'a \<Rightarrow> nat"
   1.993 +  assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x"
   1.994 +    and 2: "\<And>x. V x > 0 \<Longrightarrow> \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y"
   1.995    shows "P x"
   1.996  proof -
   1.997    obtain n where "n = V x" by auto
   1.998    moreover have "\<And>x. V x = n \<Longrightarrow> P x"
   1.999    proof (induct n rule: infinite_descent0)
  1.1000 -    case 0 \<comment> "i.e. $V(x) = 0$"
  1.1001 -    with A0 show "P x" by auto
  1.1002 -  next \<comment> "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
  1.1003 +    case 0
  1.1004 +    with 1 show "P x" by auto
  1.1005 +  next
  1.1006      case (smaller n)
  1.1007 -    then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
  1.1008 -    with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
  1.1009 -    with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
  1.1010 +    then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
  1.1011 +    with 2 obtain y where "V y < V x \<and> \<not> P y" by auto
  1.1012 +    with * obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
  1.1013      then show ?case by auto
  1.1014    qed
  1.1015    ultimately show "P x" by auto
  1.1016 @@ -998,96 +1006,97 @@
  1.1017  
  1.1018  text\<open>Again, without explicit base case:\<close>
  1.1019  lemma infinite_descent_measure:
  1.1020 -assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"
  1.1021 +  fixes V :: "'a \<Rightarrow> nat"
  1.1022 +  assumes "\<And>x. \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y"
  1.1023 +  shows "P x"
  1.1024  proof -
  1.1025    from assms obtain n where "n = V x" by auto
  1.1026 -  moreover have "!!x. V x = n \<Longrightarrow> P x"
  1.1027 +  moreover have "\<And>x. V x = n \<Longrightarrow> P x"
  1.1028    proof (induct n rule: infinite_descent, auto)
  1.1029 -    fix x assume "\<not> P x"
  1.1030 +    fix x
  1.1031 +    assume "\<not> P x"
  1.1032      with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto
  1.1033    qed
  1.1034    ultimately show "P x" by auto
  1.1035  qed
  1.1036  
  1.1037 -text \<open>A [clumsy] way of lifting \<open><\<close>
  1.1038 -  monotonicity to \<open>\<le>\<close> monotonicity\<close>
  1.1039 +text \<open>A [clumsy] way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close>
  1.1040  lemma less_mono_imp_le_mono:
  1.1041 -  "\<lbrakk> !!i j::nat. i < j \<Longrightarrow> f i < f j; i \<le> j \<rbrakk> \<Longrightarrow> f i \<le> ((f j)::nat)"
  1.1042 -by (simp add: order_le_less) (blast)
  1.1043 +  fixes f :: "nat \<Rightarrow> nat"
  1.1044 +    and i j :: nat
  1.1045 +  assumes "\<And>i j::nat. i < j \<Longrightarrow> f i < f j"
  1.1046 +    and "i \<le> j"
  1.1047 +  shows "f i \<le> f j"
  1.1048 +  using assms by (auto simp add: order_le_less)
  1.1049  
  1.1050  
  1.1051  text \<open>non-strict, in 1st argument\<close>
  1.1052 -lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)"
  1.1053 -by (rule add_right_mono)
  1.1054 +lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k" for i j k :: nat
  1.1055 +  by (rule add_right_mono)
  1.1056  
  1.1057  text \<open>non-strict, in both arguments\<close>
  1.1058 -lemma add_le_mono: "[| i \<le> j;  k \<le> l |] ==> i + k \<le> j + (l::nat)"
  1.1059 -by (rule add_mono)
  1.1060 -
  1.1061 -lemma le_add2: "n \<le> ((m + n)::nat)"
  1.1062 +lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l" for i j k l :: nat
  1.1063 +  by (rule add_mono)
  1.1064 +
  1.1065 +lemma le_add2: "n \<le> m + n" for m n :: nat
  1.1066    by simp
  1.1067  
  1.1068 -lemma le_add1: "n \<le> ((n + m)::nat)"
  1.1069 +lemma le_add1: "n \<le> n + m" for m n :: nat
  1.1070    by simp
  1.1071  
  1.1072  lemma less_add_Suc1: "i < Suc (i + m)"
  1.1073 -by (rule le_less_trans, rule le_add1, rule lessI)
  1.1074 +  by (rule le_less_trans, rule le_add1, rule lessI)
  1.1075  
  1.1076  lemma less_add_Suc2: "i < Suc (m + i)"
  1.1077 -by (rule le_less_trans, rule le_add2, rule lessI)
  1.1078 -
  1.1079 -lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
  1.1080 -by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
  1.1081 -
  1.1082 -lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
  1.1083 -by (rule le_trans, assumption, rule le_add1)
  1.1084 -
  1.1085 -lemma trans_le_add2: "(i::nat) \<le> j ==> i \<le> m + j"
  1.1086 -by (rule le_trans, assumption, rule le_add2)
  1.1087 -
  1.1088 -lemma trans_less_add1: "(i::nat) < j ==> i < j + m"
  1.1089 -by (rule less_le_trans, assumption, rule le_add1)
  1.1090 -
  1.1091 -lemma trans_less_add2: "(i::nat) < j ==> i < m + j"
  1.1092 -by (rule less_le_trans, assumption, rule le_add2)
  1.1093 -
  1.1094 -lemma add_lessD1: "i + j < (k::nat) ==> i < k"
  1.1095 -apply (rule le_less_trans [of _ "i+j"])
  1.1096 -apply (simp_all add: le_add1)
  1.1097 -done
  1.1098 -
  1.1099 -lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
  1.1100 -apply (rule notI)
  1.1101 -apply (drule add_lessD1)
  1.1102 -apply (erule less_irrefl [THEN notE])
  1.1103 -done
  1.1104 -
  1.1105 -lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
  1.1106 -by (simp add: add.commute)
  1.1107 -
  1.1108 -lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
  1.1109 -apply (rule order_trans [of _ "m+k"])
  1.1110 -apply (simp_all add: le_add1)
  1.1111 -done
  1.1112 -
  1.1113 -lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
  1.1114 -apply (simp add: add.commute)
  1.1115 -apply (erule add_leD1)
  1.1116 -done
  1.1117 -
  1.1118 -lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
  1.1119 -by (blast dest: add_leD1 add_leD2)
  1.1120 -
  1.1121 -text \<open>needs \<open>!!k\<close> for \<open>ac_simps\<close> to work\<close>
  1.1122 -lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
  1.1123 -by (force simp del: add_Suc_right
  1.1124 -    simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
  1.1125 +  by (rule le_less_trans, rule le_add2, rule lessI)
  1.1126 +
  1.1127 +lemma less_iff_Suc_add: "m < n \<longleftrightarrow> (\<exists>k. n = Suc (m + k))"
  1.1128 +  by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
  1.1129 +
  1.1130 +lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m" for i j m :: nat
  1.1131 +  by (rule le_trans, assumption, rule le_add1)
  1.1132 +
  1.1133 +lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j" for i j m :: nat
  1.1134 +  by (rule le_trans, assumption, rule le_add2)
  1.1135 +
  1.1136 +lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m" for i j m :: nat
  1.1137 +  by (rule less_le_trans, assumption, rule le_add1)
  1.1138 +
  1.1139 +lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j" for i j m :: nat
  1.1140 +  by (rule less_le_trans, assumption, rule le_add2)
  1.1141 +
  1.1142 +lemma add_lessD1: "i + j < k \<Longrightarrow> i < k" for i j k :: nat
  1.1143 +  by (rule le_less_trans [of _ "i+j"]) (simp_all add: le_add1)
  1.1144 +
  1.1145 +lemma not_add_less1 [iff]: "\<not> i + j < i" for i j :: nat
  1.1146 +  apply (rule notI)
  1.1147 +  apply (drule add_lessD1)
  1.1148 +  apply (erule less_irrefl [THEN notE])
  1.1149 +  done
  1.1150 +
  1.1151 +lemma not_add_less2 [iff]: "\<not> j + i < i" for i j :: nat
  1.1152 +  by (simp add: add.commute)
  1.1153 +
  1.1154 +lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n" for k m n :: nat
  1.1155 +  by (rule order_trans [of _ "m+k"]) (simp_all add: le_add1)
  1.1156 +
  1.1157 +lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n" for k m n :: nat
  1.1158 +  apply (simp add: add.commute)
  1.1159 +  apply (erule add_leD1)
  1.1160 +  done
  1.1161 +
  1.1162 +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.1163 +  by (blast dest: add_leD1 add_leD2)
  1.1164 +
  1.1165 +text \<open>needs \<open>\<And>k\<close> for \<open>ac_simps\<close> to work\<close>
  1.1166 +lemma less_add_eq_less: "\<And>k::nat. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n"
  1.1167 +  by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
  1.1168  
  1.1169  
  1.1170  subsubsection \<open>More results about difference\<close>
  1.1171  
  1.1172 -lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
  1.1173 -by (induct m n rule: diff_induct) simp_all
  1.1174 +lemma Suc_diff_le: "n \<le> m \<Longrightarrow> Suc m - n = Suc (m - n)"
  1.1175 +  by (induct m n rule: diff_induct) simp_all
  1.1176  
  1.1177  lemma diff_less_Suc: "m - n < Suc m"
  1.1178  apply (induct m n rule: diff_induct)
  1.1179 @@ -1095,80 +1104,72 @@
  1.1180  apply (simp_all add: less_Suc_eq)
  1.1181  done
  1.1182  
  1.1183 -lemma diff_le_self [simp]: "m - n \<le> (m::nat)"
  1.1184 -by (induct m n rule: diff_induct) (simp_all add: le_SucI)
  1.1185 -
  1.1186 -lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
  1.1187 -by (rule le_less_trans, rule diff_le_self)
  1.1188 -
  1.1189 -lemma diff_Suc_less [simp]: "0<n ==> n - Suc i < n"
  1.1190 -by (cases n) (auto simp add: le_simps)
  1.1191 -
  1.1192 -lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
  1.1193 -by (induct j k rule: diff_induct) simp_all
  1.1194 -
  1.1195 -lemma add_diff_assoc [simp]:
  1.1196 -  fixes i j k :: nat
  1.1197 -  shows "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k"
  1.1198 +lemma diff_le_self [simp]: "m - n \<le> m" for m n :: nat
  1.1199 +  by (induct m n rule: diff_induct) (simp_all add: le_SucI)
  1.1200 +
  1.1201 +lemma less_imp_diff_less: "j < k \<Longrightarrow> j - n < k" for j k n :: nat
  1.1202 +  by (rule le_less_trans, rule diff_le_self)
  1.1203 +
  1.1204 +lemma diff_Suc_less [simp]: "0 < n \<Longrightarrow> n - Suc i < n"
  1.1205 +  by (cases n) (auto simp add: le_simps)
  1.1206 +
  1.1207 +lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j) - k = i + (j - k)" for i j k :: nat
  1.1208 +  by (induct j k rule: diff_induct) simp_all
  1.1209 +
  1.1210 +lemma add_diff_assoc [simp]: "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k" for i j k :: nat
  1.1211    by (fact diff_add_assoc [symmetric])
  1.1212  
  1.1213 -lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
  1.1214 +lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i) - k = (j - k) + i" for i j k :: nat
  1.1215    by (simp add: ac_simps)
  1.1216  
  1.1217 -lemma add_diff_assoc2 [simp]:
  1.1218 -  fixes i j k :: nat
  1.1219 -  shows "k \<le> j \<Longrightarrow> j - k + i = j + i - k"
  1.1220 +lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j - k + i = j + i - k" for i j k :: nat
  1.1221    by (fact diff_add_assoc2 [symmetric])
  1.1222  
  1.1223 -lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
  1.1224 -by auto
  1.1225 -
  1.1226 -lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m \<le> n)"
  1.1227 -by (induct m n rule: diff_induct) simp_all
  1.1228 -
  1.1229 -lemma diff_is_0_eq' [simp]: "m \<le> n ==> (m::nat) - n = 0"
  1.1230 -by (rule iffD2, rule diff_is_0_eq)
  1.1231 -
  1.1232 -lemma zero_less_diff [simp]: "(0 < n - (m::nat)) = (m < n)"
  1.1233 -by (induct m n rule: diff_induct) simp_all
  1.1234 +lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j - i = k) = (j = k + i)" for i j k :: nat
  1.1235 +  by auto
  1.1236 +
  1.1237 +lemma diff_is_0_eq [simp]: "m - n = 0 \<longleftrightarrow> m \<le> n" for m n :: nat
  1.1238 +  by (induct m n rule: diff_induct) simp_all
  1.1239 +
  1.1240 +lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0" for m n :: nat
  1.1241 +  by (rule iffD2, rule diff_is_0_eq)
  1.1242 +
  1.1243 +lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n" for m n :: nat
  1.1244 +  by (induct m n rule: diff_induct) simp_all
  1.1245  
  1.1246  lemma less_imp_add_positive:
  1.1247    assumes "i < j"
  1.1248 -  shows "\<exists>k::nat. 0 < k & i + k = j"
  1.1249 +  shows "\<exists>k::nat. 0 < k \<and> i + k = j"
  1.1250  proof
  1.1251 -  from assms show "0 < j - i & i + (j - i) = j"
  1.1252 +  from assms show "0 < j - i \<and> i + (j - i) = j"
  1.1253      by (simp add: order_less_imp_le)
  1.1254  qed
  1.1255  
  1.1256  text \<open>a nice rewrite for bounded subtraction\<close>
  1.1257 -lemma nat_minus_add_max:
  1.1258 -  fixes n m :: nat
  1.1259 -  shows "n - m + m = max n m"
  1.1260 +lemma nat_minus_add_max: "n - m + m = max n m" for m n :: nat
  1.1261      by (simp add: max_def not_le order_less_imp_le)
  1.1262  
  1.1263 -lemma nat_diff_split:
  1.1264 -  fixes a b :: nat
  1.1265 -  shows "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)"
  1.1266 +lemma nat_diff_split: "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)"
  1.1267 +  for a b :: nat
  1.1268      \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
  1.1269    by (cases "a < b")
  1.1270      (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym])
  1.1271  
  1.1272 -lemma nat_diff_split_asm:
  1.1273 -  fixes a b :: nat
  1.1274 -  shows "P (a - b) \<longleftrightarrow> \<not> (a < b \<and> \<not> P 0 \<or> (\<exists>d. a = b + d \<and> \<not> P d))"
  1.1275 +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.1276 +  for a b :: nat
  1.1277      \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
  1.1278    by (auto split: nat_diff_split)
  1.1279  
  1.1280 -lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
  1.1281 +lemma Suc_pred': "0 < n \<Longrightarrow> n = Suc(n - 1)"
  1.1282    by simp
  1.1283  
  1.1284 -lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
  1.1285 +lemma add_eq_if: "m + n = (if m = 0 then n else Suc ((m - 1) + n))"
  1.1286    unfolding One_nat_def by (cases m) simp_all
  1.1287  
  1.1288 -lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
  1.1289 +lemma mult_eq_if: "m * n = (if m = 0 then 0 else n + ((m - 1) * n))" for m n :: nat
  1.1290    unfolding One_nat_def by (cases m) simp_all
  1.1291  
  1.1292 -lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - 1)"
  1.1293 +lemma Suc_diff_eq_diff_pred: "0 < n \<Longrightarrow> Suc m - n = m - (n - 1)"
  1.1294    unfolding One_nat_def by (cases n) simp_all
  1.1295  
  1.1296  lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
  1.1297 @@ -1180,65 +1181,65 @@
  1.1298  
  1.1299  subsubsection \<open>Monotonicity of multiplication\<close>
  1.1300  
  1.1301 -lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
  1.1302 -by (simp add: mult_right_mono)
  1.1303 -
  1.1304 -lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
  1.1305 -by (simp add: mult_left_mono)
  1.1306 +lemma mult_le_mono1: "i \<le> j \<Longrightarrow> i * k \<le> j * k" for i j k :: nat
  1.1307 +  by (simp add: mult_right_mono)
  1.1308 +
  1.1309 +lemma mult_le_mono2: "i \<le> j \<Longrightarrow> k * i \<le> k * j" for i j k :: nat
  1.1310 +  by (simp add: mult_left_mono)
  1.1311  
  1.1312  text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close>
  1.1313 -lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
  1.1314 -by (simp add: mult_mono)
  1.1315 -
  1.1316 -lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
  1.1317 -by (simp add: mult_strict_right_mono)
  1.1318 +lemma mult_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i * k \<le> j * l" for i j k l :: nat
  1.1319 +  by (simp add: mult_mono)
  1.1320 +
  1.1321 +lemma mult_less_mono1: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> i * k < j * k" for i j k :: nat
  1.1322 +  by (simp add: mult_strict_right_mono)
  1.1323  
  1.1324  text\<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that
  1.1325        there are no negative numbers.\<close>
  1.1326 -lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
  1.1327 +lemma nat_0_less_mult_iff [simp]: "0 < m * n \<longleftrightarrow> 0 < m \<and> 0 < n" for m n :: nat
  1.1328    apply (induct m)
  1.1329     apply simp
  1.1330    apply (case_tac n)
  1.1331     apply simp_all
  1.1332    done
  1.1333  
  1.1334 -lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (Suc 0 \<le> m & Suc 0 \<le> n)"
  1.1335 +lemma one_le_mult_iff [simp]: "Suc 0 \<le> m * n \<longleftrightarrow> Suc 0 \<le> m \<and> Suc 0 \<le> n"
  1.1336    apply (induct m)
  1.1337     apply simp
  1.1338    apply (case_tac n)
  1.1339     apply simp_all
  1.1340    done
  1.1341  
  1.1342 -lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
  1.1343 +lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat
  1.1344    apply (safe intro!: mult_less_mono1)
  1.1345    apply (cases k, auto)
  1.1346 -  apply (simp del: le_0_eq add: linorder_not_le [symmetric])
  1.1347 +  apply (simp add: linorder_not_le [symmetric])
  1.1348    apply (blast intro: mult_le_mono1)
  1.1349    done
  1.1350  
  1.1351 -lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)"
  1.1352 -by (simp add: mult.commute [of k])
  1.1353 -
  1.1354 -lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
  1.1355 -by (simp add: linorder_not_less [symmetric], auto)
  1.1356 -
  1.1357 -lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
  1.1358 -by (simp add: linorder_not_less [symmetric], auto)
  1.1359 -
  1.1360 -lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
  1.1361 -by (subst mult_less_cancel1) simp
  1.1362 -
  1.1363 -lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)"
  1.1364 -by (subst mult_le_cancel1) simp
  1.1365 -
  1.1366 -lemma le_square: "m \<le> m * (m::nat)"
  1.1367 +lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat
  1.1368 +  by (simp add: mult.commute [of k])
  1.1369 +
  1.1370 +lemma mult_le_cancel1 [simp]: "k * m \<le> k * n \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat
  1.1371 +  by (simp add: linorder_not_less [symmetric], auto)
  1.1372 +
  1.1373 +lemma mult_le_cancel2 [simp]: "m * k \<le> n * k \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat
  1.1374 +  by (simp add: linorder_not_less [symmetric], auto)
  1.1375 +
  1.1376 +lemma Suc_mult_less_cancel1: "Suc k * m < Suc k * n \<longleftrightarrow> m < n"
  1.1377 +  by (subst mult_less_cancel1) simp
  1.1378 +
  1.1379 +lemma Suc_mult_le_cancel1: "Suc k * m \<le> Suc k * n \<longleftrightarrow> m \<le> n"
  1.1380 +  by (subst mult_le_cancel1) simp
  1.1381 +
  1.1382 +lemma le_square: "m \<le> m * m" for m :: nat
  1.1383    by (cases m) (auto intro: le_add1)
  1.1384  
  1.1385 -lemma le_cube: "(m::nat) \<le> m * (m * m)"
  1.1386 +lemma le_cube: "m \<le> m * (m * m)" for m :: nat
  1.1387    by (cases m) (auto intro: le_add1)
  1.1388  
  1.1389  text \<open>Lemma for \<open>gcd\<close>\<close>
  1.1390 -lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
  1.1391 +lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat
  1.1392    apply (drule sym)
  1.1393    apply (rule disjCI)
  1.1394    apply (rule nat_less_cases, erule_tac [2] _)
  1.1395 @@ -1261,15 +1262,14 @@
  1.1396  instantiation nat :: distrib_lattice
  1.1397  begin
  1.1398  
  1.1399 -definition
  1.1400 -  "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min"
  1.1401 -
  1.1402 -definition
  1.1403 -  "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max"
  1.1404 -
  1.1405 -instance by intro_classes
  1.1406 -  (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def
  1.1407 -    intro: order_less_imp_le antisym elim!: order_trans order_less_trans)
  1.1408 +definition "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min"
  1.1409 +
  1.1410 +definition "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max"
  1.1411 +
  1.1412 +instance
  1.1413 +  by intro_classes
  1.1414 +    (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def
  1.1415 +      intro: order_less_imp_le antisym elim!: order_trans order_less_trans)
  1.1416  
  1.1417  end
  1.1418  
  1.1419 @@ -1283,8 +1283,8 @@
  1.1420  
  1.1421  consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
  1.1422  
  1.1423 -abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80) where
  1.1424 -  "f ^^ n \<equiv> compow n f"
  1.1425 +abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80)
  1.1426 +  where "f ^^ n \<equiv> compow n f"
  1.1427  
  1.1428  notation (latex output)
  1.1429    compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
  1.1430 @@ -1292,7 +1292,7 @@
  1.1431  text \<open>\<open>f ^^ n = f o ... o f\<close>, the n-fold composition of \<open>f\<close>\<close>
  1.1432  
  1.1433  overloading
  1.1434 -  funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
  1.1435 +  funpow \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
  1.1436  begin
  1.1437  
  1.1438  primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
  1.1439 @@ -1304,10 +1304,10 @@
  1.1440  lemma funpow_0 [simp]: "(f ^^ 0) x = x"
  1.1441    by simp
  1.1442  
  1.1443 -lemma funpow_Suc_right:
  1.1444 -  "f ^^ Suc n = f ^^ n \<circ> f"
  1.1445 +lemma funpow_Suc_right: "f ^^ Suc n = f ^^ n \<circ> f"
  1.1446  proof (induct n)
  1.1447 -  case 0 then show ?case by simp
  1.1448 +  case 0
  1.1449 +  then show ?case by simp
  1.1450  next
  1.1451    fix n
  1.1452    assume "f ^^ Suc n = f ^^ n \<circ> f"
  1.1453 @@ -1319,27 +1319,23 @@
  1.1454  
  1.1455  text \<open>for code generation\<close>
  1.1456  
  1.1457 -definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
  1.1458 -  funpow_code_def [code_abbrev]: "funpow = compow"
  1.1459 +definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
  1.1460 +  where funpow_code_def [code_abbrev]: "funpow = compow"
  1.1461  
  1.1462  lemma [code]:
  1.1463 -  "funpow (Suc n) f = f o funpow n f"
  1.1464 +  "funpow (Suc n) f = f \<circ> funpow n f"
  1.1465    "funpow 0 f = id"
  1.1466    by (simp_all add: funpow_code_def)
  1.1467  
  1.1468  hide_const (open) funpow
  1.1469  
  1.1470 -lemma funpow_add:
  1.1471 -  "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
  1.1472 +lemma funpow_add: "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
  1.1473    by (induct m) simp_all
  1.1474  
  1.1475 -lemma funpow_mult:
  1.1476 -  fixes f :: "'a \<Rightarrow> 'a"
  1.1477 -  shows "(f ^^ m) ^^ n = f ^^ (m * n)"
  1.1478 +lemma funpow_mult: "(f ^^ m) ^^ n = f ^^ (m * n)" for f :: "'a \<Rightarrow> 'a"
  1.1479    by (induct n) (simp_all add: funpow_add)
  1.1480  
  1.1481 -lemma funpow_swap1:
  1.1482 -  "f ((f ^^ n) x) = (f ^^ n) (f x)"
  1.1483 +lemma funpow_swap1: "f ((f ^^ n) x) = (f ^^ n) (f x)"
  1.1484  proof -
  1.1485    have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp
  1.1486    also have "\<dots>  = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
  1.1487 @@ -1347,9 +1343,7 @@
  1.1488    finally show ?thesis .
  1.1489  qed
  1.1490  
  1.1491 -lemma comp_funpow:
  1.1492 -  fixes f :: "'a \<Rightarrow> 'a"
  1.1493 -  shows "comp f ^^ n = comp (f ^^ n)"
  1.1494 +lemma comp_funpow: "comp f ^^ n = comp (f ^^ n)" for f :: "'a \<Rightarrow> 'a"
  1.1495    by (induct n) simp_all
  1.1496  
  1.1497  lemma Suc_funpow[simp]: "Suc ^^ n = (op + n)"
  1.1498 @@ -1358,43 +1352,46 @@
  1.1499  lemma id_funpow[simp]: "id ^^ n = id"
  1.1500    by (induct n) simp_all
  1.1501  
  1.1502 -lemma funpow_mono:
  1.1503 -  fixes f :: "'a \<Rightarrow> ('a::lattice)"
  1.1504 -  shows "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
  1.1505 +lemma funpow_mono: "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
  1.1506 +  for f :: "'a \<Rightarrow> ('a::lattice)"
  1.1507    by (induct n arbitrary: A B)
  1.1508       (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
  1.1509  
  1.1510 +
  1.1511  subsection \<open>Kleene iteration\<close>
  1.1512  
  1.1513  lemma Kleene_iter_lpfp:
  1.1514 -assumes "mono f" and "f p \<le> p" shows "(f^^k) (bot::'a::order_bot) \<le> p"
  1.1515 +  assumes "mono f"
  1.1516 +    and "f p \<le> p"
  1.1517 +  shows "(f^^k) (bot::'a::order_bot) \<le> p"
  1.1518  proof(induction k)
  1.1519 -  case 0 show ?case by simp
  1.1520 +  case 0
  1.1521 +  show ?case by simp
  1.1522  next
  1.1523    case Suc
  1.1524 -  from monoD[OF assms(1) Suc] assms(2)
  1.1525 -  show ?case by simp
  1.1526 +  from monoD[OF assms(1) Suc] assms(2) show ?case by simp
  1.1527  qed
  1.1528  
  1.1529 -lemma lfp_Kleene_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot"
  1.1530 -shows "lfp f = (f^^k) bot"
  1.1531 -proof(rule antisym)
  1.1532 +lemma lfp_Kleene_iter:
  1.1533 +  assumes "mono f"
  1.1534 +    and "(f^^Suc k) bot = (f^^k) bot"
  1.1535 +  shows "lfp f = (f^^k) bot"
  1.1536 +proof (rule antisym)
  1.1537    show "lfp f \<le> (f^^k) bot"
  1.1538 -  proof(rule lfp_lowerbound)
  1.1539 -    show "f ((f^^k) bot) \<le> (f^^k) bot" using assms(2) by simp
  1.1540 +  proof (rule lfp_lowerbound)
  1.1541 +    show "f ((f^^k) bot) \<le> (f^^k) bot"
  1.1542 +      using assms(2) by simp
  1.1543    qed
  1.1544 -next
  1.1545    show "(f^^k) bot \<le> lfp f"
  1.1546      using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
  1.1547  qed
  1.1548  
  1.1549 -lemma mono_pow:
  1.1550 -  fixes f :: "'a \<Rightarrow> 'a::complete_lattice"
  1.1551 -  shows "mono f \<Longrightarrow> mono (f ^^ n)"
  1.1552 -  by (induction n) (auto simp: mono_def)
  1.1553 +lemma mono_pow: "mono f \<Longrightarrow> mono (f ^^ n)" for f :: "'a \<Rightarrow> 'a::complete_lattice"
  1.1554 +  by (induct n) (auto simp: mono_def)
  1.1555  
  1.1556  lemma lfp_funpow:
  1.1557 -  assumes f: "mono f" shows "lfp (f ^^ Suc n) = lfp f"
  1.1558 +  assumes f: "mono f"
  1.1559 +  shows "lfp (f ^^ Suc n) = lfp f"
  1.1560  proof (rule antisym)
  1.1561    show "lfp f \<le> lfp (f ^^ Suc n)"
  1.1562    proof (rule lfp_lowerbound)
  1.1563 @@ -1404,13 +1401,14 @@
  1.1564        by (simp add: comp_def)
  1.1565    qed
  1.1566    have "(f^^n) (lfp f) = lfp f" for n
  1.1567 -    by (induction n) (auto intro: f lfp_unfold[symmetric])
  1.1568 +    by (induct n) (auto intro: f lfp_unfold[symmetric])
  1.1569    then show "lfp (f^^Suc n) \<le> lfp f"
  1.1570      by (intro lfp_lowerbound) (simp del: funpow.simps)
  1.1571  qed
  1.1572  
  1.1573  lemma gfp_funpow:
  1.1574 -  assumes f: "mono f" shows "gfp (f ^^ Suc n) = gfp f"
  1.1575 +  assumes f: "mono f"
  1.1576 +  shows "gfp (f ^^ Suc n) = gfp f"
  1.1577  proof (rule antisym)
  1.1578    show "gfp f \<ge> gfp (f ^^ Suc n)"
  1.1579    proof (rule gfp_upperbound)
  1.1580 @@ -1420,18 +1418,19 @@
  1.1581        by (simp add: comp_def)
  1.1582    qed
  1.1583    have "(f^^n) (gfp f) = gfp f" for n
  1.1584 -    by (induction n) (auto intro: f gfp_unfold[symmetric])
  1.1585 +    by (induct n) (auto intro: f gfp_unfold[symmetric])
  1.1586    then show "gfp (f^^Suc n) \<ge> gfp f"
  1.1587      by (intro gfp_upperbound) (simp del: funpow.simps)
  1.1588  qed
  1.1589  
  1.1590 +
  1.1591  subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: @{term of_nat}\<close>
  1.1592  
  1.1593  context semiring_1
  1.1594  begin
  1.1595  
  1.1596 -definition of_nat :: "nat \<Rightarrow> 'a" where
  1.1597 -  "of_nat n = (plus 1 ^^ n) 0"
  1.1598 +definition of_nat :: "nat \<Rightarrow> 'a"
  1.1599 +  where "of_nat n = (plus 1 ^^ n) 0"
  1.1600  
  1.1601  lemma of_nat_simps [simp]:
  1.1602    shows of_nat_0: "of_nat 0 = 0"
  1.1603 @@ -1448,16 +1447,16 @@
  1.1604    by (induct m) (simp_all add: ac_simps distrib_right)
  1.1605  
  1.1606  lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
  1.1607 -  by (induction x) (simp_all add: algebra_simps)
  1.1608 +  by (induct x) (simp_all add: algebra_simps)
  1.1609  
  1.1610  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
  1.1611    "of_nat_aux inc 0 i = i"
  1.1612  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close>
  1.1613  
  1.1614 -lemma of_nat_code:
  1.1615 -  "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
  1.1616 +lemma of_nat_code: "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
  1.1617  proof (induct n)
  1.1618 -  case 0 then show ?case by simp
  1.1619 +  case 0
  1.1620 +  then show ?case by simp
  1.1621  next
  1.1622    case (Suc n)
  1.1623    have "\<And>i. of_nat_aux (\<lambda>i. i + 1) n (i + 1) = of_nat_aux (\<lambda>i. i + 1) n i + 1"
  1.1624 @@ -1475,11 +1474,11 @@
  1.1625  begin
  1.1626  
  1.1627  lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
  1.1628 -by (simp add: algebra_simps of_nat_add [symmetric])
  1.1629 +  by (simp add: algebra_simps of_nat_add [symmetric])
  1.1630  
  1.1631  end
  1.1632  
  1.1633 -text\<open>Class for unital semirings with characteristic zero.
  1.1634 +text \<open>Class for unital semirings with characteristic zero.
  1.1635   Includes non-ordered rings like the complex numbers.\<close>
  1.1636  
  1.1637  class semiring_char_0 = semiring_1 +
  1.1638 @@ -1489,7 +1488,7 @@
  1.1639  lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
  1.1640    by (auto intro: inj_of_nat injD)
  1.1641  
  1.1642 -text\<open>Special cases where either operand is zero\<close>
  1.1643 +text \<open>Special cases where either operand is zero\<close>
  1.1644  
  1.1645  lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
  1.1646    by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
  1.1647 @@ -1530,12 +1529,12 @@
  1.1648  lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
  1.1649    by simp
  1.1650  
  1.1651 -text\<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
  1.1652 -
  1.1653 -subclass semiring_char_0 proof
  1.1654 -qed (auto intro!: injI simp add: eq_iff)
  1.1655 -
  1.1656 -text\<open>Special cases where either operand is zero\<close>
  1.1657 +text \<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
  1.1658 +
  1.1659 +subclass semiring_char_0
  1.1660 +  by standard (auto intro!: injI simp add: eq_iff)
  1.1661 +
  1.1662 +text \<open>Special cases where either operand is zero\<close>
  1.1663  
  1.1664  lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
  1.1665    by (rule of_nat_le_iff [of _ 0, simplified])
  1.1666 @@ -1615,9 +1614,9 @@
  1.1667  subsection \<open>Further arithmetic facts concerning the natural numbers\<close>
  1.1668  
  1.1669  lemma subst_equals:
  1.1670 -  assumes 1: "t = s" and 2: "u = t"
  1.1671 +  assumes "t = s" and "u = t"
  1.1672    shows "u = s"
  1.1673 -  using 2 1 by (rule trans)
  1.1674 +  using assms(2,1) by (rule trans)
  1.1675  
  1.1676  ML_file "Tools/nat_arith.ML"
  1.1677  
  1.1678 @@ -1647,7 +1646,10 @@
  1.1679    case True
  1.1680    then show ?thesis
  1.1681      by (induct n n' rule: less_Suc_induct) (auto intro: mono)
  1.1682 -qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
  1.1683 +next
  1.1684 +  case False
  1.1685 +  with \<open>n \<le> n'\<close> show ?thesis by auto
  1.1686 +qed
  1.1687  
  1.1688  lemma lift_Suc_antimono_le:
  1.1689    assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
  1.1690 @@ -1656,27 +1658,26 @@
  1.1691    case True
  1.1692    then show ?thesis
  1.1693      by (induct n n' rule: less_Suc_induct) (auto intro: mono)
  1.1694 -qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
  1.1695 +next
  1.1696 +  case False
  1.1697 +  with \<open>n \<le> n'\<close> show ?thesis by auto
  1.1698 +qed
  1.1699  
  1.1700  lemma lift_Suc_mono_less:
  1.1701    assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
  1.1702    shows "f n < f n'"
  1.1703 -using \<open>n < n'\<close>
  1.1704 -by (induct n n' rule: less_Suc_induct) (auto intro: mono)
  1.1705 -
  1.1706 -lemma lift_Suc_mono_less_iff:
  1.1707 -  "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"
  1.1708 +  using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono)
  1.1709 +
  1.1710 +lemma lift_Suc_mono_less_iff: "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"
  1.1711    by (blast intro: less_asym' lift_Suc_mono_less [of f]
  1.1712      dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq [THEN iffD1])
  1.1713  
  1.1714  end
  1.1715  
  1.1716 -lemma mono_iff_le_Suc:
  1.1717 -  "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
  1.1718 +lemma mono_iff_le_Suc: "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
  1.1719    unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
  1.1720  
  1.1721 -lemma antimono_iff_le_Suc:
  1.1722 -  "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
  1.1723 +lemma antimono_iff_le_Suc: "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
  1.1724    unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])
  1.1725  
  1.1726  lemma mono_nat_linear_lb:
  1.1727 @@ -1684,7 +1685,8 @@
  1.1728    assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
  1.1729    shows "f m + k \<le> f (m + k)"
  1.1730  proof (induct k)
  1.1731 -  case 0 then show ?case by simp
  1.1732 +  case 0
  1.1733 +  then show ?case by simp
  1.1734  next
  1.1735    case (Suc k)
  1.1736    then have "Suc (f m + k) \<le> Suc (f (m + k))" by simp
  1.1737 @@ -1694,7 +1696,7 @@
  1.1738  qed
  1.1739  
  1.1740  
  1.1741 -text\<open>Subtraction laws, mostly by Clemens Ballarin\<close>
  1.1742 +text \<open>Subtraction laws, mostly by Clemens Ballarin\<close>
  1.1743  
  1.1744  lemma diff_less_mono:
  1.1745    fixes a b c :: nat
  1.1746 @@ -1706,105 +1708,73 @@
  1.1747    then show ?thesis by simp
  1.1748  qed
  1.1749  
  1.1750 -lemma less_diff_conv:
  1.1751 -  fixes i j k :: nat
  1.1752 -  shows "i < j - k \<longleftrightarrow> i + k < j" (is "?P \<longleftrightarrow> ?Q")
  1.1753 -  by (cases "k \<le> j")
  1.1754 -    (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
  1.1755 -
  1.1756 -lemma less_diff_conv2:
  1.1757 -  fixes j k i :: nat
  1.1758 -  assumes "k \<le> j"
  1.1759 -  shows "j - k < i \<longleftrightarrow> j < i + k" (is "?P \<longleftrightarrow> ?Q")
  1.1760 -  using assms by (auto dest: le_Suc_ex)
  1.1761 -
  1.1762 -lemma le_diff_conv:
  1.1763 -  fixes j k i :: nat
  1.1764 -  shows "j - k \<le> i \<longleftrightarrow> j \<le> i + k"
  1.1765 -  by (cases "k \<le> j")
  1.1766 -    (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
  1.1767 -
  1.1768 -lemma diff_diff_cancel [simp]:
  1.1769 -  fixes i n :: nat
  1.1770 -  shows "i \<le> n \<Longrightarrow> n - (n - i) = i"
  1.1771 +lemma less_diff_conv: "i < j - k \<longleftrightarrow> i + k < j" for i j k :: nat
  1.1772 +  by (cases "k \<le> j") (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
  1.1773 +
  1.1774 +lemma less_diff_conv2: "k \<le> j \<Longrightarrow> j - k < i \<longleftrightarrow> j < i + k" for j k i :: nat
  1.1775    by (auto dest: le_Suc_ex)
  1.1776  
  1.1777 -lemma diff_less [simp]:
  1.1778 -  fixes i n :: nat
  1.1779 -  shows "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m"
  1.1780 +lemma le_diff_conv: "j - k \<le> i \<longleftrightarrow> j \<le> i + k" for j k i :: nat
  1.1781 +  by (cases "k \<le> j") (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
  1.1782 +
  1.1783 +lemma diff_diff_cancel [simp]: "i \<le> n \<Longrightarrow> n - (n - i) = i" for i n :: nat
  1.1784 +  by (auto dest: le_Suc_ex)
  1.1785 +
  1.1786 +lemma diff_less [simp]: "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m" for i n :: nat
  1.1787    by (auto dest: less_imp_Suc_add)
  1.1788  
  1.1789  text \<open>Simplification of relational expressions involving subtraction\<close>
  1.1790  
  1.1791 -lemma diff_diff_eq:
  1.1792 -  fixes m n k :: nat
  1.1793 -  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n"
  1.1794 +lemma diff_diff_eq: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n" for m n k :: nat
  1.1795    by (auto dest!: le_Suc_ex)
  1.1796  
  1.1797  hide_fact (open) diff_diff_eq
  1.1798  
  1.1799 -lemma eq_diff_iff:
  1.1800 -  fixes m n k :: nat
  1.1801 -  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n"
  1.1802 +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.1803    by (auto dest: le_Suc_ex)
  1.1804  
  1.1805 -lemma less_diff_iff:
  1.1806 -  fixes m n k :: nat
  1.1807 -  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n"
  1.1808 +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.1809    by (auto dest!: le_Suc_ex)
  1.1810  
  1.1811 -lemma le_diff_iff:
  1.1812 -  fixes m n k :: nat
  1.1813 -  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
  1.1814 +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.1815    by (auto dest!: le_Suc_ex)
  1.1816  
  1.1817 -lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> (a::nat)"
  1.1818 +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.1819    by (force dest: le_Suc_ex)
  1.1820 -  
  1.1821 -
  1.1822 -text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
  1.1823 -
  1.1824 -lemma diff_le_mono:
  1.1825 -  fixes m n l :: nat
  1.1826 -  shows "m \<le> n \<Longrightarrow> m - l \<le> n - l"
  1.1827 +
  1.1828 +
  1.1829 +text \<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
  1.1830 +
  1.1831 +lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l" for m n l :: nat
  1.1832    by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
  1.1833  
  1.1834 -lemma diff_le_mono2:
  1.1835 -  fixes m n l :: nat
  1.1836 -  shows "m \<le> n \<Longrightarrow> l - n \<le> l - m"
  1.1837 +lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m" for m n l :: nat
  1.1838    by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
  1.1839  
  1.1840 -lemma diff_less_mono2:
  1.1841 -  fixes m n l :: nat
  1.1842 -  shows "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
  1.1843 +lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m" for m n l :: nat
  1.1844    by (auto dest: less_imp_Suc_add split add: nat_diff_split)
  1.1845  
  1.1846 -lemma diffs0_imp_equal:
  1.1847 -  fixes m n :: nat
  1.1848 -  shows "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
  1.1849 +lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n" for m n :: nat
  1.1850    by (simp split add: nat_diff_split)
  1.1851  
  1.1852 -lemma min_diff:
  1.1853 -  fixes m n i :: nat
  1.1854 -  shows "min (m - i) (n - i) = min m n - i" (is "?lhs = ?rhs")
  1.1855 +lemma min_diff: "min (m - i) (n - i) = min m n - i" for m n i :: nat
  1.1856    by (cases m n rule: le_cases)
  1.1857      (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono)
  1.1858  
  1.1859  lemma inj_on_diff_nat:
  1.1860 -  assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
  1.1861 +  fixes k :: nat
  1.1862 +  assumes "\<forall>n \<in> N. k \<le> n"
  1.1863    shows "inj_on (\<lambda>n. n - k) N"
  1.1864  proof (rule inj_onI)
  1.1865    fix x y
  1.1866    assume a: "x \<in> N" "y \<in> N" "x - k = y - k"
  1.1867 -  with k_le_n have "x - k + k = y - k + k" by auto
  1.1868 -  with a k_le_n show "x = y" by (auto simp add: eq_diff_iff)
  1.1869 +  with assms have "x - k + k = y - k + k" by auto
  1.1870 +  with a assms show "x = y" by (auto simp add: eq_diff_iff)
  1.1871  qed
  1.1872  
  1.1873 -text\<open>Rewriting to pull differences out\<close>
  1.1874 -
  1.1875 -lemma diff_diff_right [simp]:
  1.1876 -  fixes i j k :: nat
  1.1877 -  shows "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j"
  1.1878 +text \<open>Rewriting to pull differences out\<close>
  1.1879 +
  1.1880 +lemma diff_diff_right [simp]: "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j" for i j k :: nat
  1.1881    by (fact diff_diff_right)
  1.1882  
  1.1883  lemma diff_Suc_diff_eq1 [simp]:
  1.1884 @@ -1842,24 +1812,22 @@
  1.1885    then show ?thesis by simp
  1.1886  qed
  1.1887  
  1.1888 -lemma one_less_mult:
  1.1889 -  "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
  1.1890 +lemma one_less_mult: "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
  1.1891    using less_1_mult [of n m] by (simp add: ac_simps)
  1.1892  
  1.1893 -lemma n_less_m_mult_n:
  1.1894 -  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
  1.1895 +lemma n_less_m_mult_n: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
  1.1896    using mult_strict_right_mono [of 1 m n] by simp
  1.1897  
  1.1898 -lemma n_less_n_mult_m:
  1.1899 -  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
  1.1900 +lemma n_less_n_mult_m: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
  1.1901    using mult_strict_left_mono [of 1 m n] by simp
  1.1902  
  1.1903 +
  1.1904  text \<open>Specialized induction principles that work "backwards":\<close>
  1.1905  
  1.1906  lemma inc_induct [consumes 1, case_names base step]:
  1.1907    assumes less: "i \<le> j"
  1.1908 -  assumes base: "P j"
  1.1909 -  assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
  1.1910 +    and base: "P j"
  1.1911 +    and step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
  1.1912    shows "P i"
  1.1913    using less step
  1.1914  proof (induct "j - i" arbitrary: i)
  1.1915 @@ -1873,7 +1841,7 @@
  1.1916    from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp
  1.1917    then have "d + 1 - 1 = j - n - 1" by simp
  1.1918    then have "d = j - n - 1" by simp
  1.1919 -  then have "d = j - (n + 1)" 
  1.1920 +  then have "d = j - (n + 1)"
  1.1921      by (simp add: diff_diff_eq)
  1.1922    then have "d = j - Suc n"
  1.1923      by simp
  1.1924 @@ -1892,11 +1860,11 @@
  1.1925    with order_refl \<open>n < j\<close> show "P n"
  1.1926      by (rule Suc.prems)
  1.1927  qed
  1.1928 -    
  1.1929 +
  1.1930  lemma strict_inc_induct [consumes 1, case_names base step]:
  1.1931    assumes less: "i < j"
  1.1932 -  assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i"
  1.1933 -  assumes step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
  1.1934 +    and base: "\<And>i. j = Suc i \<Longrightarrow> P i"
  1.1935 +    and step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
  1.1936    shows "P i"
  1.1937  using less proof (induct "j - i - 1" arbitrary: i)
  1.1938    case (0 i)
  1.1939 @@ -1922,10 +1890,10 @@
  1.1940    with \<open>i < j\<close> show "P i" by (rule step)
  1.1941  qed
  1.1942  
  1.1943 -lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
  1.1944 +lemma zero_induct_lemma: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P (k - i)"
  1.1945    using inc_induct[of "k - i" k P, simplified] by blast
  1.1946  
  1.1947 -lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
  1.1948 +lemma zero_induct: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P 0"
  1.1949    using inc_induct[of 0 k P] by blast
  1.1950  
  1.1951  text \<open>Further induction rule similar to @{thm inc_induct}\<close>
  1.1952 @@ -1933,13 +1901,15 @@
  1.1953  lemma dec_induct [consumes 1, case_names base step]:
  1.1954    "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.1955  proof (induct j arbitrary: i)
  1.1956 -  case 0 then show ?case by simp
  1.1957 +  case 0
  1.1958 +  then show ?case by simp
  1.1959  next
  1.1960    case (Suc j)
  1.1961 -  from Suc.prems have "i \<le> j \<or> i = Suc j"
  1.1962 -    by (simp add: le_Suc_eq)
  1.1963 -  then show ?case proof
  1.1964 -    assume "i \<le> j"
  1.1965 +  from Suc.prems consider "i \<le> j" | "i = Suc j"
  1.1966 +    by (auto simp add: le_Suc_eq)
  1.1967 +  then show ?case
  1.1968 +  proof cases
  1.1969 +    case 1
  1.1970      moreover have "j < Suc j" by simp
  1.1971      moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close>
  1.1972      proof (rule Suc.hyps)
  1.1973 @@ -1954,70 +1924,62 @@
  1.1974      ultimately show "P (Suc j)"
  1.1975        by (rule Suc.prems)
  1.1976    next
  1.1977 -    assume "i = Suc j"
  1.1978 +    case 2
  1.1979      with \<open>P i\<close> show "P (Suc j)" by simp
  1.1980    qed
  1.1981  qed
  1.1982  
  1.1983  
  1.1984 -subsection \<open> Monotonicity of funpow \<close>
  1.1985 +subsection \<open>Monotonicity of \<open>funpow\<close>\<close>
  1.1986  
  1.1987  lemma funpow_increasing:
  1.1988 -  fixes f :: "'a \<Rightarrow> ('a::{lattice, order_top})"
  1.1989 +  fixes f :: "'a \<Rightarrow> 'a::{lattice,order_top}"
  1.1990    shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>"
  1.1991    by (induct rule: inc_induct)
  1.1992       (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
  1.1993             intro: order_trans[OF _ funpow_mono])
  1.1994  
  1.1995  lemma funpow_decreasing:
  1.1996 -  fixes f :: "'a \<Rightarrow> ('a::{lattice, order_bot})"
  1.1997 +  fixes f :: "'a \<Rightarrow> 'a::{lattice,order_bot}"
  1.1998    shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>"
  1.1999    by (induct rule: dec_induct)
  1.2000       (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
  1.2001             intro: order_trans[OF _ funpow_mono])
  1.2002  
  1.2003  lemma mono_funpow:
  1.2004 -  fixes Q :: "'a::{lattice, order_bot} \<Rightarrow> 'a"
  1.2005 +  fixes Q :: "'a::{lattice,order_bot} \<Rightarrow> 'a"
  1.2006    shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
  1.2007    by (auto intro!: funpow_decreasing simp: mono_def)
  1.2008  
  1.2009  lemma antimono_funpow:
  1.2010 -  fixes Q :: "'a::{lattice, order_top} \<Rightarrow> 'a"
  1.2011 +  fixes Q :: "'a::{lattice,order_top} \<Rightarrow> 'a"
  1.2012    shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
  1.2013    by (auto intro!: funpow_increasing simp: antimono_def)
  1.2014  
  1.2015 +
  1.2016  subsection \<open>The divides relation on @{typ nat}\<close>
  1.2017  
  1.2018 -lemma dvd_1_left [iff]:
  1.2019 -  "Suc 0 dvd k"
  1.2020 +lemma dvd_1_left [iff]: "Suc 0 dvd k"
  1.2021    by (simp add: dvd_def)
  1.2022  
  1.2023 -lemma dvd_1_iff_1 [simp]:
  1.2024 -  "m dvd Suc 0 \<longleftrightarrow> m = Suc 0"
  1.2025 +lemma dvd_1_iff_1 [simp]: "m dvd Suc 0 \<longleftrightarrow> m = Suc 0"
  1.2026    by (simp add: dvd_def)
  1.2027  
  1.2028 -lemma nat_dvd_1_iff_1 [simp]:
  1.2029 -  "m dvd (1::nat) \<longleftrightarrow> m = 1"
  1.2030 +lemma nat_dvd_1_iff_1 [simp]: "m dvd 1 \<longleftrightarrow> m = 1" for m :: nat
  1.2031    by (simp add: dvd_def)
  1.2032  
  1.2033 -lemma dvd_antisym:
  1.2034 -  "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = (n::nat)"
  1.2035 -  unfolding dvd_def
  1.2036 -  by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
  1.2037 -
  1.2038 -lemma dvd_diff_nat [simp]:
  1.2039 -  "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n :: nat)"
  1.2040 -  unfolding dvd_def
  1.2041 -  by (blast intro: right_diff_distrib' [symmetric])
  1.2042 -
  1.2043 -lemma dvd_diffD:
  1.2044 -  "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd (m::nat)"
  1.2045 +lemma dvd_antisym: "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n" for m n :: nat
  1.2046 +  unfolding dvd_def by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
  1.2047 +
  1.2048 +lemma dvd_diff_nat [simp]: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)" for k m n :: nat
  1.2049 +  unfolding dvd_def by (blast intro: right_diff_distrib' [symmetric])
  1.2050 +
  1.2051 +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.2052    apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
  1.2053    apply (blast intro: dvd_add)
  1.2054    done
  1.2055  
  1.2056 -lemma dvd_diffD1:
  1.2057 -  "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd (n::nat)"
  1.2058 +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.2059    by (drule_tac m = m in dvd_diff_nat) auto
  1.2060  
  1.2061  lemma dvd_mult_cancel:
  1.2062 @@ -2030,25 +1992,20 @@
  1.2063    with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel)
  1.2064    then show ?thesis ..
  1.2065  qed
  1.2066 -  
  1.2067 -lemma dvd_mult_cancel1:
  1.2068 -  "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = (1::nat)"
  1.2069 +
  1.2070 +lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1" for m n :: nat
  1.2071    apply auto
  1.2072 -   apply (subgoal_tac "m*n dvd m*1")
  1.2073 +   apply (subgoal_tac "m * n dvd m * 1")
  1.2074     apply (drule dvd_mult_cancel, auto)
  1.2075    done
  1.2076  
  1.2077 -lemma dvd_mult_cancel2:
  1.2078 -  "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = (1::nat)"
  1.2079 +lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1" for m n :: nat
  1.2080    using dvd_mult_cancel1 [of m n] by (simp add: ac_simps)
  1.2081  
  1.2082 -lemma dvd_imp_le:
  1.2083 -  "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> (n::nat)"
  1.2084 +lemma dvd_imp_le: "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> n" for k n :: nat
  1.2085    by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
  1.2086  
  1.2087 -lemma nat_dvd_not_less:
  1.2088 -  fixes m n :: nat
  1.2089 -  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
  1.2090 +lemma nat_dvd_not_less: "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m" for m n :: nat
  1.2091    by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
  1.2092  
  1.2093  lemma less_eq_dvd_minus:
  1.2094 @@ -2061,9 +2018,7 @@
  1.2095    then show ?thesis by (simp add: add.commute [of m])
  1.2096  qed
  1.2097  
  1.2098 -lemma dvd_minus_self:
  1.2099 -  fixes m n :: nat
  1.2100 -  shows "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
  1.2101 +lemma dvd_minus_self: "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n" for m n :: nat
  1.2102    by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le)
  1.2103  
  1.2104  lemma dvd_minus_add:
  1.2105 @@ -2082,61 +2037,55 @@
  1.2106  
  1.2107  subsection \<open>Aliasses\<close>
  1.2108  
  1.2109 -lemma nat_mult_1: "(1::nat) * n = n"
  1.2110 +lemma nat_mult_1: "1 * n = n" for n :: nat
  1.2111    by (fact mult_1_left)
  1.2112  
  1.2113 -lemma nat_mult_1_right: "n * (1::nat) = n"
  1.2114 +lemma nat_mult_1_right: "n * 1 = n" for n :: nat
  1.2115    by (fact mult_1_right)
  1.2116  
  1.2117 -lemma nat_add_left_cancel:
  1.2118 -  fixes k m n :: nat
  1.2119 -  shows "k + m = k + n \<longleftrightarrow> m = n"
  1.2120 +lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n" for k m n :: nat
  1.2121    by (fact add_left_cancel)
  1.2122  
  1.2123 -lemma nat_add_right_cancel:
  1.2124 -  fixes k m n :: nat
  1.2125 -  shows "m + k = n + k \<longleftrightarrow> m = n"
  1.2126 +lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n" for k m n :: nat
  1.2127    by (fact add_right_cancel)
  1.2128  
  1.2129 -lemma diff_mult_distrib:
  1.2130 -  "((m::nat) - n) * k = (m * k) - (n * k)"
  1.2131 +lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)" for k m n :: nat
  1.2132    by (fact left_diff_distrib')
  1.2133  
  1.2134 -lemma diff_mult_distrib2:
  1.2135 -  "k * ((m::nat) - n) = (k * m) - (k * n)"
  1.2136 +lemma diff_mult_distrib2: "k * (m - n) = (k * m) - (k * n)" for k m n :: nat
  1.2137    by (fact right_diff_distrib')
  1.2138  
  1.2139 -lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
  1.2140 -  by (fact le_add_diff) \<comment> \<open>FIXME delete\<close>
  1.2141 -
  1.2142 -lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
  1.2143 -  by (fact le_diff_conv2) \<comment> \<open>FIXME delete\<close>
  1.2144 -
  1.2145 -lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
  1.2146 +lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k" for k m n :: nat
  1.2147 +  by (fact le_add_diff)  (* FIXME delete *)
  1.2148 +
  1.2149 +lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)" for i j k :: nat
  1.2150 +  by (fact le_diff_conv2) (* FIXME delete *)
  1.2151 +
  1.2152 +lemma diff_self_eq_0 [simp]: "m - m = 0" for m :: nat
  1.2153    by (fact diff_cancel)
  1.2154  
  1.2155 -lemma diff_diff_left [simp]: "(i::nat) - j - k = i - (j + k)"
  1.2156 +lemma diff_diff_left [simp]: "i - j - k = i - (j + k)" for i j k :: nat
  1.2157    by (fact diff_diff_add)
  1.2158  
  1.2159 -lemma diff_commute: "(i::nat) - j - k = i - k - j"
  1.2160 +lemma diff_commute: "i - j - k = i - k - j" for i j k :: nat
  1.2161    by (fact diff_right_commute)
  1.2162  
  1.2163 -lemma diff_add_inverse: "(n + m) - n = (m::nat)"
  1.2164 +lemma diff_add_inverse: "(n + m) - n = m" for m n :: nat
  1.2165    by (fact add_diff_cancel_left')
  1.2166  
  1.2167 -lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
  1.2168 +lemma diff_add_inverse2: "(m + n) - n = m" for m n :: nat
  1.2169    by (fact add_diff_cancel_right')
  1.2170  
  1.2171 -lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
  1.2172 +lemma diff_cancel: "(k + m) - (k + n) = m - n" for k m n :: nat
  1.2173    by (fact add_diff_cancel_left)
  1.2174  
  1.2175 -lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
  1.2176 +lemma diff_cancel2: "(m + k) - (n + k) = m - n" for k m n :: nat
  1.2177    by (fact add_diff_cancel_right)
  1.2178  
  1.2179 -lemma diff_add_0: "n - (n + m) = (0::nat)"
  1.2180 +lemma diff_add_0: "n - (n + m) = 0" for m n :: nat
  1.2181    by (fact diff_add_zero)
  1.2182  
  1.2183 -lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
  1.2184 +lemma add_mult_distrib2: "k * (m + n) = (k * m) + (k * n)" for k m n :: nat
  1.2185    by (fact distrib_left)
  1.2186  
  1.2187  lemmas nat_distrib =
  1.2188 @@ -2151,8 +2100,7 @@
  1.2189  instantiation nat :: size
  1.2190  begin
  1.2191  
  1.2192 -definition size_nat where
  1.2193 -  [simp, code]: "size (n::nat) = n"
  1.2194 +definition size_nat where [simp, code]: "size (n::nat) = n"
  1.2195  
  1.2196  instance ..
  1.2197