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