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