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--
removed odd cases rule (see also 8cb42cd97579);
     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