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