src/HOL/Nat.thy
 author wenzelm Mon May 23 15:30:13 2016 +0200 (2016-05-23 ago) changeset 63113 fe31996e3898 parent 63111 caa0c513bbca child 63145 703edebd1d92 permissions -rw-r--r--
```     1 (*  Title:      HOL/Nat.thy
```
```     2     Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
```
```     3
```
```     4 Type "nat" is a linear order, and a datatype; arithmetic operators + -
```
```     5 and * (for div and mod, see theory Divides).
```
```     6 *)
```
```     7
```
```     8 section \<open>Natural numbers\<close>
```
```     9
```
```    10 theory Nat
```
```    11 imports Inductive Typedef Fun Rings
```
```    12 begin
```
```    13
```
```    14 ML_file "~~/src/Tools/rat.ML"
```
```    15
```
```    16 named_theorems arith "arith facts -- only ground formulas"
```
```    17 ML_file "Tools/arith_data.ML"
```
```    18
```
```    19
```
```    20 subsection \<open>Type \<open>ind\<close>\<close>
```
```    21
```
```    22 typedecl ind
```
```    23
```
```    24 axiomatization Zero_Rep :: ind and Suc_Rep :: "ind \<Rightarrow> ind"
```
```    25   \<comment> \<open>The axiom of infinity in 2 parts:\<close>
```
```    26 where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y"
```
```    27   and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
```
```    28
```
```    29 subsection \<open>Type nat\<close>
```
```    30
```
```    31 text \<open>Type definition\<close>
```
```    32
```
```    33 inductive Nat :: "ind \<Rightarrow> bool" where
```
```    34   Zero_RepI: "Nat Zero_Rep"
```
```    35 | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
```
```    36
```
```    37 typedef nat = "{n. Nat n}"
```
```    38   morphisms Rep_Nat Abs_Nat
```
```    39   using Nat.Zero_RepI by auto
```
```    40
```
```    41 lemma Nat_Rep_Nat:
```
```    42   "Nat (Rep_Nat n)"
```
```    43   using Rep_Nat by simp
```
```    44
```
```    45 lemma Nat_Abs_Nat_inverse:
```
```    46   "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n"
```
```    47   using Abs_Nat_inverse by simp
```
```    48
```
```    49 lemma Nat_Abs_Nat_inject:
```
```    50   "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m"
```
```    51   using Abs_Nat_inject by simp
```
```    52
```
```    53 instantiation nat :: zero
```
```    54 begin
```
```    55
```
```    56 definition Zero_nat_def:
```
```    57   "0 = Abs_Nat Zero_Rep"
```
```    58
```
```    59 instance ..
```
```    60
```
```    61 end
```
```    62
```
```    63 definition Suc :: "nat \<Rightarrow> nat" where
```
```    64   "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
```
```    65
```
```    66 lemma Suc_not_Zero: "Suc m \<noteq> 0"
```
```    67   by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat)
```
```    68
```
```    69 lemma Zero_not_Suc: "0 \<noteq> Suc m"
```
```    70   by (rule not_sym, rule Suc_not_Zero not_sym)
```
```    71
```
```    72 lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y"
```
```    73   by (rule iffI, rule Suc_Rep_inject) simp_all
```
```    74
```
```    75 lemma nat_induct0:
```
```    76   fixes n
```
```    77   assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
```
```    78   shows "P n"
```
```    79 using assms
```
```    80 apply (unfold Zero_nat_def Suc_def)
```
```    81 apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<close>
```
```    82 apply (erule Nat_Rep_Nat [THEN Nat.induct])
```
```    83 apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
```
```    84 done
```
```    85
```
```    86 free_constructors case_nat for
```
```    87     "0 :: nat"
```
```    88   | Suc pred
```
```    89 where
```
```    90   "pred (0 :: nat) = (0 :: nat)"
```
```    91     apply atomize_elim
```
```    92     apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
```
```    93    apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject'
```
```    94      Rep_Nat_inject)
```
```    95   apply (simp only: Suc_not_Zero)
```
```    96   done
```
```    97
```
```    98 \<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
```
```    99 setup \<open>Sign.mandatory_path "old"\<close>
```
```   100
```
```   101 old_rep_datatype "0 :: nat" Suc
```
```   102   apply (erule nat_induct0, assumption)
```
```   103  apply (rule nat.inject)
```
```   104 apply (rule nat.distinct(1))
```
```   105 done
```
```   106
```
```   107 setup \<open>Sign.parent_path\<close>
```
```   108
```
```   109 \<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
```
```   110 setup \<open>Sign.mandatory_path "nat"\<close>
```
```   111
```
```   112 declare
```
```   113   old.nat.inject[iff del]
```
```   114   old.nat.distinct(1)[simp del, induct_simp del]
```
```   115
```
```   116 lemmas induct = old.nat.induct
```
```   117 lemmas inducts = old.nat.inducts
```
```   118 lemmas rec = old.nat.rec
```
```   119 lemmas simps = nat.inject nat.distinct nat.case nat.rec
```
```   120
```
```   121 setup \<open>Sign.parent_path\<close>
```
```   122
```
```   123 abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
```
```   124   where "rec_nat \<equiv> old.rec_nat"
```
```   125
```
```   126 declare nat.sel[code del]
```
```   127
```
```   128 hide_const (open) Nat.pred \<comment> \<open>hide everything related to the selector\<close>
```
```   129 hide_fact
```
```   130   nat.case_eq_if
```
```   131   nat.collapse
```
```   132   nat.expand
```
```   133   nat.sel
```
```   134   nat.exhaust_sel
```
```   135   nat.split_sel
```
```   136   nat.split_sel_asm
```
```   137
```
```   138 lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
```
```   139   \<comment> \<open>for backward compatibility -- names of variables differ\<close>
```
```   140   "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
```
```   141 by (rule old.nat.exhaust)
```
```   142
```
```   143 lemma nat_induct [case_names 0 Suc, induct type: nat]:
```
```   144   \<comment> \<open>for backward compatibility -- names of variables differ\<close>
```
```   145   fixes n
```
```   146   assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
```
```   147   shows "P n"
```
```   148 using assms by (rule nat.induct)
```
```   149
```
```   150 hide_fact
```
```   151   nat_exhaust
```
```   152   nat_induct0
```
```   153
```
```   154 ML \<open>
```
```   155 val nat_basic_lfp_sugar =
```
```   156   let
```
```   157     val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global @{theory} @{type_name nat});
```
```   158     val recx = Logic.varify_types_global @{term rec_nat};
```
```   159     val C = body_type (fastype_of recx);
```
```   160   in
```
```   161     {T = HOLogic.natT, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[HOLogic.natT, C]]],
```
```   162      ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms nat.rec}}
```
```   163   end;
```
```   164 \<close>
```
```   165
```
```   166 setup \<open>
```
```   167 let
```
```   168   fun basic_lfp_sugars_of _ [@{typ nat}] _ _ ctxt =
```
```   169       ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt)
```
```   170     | basic_lfp_sugars_of bs arg_Ts callers callssss ctxt =
```
```   171       BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt;
```
```   172 in
```
```   173   BNF_LFP_Rec_Sugar.register_lfp_rec_extension
```
```   174     {nested_simps = [], is_new_datatype = K (K true), basic_lfp_sugars_of = basic_lfp_sugars_of,
```
```   175      rewrite_nested_rec_call = NONE}
```
```   176 end
```
```   177 \<close>
```
```   178
```
```   179 text \<open>Injectiveness and distinctness lemmas\<close>
```
```   180
```
```   181 lemma inj_Suc[simp]: "inj_on Suc N"
```
```   182   by (simp add: inj_on_def)
```
```   183
```
```   184 lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
```
```   185 by (rule notE, rule Suc_not_Zero)
```
```   186
```
```   187 lemma Zero_neq_Suc: "0 = Suc m \<Longrightarrow> R"
```
```   188 by (rule Suc_neq_Zero, erule sym)
```
```   189
```
```   190 lemma Suc_inject: "Suc x = Suc y \<Longrightarrow> x = y"
```
```   191 by (rule inj_Suc [THEN injD])
```
```   192
```
```   193 lemma n_not_Suc_n: "n \<noteq> Suc n"
```
```   194 by (induct n) simp_all
```
```   195
```
```   196 lemma Suc_n_not_n: "Suc n \<noteq> n"
```
```   197 by (rule not_sym, rule n_not_Suc_n)
```
```   198
```
```   199 text \<open>A special form of induction for reasoning
```
```   200   about @{term "m < n"} and @{term "m - n"}\<close>
```
```   201
```
```   202 lemma diff_induct:
```
```   203   assumes "\<And>x. P x 0"
```
```   204     and "\<And>y. P 0 (Suc y)"
```
```   205     and "\<And>x y. P x y \<Longrightarrow> P (Suc x) (Suc y)"
```
```   206   shows "P m n"
```
```   207   using assms
```
```   208   apply (rule_tac x = m in spec)
```
```   209   apply (induct n)
```
```   210   prefer 2
```
```   211   apply (rule allI)
```
```   212   apply (induct_tac x, iprover+)
```
```   213   done
```
```   214
```
```   215
```
```   216 subsection \<open>Arithmetic operators\<close>
```
```   217
```
```   218 instantiation nat :: comm_monoid_diff
```
```   219 begin
```
```   220
```
```   221 primrec plus_nat where
```
```   222   add_0: "0 + n = (n::nat)"
```
```   223 | add_Suc: "Suc m + n = Suc (m + n)"
```
```   224
```
```   225 lemma add_0_right [simp]: "m + 0 = m" for m :: nat
```
```   226   by (induct m) simp_all
```
```   227
```
```   228 lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
```
```   229   by (induct m) simp_all
```
```   230
```
```   231 declare add_0 [code]
```
```   232
```
```   233 lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
```
```   234   by simp
```
```   235
```
```   236 primrec minus_nat where
```
```   237   diff_0 [code]: "m - 0 = (m::nat)"
```
```   238 | diff_Suc: "m - Suc n = (case m - n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k)"
```
```   239
```
```   240 declare diff_Suc [simp del]
```
```   241
```
```   242 lemma diff_0_eq_0 [simp, code]: "0 - n = 0" for n :: nat
```
```   243   by (induct n) (simp_all add: diff_Suc)
```
```   244
```
```   245 lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n"
```
```   246   by (induct n) (simp_all add: diff_Suc)
```
```   247
```
```   248 instance
```
```   249 proof
```
```   250   fix n m q :: nat
```
```   251   show "(n + m) + q = n + (m + q)" by (induct n) simp_all
```
```   252   show "n + m = m + n" by (induct n) simp_all
```
```   253   show "m + n - m = n" by (induct m) simp_all
```
```   254   show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc)
```
```   255   show "0 + n = n" by simp
```
```   256   show "0 - n = 0" by simp
```
```   257 qed
```
```   258
```
```   259 end
```
```   260
```
```   261 hide_fact (open) add_0 add_0_right diff_0
```
```   262
```
```   263 instantiation nat :: comm_semiring_1_cancel
```
```   264 begin
```
```   265
```
```   266 definition
```
```   267   One_nat_def [simp]: "1 = Suc 0"
```
```   268
```
```   269 primrec times_nat where
```
```   270   mult_0: "0 * n = (0::nat)"
```
```   271 | mult_Suc: "Suc m * n = n + (m * n)"
```
```   272
```
```   273 lemma mult_0_right [simp]: "m * 0 = 0" for m :: nat
```
```   274   by (induct m) simp_all
```
```   275
```
```   276 lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
```
```   277   by (induct m) (simp_all add: add.left_commute)
```
```   278
```
```   279 lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)" for m n k :: nat
```
```   280   by (induct m) (simp_all add: add.assoc)
```
```   281
```
```   282 instance
```
```   283 proof
```
```   284   fix k n m q :: nat
```
```   285   show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp
```
```   286   show "1 * n = n" unfolding One_nat_def by simp
```
```   287   show "n * m = m * n" by (induct n) simp_all
```
```   288   show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
```
```   289   show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
```
```   290   show "k * (m - n) = (k * m) - (k * n)"
```
```   291     by (induct m n rule: diff_induct) simp_all
```
```   292 qed
```
```   293
```
```   294 end
```
```   295
```
```   296
```
```   297 subsubsection \<open>Addition\<close>
```
```   298
```
```   299 text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close>
```
```   300
```
```   301 lemma add_is_0 [iff]: "(m + n = 0) = (m = 0 \<and> n = 0)" for m n :: nat
```
```   302   by (cases m) simp_all
```
```   303
```
```   304 lemma add_is_1: "m + n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
```
```   305   by (cases m) simp_all
```
```   306
```
```   307 lemma one_is_add: "Suc 0 = m + n \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
```
```   308   by (rule trans, rule eq_commute, rule add_is_1)
```
```   309
```
```   310 lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0" for m n :: nat
```
```   311   by (induct m) simp_all
```
```   312
```
```   313 lemma inj_on_add_nat[simp]: "inj_on (\<lambda>n. n + k) N" for k :: nat
```
```   314   apply (induct k)
```
```   315    apply simp
```
```   316   apply (drule comp_inj_on[OF _ inj_Suc])
```
```   317   apply (simp add: o_def)
```
```   318   done
```
```   319
```
```   320 lemma Suc_eq_plus1: "Suc n = n + 1"
```
```   321   unfolding One_nat_def by simp
```
```   322
```
```   323 lemma Suc_eq_plus1_left: "Suc n = 1 + n"
```
```   324   unfolding One_nat_def by simp
```
```   325
```
```   326
```
```   327 subsubsection \<open>Difference\<close>
```
```   328
```
```   329 lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
```
```   330   by (simp add: diff_diff_add)
```
```   331
```
```   332 lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
```
```   333   unfolding One_nat_def by simp
```
```   334
```
```   335 subsubsection \<open>Multiplication\<close>
```
```   336
```
```   337 lemma mult_is_0 [simp]: "m * n = 0 \<longleftrightarrow> m = 0 \<or> n = 0" for m n :: nat
```
```   338   by (induct m) auto
```
```   339
```
```   340 lemma mult_eq_1_iff [simp]: "m * n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
```
```   341   apply (induct m)
```
```   342    apply simp
```
```   343   apply (induct n)
```
```   344    apply auto
```
```   345   done
```
```   346
```
```   347 lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
```
```   348   apply (rule trans)
```
```   349   apply (rule_tac [2] mult_eq_1_iff, fastforce)
```
```   350   done
```
```   351
```
```   352 lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
```
```   353   unfolding One_nat_def by (rule mult_eq_1_iff)
```
```   354
```
```   355 lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
```
```   356   unfolding One_nat_def by (rule one_eq_mult_iff)
```
```   357
```
```   358 lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0" for k m n :: nat
```
```   359 proof -
```
```   360   have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
```
```   361   proof (induct n arbitrary: m)
```
```   362     case 0
```
```   363     then show "m = 0" by simp
```
```   364   next
```
```   365     case (Suc n)
```
```   366     then show "m = Suc n"
```
```   367       by (cases m) (simp_all add: eq_commute [of 0])
```
```   368   qed
```
```   369   then show ?thesis by auto
```
```   370 qed
```
```   371
```
```   372 lemma mult_cancel2 [simp]: "m * k = n * k \<longleftrightarrow> m = n \<or> k = 0" for k m n :: nat
```
```   373   by (simp add: mult.commute)
```
```   374
```
```   375 lemma Suc_mult_cancel1: "Suc k * m = Suc k * n \<longleftrightarrow> m = n"
```
```   376   by (subst mult_cancel1) simp
```
```   377
```
```   378
```
```   379 subsection \<open>Orders on @{typ nat}\<close>
```
```   380
```
```   381 subsubsection \<open>Operation definition\<close>
```
```   382
```
```   383 instantiation nat :: linorder
```
```   384 begin
```
```   385
```
```   386 primrec less_eq_nat where
```
```   387   "(0::nat) \<le> n \<longleftrightarrow> True"
```
```   388 | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
```
```   389
```
```   390 declare less_eq_nat.simps [simp del]
```
```   391
```
```   392 lemma le0 [iff]: "0 \<le> n" for n :: nat
```
```   393   by (simp add: less_eq_nat.simps)
```
```   394
```
```   395 lemma [code]: "0 \<le> n \<longleftrightarrow> True" for n :: nat
```
```   396   by simp
```
```   397
```
```   398 definition less_nat where
```
```   399   less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
```
```   400
```
```   401 lemma Suc_le_mono [iff]: "Suc n \<le> Suc m \<longleftrightarrow> n \<le> m"
```
```   402   by (simp add: less_eq_nat.simps(2))
```
```   403
```
```   404 lemma Suc_le_eq [code]: "Suc m \<le> n \<longleftrightarrow> m < n"
```
```   405   unfolding less_eq_Suc_le ..
```
```   406
```
```   407 lemma le_0_eq [iff]: "n \<le> 0 \<longleftrightarrow> n = 0" for n :: nat
```
```   408   by (induct n) (simp_all add: less_eq_nat.simps(2))
```
```   409
```
```   410 lemma not_less0 [iff]: "\<not> n < 0" for n :: nat
```
```   411   by (simp add: less_eq_Suc_le)
```
```   412
```
```   413 lemma less_nat_zero_code [code]: "n < 0 \<longleftrightarrow> False" for n :: nat
```
```   414   by simp
```
```   415
```
```   416 lemma Suc_less_eq [iff]: "Suc m < Suc n \<longleftrightarrow> m < n"
```
```   417   by (simp add: less_eq_Suc_le)
```
```   418
```
```   419 lemma less_Suc_eq_le [code]: "m < Suc n \<longleftrightarrow> m \<le> n"
```
```   420   by (simp add: less_eq_Suc_le)
```
```   421
```
```   422 lemma Suc_less_eq2: "Suc n < m \<longleftrightarrow> (\<exists>m'. m = Suc m' \<and> n < m')"
```
```   423   by (cases m) auto
```
```   424
```
```   425 lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n"
```
```   426   by (induct m arbitrary: n) (simp_all add: less_eq_nat.simps(2) split: nat.splits)
```
```   427
```
```   428 lemma Suc_leD: "Suc m \<le> n \<Longrightarrow> m \<le> n"
```
```   429   by (cases n) (auto intro: le_SucI)
```
```   430
```
```   431 lemma less_SucI: "m < n \<Longrightarrow> m < Suc n"
```
```   432   by (simp add: less_eq_Suc_le) (erule Suc_leD)
```
```   433
```
```   434 lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n"
```
```   435   by (simp add: less_eq_Suc_le) (erule Suc_leD)
```
```   436
```
```   437 instance
```
```   438 proof
```
```   439   fix n m q :: nat
```
```   440   show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
```
```   441   proof (induct n arbitrary: m)
```
```   442     case 0
```
```   443     then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
```
```   444   next
```
```   445     case (Suc n)
```
```   446     then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
```
```   447   qed
```
```   448   show "n \<le> n" by (induct n) simp_all
```
```   449   then show "n = m" if "n \<le> m" and "m \<le> n"
```
```   450     using that by (induct n arbitrary: m)
```
```   451       (simp_all add: less_eq_nat.simps(2) split: nat.splits)
```
```   452   show "n \<le> q" if "n \<le> m" and "m \<le> q"
```
```   453     using that
```
```   454   proof (induct n arbitrary: m q)
```
```   455     case 0
```
```   456     show ?case by simp
```
```   457   next
```
```   458     case (Suc n)
```
```   459     then show ?case
```
```   460       by (simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
```
```   461         simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
```
```   462         simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits)
```
```   463   qed
```
```   464   show "n \<le> m \<or> m \<le> n"
```
```   465     by (induct n arbitrary: m)
```
```   466       (simp_all add: less_eq_nat.simps(2) split: nat.splits)
```
```   467 qed
```
```   468
```
```   469 end
```
```   470
```
```   471 instantiation nat :: order_bot
```
```   472 begin
```
```   473
```
```   474 definition bot_nat :: nat where "bot_nat = 0"
```
```   475
```
```   476 instance by standard (simp add: bot_nat_def)
```
```   477
```
```   478 end
```
```   479
```
```   480 instance nat :: no_top
```
```   481   by standard (auto intro: less_Suc_eq_le [THEN iffD2])
```
```   482
```
```   483
```
```   484 subsubsection \<open>Introduction properties\<close>
```
```   485
```
```   486 lemma lessI [iff]: "n < Suc n"
```
```   487   by (simp add: less_Suc_eq_le)
```
```   488
```
```   489 lemma zero_less_Suc [iff]: "0 < Suc n"
```
```   490   by (simp add: less_Suc_eq_le)
```
```   491
```
```   492
```
```   493 subsubsection \<open>Elimination properties\<close>
```
```   494
```
```   495 lemma less_not_refl: "\<not> n < n" for n :: nat
```
```   496   by (rule order_less_irrefl)
```
```   497
```
```   498 lemma less_not_refl2: "n < m \<Longrightarrow> m \<noteq> n" for m n :: nat
```
```   499   by (rule not_sym) (rule less_imp_neq)
```
```   500
```
```   501 lemma less_not_refl3: "s < t \<Longrightarrow> s \<noteq> t" for s t :: nat
```
```   502   by (rule less_imp_neq)
```
```   503
```
```   504 lemma less_irrefl_nat: "n < n \<Longrightarrow> R" for n :: nat
```
```   505   by (rule notE, rule less_not_refl)
```
```   506
```
```   507 lemma less_zeroE: "n < 0 \<Longrightarrow> R" for n :: nat
```
```   508   by (rule notE) (rule not_less0)
```
```   509
```
```   510 lemma less_Suc_eq: "m < Suc n \<longleftrightarrow> m < n \<or> m = n"
```
```   511   unfolding less_Suc_eq_le le_less ..
```
```   512
```
```   513 lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
```
```   514   by (simp add: less_Suc_eq)
```
```   515
```
```   516 lemma less_one [iff]: "n < 1 \<longleftrightarrow> n = 0" for n :: nat
```
```   517   unfolding One_nat_def by (rule less_Suc0)
```
```   518
```
```   519 lemma Suc_mono: "m < n \<Longrightarrow> Suc m < Suc n"
```
```   520   by simp
```
```   521
```
```   522 text \<open>"Less than" is antisymmetric, sort of\<close>
```
```   523 lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
```
```   524   unfolding not_less less_Suc_eq_le by (rule antisym)
```
```   525
```
```   526 lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat
```
```   527   by (rule linorder_neq_iff)
```
```   528
```
```   529
```
```   530 subsubsection \<open>Inductive (?) properties\<close>
```
```   531
```
```   532 lemma Suc_lessI: "m < n \<Longrightarrow> Suc m \<noteq> n \<Longrightarrow> Suc m < n"
```
```   533   unfolding less_eq_Suc_le [of m] le_less by simp
```
```   534
```
```   535 lemma lessE:
```
```   536   assumes major: "i < k"
```
```   537     and 1: "k = Suc i \<Longrightarrow> P"
```
```   538     and 2: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
```
```   539   shows P
```
```   540 proof -
```
```   541   from major have "\<exists>j. i \<le> j \<and> k = Suc j"
```
```   542     unfolding less_eq_Suc_le by (induct k) simp_all
```
```   543   then have "(\<exists>j. i < j \<and> k = Suc j) \<or> k = Suc i"
```
```   544     by (auto simp add: less_le)
```
```   545   with 1 2 show P by auto
```
```   546 qed
```
```   547
```
```   548 lemma less_SucE:
```
```   549   assumes major: "m < Suc n"
```
```   550     and less: "m < n \<Longrightarrow> P"
```
```   551     and eq: "m = n \<Longrightarrow> P"
```
```   552   shows P
```
```   553   apply (rule major [THEN lessE])
```
```   554   apply (rule eq, blast)
```
```   555   apply (rule less, blast)
```
```   556   done
```
```   557
```
```   558 lemma Suc_lessE:
```
```   559   assumes major: "Suc i < k"
```
```   560     and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
```
```   561   shows P
```
```   562   apply (rule major [THEN lessE])
```
```   563   apply (erule lessI [THEN minor])
```
```   564   apply (erule Suc_lessD [THEN minor], assumption)
```
```   565   done
```
```   566
```
```   567 lemma Suc_less_SucD: "Suc m < Suc n \<Longrightarrow> m < n"
```
```   568   by simp
```
```   569
```
```   570 lemma less_trans_Suc:
```
```   571   assumes le: "i < j"
```
```   572   shows "j < k \<Longrightarrow> Suc i < k"
```
```   573   apply (induct k, simp_all)
```
```   574   using le
```
```   575   apply (simp add: less_Suc_eq)
```
```   576   apply (blast dest: Suc_lessD)
```
```   577   done
```
```   578
```
```   579 text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{prop "n = m \<or> n < m"}\<close>
```
```   580 lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m"
```
```   581   unfolding not_less less_Suc_eq_le ..
```
```   582
```
```   583 lemma not_less_eq_eq: "\<not> m \<le> n \<longleftrightarrow> Suc n \<le> m"
```
```   584   unfolding not_le Suc_le_eq ..
```
```   585
```
```   586 text \<open>Properties of "less than or equal"\<close>
```
```   587
```
```   588 lemma le_imp_less_Suc: "m \<le> n \<Longrightarrow> m < Suc n"
```
```   589   unfolding less_Suc_eq_le .
```
```   590
```
```   591 lemma Suc_n_not_le_n: "\<not> Suc n \<le> n"
```
```   592   unfolding not_le less_Suc_eq_le ..
```
```   593
```
```   594 lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
```
```   595   by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq)
```
```   596
```
```   597 lemma le_SucE: "m \<le> Suc n \<Longrightarrow> (m \<le> n \<Longrightarrow> R) \<Longrightarrow> (m = Suc n \<Longrightarrow> R) \<Longrightarrow> R"
```
```   598   by (drule le_Suc_eq [THEN iffD1], iprover+)
```
```   599
```
```   600 lemma Suc_leI: "m < n \<Longrightarrow> Suc(m) \<le> n"
```
```   601   unfolding Suc_le_eq .
```
```   602
```
```   603 text \<open>Stronger version of \<open>Suc_leD\<close>\<close>
```
```   604 lemma Suc_le_lessD: "Suc m \<le> n \<Longrightarrow> m < n"
```
```   605   unfolding Suc_le_eq .
```
```   606
```
```   607 lemma less_imp_le_nat: "m < n \<Longrightarrow> m \<le> n" for m n :: nat
```
```   608   unfolding less_eq_Suc_le by (rule Suc_leD)
```
```   609
```
```   610 text \<open>For instance, \<open>(Suc m < Suc n) = (Suc m \<le> n) = (m < n)\<close>\<close>
```
```   611 lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
```
```   612
```
```   613
```
```   614 text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close>
```
```   615
```
```   616 lemma less_or_eq_imp_le: "m < n \<or> m = n \<Longrightarrow> m \<le> n" for m n :: nat
```
```   617   unfolding le_less .
```
```   618
```
```   619 lemma le_eq_less_or_eq: "m \<le> n \<longleftrightarrow> m < n \<or> m = n" for m n :: nat
```
```   620   by (rule le_less)
```
```   621
```
```   622 text \<open>Useful with \<open>blast\<close>.\<close>
```
```   623 lemma eq_imp_le: "m = n \<Longrightarrow> m \<le> n" for m n :: nat
```
```   624   by auto
```
```   625
```
```   626 lemma le_refl: "n \<le> n" for n :: nat
```
```   627   by simp
```
```   628
```
```   629 lemma le_trans: "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" for i j k :: nat
```
```   630   by (rule order_trans)
```
```   631
```
```   632 lemma le_antisym: "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n" for m n :: nat
```
```   633   by (rule antisym)
```
```   634
```
```   635 lemma nat_less_le: "m < n \<longleftrightarrow> m \<le> n \<and> m \<noteq> n" for m n :: nat
```
```   636   by (rule less_le)
```
```   637
```
```   638 lemma le_neq_implies_less: "m \<le> n \<Longrightarrow> m \<noteq> n \<Longrightarrow> m < n" for m n :: nat
```
```   639   unfolding less_le ..
```
```   640
```
```   641 lemma nat_le_linear: "m \<le> n | n \<le> m" for m n :: nat
```
```   642   by (rule linear)
```
```   643
```
```   644 lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
```
```   645
```
```   646 lemma le_less_Suc_eq: "m \<le> n \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m"
```
```   647   unfolding less_Suc_eq_le by auto
```
```   648
```
```   649 lemma not_less_less_Suc_eq: "\<not> n < m \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m"
```
```   650   unfolding not_less by (rule le_less_Suc_eq)
```
```   651
```
```   652 lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
```
```   653
```
```   654 lemma not0_implies_Suc: "n \<noteq> 0 \<Longrightarrow> \<exists>m. n = Suc m"
```
```   655   by (cases n) simp_all
```
```   656
```
```   657 lemma gr0_implies_Suc: "n > 0 \<Longrightarrow> \<exists>m. n = Suc m"
```
```   658   by (cases n) simp_all
```
```   659
```
```   660 lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0" for m n :: nat
```
```   661   by (cases n) simp_all
```
```   662
```
```   663 lemma neq0_conv[iff]: "n \<noteq> 0 \<longleftrightarrow> 0 < n" for n :: nat
```
```   664   by (cases n) simp_all
```
```   665
```
```   666 text \<open>This theorem is useful with \<open>blast\<close>\<close>
```
```   667 lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n" for n :: nat
```
```   668   by (rule neq0_conv[THEN iffD1], iprover)
```
```   669
```
```   670 lemma gr0_conv_Suc: "0 < n \<longleftrightarrow> (\<exists>m. n = Suc m)"
```
```   671   by (fast intro: not0_implies_Suc)
```
```   672
```
```   673 lemma not_gr0 [iff]: "\<not> 0 < n \<longleftrightarrow> n = 0" for n :: nat
```
```   674   using neq0_conv by blast
```
```   675
```
```   676 lemma Suc_le_D: "Suc n \<le> m' \<Longrightarrow> \<exists>m. m' = Suc m"
```
```   677   by (induct m') simp_all
```
```   678
```
```   679 text \<open>Useful in certain inductive arguments\<close>
```
```   680 lemma less_Suc_eq_0_disj: "m < Suc n \<longleftrightarrow> m = 0 \<or> (\<exists>j. m = Suc j \<and> j < n)"
```
```   681   by (cases m) simp_all
```
```   682
```
```   683
```
```   684 subsubsection \<open>Monotonicity of Addition\<close>
```
```   685
```
```   686 lemma Suc_pred [simp]: "n > 0 \<Longrightarrow> Suc (n - Suc 0) = n"
```
```   687   by (simp add: diff_Suc split: nat.split)
```
```   688
```
```   689 lemma Suc_diff_1 [simp]: "0 < n \<Longrightarrow> Suc (n - 1) = n"
```
```   690   unfolding One_nat_def by (rule Suc_pred)
```
```   691
```
```   692 lemma nat_add_left_cancel_le [simp]: "k + m \<le> k + n \<longleftrightarrow> m \<le> n" for k m n :: nat
```
```   693   by (induct k) simp_all
```
```   694
```
```   695 lemma nat_add_left_cancel_less [simp]: "k + m < k + n \<longleftrightarrow> m < n" for k m n :: nat
```
```   696   by (induct k) simp_all
```
```   697
```
```   698 lemma add_gr_0 [iff]: "m + n > 0 \<longleftrightarrow> m > 0 \<or> n > 0" for m n :: nat
```
```   699   by (auto dest: gr0_implies_Suc)
```
```   700
```
```   701 text \<open>strict, in 1st argument\<close>
```
```   702 lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k" for i j k :: nat
```
```   703   by (induct k) simp_all
```
```   704
```
```   705 text \<open>strict, in both arguments\<close>
```
```   706 lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l" for i j k l :: nat
```
```   707   apply (rule add_less_mono1 [THEN less_trans], assumption+)
```
```   708   apply (induct j, simp_all)
```
```   709   done
```
```   710
```
```   711 text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close>
```
```   712 lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)"
```
```   713   apply (induct n)
```
```   714   apply (simp_all add: order_le_less)
```
```   715   apply (blast elim!: less_SucE
```
```   716                intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
```
```   717   done
```
```   718
```
```   719 lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)" for k l :: nat
```
```   720   by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
```
```   721
```
```   722 text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
```
```   723 lemma mult_less_mono2:
```
```   724   fixes i j :: nat
```
```   725   assumes "i < j" and "0 < k"
```
```   726   shows "k * i < k * j"
```
```   727   using \<open>0 < k\<close>
```
```   728 proof (induct k)
```
```   729   case 0
```
```   730   then show ?case by simp
```
```   731 next
```
```   732   case (Suc k)
```
```   733   with \<open>i < j\<close> show ?case
```
```   734     by (cases k) (simp_all add: add_less_mono)
```
```   735 qed
```
```   736
```
```   737 text \<open>Addition is the inverse of subtraction:
```
```   738   if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close>
```
```   739 lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m - n) = m" for m n :: nat
```
```   740   by (induct m n rule: diff_induct) simp_all
```
```   741
```
```   742 lemma nat_le_iff_add: "m \<le> n \<longleftrightarrow> (\<exists>k. n = m + k)" for m n :: nat
```
```   743   using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)
```
```   744
```
```   745 text\<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>\<close>
```
```   746
```
```   747 instance nat :: linordered_semidom
```
```   748 proof
```
```   749   fix m n q :: nat
```
```   750   show "0 < (1::nat)" by simp
```
```   751   show "m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
```
```   752   show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
```
```   753   show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
```
```   754   show "n \<le> m \<Longrightarrow> (m - n) + n = m"
```
```   755     by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
```
```   756 qed
```
```   757
```
```   758 instance nat :: dioid
```
```   759   by standard (rule nat_le_iff_add)
```
```   760 declare le0[simp del] -- \<open>This is now @{thm zero_le}\<close>
```
```   761 declare le_0_eq[simp del] -- \<open>This is now @{thm le_zero_eq}\<close>
```
```   762 declare not_less0[simp del] -- \<open>This is now @{thm not_less_zero}\<close>
```
```   763 declare not_gr0[simp del] -- \<open>This is now @{thm not_gr_zero}\<close>
```
```   764
```
```   765 instance nat :: ordered_cancel_comm_monoid_add ..
```
```   766 instance nat :: ordered_cancel_comm_monoid_diff ..
```
```   767
```
```   768
```
```   769 subsubsection \<open>@{term min} and @{term max}\<close>
```
```   770
```
```   771 lemma mono_Suc: "mono Suc"
```
```   772   by (rule monoI) simp
```
```   773
```
```   774 lemma min_0L [simp]: "min 0 n = 0" for n :: nat
```
```   775   by (rule min_absorb1) simp
```
```   776
```
```   777 lemma min_0R [simp]: "min n 0 = 0" for n :: nat
```
```   778   by (rule min_absorb2) simp
```
```   779
```
```   780 lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
```
```   781   by (simp add: mono_Suc min_of_mono)
```
```   782
```
```   783 lemma min_Suc1: "min (Suc n) m = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min n m'))"
```
```   784   by (simp split: nat.split)
```
```   785
```
```   786 lemma min_Suc2: "min m (Suc n) = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min m' n))"
```
```   787   by (simp split: nat.split)
```
```   788
```
```   789 lemma max_0L [simp]: "max 0 n = n" for n :: nat
```
```   790   by (rule max_absorb2) simp
```
```   791
```
```   792 lemma max_0R [simp]: "max n 0 = n" for n :: nat
```
```   793   by (rule max_absorb1) simp
```
```   794
```
```   795 lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)"
```
```   796   by (simp add: mono_Suc max_of_mono)
```
```   797
```
```   798 lemma max_Suc1: "max (Suc n) m = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max n m'))"
```
```   799   by (simp split: nat.split)
```
```   800
```
```   801 lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
```
```   802   by (simp split: nat.split)
```
```   803
```
```   804 lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)" for m n q :: nat
```
```   805   by (simp add: min_def not_le)
```
```   806     (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
```
```   807
```
```   808 lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)" for m n q :: nat
```
```   809   by (simp add: min_def not_le)
```
```   810     (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
```
```   811
```
```   812 lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)" for m n q :: nat
```
```   813   by (simp add: max_def)
```
```   814
```
```   815 lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)" for m n q :: nat
```
```   816   by (simp add: max_def)
```
```   817
```
```   818 lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)" for m n q :: nat
```
```   819   by (simp add: max_def not_le)
```
```   820     (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
```
```   821
```
```   822 lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)" for m n q :: nat
```
```   823   by (simp add: max_def not_le)
```
```   824     (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
```
```   825
```
```   826
```
```   827 subsubsection \<open>Additional theorems about @{term "op \<le>"}\<close>
```
```   828
```
```   829 text \<open>Complete induction, aka course-of-values induction\<close>
```
```   830
```
```   831 instance nat :: wellorder
```
```   832 proof
```
```   833   fix P and n :: nat
```
```   834   assume step: "(\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n" for n :: nat
```
```   835   have "\<And>q. q \<le> n \<Longrightarrow> P q"
```
```   836   proof (induct n)
```
```   837     case (0 n)
```
```   838     have "P 0" by (rule step) auto
```
```   839     then show ?case using 0 by auto
```
```   840   next
```
```   841     case (Suc m n)
```
```   842     then have "n \<le> m \<or> n = Suc m" by (simp add: le_Suc_eq)
```
```   843     then show ?case
```
```   844     proof
```
```   845       assume "n \<le> m"
```
```   846       then show "P n" by (rule Suc(1))
```
```   847     next
```
```   848       assume n: "n = Suc m"
```
```   849       show "P n" by (rule step) (rule Suc(1), simp add: n le_simps)
```
```   850     qed
```
```   851   qed
```
```   852   then show "P n" by auto
```
```   853 qed
```
```   854
```
```   855
```
```   856 lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0" for P :: "nat \<Rightarrow> bool"
```
```   857   by (rule Least_equality[OF _ le0])
```
```   858
```
```   859 lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
```
```   860   apply (cases n, auto)
```
```   861   apply (frule LeastI)
```
```   862   apply (drule_tac P = "\<lambda>x. P (Suc x) " in LeastI)
```
```   863   apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
```
```   864   apply (erule_tac [2] Least_le)
```
```   865   apply (cases "LEAST x. P x", auto)
```
```   866   apply (drule_tac P = "\<lambda>x. P (Suc x) " in Least_le)
```
```   867   apply (blast intro: order_antisym)
```
```   868   done
```
```   869
```
```   870 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)"
```
```   871   apply (erule (1) Least_Suc [THEN ssubst])
```
```   872   apply simp
```
```   873   done
```
```   874
```
```   875 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"
```
```   876   apply (cases n)
```
```   877    apply blast
```
```   878   apply (rule_tac x="LEAST k. P k" in exI)
```
```   879   apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
```
```   880   done
```
```   881
```
```   882 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"
```
```   883   unfolding One_nat_def
```
```   884   apply (cases n)
```
```   885    apply blast
```
```   886   apply (frule (1) ex_least_nat_le)
```
```   887   apply (erule exE)
```
```   888   apply (case_tac k)
```
```   889    apply simp
```
```   890   apply (rename_tac k1)
```
```   891   apply (rule_tac x=k1 in exI)
```
```   892   apply (auto simp add: less_eq_Suc_le)
```
```   893   done
```
```   894
```
```   895 lemma nat_less_induct:
```
```   896   fixes P :: "nat \<Rightarrow> bool"
```
```   897   assumes "\<And>n. \<forall>m. m < n \<longrightarrow> P m \<Longrightarrow> P n"
```
```   898   shows "P n"
```
```   899   using assms less_induct by blast
```
```   900
```
```   901 lemma measure_induct_rule [case_names less]:
```
```   902   fixes f :: "'a \<Rightarrow> nat"
```
```   903   assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
```
```   904   shows "P a"
```
```   905   by (induct m \<equiv> "f a" arbitrary: a rule: less_induct) (auto intro: step)
```
```   906
```
```   907 text \<open>old style induction rules:\<close>
```
```   908 lemma measure_induct:
```
```   909   fixes f :: "'a \<Rightarrow> nat"
```
```   910   shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
```
```   911   by (rule measure_induct_rule [of f P a]) iprover
```
```   912
```
```   913 lemma full_nat_induct:
```
```   914   assumes step: "\<And>n. (\<forall>m. Suc m \<le> n \<longrightarrow> P m) \<Longrightarrow> P n"
```
```   915   shows "P n"
```
```   916   by (rule less_induct) (auto intro: step simp:le_simps)
```
```   917
```
```   918 text\<open>An induction rule for establishing binary relations\<close>
```
```   919 lemma less_Suc_induct [consumes 1]:
```
```   920   assumes less: "i < j"
```
```   921     and step: "\<And>i. P i (Suc i)"
```
```   922     and trans: "\<And>i j k. i < j \<Longrightarrow> j < k \<Longrightarrow> P i j \<Longrightarrow> P j k \<Longrightarrow> P i k"
```
```   923   shows "P i j"
```
```   924 proof -
```
```   925   from less obtain k where j: "j = Suc (i + k)"
```
```   926     by (auto dest: less_imp_Suc_add)
```
```   927   have "P i (Suc (i + k))"
```
```   928   proof (induct k)
```
```   929     case 0
```
```   930     show ?case by (simp add: step)
```
```   931   next
```
```   932     case (Suc k)
```
```   933     have "0 + i < Suc k + i" by (rule add_less_mono1) simp
```
```   934     then have "i < Suc (i + k)" by (simp add: add.commute)
```
```   935     from trans[OF this lessI Suc step]
```
```   936     show ?case by simp
```
```   937   qed
```
```   938   then show "P i j" by (simp add: j)
```
```   939 qed
```
```   940
```
```   941 text \<open>
```
```   942   The method of infinite descent, frequently used in number theory.
```
```   943   Provided by Roelof Oosterhuis.
```
```   944   \<open>P n\<close> is true for all natural numbers if
```
```   945   \<^item> case ``0'': given \<open>n = 0\<close> prove \<open>P n\<close>
```
```   946   \<^item> case ``smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists
```
```   947     a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>.
```
```   948 \<close>
```
```   949
```
```   950 lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool"
```
```   951   \<comment> \<open>compact version without explicit base case\<close>
```
```   952   by (induct n rule: less_induct) auto
```
```   953
```
```   954 lemma infinite_descent0 [case_names 0 smaller]:
```
```   955   fixes P :: "nat \<Rightarrow> bool"
```
```   956   assumes "P 0"
```
```   957     and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m"
```
```   958   shows "P n"
```
```   959   apply (rule infinite_descent)
```
```   960   using assms
```
```   961   apply (case_tac "n > 0")
```
```   962   apply auto
```
```   963   done
```
```   964
```
```   965 text \<open>
```
```   966   Infinite descent using a mapping to \<open>nat\<close>:
```
```   967   \<open>P x\<close> is true for all \<open>x \<in> D\<close> if there exists a \<open>V \<in> D \<Rightarrow> nat\<close> and
```
```   968   \<^item> case ``0'': given \<open>V x = 0\<close> prove \<open>P x\<close>
```
```   969   \<^item> ``smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove
```
```   970   there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>.
```
```   971 \<close>
```
```   972 corollary infinite_descent0_measure [case_names 0 smaller]:
```
```   973   fixes V :: "'a \<Rightarrow> nat"
```
```   974   assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x"
```
```   975     and 2: "\<And>x. V x > 0 \<Longrightarrow> \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y"
```
```   976   shows "P x"
```
```   977 proof -
```
```   978   obtain n where "n = V x" by auto
```
```   979   moreover have "\<And>x. V x = n \<Longrightarrow> P x"
```
```   980   proof (induct n rule: infinite_descent0)
```
```   981     case 0
```
```   982     with 1 show "P x" by auto
```
```   983   next
```
```   984     case (smaller n)
```
```   985     then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
```
```   986     with 2 obtain y where "V y < V x \<and> \<not> P y" by auto
```
```   987     with * obtain m where "m = V y \<and> m < n \<and> \<not> P y" by auto
```
```   988     then show ?case by auto
```
```   989   qed
```
```   990   ultimately show "P x" by auto
```
```   991 qed
```
```   992
```
```   993 text\<open>Again, without explicit base case:\<close>
```
```   994 lemma infinite_descent_measure:
```
```   995   fixes V :: "'a \<Rightarrow> nat"
```
```   996   assumes "\<And>x. \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y"
```
```   997   shows "P x"
```
```   998 proof -
```
```   999   from assms obtain n where "n = V x" by auto
```
```  1000   moreover have "\<And>x. V x = n \<Longrightarrow> P x"
```
```  1001   proof (induct n rule: infinite_descent, auto)
```
```  1002     show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x
```
```  1003       using assms and that by auto
```
```  1004   qed
```
```  1005   ultimately show "P x" by auto
```
```  1006 qed
```
```  1007
```
```  1008 text \<open>A (clumsy) way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close>
```
```  1009 lemma less_mono_imp_le_mono:
```
```  1010   fixes f :: "nat \<Rightarrow> nat"
```
```  1011     and i j :: nat
```
```  1012   assumes "\<And>i j::nat. i < j \<Longrightarrow> f i < f j"
```
```  1013     and "i \<le> j"
```
```  1014   shows "f i \<le> f j"
```
```  1015   using assms by (auto simp add: order_le_less)
```
```  1016
```
```  1017
```
```  1018 text \<open>non-strict, in 1st argument\<close>
```
```  1019 lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k" for i j k :: nat
```
```  1020   by (rule add_right_mono)
```
```  1021
```
```  1022 text \<open>non-strict, in both arguments\<close>
```
```  1023 lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l" for i j k l :: nat
```
```  1024   by (rule add_mono)
```
```  1025
```
```  1026 lemma le_add2: "n \<le> m + n" for m n :: nat
```
```  1027   by simp
```
```  1028
```
```  1029 lemma le_add1: "n \<le> n + m" for m n :: nat
```
```  1030   by simp
```
```  1031
```
```  1032 lemma less_add_Suc1: "i < Suc (i + m)"
```
```  1033   by (rule le_less_trans, rule le_add1, rule lessI)
```
```  1034
```
```  1035 lemma less_add_Suc2: "i < Suc (m + i)"
```
```  1036   by (rule le_less_trans, rule le_add2, rule lessI)
```
```  1037
```
```  1038 lemma less_iff_Suc_add: "m < n \<longleftrightarrow> (\<exists>k. n = Suc (m + k))"
```
```  1039   by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
```
```  1040
```
```  1041 lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m" for i j m :: nat
```
```  1042   by (rule le_trans, assumption, rule le_add1)
```
```  1043
```
```  1044 lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j" for i j m :: nat
```
```  1045   by (rule le_trans, assumption, rule le_add2)
```
```  1046
```
```  1047 lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m" for i j m :: nat
```
```  1048   by (rule less_le_trans, assumption, rule le_add1)
```
```  1049
```
```  1050 lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j" for i j m :: nat
```
```  1051   by (rule less_le_trans, assumption, rule le_add2)
```
```  1052
```
```  1053 lemma add_lessD1: "i + j < k \<Longrightarrow> i < k" for i j k :: nat
```
```  1054   by (rule le_less_trans [of _ "i+j"]) (simp_all add: le_add1)
```
```  1055
```
```  1056 lemma not_add_less1 [iff]: "\<not> i + j < i" for i j :: nat
```
```  1057   apply (rule notI)
```
```  1058   apply (drule add_lessD1)
```
```  1059   apply (erule less_irrefl [THEN notE])
```
```  1060   done
```
```  1061
```
```  1062 lemma not_add_less2 [iff]: "\<not> j + i < i" for i j :: nat
```
```  1063   by (simp add: add.commute)
```
```  1064
```
```  1065 lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n" for k m n :: nat
```
```  1066   by (rule order_trans [of _ "m+k"]) (simp_all add: le_add1)
```
```  1067
```
```  1068 lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n" for k m n :: nat
```
```  1069   apply (simp add: add.commute)
```
```  1070   apply (erule add_leD1)
```
```  1071   done
```
```  1072
```
```  1073 lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R" for k m n :: nat
```
```  1074   by (blast dest: add_leD1 add_leD2)
```
```  1075
```
```  1076 text \<open>needs \<open>\<And>k\<close> for \<open>ac_simps\<close> to work\<close>
```
```  1077 lemma less_add_eq_less: "\<And>k::nat. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n"
```
```  1078   by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
```
```  1079
```
```  1080
```
```  1081 subsubsection \<open>More results about difference\<close>
```
```  1082
```
```  1083 lemma Suc_diff_le: "n \<le> m \<Longrightarrow> Suc m - n = Suc (m - n)"
```
```  1084   by (induct m n rule: diff_induct) simp_all
```
```  1085
```
```  1086 lemma diff_less_Suc: "m - n < Suc m"
```
```  1087 apply (induct m n rule: diff_induct)
```
```  1088 apply (erule_tac [3] less_SucE)
```
```  1089 apply (simp_all add: less_Suc_eq)
```
```  1090 done
```
```  1091
```
```  1092 lemma diff_le_self [simp]: "m - n \<le> m" for m n :: nat
```
```  1093   by (induct m n rule: diff_induct) (simp_all add: le_SucI)
```
```  1094
```
```  1095 lemma less_imp_diff_less: "j < k \<Longrightarrow> j - n < k" for j k n :: nat
```
```  1096   by (rule le_less_trans, rule diff_le_self)
```
```  1097
```
```  1098 lemma diff_Suc_less [simp]: "0 < n \<Longrightarrow> n - Suc i < n"
```
```  1099   by (cases n) (auto simp add: le_simps)
```
```  1100
```
```  1101 lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j) - k = i + (j - k)" for i j k :: nat
```
```  1102   by (induct j k rule: diff_induct) simp_all
```
```  1103
```
```  1104 lemma add_diff_assoc [simp]: "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k" for i j k :: nat
```
```  1105   by (fact diff_add_assoc [symmetric])
```
```  1106
```
```  1107 lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i) - k = (j - k) + i" for i j k :: nat
```
```  1108   by (simp add: ac_simps)
```
```  1109
```
```  1110 lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j - k + i = j + i - k" for i j k :: nat
```
```  1111   by (fact diff_add_assoc2 [symmetric])
```
```  1112
```
```  1113 lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j - i = k) = (j = k + i)" for i j k :: nat
```
```  1114   by auto
```
```  1115
```
```  1116 lemma diff_is_0_eq [simp]: "m - n = 0 \<longleftrightarrow> m \<le> n" for m n :: nat
```
```  1117   by (induct m n rule: diff_induct) simp_all
```
```  1118
```
```  1119 lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0" for m n :: nat
```
```  1120   by (rule iffD2, rule diff_is_0_eq)
```
```  1121
```
```  1122 lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n" for m n :: nat
```
```  1123   by (induct m n rule: diff_induct) simp_all
```
```  1124
```
```  1125 lemma less_imp_add_positive:
```
```  1126   assumes "i < j"
```
```  1127   shows "\<exists>k::nat. 0 < k \<and> i + k = j"
```
```  1128 proof
```
```  1129   from assms show "0 < j - i \<and> i + (j - i) = j"
```
```  1130     by (simp add: order_less_imp_le)
```
```  1131 qed
```
```  1132
```
```  1133 text \<open>a nice rewrite for bounded subtraction\<close>
```
```  1134 lemma nat_minus_add_max: "n - m + m = max n m" for m n :: nat
```
```  1135     by (simp add: max_def not_le order_less_imp_le)
```
```  1136
```
```  1137 lemma nat_diff_split: "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)"
```
```  1138   for a b :: nat
```
```  1139     \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
```
```  1140   by (cases "a < b")
```
```  1141     (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym])
```
```  1142
```
```  1143 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))"
```
```  1144   for a b :: nat
```
```  1145     \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
```
```  1146   by (auto split: nat_diff_split)
```
```  1147
```
```  1148 lemma Suc_pred': "0 < n \<Longrightarrow> n = Suc(n - 1)"
```
```  1149   by simp
```
```  1150
```
```  1151 lemma add_eq_if: "m + n = (if m = 0 then n else Suc ((m - 1) + n))"
```
```  1152   unfolding One_nat_def by (cases m) simp_all
```
```  1153
```
```  1154 lemma mult_eq_if: "m * n = (if m = 0 then 0 else n + ((m - 1) * n))" for m n :: nat
```
```  1155   unfolding One_nat_def by (cases m) simp_all
```
```  1156
```
```  1157 lemma Suc_diff_eq_diff_pred: "0 < n \<Longrightarrow> Suc m - n = m - (n - 1)"
```
```  1158   unfolding One_nat_def by (cases n) simp_all
```
```  1159
```
```  1160 lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
```
```  1161   unfolding One_nat_def by (cases m) simp_all
```
```  1162
```
```  1163 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
```
```  1164   by (fact Let_def)
```
```  1165
```
```  1166
```
```  1167 subsubsection \<open>Monotonicity of multiplication\<close>
```
```  1168
```
```  1169 lemma mult_le_mono1: "i \<le> j \<Longrightarrow> i * k \<le> j * k" for i j k :: nat
```
```  1170   by (simp add: mult_right_mono)
```
```  1171
```
```  1172 lemma mult_le_mono2: "i \<le> j \<Longrightarrow> k * i \<le> k * j" for i j k :: nat
```
```  1173   by (simp add: mult_left_mono)
```
```  1174
```
```  1175 text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close>
```
```  1176 lemma mult_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i * k \<le> j * l" for i j k l :: nat
```
```  1177   by (simp add: mult_mono)
```
```  1178
```
```  1179 lemma mult_less_mono1: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> i * k < j * k" for i j k :: nat
```
```  1180   by (simp add: mult_strict_right_mono)
```
```  1181
```
```  1182 text\<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that
```
```  1183       there are no negative numbers.\<close>
```
```  1184 lemma nat_0_less_mult_iff [simp]: "0 < m * n \<longleftrightarrow> 0 < m \<and> 0 < n" for m n :: nat
```
```  1185   apply (induct m)
```
```  1186    apply simp
```
```  1187   apply (case_tac n)
```
```  1188    apply simp_all
```
```  1189   done
```
```  1190
```
```  1191 lemma one_le_mult_iff [simp]: "Suc 0 \<le> m * n \<longleftrightarrow> Suc 0 \<le> m \<and> Suc 0 \<le> n"
```
```  1192   apply (induct m)
```
```  1193    apply simp
```
```  1194   apply (case_tac n)
```
```  1195    apply simp_all
```
```  1196   done
```
```  1197
```
```  1198 lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat
```
```  1199   apply (safe intro!: mult_less_mono1)
```
```  1200   apply (cases k, auto)
```
```  1201   apply (simp add: linorder_not_le [symmetric])
```
```  1202   apply (blast intro: mult_le_mono1)
```
```  1203   done
```
```  1204
```
```  1205 lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat
```
```  1206   by (simp add: mult.commute [of k])
```
```  1207
```
```  1208 lemma mult_le_cancel1 [simp]: "k * m \<le> k * n \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat
```
```  1209   by (simp add: linorder_not_less [symmetric], auto)
```
```  1210
```
```  1211 lemma mult_le_cancel2 [simp]: "m * k \<le> n * k \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat
```
```  1212   by (simp add: linorder_not_less [symmetric], auto)
```
```  1213
```
```  1214 lemma Suc_mult_less_cancel1: "Suc k * m < Suc k * n \<longleftrightarrow> m < n"
```
```  1215   by (subst mult_less_cancel1) simp
```
```  1216
```
```  1217 lemma Suc_mult_le_cancel1: "Suc k * m \<le> Suc k * n \<longleftrightarrow> m \<le> n"
```
```  1218   by (subst mult_le_cancel1) simp
```
```  1219
```
```  1220 lemma le_square: "m \<le> m * m" for m :: nat
```
```  1221   by (cases m) (auto intro: le_add1)
```
```  1222
```
```  1223 lemma le_cube: "m \<le> m * (m * m)" for m :: nat
```
```  1224   by (cases m) (auto intro: le_add1)
```
```  1225
```
```  1226 text \<open>Lemma for \<open>gcd\<close>\<close>
```
```  1227 lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat
```
```  1228   apply (drule sym)
```
```  1229   apply (rule disjCI)
```
```  1230   apply (rule linorder_cases, erule_tac [2] _)
```
```  1231    apply (drule_tac [2] mult_less_mono2)
```
```  1232     apply (auto)
```
```  1233   done
```
```  1234
```
```  1235 lemma mono_times_nat:
```
```  1236   fixes n :: nat
```
```  1237   assumes "n > 0"
```
```  1238   shows "mono (times n)"
```
```  1239 proof
```
```  1240   fix m q :: nat
```
```  1241   assume "m \<le> q"
```
```  1242   with assms show "n * m \<le> n * q" by simp
```
```  1243 qed
```
```  1244
```
```  1245 text \<open>the lattice order on @{typ nat}\<close>
```
```  1246
```
```  1247 instantiation nat :: distrib_lattice
```
```  1248 begin
```
```  1249
```
```  1250 definition "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min"
```
```  1251
```
```  1252 definition "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max"
```
```  1253
```
```  1254 instance
```
```  1255   by intro_classes
```
```  1256     (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def
```
```  1257       intro: order_less_imp_le antisym elim!: order_trans order_less_trans)
```
```  1258
```
```  1259 end
```
```  1260
```
```  1261
```
```  1262 subsection \<open>Natural operation of natural numbers on functions\<close>
```
```  1263
```
```  1264 text \<open>
```
```  1265   We use the same logical constant for the power operations on
```
```  1266   functions and relations, in order to share the same syntax.
```
```  1267 \<close>
```
```  1268
```
```  1269 consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
```
```  1270
```
```  1271 abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80)
```
```  1272   where "f ^^ n \<equiv> compow n f"
```
```  1273
```
```  1274 notation (latex output)
```
```  1275   compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
```
```  1276
```
```  1277 text \<open>\<open>f ^^ n = f o ... o f\<close>, the n-fold composition of \<open>f\<close>\<close>
```
```  1278
```
```  1279 overloading
```
```  1280   funpow \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
```
```  1281 begin
```
```  1282
```
```  1283 primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
```
```  1284   "funpow 0 f = id"
```
```  1285 | "funpow (Suc n) f = f o funpow n f"
```
```  1286
```
```  1287 end
```
```  1288
```
```  1289 lemma funpow_0 [simp]: "(f ^^ 0) x = x"
```
```  1290   by simp
```
```  1291
```
```  1292 lemma funpow_Suc_right: "f ^^ Suc n = f ^^ n \<circ> f"
```
```  1293 proof (induct n)
```
```  1294   case 0
```
```  1295   then show ?case by simp
```
```  1296 next
```
```  1297   fix n
```
```  1298   assume "f ^^ Suc n = f ^^ n \<circ> f"
```
```  1299   then show "f ^^ Suc (Suc n) = f ^^ Suc n \<circ> f"
```
```  1300     by (simp add: o_assoc)
```
```  1301 qed
```
```  1302
```
```  1303 lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right
```
```  1304
```
```  1305 text \<open>for code generation\<close>
```
```  1306
```
```  1307 definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
```
```  1308   where funpow_code_def [code_abbrev]: "funpow = compow"
```
```  1309
```
```  1310 lemma [code]:
```
```  1311   "funpow (Suc n) f = f \<circ> funpow n f"
```
```  1312   "funpow 0 f = id"
```
```  1313   by (simp_all add: funpow_code_def)
```
```  1314
```
```  1315 hide_const (open) funpow
```
```  1316
```
```  1317 lemma funpow_add: "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
```
```  1318   by (induct m) simp_all
```
```  1319
```
```  1320 lemma funpow_mult: "(f ^^ m) ^^ n = f ^^ (m * n)" for f :: "'a \<Rightarrow> 'a"
```
```  1321   by (induct n) (simp_all add: funpow_add)
```
```  1322
```
```  1323 lemma funpow_swap1: "f ((f ^^ n) x) = (f ^^ n) (f x)"
```
```  1324 proof -
```
```  1325   have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp
```
```  1326   also have "\<dots>  = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
```
```  1327   also have "\<dots> = (f ^^ n) (f x)" by simp
```
```  1328   finally show ?thesis .
```
```  1329 qed
```
```  1330
```
```  1331 lemma comp_funpow: "comp f ^^ n = comp (f ^^ n)" for f :: "'a \<Rightarrow> 'a"
```
```  1332   by (induct n) simp_all
```
```  1333
```
```  1334 lemma Suc_funpow[simp]: "Suc ^^ n = (op + n)"
```
```  1335   by (induct n) simp_all
```
```  1336
```
```  1337 lemma id_funpow[simp]: "id ^^ n = id"
```
```  1338   by (induct n) simp_all
```
```  1339
```
```  1340 lemma funpow_mono: "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
```
```  1341   for f :: "'a \<Rightarrow> ('a::lattice)"
```
```  1342   by (induct n arbitrary: A B)
```
```  1343      (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
```
```  1344
```
```  1345
```
```  1346 subsection \<open>Kleene iteration\<close>
```
```  1347
```
```  1348 lemma Kleene_iter_lpfp:
```
```  1349   assumes "mono f"
```
```  1350     and "f p \<le> p"
```
```  1351   shows "(f^^k) (bot::'a::order_bot) \<le> p"
```
```  1352 proof(induction k)
```
```  1353   case 0
```
```  1354   show ?case by simp
```
```  1355 next
```
```  1356   case Suc
```
```  1357   from monoD[OF assms(1) Suc] assms(2) show ?case by simp
```
```  1358 qed
```
```  1359
```
```  1360 lemma lfp_Kleene_iter:
```
```  1361   assumes "mono f"
```
```  1362     and "(f^^Suc k) bot = (f^^k) bot"
```
```  1363   shows "lfp f = (f^^k) bot"
```
```  1364 proof (rule antisym)
```
```  1365   show "lfp f \<le> (f^^k) bot"
```
```  1366   proof (rule lfp_lowerbound)
```
```  1367     show "f ((f^^k) bot) \<le> (f^^k) bot"
```
```  1368       using assms(2) by simp
```
```  1369   qed
```
```  1370   show "(f^^k) bot \<le> lfp f"
```
```  1371     using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
```
```  1372 qed
```
```  1373
```
```  1374 lemma mono_pow: "mono f \<Longrightarrow> mono (f ^^ n)" for f :: "'a \<Rightarrow> 'a::complete_lattice"
```
```  1375   by (induct n) (auto simp: mono_def)
```
```  1376
```
```  1377 lemma lfp_funpow:
```
```  1378   assumes f: "mono f"
```
```  1379   shows "lfp (f ^^ Suc n) = lfp f"
```
```  1380 proof (rule antisym)
```
```  1381   show "lfp f \<le> lfp (f ^^ Suc n)"
```
```  1382   proof (rule lfp_lowerbound)
```
```  1383     have "f (lfp (f ^^ Suc n)) = lfp (\<lambda>x. f ((f ^^ n) x))"
```
```  1384       unfolding funpow_Suc_right by (simp add: lfp_rolling f mono_pow comp_def)
```
```  1385     then show "f (lfp (f ^^ Suc n)) \<le> lfp (f ^^ Suc n)"
```
```  1386       by (simp add: comp_def)
```
```  1387   qed
```
```  1388   have "(f^^n) (lfp f) = lfp f" for n
```
```  1389     by (induct n) (auto intro: f lfp_unfold[symmetric])
```
```  1390   then show "lfp (f^^Suc n) \<le> lfp f"
```
```  1391     by (intro lfp_lowerbound) (simp del: funpow.simps)
```
```  1392 qed
```
```  1393
```
```  1394 lemma gfp_funpow:
```
```  1395   assumes f: "mono f"
```
```  1396   shows "gfp (f ^^ Suc n) = gfp f"
```
```  1397 proof (rule antisym)
```
```  1398   show "gfp f \<ge> gfp (f ^^ Suc n)"
```
```  1399   proof (rule gfp_upperbound)
```
```  1400     have "f (gfp (f ^^ Suc n)) = gfp (\<lambda>x. f ((f ^^ n) x))"
```
```  1401       unfolding funpow_Suc_right by (simp add: gfp_rolling f mono_pow comp_def)
```
```  1402     then show "f (gfp (f ^^ Suc n)) \<ge> gfp (f ^^ Suc n)"
```
```  1403       by (simp add: comp_def)
```
```  1404   qed
```
```  1405   have "(f^^n) (gfp f) = gfp f" for n
```
```  1406     by (induct n) (auto intro: f gfp_unfold[symmetric])
```
```  1407   then show "gfp (f^^Suc n) \<ge> gfp f"
```
```  1408     by (intro gfp_upperbound) (simp del: funpow.simps)
```
```  1409 qed
```
```  1410
```
```  1411
```
```  1412 subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: @{term of_nat}\<close>
```
```  1413
```
```  1414 context semiring_1
```
```  1415 begin
```
```  1416
```
```  1417 definition of_nat :: "nat \<Rightarrow> 'a"
```
```  1418   where "of_nat n = (plus 1 ^^ n) 0"
```
```  1419
```
```  1420 lemma of_nat_simps [simp]:
```
```  1421   shows of_nat_0: "of_nat 0 = 0"
```
```  1422     and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
```
```  1423   by (simp_all add: of_nat_def)
```
```  1424
```
```  1425 lemma of_nat_1 [simp]: "of_nat 1 = 1"
```
```  1426   by (simp add: of_nat_def)
```
```  1427
```
```  1428 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
```
```  1429   by (induct m) (simp_all add: ac_simps)
```
```  1430
```
```  1431 lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n"
```
```  1432   by (induct m) (simp_all add: ac_simps distrib_right)
```
```  1433
```
```  1434 lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
```
```  1435   by (induct x) (simp_all add: algebra_simps)
```
```  1436
```
```  1437 primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
```
```  1438   "of_nat_aux inc 0 i = i"
```
```  1439 | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close>
```
```  1440
```
```  1441 lemma of_nat_code: "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
```
```  1442 proof (induct n)
```
```  1443   case 0
```
```  1444   then show ?case by simp
```
```  1445 next
```
```  1446   case (Suc n)
```
```  1447   have "\<And>i. of_nat_aux (\<lambda>i. i + 1) n (i + 1) = of_nat_aux (\<lambda>i. i + 1) n i + 1"
```
```  1448     by (induct n) simp_all
```
```  1449   from this [of 0] have "of_nat_aux (\<lambda>i. i + 1) n 1 = of_nat_aux (\<lambda>i. i + 1) n 0 + 1"
```
```  1450     by simp
```
```  1451   with Suc show ?case by (simp add: add.commute)
```
```  1452 qed
```
```  1453
```
```  1454 end
```
```  1455
```
```  1456 declare of_nat_code [code]
```
```  1457
```
```  1458 context ring_1
```
```  1459 begin
```
```  1460
```
```  1461 lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
```
```  1462   by (simp add: algebra_simps of_nat_add [symmetric])
```
```  1463
```
```  1464 end
```
```  1465
```
```  1466 text \<open>Class for unital semirings with characteristic zero.
```
```  1467  Includes non-ordered rings like the complex numbers.\<close>
```
```  1468
```
```  1469 class semiring_char_0 = semiring_1 +
```
```  1470   assumes inj_of_nat: "inj of_nat"
```
```  1471 begin
```
```  1472
```
```  1473 lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
```
```  1474   by (auto intro: inj_of_nat injD)
```
```  1475
```
```  1476 text \<open>Special cases where either operand is zero\<close>
```
```  1477
```
```  1478 lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
```
```  1479   by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
```
```  1480
```
```  1481 lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
```
```  1482   by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
```
```  1483
```
```  1484 lemma of_nat_neq_0 [simp]:
```
```  1485   "of_nat (Suc n) \<noteq> 0"
```
```  1486   unfolding of_nat_eq_0_iff by simp
```
```  1487
```
```  1488 lemma of_nat_0_neq [simp]:
```
```  1489   "0 \<noteq> of_nat (Suc n)"
```
```  1490   unfolding of_nat_0_eq_iff by simp
```
```  1491
```
```  1492 end
```
```  1493
```
```  1494 class ring_char_0 = ring_1 + semiring_char_0
```
```  1495
```
```  1496 context linordered_semidom
```
```  1497 begin
```
```  1498
```
```  1499 lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
```
```  1500   by (induct n) simp_all
```
```  1501
```
```  1502 lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
```
```  1503   by (simp add: not_less)
```
```  1504
```
```  1505 lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
```
```  1506   by (induct m n rule: diff_induct) (simp_all add: add_pos_nonneg)
```
```  1507
```
```  1508 lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
```
```  1509   by (simp add: not_less [symmetric] linorder_not_less [symmetric])
```
```  1510
```
```  1511 lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
```
```  1512   by simp
```
```  1513
```
```  1514 lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
```
```  1515   by simp
```
```  1516
```
```  1517 text \<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
```
```  1518
```
```  1519 subclass semiring_char_0
```
```  1520   by standard (auto intro!: injI simp add: eq_iff)
```
```  1521
```
```  1522 text \<open>Special cases where either operand is zero\<close>
```
```  1523
```
```  1524 lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
```
```  1525   by (rule of_nat_le_iff [of _ 0, simplified])
```
```  1526
```
```  1527 lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
```
```  1528   by (rule of_nat_less_iff [of 0, simplified])
```
```  1529
```
```  1530 end
```
```  1531
```
```  1532 context linordered_idom
```
```  1533 begin
```
```  1534
```
```  1535 lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"
```
```  1536   unfolding abs_if by auto
```
```  1537
```
```  1538 end
```
```  1539
```
```  1540 lemma of_nat_id [simp]: "of_nat n = n"
```
```  1541   by (induct n) simp_all
```
```  1542
```
```  1543 lemma of_nat_eq_id [simp]: "of_nat = id"
```
```  1544   by (auto simp add: fun_eq_iff)
```
```  1545
```
```  1546
```
```  1547 subsection \<open>The set of natural numbers\<close>
```
```  1548
```
```  1549 context semiring_1
```
```  1550 begin
```
```  1551
```
```  1552 definition Nats :: "'a set"  ("\<nat>")
```
```  1553   where "\<nat> = range of_nat"
```
```  1554
```
```  1555 lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
```
```  1556   by (simp add: Nats_def)
```
```  1557
```
```  1558 lemma Nats_0 [simp]: "0 \<in> \<nat>"
```
```  1559 apply (simp add: Nats_def)
```
```  1560 apply (rule range_eqI)
```
```  1561 apply (rule of_nat_0 [symmetric])
```
```  1562 done
```
```  1563
```
```  1564 lemma Nats_1 [simp]: "1 \<in> \<nat>"
```
```  1565 apply (simp add: Nats_def)
```
```  1566 apply (rule range_eqI)
```
```  1567 apply (rule of_nat_1 [symmetric])
```
```  1568 done
```
```  1569
```
```  1570 lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
```
```  1571 apply (auto simp add: Nats_def)
```
```  1572 apply (rule range_eqI)
```
```  1573 apply (rule of_nat_add [symmetric])
```
```  1574 done
```
```  1575
```
```  1576 lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
```
```  1577 apply (auto simp add: Nats_def)
```
```  1578 apply (rule range_eqI)
```
```  1579 apply (rule of_nat_mult [symmetric])
```
```  1580 done
```
```  1581
```
```  1582 lemma Nats_cases [cases set: Nats]:
```
```  1583   assumes "x \<in> \<nat>"
```
```  1584   obtains (of_nat) n where "x = of_nat n"
```
```  1585   unfolding Nats_def
```
```  1586 proof -
```
```  1587   from \<open>x \<in> \<nat>\<close> have "x \<in> range of_nat" unfolding Nats_def .
```
```  1588   then obtain n where "x = of_nat n" ..
```
```  1589   then show thesis ..
```
```  1590 qed
```
```  1591
```
```  1592 lemma Nats_induct [case_names of_nat, induct set: Nats]:
```
```  1593   "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x"
```
```  1594   by (rule Nats_cases) auto
```
```  1595
```
```  1596 end
```
```  1597
```
```  1598
```
```  1599 subsection \<open>Further arithmetic facts concerning the natural numbers\<close>
```
```  1600
```
```  1601 lemma subst_equals:
```
```  1602   assumes "t = s" and "u = t"
```
```  1603   shows "u = s"
```
```  1604   using assms(2,1) by (rule trans)
```
```  1605
```
```  1606 ML_file "Tools/nat_arith.ML"
```
```  1607
```
```  1608 simproc_setup nateq_cancel_sums
```
```  1609   ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
```
```  1610   \<open>fn phi => try o Nat_Arith.cancel_eq_conv\<close>
```
```  1611
```
```  1612 simproc_setup natless_cancel_sums
```
```  1613   ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
```
```  1614   \<open>fn phi => try o Nat_Arith.cancel_less_conv\<close>
```
```  1615
```
```  1616 simproc_setup natle_cancel_sums
```
```  1617   ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") =
```
```  1618   \<open>fn phi => try o Nat_Arith.cancel_le_conv\<close>
```
```  1619
```
```  1620 simproc_setup natdiff_cancel_sums
```
```  1621   ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
```
```  1622   \<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close>
```
```  1623
```
```  1624 context order
```
```  1625 begin
```
```  1626
```
```  1627 lemma lift_Suc_mono_le:
```
```  1628   assumes mono: "\<And>n. f n \<le> f (Suc n)" and "n \<le> n'"
```
```  1629   shows "f n \<le> f n'"
```
```  1630 proof (cases "n < n'")
```
```  1631   case True
```
```  1632   then show ?thesis
```
```  1633     by (induct n n' rule: less_Suc_induct) (auto intro: mono)
```
```  1634 next
```
```  1635   case False
```
```  1636   with \<open>n \<le> n'\<close> show ?thesis by auto
```
```  1637 qed
```
```  1638
```
```  1639 lemma lift_Suc_antimono_le:
```
```  1640   assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
```
```  1641   shows "f n \<ge> f n'"
```
```  1642 proof (cases "n < n'")
```
```  1643   case True
```
```  1644   then show ?thesis
```
```  1645     by (induct n n' rule: less_Suc_induct) (auto intro: mono)
```
```  1646 next
```
```  1647   case False
```
```  1648   with \<open>n \<le> n'\<close> show ?thesis by auto
```
```  1649 qed
```
```  1650
```
```  1651 lemma lift_Suc_mono_less:
```
```  1652   assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
```
```  1653   shows "f n < f n'"
```
```  1654   using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono)
```
```  1655
```
```  1656 lemma lift_Suc_mono_less_iff: "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"
```
```  1657   by (blast intro: less_asym' lift_Suc_mono_less [of f]
```
```  1658     dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq [THEN iffD1])
```
```  1659
```
```  1660 end
```
```  1661
```
```  1662 lemma mono_iff_le_Suc: "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
```
```  1663   unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
```
```  1664
```
```  1665 lemma antimono_iff_le_Suc: "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
```
```  1666   unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])
```
```  1667
```
```  1668 lemma mono_nat_linear_lb:
```
```  1669   fixes f :: "nat \<Rightarrow> nat"
```
```  1670   assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
```
```  1671   shows "f m + k \<le> f (m + k)"
```
```  1672 proof (induct k)
```
```  1673   case 0
```
```  1674   then show ?case by simp
```
```  1675 next
```
```  1676   case (Suc k)
```
```  1677   then have "Suc (f m + k) \<le> Suc (f (m + k))" by simp
```
```  1678   also from assms [of "m + k" "Suc (m + k)"] have "Suc (f (m + k)) \<le> f (Suc (m + k))"
```
```  1679     by (simp add: Suc_le_eq)
```
```  1680   finally show ?case by simp
```
```  1681 qed
```
```  1682
```
```  1683
```
```  1684 text \<open>Subtraction laws, mostly by Clemens Ballarin\<close>
```
```  1685
```
```  1686 lemma diff_less_mono:
```
```  1687   fixes a b c :: nat
```
```  1688   assumes "a < b" and "c \<le> a"
```
```  1689   shows "a - c < b - c"
```
```  1690 proof -
```
```  1691   from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0"
```
```  1692     by (auto dest!: le_Suc_ex less_imp_Suc_add simp add: ac_simps)
```
```  1693   then show ?thesis by simp
```
```  1694 qed
```
```  1695
```
```  1696 lemma less_diff_conv: "i < j - k \<longleftrightarrow> i + k < j" for i j k :: nat
```
```  1697   by (cases "k \<le> j") (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
```
```  1698
```
```  1699 lemma less_diff_conv2: "k \<le> j \<Longrightarrow> j - k < i \<longleftrightarrow> j < i + k" for j k i :: nat
```
```  1700   by (auto dest: le_Suc_ex)
```
```  1701
```
```  1702 lemma le_diff_conv: "j - k \<le> i \<longleftrightarrow> j \<le> i + k" for j k i :: nat
```
```  1703   by (cases "k \<le> j") (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
```
```  1704
```
```  1705 lemma diff_diff_cancel [simp]: "i \<le> n \<Longrightarrow> n - (n - i) = i" for i n :: nat
```
```  1706   by (auto dest: le_Suc_ex)
```
```  1707
```
```  1708 lemma diff_less [simp]: "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m" for i n :: nat
```
```  1709   by (auto dest: less_imp_Suc_add)
```
```  1710
```
```  1711 text \<open>Simplification of relational expressions involving subtraction\<close>
```
```  1712
```
```  1713 lemma diff_diff_eq: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n" for m n k :: nat
```
```  1714   by (auto dest!: le_Suc_ex)
```
```  1715
```
```  1716 hide_fact (open) diff_diff_eq
```
```  1717
```
```  1718 lemma eq_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n" for m n k :: nat
```
```  1719   by (auto dest: le_Suc_ex)
```
```  1720
```
```  1721 lemma less_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n" for m n k :: nat
```
```  1722   by (auto dest!: le_Suc_ex)
```
```  1723
```
```  1724 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
```
```  1725   by (auto dest!: le_Suc_ex)
```
```  1726
```
```  1727 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
```
```  1728   by (force dest: le_Suc_ex)
```
```  1729
```
```  1730
```
```  1731 text \<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
```
```  1732
```
```  1733 lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l" for m n l :: nat
```
```  1734   by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
```
```  1735
```
```  1736 lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m" for m n l :: nat
```
```  1737   by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
```
```  1738
```
```  1739 lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m" for m n l :: nat
```
```  1740   by (auto dest: less_imp_Suc_add split add: nat_diff_split)
```
```  1741
```
```  1742 lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n" for m n :: nat
```
```  1743   by (simp split add: nat_diff_split)
```
```  1744
```
```  1745 lemma min_diff: "min (m - i) (n - i) = min m n - i" for m n i :: nat
```
```  1746   by (cases m n rule: le_cases)
```
```  1747     (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono)
```
```  1748
```
```  1749 lemma inj_on_diff_nat:
```
```  1750   fixes k :: nat
```
```  1751   assumes "\<forall>n \<in> N. k \<le> n"
```
```  1752   shows "inj_on (\<lambda>n. n - k) N"
```
```  1753 proof (rule inj_onI)
```
```  1754   fix x y
```
```  1755   assume a: "x \<in> N" "y \<in> N" "x - k = y - k"
```
```  1756   with assms have "x - k + k = y - k + k" by auto
```
```  1757   with a assms show "x = y" by (auto simp add: eq_diff_iff)
```
```  1758 qed
```
```  1759
```
```  1760 text \<open>Rewriting to pull differences out\<close>
```
```  1761
```
```  1762 lemma diff_diff_right [simp]: "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j" for i j k :: nat
```
```  1763   by (fact diff_diff_right)
```
```  1764
```
```  1765 lemma diff_Suc_diff_eq1 [simp]:
```
```  1766   assumes "k \<le> j"
```
```  1767   shows "i - Suc (j - k) = i + k - Suc j"
```
```  1768 proof -
```
```  1769   from assms have *: "Suc (j - k) = Suc j - k"
```
```  1770     by (simp add: Suc_diff_le)
```
```  1771   from assms have "k \<le> Suc j"
```
```  1772     by (rule order_trans) simp
```
```  1773   with diff_diff_right [of k "Suc j" i] * show ?thesis
```
```  1774     by simp
```
```  1775 qed
```
```  1776
```
```  1777 lemma diff_Suc_diff_eq2 [simp]:
```
```  1778   assumes "k \<le> j"
```
```  1779   shows "Suc (j - k) - i = Suc j - (k + i)"
```
```  1780 proof -
```
```  1781   from assms obtain n where "j = k + n"
```
```  1782     by (auto dest: le_Suc_ex)
```
```  1783   moreover have "Suc n - i = (k + Suc n) - (k + i)"
```
```  1784     using add_diff_cancel_left [of k "Suc n" i] by simp
```
```  1785   ultimately show ?thesis by simp
```
```  1786 qed
```
```  1787
```
```  1788 lemma Suc_diff_Suc:
```
```  1789   assumes "n < m"
```
```  1790   shows "Suc (m - Suc n) = m - n"
```
```  1791 proof -
```
```  1792   from assms obtain q where "m = n + Suc q"
```
```  1793     by (auto dest: less_imp_Suc_add)
```
```  1794   moreover define r where "r = Suc q"
```
```  1795   ultimately have "Suc (m - Suc n) = r" and "m = n + r"
```
```  1796     by simp_all
```
```  1797   then show ?thesis by simp
```
```  1798 qed
```
```  1799
```
```  1800 lemma one_less_mult: "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
```
```  1801   using less_1_mult [of n m] by (simp add: ac_simps)
```
```  1802
```
```  1803 lemma n_less_m_mult_n: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
```
```  1804   using mult_strict_right_mono [of 1 m n] by simp
```
```  1805
```
```  1806 lemma n_less_n_mult_m: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
```
```  1807   using mult_strict_left_mono [of 1 m n] by simp
```
```  1808
```
```  1809
```
```  1810 text \<open>Specialized induction principles that work "backwards":\<close>
```
```  1811
```
```  1812 lemma inc_induct [consumes 1, case_names base step]:
```
```  1813   assumes less: "i \<le> j"
```
```  1814     and base: "P j"
```
```  1815     and step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
```
```  1816   shows "P i"
```
```  1817   using less step
```
```  1818 proof (induct "j - i" arbitrary: i)
```
```  1819   case (0 i)
```
```  1820   then have "i = j" by simp
```
```  1821   with base show ?case by simp
```
```  1822 next
```
```  1823   case (Suc d n)
```
```  1824   from Suc.hyps have "n \<noteq> j" by auto
```
```  1825   with Suc have "n < j" by (simp add: less_le)
```
```  1826   from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp
```
```  1827   then have "d + 1 - 1 = j - n - 1" by simp
```
```  1828   then have "d = j - n - 1" by simp
```
```  1829   then have "d = j - (n + 1)"
```
```  1830     by (simp add: diff_diff_eq)
```
```  1831   then have "d = j - Suc n"
```
```  1832     by simp
```
```  1833   moreover from \<open>n < j\<close> have "Suc n \<le> j"
```
```  1834     by (simp add: Suc_le_eq)
```
```  1835   ultimately have "P (Suc n)"
```
```  1836   proof (rule Suc.hyps)
```
```  1837     fix q
```
```  1838     assume "Suc n \<le> q"
```
```  1839     then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le)
```
```  1840     moreover assume "q < j"
```
```  1841     moreover assume "P (Suc q)"
```
```  1842     ultimately show "P q"
```
```  1843       by (rule Suc.prems)
```
```  1844   qed
```
```  1845   with order_refl \<open>n < j\<close> show "P n"
```
```  1846     by (rule Suc.prems)
```
```  1847 qed
```
```  1848
```
```  1849 lemma strict_inc_induct [consumes 1, case_names base step]:
```
```  1850   assumes less: "i < j"
```
```  1851     and base: "\<And>i. j = Suc i \<Longrightarrow> P i"
```
```  1852     and step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
```
```  1853   shows "P i"
```
```  1854 using less proof (induct "j - i - 1" arbitrary: i)
```
```  1855   case (0 i)
```
```  1856   from \<open>i < j\<close> obtain n where "j = i + n" and "n > 0"
```
```  1857     by (auto dest!: less_imp_Suc_add)
```
```  1858   with 0 have "j = Suc i"
```
```  1859     by (auto intro: order_antisym simp add: Suc_le_eq)
```
```  1860   with base show ?case by simp
```
```  1861 next
```
```  1862   case (Suc d i)
```
```  1863   from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i"
```
```  1864     by (simp add: diff_diff_add)
```
```  1865   then have "Suc d - 1 = j - Suc i - 1"
```
```  1866     by simp
```
```  1867   then have "d = j - Suc i - 1"
```
```  1868     by simp
```
```  1869   moreover from * have "j - Suc i \<noteq> 0"
```
```  1870     by auto
```
```  1871   then have "Suc i < j"
```
```  1872     by (simp add: not_le)
```
```  1873   ultimately have "P (Suc i)"
```
```  1874     by (rule Suc.hyps)
```
```  1875   with \<open>i < j\<close> show "P i" by (rule step)
```
```  1876 qed
```
```  1877
```
```  1878 lemma zero_induct_lemma: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P (k - i)"
```
```  1879   using inc_induct[of "k - i" k P, simplified] by blast
```
```  1880
```
```  1881 lemma zero_induct: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P 0"
```
```  1882   using inc_induct[of 0 k P] by blast
```
```  1883
```
```  1884 text \<open>Further induction rule similar to @{thm inc_induct}\<close>
```
```  1885
```
```  1886 lemma dec_induct [consumes 1, case_names base step]:
```
```  1887   "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"
```
```  1888 proof (induct j arbitrary: i)
```
```  1889   case 0
```
```  1890   then show ?case by simp
```
```  1891 next
```
```  1892   case (Suc j)
```
```  1893   from Suc.prems consider "i \<le> j" | "i = Suc j"
```
```  1894     by (auto simp add: le_Suc_eq)
```
```  1895   then show ?case
```
```  1896   proof cases
```
```  1897     case 1
```
```  1898     moreover have "j < Suc j" by simp
```
```  1899     moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close>
```
```  1900     proof (rule Suc.hyps)
```
```  1901       fix q
```
```  1902       assume "i \<le> q"
```
```  1903       moreover assume "q < j" then have "q < Suc j"
```
```  1904         by (simp add: less_Suc_eq)
```
```  1905       moreover assume "P q"
```
```  1906       ultimately show "P (Suc q)"
```
```  1907         by (rule Suc.prems)
```
```  1908     qed
```
```  1909     ultimately show "P (Suc j)"
```
```  1910       by (rule Suc.prems)
```
```  1911   next
```
```  1912     case 2
```
```  1913     with \<open>P i\<close> show "P (Suc j)" by simp
```
```  1914   qed
```
```  1915 qed
```
```  1916
```
```  1917
```
```  1918 subsection \<open>Monotonicity of \<open>funpow\<close>\<close>
```
```  1919
```
```  1920 lemma funpow_increasing:
```
```  1921   fixes f :: "'a \<Rightarrow> 'a::{lattice,order_top}"
```
```  1922   shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>"
```
```  1923   by (induct rule: inc_induct)
```
```  1924      (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
```
```  1925            intro: order_trans[OF _ funpow_mono])
```
```  1926
```
```  1927 lemma funpow_decreasing:
```
```  1928   fixes f :: "'a \<Rightarrow> 'a::{lattice,order_bot}"
```
```  1929   shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>"
```
```  1930   by (induct rule: dec_induct)
```
```  1931      (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
```
```  1932            intro: order_trans[OF _ funpow_mono])
```
```  1933
```
```  1934 lemma mono_funpow:
```
```  1935   fixes Q :: "'a::{lattice,order_bot} \<Rightarrow> 'a"
```
```  1936   shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
```
```  1937   by (auto intro!: funpow_decreasing simp: mono_def)
```
```  1938
```
```  1939 lemma antimono_funpow:
```
```  1940   fixes Q :: "'a::{lattice,order_top} \<Rightarrow> 'a"
```
```  1941   shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
```
```  1942   by (auto intro!: funpow_increasing simp: antimono_def)
```
```  1943
```
```  1944
```
```  1945 subsection \<open>The divides relation on @{typ nat}\<close>
```
```  1946
```
```  1947 lemma dvd_1_left [iff]: "Suc 0 dvd k"
```
```  1948   by (simp add: dvd_def)
```
```  1949
```
```  1950 lemma dvd_1_iff_1 [simp]: "m dvd Suc 0 \<longleftrightarrow> m = Suc 0"
```
```  1951   by (simp add: dvd_def)
```
```  1952
```
```  1953 lemma nat_dvd_1_iff_1 [simp]: "m dvd 1 \<longleftrightarrow> m = 1" for m :: nat
```
```  1954   by (simp add: dvd_def)
```
```  1955
```
```  1956 lemma dvd_antisym: "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n" for m n :: nat
```
```  1957   unfolding dvd_def by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
```
```  1958
```
```  1959 lemma dvd_diff_nat [simp]: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)" for k m n :: nat
```
```  1960   unfolding dvd_def by (blast intro: right_diff_distrib' [symmetric])
```
```  1961
```
```  1962 lemma dvd_diffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd m" for k m n :: nat
```
```  1963   apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
```
```  1964   apply (blast intro: dvd_add)
```
```  1965   done
```
```  1966
```
```  1967 lemma dvd_diffD1: "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd n" for k m n :: nat
```
```  1968   by (drule_tac m = m in dvd_diff_nat) auto
```
```  1969
```
```  1970 lemma dvd_mult_cancel:
```
```  1971   fixes m n k :: nat
```
```  1972   assumes "k * m dvd k * n" and "0 < k"
```
```  1973   shows "m dvd n"
```
```  1974 proof -
```
```  1975   from assms(1) obtain q where "k * n = (k * m) * q" ..
```
```  1976   then have "k * n = k * (m * q)" by (simp add: ac_simps)
```
```  1977   with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel)
```
```  1978   then show ?thesis ..
```
```  1979 qed
```
```  1980
```
```  1981 lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1" for m n :: nat
```
```  1982   apply auto
```
```  1983    apply (subgoal_tac "m * n dvd m * 1")
```
```  1984    apply (drule dvd_mult_cancel, auto)
```
```  1985   done
```
```  1986
```
```  1987 lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1" for m n :: nat
```
```  1988   using dvd_mult_cancel1 [of m n] by (simp add: ac_simps)
```
```  1989
```
```  1990 lemma dvd_imp_le: "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> n" for k n :: nat
```
```  1991   by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
```
```  1992
```
```  1993 lemma nat_dvd_not_less: "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m" for m n :: nat
```
```  1994   by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
```
```  1995
```
```  1996 lemma less_eq_dvd_minus:
```
```  1997   fixes m n :: nat
```
```  1998   assumes "m \<le> n"
```
```  1999   shows "m dvd n \<longleftrightarrow> m dvd n - m"
```
```  2000 proof -
```
```  2001   from assms have "n = m + (n - m)" by simp
```
```  2002   then obtain q where "n = m + q" ..
```
```  2003   then show ?thesis by (simp add: add.commute [of m])
```
```  2004 qed
```
```  2005
```
```  2006 lemma dvd_minus_self: "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n" for m n :: nat
```
```  2007   by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le)
```
```  2008
```
```  2009 lemma dvd_minus_add:
```
```  2010   fixes m n q r :: nat
```
```  2011   assumes "q \<le> n" "q \<le> r * m"
```
```  2012   shows "m dvd n - q \<longleftrightarrow> m dvd n + (r * m - q)"
```
```  2013 proof -
```
```  2014   have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
```
```  2015     using dvd_add_times_triv_left_iff [of m r] by simp
```
```  2016   also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
```
```  2017   also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
```
```  2018   also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add.commute)
```
```  2019   finally show ?thesis .
```
```  2020 qed
```
```  2021
```
```  2022
```
```  2023 subsection \<open>Aliasses\<close>
```
```  2024
```
```  2025 lemma nat_mult_1: "1 * n = n" for n :: nat
```
```  2026   by (fact mult_1_left)
```
```  2027
```
```  2028 lemma nat_mult_1_right: "n * 1 = n" for n :: nat
```
```  2029   by (fact mult_1_right)
```
```  2030
```
```  2031 lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n" for k m n :: nat
```
```  2032   by (fact add_left_cancel)
```
```  2033
```
```  2034 lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n" for k m n :: nat
```
```  2035   by (fact add_right_cancel)
```
```  2036
```
```  2037 lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)" for k m n :: nat
```
```  2038   by (fact left_diff_distrib')
```
```  2039
```
```  2040 lemma diff_mult_distrib2: "k * (m - n) = (k * m) - (k * n)" for k m n :: nat
```
```  2041   by (fact right_diff_distrib')
```
```  2042
```
```  2043 lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k" for k m n :: nat
```
```  2044   by (fact le_add_diff)  (* FIXME delete *)
```
```  2045
```
```  2046 lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)" for i j k :: nat
```
```  2047   by (fact le_diff_conv2) (* FIXME delete *)
```
```  2048
```
```  2049 lemma diff_self_eq_0 [simp]: "m - m = 0" for m :: nat
```
```  2050   by (fact diff_cancel)
```
```  2051
```
```  2052 lemma diff_diff_left [simp]: "i - j - k = i - (j + k)" for i j k :: nat
```
```  2053   by (fact diff_diff_add)
```
```  2054
```
```  2055 lemma diff_commute: "i - j - k = i - k - j" for i j k :: nat
```
```  2056   by (fact diff_right_commute)
```
```  2057
```
```  2058 lemma diff_add_inverse: "(n + m) - n = m" for m n :: nat
```
```  2059   by (fact add_diff_cancel_left')
```
```  2060
```
```  2061 lemma diff_add_inverse2: "(m + n) - n = m" for m n :: nat
```
```  2062   by (fact add_diff_cancel_right')
```
```  2063
```
```  2064 lemma diff_cancel: "(k + m) - (k + n) = m - n" for k m n :: nat
```
```  2065   by (fact add_diff_cancel_left)
```
```  2066
```
```  2067 lemma diff_cancel2: "(m + k) - (n + k) = m - n" for k m n :: nat
```
```  2068   by (fact add_diff_cancel_right)
```
```  2069
```
```  2070 lemma diff_add_0: "n - (n + m) = 0" for m n :: nat
```
```  2071   by (fact diff_add_zero)
```
```  2072
```
```  2073 lemma add_mult_distrib2: "k * (m + n) = (k * m) + (k * n)" for k m n :: nat
```
```  2074   by (fact distrib_left)
```
```  2075
```
```  2076 lemmas nat_distrib =
```
```  2077   add_mult_distrib distrib_left diff_mult_distrib diff_mult_distrib2
```
```  2078
```
```  2079
```
```  2080 subsection \<open>Size of a datatype value\<close>
```
```  2081
```
```  2082 class size =
```
```  2083   fixes size :: "'a \<Rightarrow> nat" \<comment> \<open>see further theory \<open>Wellfounded\<close>\<close>
```
```  2084
```
```  2085 instantiation nat :: size
```
```  2086 begin
```
```  2087
```
```  2088 definition size_nat where [simp, code]: "size (n::nat) = n"
```
```  2089
```
```  2090 instance ..
```
```  2091
```
```  2092 end
```
```  2093
```
```  2094
```
```  2095 subsection \<open>Code module namespace\<close>
```
```  2096
```
```  2097 code_identifier
```
```  2098   code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
```
```  2099
```
```  2100 hide_const (open) of_nat_aux
```
```  2101
```
```  2102 end
```