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