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