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