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