src/HOL/Nat.thy
author haftmann
Fri Dec 07 15:07:59 2007 +0100 (2007-12-07)
changeset 25571 c9e39eafc7a0
parent 25563 cab4f808f791
child 25612 314d949c70b5
permissions -rw-r--r--
instantiation target rather than legacy instance
     1 (*  Title:      HOL/Nat.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
     4 
     5 Type "nat" is a linear order, and a datatype; arithmetic operators + -
     6 and * (for div, mod and dvd, see theory Divides).
     7 *)
     8 
     9 header {* Natural numbers *}
    10 
    11 theory Nat
    12 imports Wellfounded_Recursion Ring_and_Field
    13 uses
    14   "~~/src/Tools/rat.ML"
    15   "~~/src/Provers/Arith/cancel_sums.ML"
    16   ("arith_data.ML")
    17   "~~/src/Provers/Arith/fast_lin_arith.ML"
    18   ("Tools/lin_arith.ML")
    19   ("Tools/function_package/size.ML")
    20 begin
    21 
    22 subsection {* Type @{text ind} *}
    23 
    24 typedecl ind
    25 
    26 axiomatization
    27   Zero_Rep :: ind and
    28   Suc_Rep :: "ind => ind"
    29 where
    30   -- {* the axiom of infinity in 2 parts *}
    31   inj_Suc_Rep:          "inj Suc_Rep" and
    32   Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    33 
    34 
    35 subsection {* Type nat *}
    36 
    37 text {* Type definition *}
    38 
    39 inductive_set Nat :: "ind set"
    40 where
    41     Zero_RepI: "Zero_Rep : Nat"
    42   | Suc_RepI: "i : Nat ==> Suc_Rep i : Nat"
    43 
    44 global
    45 
    46 typedef (open Nat)
    47   nat = Nat
    48 proof
    49   show "Zero_Rep : Nat" by (rule Nat.Zero_RepI)
    50 qed
    51 
    52 consts
    53   Suc :: "nat => nat"
    54 
    55 local
    56 
    57 instantiation nat :: zero
    58 begin
    59 
    60 definition Zero_nat_def [code func del]:
    61   "0 = Abs_Nat Zero_Rep"
    62 
    63 instance ..
    64 
    65 end
    66 
    67 defs
    68   Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    69 
    70 theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
    71   apply (unfold Zero_nat_def Suc_def)
    72   apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    73   apply (erule Rep_Nat [THEN Nat.induct])
    74   apply (iprover elim: Abs_Nat_inverse [THEN subst])
    75   done
    76 
    77 lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
    78   by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI
    79                 Suc_Rep_not_Zero_Rep)
    80 
    81 lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
    82   by (rule not_sym, rule Suc_not_Zero not_sym)
    83 
    84 lemma inj_Suc[simp]: "inj_on Suc N"
    85   by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI
    86                 inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    87 
    88 lemma Suc_Suc_eq [iff]: "(Suc m = Suc n) = (m = n)"
    89   by (rule inj_Suc [THEN inj_eq])
    90 
    91 rep_datatype nat
    92   distinct  Suc_not_Zero Zero_not_Suc
    93   inject    Suc_Suc_eq
    94   induction nat_induct
    95 
    96 declare nat.induct [case_names 0 Suc, induct type: nat]
    97 declare nat.exhaust [case_names 0 Suc, cases type: nat]
    98 
    99 lemmas nat_rec_0 = nat.recs(1)
   100   and nat_rec_Suc = nat.recs(2)
   101 
   102 lemmas nat_case_0 = nat.cases(1)
   103   and nat_case_Suc = nat.cases(2)
   104 
   105 
   106 text {* Injectiveness and distinctness lemmas *}
   107 
   108 lemma Suc_neq_Zero: "Suc m = 0 ==> R"
   109 by (rule notE, rule Suc_not_Zero)
   110 
   111 lemma Zero_neq_Suc: "0 = Suc m ==> R"
   112 by (rule Suc_neq_Zero, erule sym)
   113 
   114 lemma Suc_inject: "Suc x = Suc y ==> x = y"
   115 by (rule inj_Suc [THEN injD])
   116 
   117 lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
   118 by auto
   119 
   120 lemma n_not_Suc_n: "n \<noteq> Suc n"
   121 by (induct n) simp_all
   122 
   123 lemma Suc_n_not_n: "Suc t \<noteq> t"
   124 by (rule not_sym, rule n_not_Suc_n)
   125 
   126 
   127 text {* A special form of induction for reasoning
   128   about @{term "m < n"} and @{term "m - n"} *}
   129 
   130 theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
   131     (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
   132   apply (rule_tac x = m in spec)
   133   apply (induct n)
   134   prefer 2
   135   apply (rule allI)
   136   apply (induct_tac x, iprover+)
   137   done
   138 
   139 
   140 subsection {* Arithmetic operators *}
   141 
   142 instantiation nat :: "{one, plus, minus, times}"
   143 begin
   144 
   145 definition
   146   One_nat_def [simp]: "1 = Suc 0"
   147 
   148 primrec plus_nat
   149 where
   150   add_0:      "0 + n = (n\<Colon>nat)"
   151   | add_Suc:  "Suc m + n = Suc (m + n)"
   152 
   153 primrec minus_nat
   154 where
   155   diff_0:     "m - 0 = (m\<Colon>nat)"
   156   | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
   157 
   158 primrec times_nat
   159 where
   160   mult_0:     "0 * n = (0\<Colon>nat)"
   161   | mult_Suc: "Suc m * n = n + (m * n)"
   162 
   163 instance ..
   164 
   165 end
   166 
   167 
   168 subsection {* Orders on @{typ nat} *}
   169 
   170 definition
   171   pred_nat :: "(nat * nat) set" where
   172   "pred_nat = {(m, n). n = Suc m}"
   173 
   174 instantiation nat :: ord
   175 begin
   176 
   177 definition
   178   less_def [code func del]: "m < n \<longleftrightarrow> (m, n) : pred_nat^+"
   179 
   180 definition
   181   le_def [code func del]:   "m \<le> (n\<Colon>nat) \<longleftrightarrow> \<not> n < m"
   182 
   183 instance ..
   184 
   185 end
   186 
   187 lemma wf_pred_nat: "wf pred_nat"
   188   apply (unfold wf_def pred_nat_def, clarify)
   189   apply (induct_tac x, blast+)
   190   done
   191 
   192 lemma wf_less: "wf {(x, y::nat). x < y}"
   193   apply (unfold less_def)
   194   apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset], blast)
   195   done
   196 
   197 lemma less_eq: "((m, n) : pred_nat^+) = (m < n)"
   198   apply (unfold less_def)
   199   apply (rule refl)
   200   done
   201 
   202 subsubsection {* Introduction properties *}
   203 
   204 lemma less_trans: "i < j ==> j < k ==> i < (k::nat)"
   205   apply (unfold less_def)
   206   apply (rule trans_trancl [THEN transD], assumption+)
   207   done
   208 
   209 lemma lessI [iff]: "n < Suc n"
   210   apply (unfold less_def pred_nat_def)
   211   apply (simp add: r_into_trancl)
   212   done
   213 
   214 lemma less_SucI: "i < j ==> i < Suc j"
   215   apply (rule less_trans, assumption)
   216   apply (rule lessI)
   217   done
   218 
   219 lemma zero_less_Suc [iff]: "0 < Suc n"
   220   apply (induct n)
   221   apply (rule lessI)
   222   apply (erule less_trans)
   223   apply (rule lessI)
   224   done
   225 
   226 subsubsection {* Elimination properties *}
   227 
   228 lemma less_not_sym: "n < m ==> ~ m < (n::nat)"
   229   apply (unfold less_def)
   230   apply (blast intro: wf_pred_nat wf_trancl [THEN wf_asym])
   231   done
   232 
   233 lemma less_asym:
   234   assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P
   235   apply (rule contrapos_np)
   236   apply (rule less_not_sym)
   237   apply (rule h1)
   238   apply (erule h2)
   239   done
   240 
   241 lemma less_not_refl: "~ n < (n::nat)"
   242   apply (unfold less_def)
   243   apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_not_refl])
   244   done
   245 
   246 lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
   247 by (rule notE, rule less_not_refl)
   248 
   249 lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast
   250 
   251 lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
   252 by (rule not_sym, rule less_not_refl2)
   253 
   254 lemma lessE:
   255   assumes major: "i < k"
   256   and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P"
   257   shows P
   258   apply (rule major [unfolded less_def pred_nat_def, THEN tranclE], simp_all)
   259   apply (erule p1)
   260   apply (rule p2)
   261   apply (simp add: less_def pred_nat_def, assumption)
   262   done
   263 
   264 lemma not_less0 [iff]: "~ n < (0::nat)"
   265 by (blast elim: lessE)
   266 
   267 lemma less_zeroE: "(n::nat) < 0 ==> R"
   268 by (rule notE, rule not_less0)
   269 
   270 lemma less_SucE: assumes major: "m < Suc n"
   271   and less: "m < n ==> P" and eq: "m = n ==> P" shows P
   272   apply (rule major [THEN lessE])
   273   apply (rule eq, blast)
   274   apply (rule less, blast)
   275   done
   276 
   277 lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
   278 by (blast elim!: less_SucE intro: less_trans)
   279 
   280 lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)"
   281 by (simp add: less_Suc_eq)
   282 
   283 lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   284 by (simp add: less_Suc_eq)
   285 
   286 lemma Suc_mono: "m < n ==> Suc m < Suc n"
   287 by (induct n) (fast elim: less_trans lessE)+
   288 
   289 text {* "Less than" is a linear ordering *}
   290 lemma less_linear: "m < n | m = n | n < (m::nat)"
   291   apply (induct m)
   292   apply (induct n)
   293   apply (rule refl [THEN disjI1, THEN disjI2])
   294   apply (rule zero_less_Suc [THEN disjI1])
   295   apply (blast intro: Suc_mono less_SucI elim: lessE)
   296   done
   297 
   298 text {* "Less than" is antisymmetric, sort of *}
   299 lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
   300   apply(simp only:less_Suc_eq)
   301   apply blast
   302   done
   303 
   304 lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
   305   using less_linear by blast
   306 
   307 lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m"
   308   and eqCase: "m = n ==> P n m" and lessCase: "n<m ==> P n m"
   309   shows "P n m"
   310   apply (rule less_linear [THEN disjE])
   311   apply (erule_tac [2] disjE)
   312   apply (erule lessCase)
   313   apply (erule sym [THEN eqCase])
   314   apply (erule major)
   315   done
   316 
   317 
   318 subsubsection {* Inductive (?) properties *}
   319 
   320 lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
   321   apply (simp add: nat_neq_iff)
   322   apply (blast elim!: less_irrefl less_SucE elim: less_asym)
   323   done
   324 
   325 lemma Suc_lessD: "Suc m < n ==> m < n"
   326   apply (induct n)
   327   apply (fast intro!: lessI [THEN less_SucI] elim: less_trans lessE)+
   328   done
   329 
   330 lemma Suc_lessE: assumes major: "Suc i < k"
   331   and minor: "!!j. i < j ==> k = Suc j ==> P" shows P
   332   apply (rule major [THEN lessE])
   333   apply (erule lessI [THEN minor])
   334   apply (erule Suc_lessD [THEN minor], assumption)
   335   done
   336 
   337 lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
   338 by (blast elim: lessE dest: Suc_lessD)
   339 
   340 lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)"
   341   apply (rule iffI)
   342   apply (erule Suc_less_SucD)
   343   apply (erule Suc_mono)
   344   done
   345 
   346 lemma less_trans_Suc:
   347   assumes le: "i < j" shows "j < k ==> Suc i < k"
   348   apply (induct k, simp_all)
   349   apply (insert le)
   350   apply (simp add: less_Suc_eq)
   351   apply (blast dest: Suc_lessD)
   352   done
   353 
   354 text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
   355 lemma not_less_eq: "(~ m < n) = (n < Suc m)"
   356 by (induct m n rule: diff_induct) simp_all
   357 
   358 text {* Complete induction, aka course-of-values induction *}
   359 lemma nat_less_induct:
   360   assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
   361   apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]])
   362   apply (rule prem)
   363   apply (unfold less_def, assumption)
   364   done
   365 
   366 lemmas less_induct = nat_less_induct [rule_format, case_names less]
   367 
   368 
   369 text {* Properties of "less than or equal" *}
   370 
   371 text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
   372 lemma less_Suc_eq_le: "(m < Suc n) = (m \<le> n)"
   373   unfolding le_def by (rule not_less_eq [symmetric])
   374 
   375 lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
   376 by (rule less_Suc_eq_le [THEN iffD2])
   377 
   378 lemma le0 [iff]: "(0::nat) \<le> n"
   379   unfolding le_def by (rule not_less0)
   380 
   381 lemma Suc_n_not_le_n: "~ Suc n \<le> n"
   382 by (simp add: le_def)
   383 
   384 lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)"
   385 by (induct i) (simp_all add: le_def)
   386 
   387 lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
   388 by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
   389 
   390 lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
   391 by (drule le_Suc_eq [THEN iffD1], iprover+)
   392 
   393 lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   394   apply (simp add: le_def less_Suc_eq)
   395   apply (blast elim!: less_irrefl less_asym)
   396   done -- {* formerly called lessD *}
   397 
   398 lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n"
   399 by (simp add: le_def less_Suc_eq)
   400 
   401 text {* Stronger version of @{text Suc_leD} *}
   402 lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
   403   apply (simp add: le_def less_Suc_eq)
   404   using less_linear
   405   apply blast
   406   done
   407 
   408 lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)"
   409 by (blast intro: Suc_leI Suc_le_lessD)
   410 
   411 lemma le_SucI: "m \<le> n ==> m \<le> Suc n"
   412 by (unfold le_def) (blast dest: Suc_lessD)
   413 
   414 lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
   415 by (unfold le_def) (blast elim: less_asym)
   416 
   417 text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
   418 lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
   419 
   420 
   421 text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}
   422 
   423 lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)"
   424   unfolding le_def
   425   using less_linear
   426   by (blast elim: less_irrefl less_asym)
   427 
   428 lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
   429   unfolding le_def
   430   using less_linear
   431   by (blast elim!: less_irrefl elim: less_asym)
   432 
   433 lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
   434 by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
   435 
   436 text {* Useful with @{text blast}. *}
   437 lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
   438 by (rule less_or_eq_imp_le) (rule disjI2)
   439 
   440 lemma le_refl: "n \<le> (n::nat)"
   441 by (simp add: le_eq_less_or_eq)
   442 
   443 lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
   444 by (blast dest!: le_imp_less_or_eq intro: less_trans)
   445 
   446 lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
   447 by (blast dest!: le_imp_less_or_eq intro: less_trans)
   448 
   449 lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
   450 by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
   451 
   452 lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
   453 by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
   454 
   455 lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)"
   456 by (simp add: le_simps)
   457 
   458 text {* Axiom @{text order_less_le} of class @{text order}: *}
   459 lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
   460 by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
   461 
   462 lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
   463 by (rule iffD2, rule nat_less_le, rule conjI)
   464 
   465 text {* Axiom @{text linorder_linear} of class @{text linorder}: *}
   466 lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
   467   apply (simp add: le_eq_less_or_eq)
   468   using less_linear by blast
   469 
   470 text {* Type @{typ nat} is a wellfounded linear order *}
   471 
   472 instance nat :: wellorder
   473   by intro_classes
   474     (assumption |
   475       rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
   476 
   477 lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
   478 
   479 lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   480 by (blast elim!: less_SucE)
   481 
   482 text {*
   483   Rewrite @{term "n < Suc m"} to @{term "n = m"}
   484   if @{term "~ n < m"} or @{term "m \<le> n"} hold.
   485   Not suitable as default simprules because they often lead to looping
   486 *}
   487 lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
   488 by (rule not_less_less_Suc_eq, rule leD)
   489 
   490 lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
   491 
   492 
   493 text {*
   494   Re-orientation of the equations @{text "0 = x"} and @{text "1 = x"}.
   495   No longer added as simprules (they loop)
   496   but via @{text reorient_simproc} in Bin
   497 *}
   498 
   499 text {* Polymorphic, not just for @{typ nat} *}
   500 lemma zero_reorient: "(0 = x) = (x = 0)"
   501 by auto
   502 
   503 lemma one_reorient: "(1 = x) = (x = 1)"
   504 by auto
   505 
   506 text {* These two rules ease the use of primitive recursion.
   507 NOTE USE OF @{text "=="} *}
   508 lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
   509 by simp
   510 
   511 lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
   512 by simp
   513 
   514 lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
   515 by (cases n) simp_all
   516 
   517 lemma gr0_implies_Suc: "n > 0 ==> \<exists>m. n = Suc m"
   518 by (cases n) simp_all
   519 
   520 lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0"
   521 by (cases n) simp_all
   522 
   523 lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
   524 by (cases n) simp_all
   525 
   526 text {* This theorem is useful with @{text blast} *}
   527 lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   528 by (rule neq0_conv[THEN iffD1], iprover)
   529 
   530 lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   531 by (fast intro: not0_implies_Suc)
   532 
   533 lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   534 using neq0_conv by blast
   535 
   536 lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   537 by (induct m') simp_all
   538 
   539 text {* Useful in certain inductive arguments *}
   540 lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
   541 by (cases m) simp_all
   542 
   543 lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
   544   apply (rule nat_less_induct)
   545   apply (case_tac n)
   546   apply (case_tac [2] nat)
   547   apply (blast intro: less_trans)+
   548   done
   549 
   550 
   551 subsection {* @{text LEAST} theorems for type @{typ nat}*}
   552 
   553 lemma Least_Suc:
   554      "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   555   apply (case_tac "n", auto)
   556   apply (frule LeastI)
   557   apply (drule_tac P = "%x. P (Suc x) " in LeastI)
   558   apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
   559   apply (erule_tac [2] Least_le)
   560   apply (case_tac "LEAST x. P x", auto)
   561   apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   562   apply (blast intro: order_antisym)
   563   done
   564 
   565 lemma Least_Suc2:
   566    "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   567 by (erule (1) Least_Suc [THEN ssubst], simp)
   568 
   569 
   570 subsection {* @{term min} and @{term max} *}
   571 
   572 lemma mono_Suc: "mono Suc"
   573 by (rule monoI) simp
   574 
   575 lemma min_0L [simp]: "min 0 n = (0::nat)"
   576 by (rule min_leastL) simp
   577 
   578 lemma min_0R [simp]: "min n 0 = (0::nat)"
   579 by (rule min_leastR) simp
   580 
   581 lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
   582 by (simp add: mono_Suc min_of_mono)
   583 
   584 lemma min_Suc1:
   585    "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
   586 by (simp split: nat.split)
   587 
   588 lemma min_Suc2:
   589    "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
   590 by (simp split: nat.split)
   591 
   592 lemma max_0L [simp]: "max 0 n = (n::nat)"
   593 by (rule max_leastL) simp
   594 
   595 lemma max_0R [simp]: "max n 0 = (n::nat)"
   596 by (rule max_leastR) simp
   597 
   598 lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
   599 by (simp add: mono_Suc max_of_mono)
   600 
   601 lemma max_Suc1:
   602    "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
   603 by (simp split: nat.split)
   604 
   605 lemma max_Suc2:
   606    "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
   607 by (simp split: nat.split)
   608 
   609 
   610 subsection {* Basic rewrite rules for the arithmetic operators *}
   611 
   612 text {* Difference *}
   613 
   614 lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
   615 by (induct n) simp_all
   616 
   617 lemma diff_Suc_Suc [simp, code]: "Suc(m) - Suc(n) = m - n"
   618 by (induct n) simp_all
   619 
   620 
   621 text {*
   622   Could be (and is, below) generalized in various ways
   623   However, none of the generalizations are currently in the simpset,
   624   and I dread to think what happens if I put them in
   625 *}
   626 lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
   627 by (simp split add: nat.split)
   628 
   629 declare diff_Suc [simp del, code del]
   630 
   631 lemma [code]:
   632   "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
   633   "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
   634   "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
   635   "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
   636   using Suc_le_eq less_Suc_eq_le by simp_all
   637 
   638 
   639 subsection {* Addition *}
   640 
   641 lemma add_0_right [simp]: "m + 0 = (m::nat)"
   642 by (induct m) simp_all
   643 
   644 lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   645 by (induct m) simp_all
   646 
   647 lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
   648 by simp
   649 
   650 
   651 text {* Associative law for addition *}
   652 lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
   653 by (induct m) simp_all
   654 
   655 text {* Commutative law for addition *}
   656 lemma nat_add_commute: "m + n = n + (m::nat)"
   657 by (induct m) simp_all
   658 
   659 lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
   660   apply (rule mk_left_commute [of "op +"])
   661   apply (rule nat_add_assoc)
   662   apply (rule nat_add_commute)
   663   done
   664 
   665 lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
   666 by (induct k) simp_all
   667 
   668 lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
   669 by (induct k) simp_all
   670 
   671 lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
   672 by (induct k) simp_all
   673 
   674 lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
   675 by (induct k) simp_all
   676 
   677 text {* Reasoning about @{text "m + 0 = 0"}, etc. *}
   678 
   679 lemma add_is_0 [iff]: fixes m :: nat shows "(m + n = 0) = (m = 0 & n = 0)"
   680 by (cases m) simp_all
   681 
   682 lemma add_is_1: "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)"
   683 by (cases m) simp_all
   684 
   685 lemma one_is_add: "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
   686 by (rule trans, rule eq_commute, rule add_is_1)
   687 
   688 lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)"
   689 by(auto dest:gr0_implies_Suc)
   690 
   691 lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
   692   apply (drule add_0_right [THEN ssubst])
   693   apply (simp add: nat_add_assoc del: add_0_right)
   694   done
   695 
   696 lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N"
   697   apply (induct k)
   698    apply simp
   699   apply(drule comp_inj_on[OF _ inj_Suc])
   700   apply (simp add:o_def)
   701   done
   702 
   703 
   704 subsection {* Multiplication *}
   705 
   706 text {* right annihilation in product *}
   707 lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
   708 by (induct m) simp_all
   709 
   710 text {* right successor law for multiplication *}
   711 lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
   712 by (induct m) (simp_all add: nat_add_left_commute)
   713 
   714 text {* Commutative law for multiplication *}
   715 lemma nat_mult_commute: "m * n = n * (m::nat)"
   716 by (induct m) simp_all
   717 
   718 text {* addition distributes over multiplication *}
   719 lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
   720 by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
   721 
   722 lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
   723 by (induct m) (simp_all add: nat_add_assoc)
   724 
   725 text {* Associative law for multiplication *}
   726 lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
   727 by (induct m) (simp_all add: add_mult_distrib)
   728 
   729 
   730 text{*The naturals form a @{text comm_semiring_1_cancel}*}
   731 instance nat :: comm_semiring_1_cancel
   732 proof
   733   fix i j k :: nat
   734   show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
   735   show "i + j = j + i" by (rule nat_add_commute)
   736   show "0 + i = i" by simp
   737   show "(i * j) * k = i * (j * k)" by (rule nat_mult_assoc)
   738   show "i * j = j * i" by (rule nat_mult_commute)
   739   show "1 * i = i" by simp
   740   show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
   741   show "0 \<noteq> (1::nat)" by simp
   742   assume "k+i = k+j" thus "i=j" by simp
   743 qed
   744 
   745 lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   746   apply (induct m)
   747    apply (induct_tac [2] n)
   748     apply simp_all
   749   done
   750 
   751 
   752 subsection {* Monotonicity of Addition *}
   753 
   754 text {* strict, in 1st argument *}
   755 lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   756 by (induct k) simp_all
   757 
   758 text {* strict, in both arguments *}
   759 lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   760   apply (rule add_less_mono1 [THEN less_trans], assumption+)
   761   apply (induct j, simp_all)
   762   done
   763 
   764 text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
   765 lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
   766   apply (induct n)
   767   apply (simp_all add: order_le_less)
   768   apply (blast elim!: less_SucE
   769                intro!: add_0_right [symmetric] add_Suc_right [symmetric])
   770   done
   771 
   772 text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
   773 lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j"
   774 apply(auto simp: gr0_conv_Suc)
   775 apply (induct_tac m)
   776 apply (simp_all add: add_less_mono)
   777 done
   778 
   779 
   780 text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
   781 instance nat :: ordered_semidom
   782 proof
   783   fix i j k :: nat
   784   show "0 < (1::nat)" by simp
   785   show "i \<le> j ==> k + i \<le> k + j" by simp
   786   show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
   787 qed
   788 
   789 lemma nat_mult_1: "(1::nat) * n = n"
   790 by simp
   791 
   792 lemma nat_mult_1_right: "n * (1::nat) = n"
   793 by simp
   794 
   795 
   796 subsection {* Additional theorems about "less than" *}
   797 
   798 text{*An induction rule for estabilishing binary relations*}
   799 lemma less_Suc_induct:
   800   assumes less:  "i < j"
   801      and  step:  "!!i. P i (Suc i)"
   802      and  trans: "!!i j k. P i j ==> P j k ==> P i k"
   803   shows "P i j"
   804 proof -
   805   from less obtain k where j: "j = Suc(i+k)" by (auto dest: less_imp_Suc_add)
   806   have "P i (Suc (i + k))"
   807   proof (induct k)
   808     case 0
   809     show ?case by (simp add: step)
   810   next
   811     case (Suc k)
   812     thus ?case by (auto intro: assms)
   813   qed
   814   thus "P i j" by (simp add: j)
   815 qed
   816 
   817 text {* The method of infinite descent, frequently used in number theory.
   818 Provided by Roelof Oosterhuis.
   819 $P(n)$ is true for all $n\in\mathbb{N}$ if
   820 \begin{itemize}
   821   \item case ``0'': given $n=0$ prove $P(n)$,
   822   \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists
   823         a smaller integer $m$ such that $\neg P(m)$.
   824 \end{itemize} *}
   825 
   826 lemma infinite_descent0[case_names 0 smaller]: 
   827   "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
   828 by (induct n rule: less_induct, case_tac "n>0", auto)
   829 
   830 text{* A compact version without explicit base case: *}
   831 lemma infinite_descent:
   832   "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
   833 by (induct n rule: less_induct, auto)
   834 
   835 
   836 text {* Infinite descent using a mapping to $\mathbb{N}$:
   837 $P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and
   838 \begin{itemize}
   839 \item case ``0'': given $V(x)=0$ prove $P(x)$,
   840 \item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
   841 \end{itemize}
   842 NB: the proof also shows how to use the previous lemma. *}
   843 corollary infinite_descent0_measure [case_names 0 smaller]:
   844   assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
   845     and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
   846   shows "P x"
   847 proof -
   848   obtain n where "n = V x" by auto
   849   moreover have "\<And>x. V x = n \<Longrightarrow> P x"
   850   proof (induct n rule: infinite_descent0)
   851     case 0 -- "i.e. $V(x) = 0$"
   852     with A0 show "P x" by auto
   853   next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
   854     case (smaller n)
   855     then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
   856     with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
   857     with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
   858     thus ?case by auto
   859   qed
   860   ultimately show "P x" by auto
   861 qed
   862 
   863 text{* Again, without explicit base case: *}
   864 lemma infinite_descent_measure:
   865 assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"
   866 proof -
   867   from assms obtain n where "n = V x" by auto
   868   moreover have "!!x. V x = n \<Longrightarrow> P x"
   869   proof (induct n rule: infinite_descent, auto)
   870     fix x assume "\<not> P x"
   871     with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto
   872   qed
   873   ultimately show "P x" by auto
   874 qed
   875 
   876 
   877 
   878 text {* A [clumsy] way of lifting @{text "<"}
   879   monotonicity to @{text "\<le>"} monotonicity *}
   880 lemma less_mono_imp_le_mono:
   881   "\<lbrakk> !!i j::nat. i < j \<Longrightarrow> f i < f j; i \<le> j \<rbrakk> \<Longrightarrow> f i \<le> ((f j)::nat)"
   882 by (simp add: order_le_less) (blast)
   883 
   884 
   885 text {* non-strict, in 1st argument *}
   886 lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)"
   887 by (rule add_right_mono)
   888 
   889 text {* non-strict, in both arguments *}
   890 lemma add_le_mono: "[| i \<le> j;  k \<le> l |] ==> i + k \<le> j + (l::nat)"
   891 by (rule add_mono)
   892 
   893 lemma le_add2: "n \<le> ((m + n)::nat)"
   894 by (insert add_right_mono [of 0 m n], simp)
   895 
   896 lemma le_add1: "n \<le> ((n + m)::nat)"
   897 by (simp add: add_commute, rule le_add2)
   898 
   899 lemma less_add_Suc1: "i < Suc (i + m)"
   900 by (rule le_less_trans, rule le_add1, rule lessI)
   901 
   902 lemma less_add_Suc2: "i < Suc (m + i)"
   903 by (rule le_less_trans, rule le_add2, rule lessI)
   904 
   905 lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
   906 by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
   907 
   908 lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
   909 by (rule le_trans, assumption, rule le_add1)
   910 
   911 lemma trans_le_add2: "(i::nat) \<le> j ==> i \<le> m + j"
   912 by (rule le_trans, assumption, rule le_add2)
   913 
   914 lemma trans_less_add1: "(i::nat) < j ==> i < j + m"
   915 by (rule less_le_trans, assumption, rule le_add1)
   916 
   917 lemma trans_less_add2: "(i::nat) < j ==> i < m + j"
   918 by (rule less_le_trans, assumption, rule le_add2)
   919 
   920 lemma add_lessD1: "i + j < (k::nat) ==> i < k"
   921 apply (rule le_less_trans [of _ "i+j"])
   922 apply (simp_all add: le_add1)
   923 done
   924 
   925 lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
   926 apply (rule notI)
   927 apply (erule add_lessD1 [THEN less_irrefl])
   928 done
   929 
   930 lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
   931 by (simp add: add_commute not_add_less1)
   932 
   933 lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
   934 apply (rule order_trans [of _ "m+k"])
   935 apply (simp_all add: le_add1)
   936 done
   937 
   938 lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
   939 apply (simp add: add_commute)
   940 apply (erule add_leD1)
   941 done
   942 
   943 lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
   944 by (blast dest: add_leD1 add_leD2)
   945 
   946 text {* needs @{text "!!k"} for @{text add_ac} to work *}
   947 lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
   948 by (force simp del: add_Suc_right
   949     simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
   950 
   951 
   952 subsection {* Difference *}
   953 
   954 lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
   955 by (induct m) simp_all
   956 
   957 text {* Addition is the inverse of subtraction:
   958   if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
   959 lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"
   960 by (induct m n rule: diff_induct) simp_all
   961 
   962 lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)"
   963 by (simp add: add_diff_inverse linorder_not_less)
   964 
   965 lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
   966 by (simp add: le_add_diff_inverse add_commute)
   967 
   968 
   969 subsection {* More results about difference *}
   970 
   971 lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
   972 by (induct m n rule: diff_induct) simp_all
   973 
   974 lemma diff_less_Suc: "m - n < Suc m"
   975 apply (induct m n rule: diff_induct)
   976 apply (erule_tac [3] less_SucE)
   977 apply (simp_all add: less_Suc_eq)
   978 done
   979 
   980 lemma diff_le_self [simp]: "m - n \<le> (m::nat)"
   981 by (induct m n rule: diff_induct) (simp_all add: le_SucI)
   982 
   983 lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
   984 by (rule le_less_trans, rule diff_le_self)
   985 
   986 lemma diff_diff_left: "(i::nat) - j - k = i - (j + k)"
   987 by (induct i j rule: diff_induct) simp_all
   988 
   989 lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
   990 by (simp add: diff_diff_left)
   991 
   992 lemma diff_Suc_less [simp]: "0<n ==> n - Suc i < n"
   993 by (cases n) (auto simp add: le_simps)
   994 
   995 text {* This and the next few suggested by Florian Kammueller *}
   996 lemma diff_commute: "(i::nat) - j - k = i - k - j"
   997 by (simp add: diff_diff_left add_commute)
   998 
   999 lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
  1000 by (induct j k rule: diff_induct) simp_all
  1001 
  1002 lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
  1003 by (simp add: add_commute diff_add_assoc)
  1004 
  1005 lemma diff_add_inverse: "(n + m) - n = (m::nat)"
  1006 by (induct n) simp_all
  1007 
  1008 lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
  1009 by (simp add: diff_add_assoc)
  1010 
  1011 lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
  1012 by (auto simp add: diff_add_inverse2)
  1013 
  1014 lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m \<le> n)"
  1015 by (induct m n rule: diff_induct) simp_all
  1016 
  1017 lemma diff_is_0_eq' [simp]: "m \<le> n ==> (m::nat) - n = 0"
  1018 by (rule iffD2, rule diff_is_0_eq)
  1019 
  1020 lemma zero_less_diff [simp]: "(0 < n - (m::nat)) = (m < n)"
  1021 by (induct m n rule: diff_induct) simp_all
  1022 
  1023 lemma less_imp_add_positive:
  1024   assumes "i < j"
  1025   shows "\<exists>k::nat. 0 < k & i + k = j"
  1026 proof
  1027   from assms show "0 < j - i & i + (j - i) = j"
  1028     by (simp add: order_less_imp_le)
  1029 qed
  1030 
  1031 lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
  1032 by (induct k) simp_all
  1033 
  1034 lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
  1035 by (simp add: diff_cancel add_commute)
  1036 
  1037 lemma diff_add_0: "n - (n + m) = (0::nat)"
  1038 by (induct n) simp_all
  1039 
  1040 
  1041 text {* Difference distributes over multiplication *}
  1042 
  1043 lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
  1044 by (induct m n rule: diff_induct) (simp_all add: diff_cancel)
  1045 
  1046 lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)"
  1047 by (simp add: diff_mult_distrib mult_commute [of k])
  1048   -- {* NOT added as rewrites, since sometimes they are used from right-to-left *}
  1049 
  1050 lemmas nat_distrib =
  1051   add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
  1052 
  1053 
  1054 subsection {* Monotonicity of Multiplication *}
  1055 
  1056 lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
  1057 by (simp add: mult_right_mono)
  1058 
  1059 lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
  1060 by (simp add: mult_left_mono)
  1061 
  1062 text {* @{text "\<le>"} monotonicity, BOTH arguments *}
  1063 lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
  1064 by (simp add: mult_mono)
  1065 
  1066 lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
  1067 by (simp add: mult_strict_right_mono)
  1068 
  1069 text{*Differs from the standard @{text zero_less_mult_iff} in that
  1070       there are no negative numbers.*}
  1071 lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
  1072   apply (induct m)
  1073    apply simp
  1074   apply (case_tac n)
  1075    apply simp_all
  1076   done
  1077 
  1078 lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
  1079   apply (induct m)
  1080    apply simp
  1081   apply (case_tac n)
  1082    apply simp_all
  1083   done
  1084 
  1085 lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
  1086   apply (induct m)
  1087    apply simp
  1088   apply (induct n)
  1089    apply auto
  1090   done
  1091 
  1092 lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
  1093   apply (rule trans)
  1094   apply (rule_tac [2] mult_eq_1_iff, fastsimp)
  1095   done
  1096 
  1097 lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
  1098   apply (safe intro!: mult_less_mono1)
  1099   apply (case_tac k, auto)
  1100   apply (simp del: le_0_eq add: linorder_not_le [symmetric])
  1101   apply (blast intro: mult_le_mono1)
  1102   done
  1103 
  1104 lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)"
  1105 by (simp add: mult_commute [of k])
  1106 
  1107 lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
  1108 by (simp add: linorder_not_less [symmetric], auto)
  1109 
  1110 lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
  1111 by (simp add: linorder_not_less [symmetric], auto)
  1112 
  1113 lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
  1114 apply (cut_tac less_linear, safe, auto)
  1115 apply (drule mult_less_mono1, assumption, simp)+
  1116 done
  1117 
  1118 lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
  1119 by (simp add: mult_commute [of k])
  1120 
  1121 lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
  1122 by (subst mult_less_cancel1) simp
  1123 
  1124 lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)"
  1125 by (subst mult_le_cancel1) simp
  1126 
  1127 lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
  1128 by (subst mult_cancel1) simp
  1129 
  1130 text {* Lemma for @{text gcd} *}
  1131 lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
  1132   apply (drule sym)
  1133   apply (rule disjCI)
  1134   apply (rule nat_less_cases, erule_tac [2] _)
  1135    apply (drule_tac [2] mult_less_mono2)
  1136     apply (auto)
  1137   done
  1138 
  1139 
  1140 subsection {* size of a datatype value *}
  1141 
  1142 class size = type +
  1143   fixes size :: "'a \<Rightarrow> nat"
  1144 
  1145 use "Tools/function_package/size.ML"
  1146 
  1147 setup Size.setup
  1148 
  1149 lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
  1150 by (induct n) simp_all
  1151 
  1152 lemma size_bool [code func]:
  1153   "size (b\<Colon>bool) = 0" by (cases b) auto
  1154 
  1155 declare "*.size" [noatp]
  1156 
  1157 
  1158 subsection {* Embedding of the Naturals into any
  1159   @{text semiring_1}: @{term of_nat} *}
  1160 
  1161 context semiring_1
  1162 begin
  1163 
  1164 primrec
  1165   of_nat :: "nat \<Rightarrow> 'a"
  1166 where
  1167   of_nat_0:     "of_nat 0 = 0"
  1168   | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
  1169 
  1170 lemma of_nat_1 [simp]: "of_nat 1 = 1"
  1171   by simp
  1172 
  1173 lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
  1174   by (induct m) (simp_all add: add_ac)
  1175 
  1176 lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
  1177   by (induct m) (simp_all add: add_ac left_distrib)
  1178 
  1179 end
  1180 
  1181 context ordered_semidom
  1182 begin
  1183 
  1184 lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
  1185   apply (induct m, simp_all)
  1186   apply (erule order_trans)
  1187   apply (rule ord_le_eq_trans [OF _ add_commute])
  1188   apply (rule less_add_one [THEN less_imp_le])
  1189   done
  1190 
  1191 lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
  1192   apply (induct m n rule: diff_induct, simp_all)
  1193   apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
  1194   done
  1195 
  1196 lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
  1197   apply (induct m n rule: diff_induct, simp_all)
  1198   apply (insert zero_le_imp_of_nat)
  1199   apply (force simp add: not_less [symmetric])
  1200   done
  1201 
  1202 lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
  1203   by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
  1204 
  1205 text{*Special cases where either operand is zero*}
  1206 
  1207 lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
  1208   by (rule of_nat_less_iff [of 0, simplified])
  1209 
  1210 lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
  1211   by (rule of_nat_less_iff [of _ 0, simplified])
  1212 
  1213 lemma of_nat_le_iff [simp]:
  1214   "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
  1215   by (simp add: not_less [symmetric] linorder_not_less [symmetric])
  1216 
  1217 text{*Special cases where either operand is zero*}
  1218 
  1219 lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
  1220   by (rule of_nat_le_iff [of 0, simplified])
  1221 
  1222 lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
  1223   by (rule of_nat_le_iff [of _ 0, simplified])
  1224 
  1225 end
  1226 
  1227 lemma of_nat_id [simp]: "of_nat n = n"
  1228   by (induct n) auto
  1229 
  1230 lemma of_nat_eq_id [simp]: "of_nat = id"
  1231   by (auto simp add: expand_fun_eq)
  1232 
  1233 text{*Class for unital semirings with characteristic zero.
  1234  Includes non-ordered rings like the complex numbers.*}
  1235 
  1236 class semiring_char_0 = semiring_1 +
  1237   assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
  1238 
  1239 text{*Every @{text ordered_semidom} has characteristic zero.*}
  1240 
  1241 subclass (in ordered_semidom) semiring_char_0
  1242   by unfold_locales (simp add: eq_iff order_eq_iff)
  1243 
  1244 context semiring_char_0
  1245 begin
  1246 
  1247 text{*Special cases where either operand is zero*}
  1248 
  1249 lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
  1250   by (rule of_nat_eq_iff [of 0, simplified])
  1251 
  1252 lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
  1253   by (rule of_nat_eq_iff [of _ 0, simplified])
  1254 
  1255 lemma inj_of_nat: "inj of_nat"
  1256   by (simp add: inj_on_def)
  1257 
  1258 end
  1259 
  1260 
  1261 subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
  1262 
  1263 lemma subst_equals:
  1264   assumes 1: "t = s" and 2: "u = t"
  1265   shows "u = s"
  1266   using 2 1 by (rule trans)
  1267 
  1268 use "arith_data.ML"
  1269 declaration {* K arith_data_setup *}
  1270 
  1271 use "Tools/lin_arith.ML"
  1272 declaration {* K LinArith.setup *}
  1273 
  1274 
  1275 text{*The following proofs may rely on the arithmetic proof procedures.*}
  1276 
  1277 lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
  1278 by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add)
  1279 
  1280 lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
  1281 by (simp add: less_eq reflcl_trancl [symmetric] del: reflcl_trancl, arith)
  1282 
  1283 lemma nat_diff_split:
  1284   "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
  1285     -- {* elimination of @{text -} on @{text nat} *}
  1286 by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
  1287 
  1288 context ring_1
  1289 begin
  1290 
  1291 lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
  1292   by (simp del: of_nat_add
  1293     add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
  1294 
  1295 end
  1296 
  1297 lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
  1298   unfolding abs_if by auto
  1299 
  1300 lemma nat_diff_split_asm:
  1301   "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
  1302     -- {* elimination of @{text -} on @{text nat} in assumptions *}
  1303 by (simp split: nat_diff_split)
  1304 
  1305 lemmas [arith_split] = nat_diff_split split_min split_max
  1306 
  1307 
  1308 lemma le_square: "m \<le> m * (m::nat)"
  1309 by (induct m) auto
  1310 
  1311 lemma le_cube: "(m::nat) \<le> m * (m * m)"
  1312 by (induct m) auto
  1313 
  1314 
  1315 text{*Subtraction laws, mostly by Clemens Ballarin*}
  1316 
  1317 lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
  1318 by arith
  1319 
  1320 lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
  1321 by arith
  1322 
  1323 lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
  1324 by arith
  1325 
  1326 lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
  1327 by arith
  1328 
  1329 lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
  1330 by arith
  1331 
  1332 lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
  1333 by arith
  1334 
  1335 (*Replaces the previous diff_less and le_diff_less, which had the stronger
  1336   second premise n\<le>m*)
  1337 lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
  1338 by arith
  1339 
  1340 
  1341 (** Simplification of relational expressions involving subtraction **)
  1342 
  1343 lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
  1344 by (simp split add: nat_diff_split)
  1345 
  1346 lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
  1347 by (auto split add: nat_diff_split)
  1348 
  1349 lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
  1350 by (auto split add: nat_diff_split)
  1351 
  1352 lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
  1353 by (auto split add: nat_diff_split)
  1354 
  1355 
  1356 text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
  1357 
  1358 (* Monotonicity of subtraction in first argument *)
  1359 lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
  1360 by (simp split add: nat_diff_split)
  1361 
  1362 lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
  1363 by (simp split add: nat_diff_split)
  1364 
  1365 lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
  1366 by (simp split add: nat_diff_split)
  1367 
  1368 lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
  1369 by (simp split add: nat_diff_split)
  1370 
  1371 text{*Lemmas for ex/Factorization*}
  1372 
  1373 lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
  1374 by (cases m) auto
  1375 
  1376 lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
  1377 by (cases m) auto
  1378 
  1379 lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
  1380 by (cases m) auto
  1381 
  1382 text {* Specialized induction principles that work "backwards": *}
  1383 
  1384 lemma inc_induct[consumes 1, case_names base step]:
  1385   assumes less: "i <= j"
  1386   assumes base: "P j"
  1387   assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i"
  1388   shows "P i"
  1389   using less
  1390 proof (induct d=="j - i" arbitrary: i)
  1391   case (0 i)
  1392   hence "i = j" by simp
  1393   with base show ?case by simp
  1394 next
  1395   case (Suc d i)
  1396   hence "i < j" "P (Suc i)"
  1397     by simp_all
  1398   thus "P i" by (rule step)
  1399 qed
  1400 
  1401 lemma strict_inc_induct[consumes 1, case_names base step]:
  1402   assumes less: "i < j"
  1403   assumes base: "!!i. j = Suc i ==> P i"
  1404   assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i"
  1405   shows "P i"
  1406   using less
  1407 proof (induct d=="j - i - 1" arbitrary: i)
  1408   case (0 i)
  1409   with `i < j` have "j = Suc i" by simp
  1410   with base show ?case by simp
  1411 next
  1412   case (Suc d i)
  1413   hence "i < j" "P (Suc i)"
  1414     by simp_all
  1415   thus "P i" by (rule step)
  1416 qed
  1417 
  1418 lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
  1419   using inc_induct[of "k - i" k P, simplified] by blast
  1420 
  1421 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
  1422   using inc_induct[of 0 k P] by blast
  1423 
  1424 text{*Rewriting to pull differences out*}
  1425 
  1426 lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
  1427 by arith
  1428 
  1429 lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
  1430 by arith
  1431 
  1432 lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
  1433 by arith
  1434 
  1435 (*The others are
  1436       i - j - k = i - (j + k),
  1437       k \<le> j ==> j - k + i = j + i - k,
  1438       k \<le> j ==> i + (j - k) = i + j - k *)
  1439 lemmas add_diff_assoc = diff_add_assoc [symmetric]
  1440 lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
  1441 declare diff_diff_left [simp]  add_diff_assoc [simp]  add_diff_assoc2[simp]
  1442 
  1443 text{*At present we prove no analogue of @{text not_less_Least} or @{text
  1444 Least_Suc}, since there appears to be no need.*}
  1445 
  1446 
  1447 subsection {*The Set of Natural Numbers*}
  1448 
  1449 context semiring_1
  1450 begin
  1451 
  1452 definition
  1453   Nats  :: "'a set" where
  1454   "Nats = range of_nat"
  1455 
  1456 notation (xsymbols)
  1457   Nats  ("\<nat>")
  1458 
  1459 lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
  1460   by (simp add: Nats_def)
  1461 
  1462 lemma Nats_0 [simp]: "0 \<in> \<nat>"
  1463 apply (simp add: Nats_def)
  1464 apply (rule range_eqI)
  1465 apply (rule of_nat_0 [symmetric])
  1466 done
  1467 
  1468 lemma Nats_1 [simp]: "1 \<in> \<nat>"
  1469 apply (simp add: Nats_def)
  1470 apply (rule range_eqI)
  1471 apply (rule of_nat_1 [symmetric])
  1472 done
  1473 
  1474 lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
  1475 apply (auto simp add: Nats_def)
  1476 apply (rule range_eqI)
  1477 apply (rule of_nat_add [symmetric])
  1478 done
  1479 
  1480 lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
  1481 apply (auto simp add: Nats_def)
  1482 apply (rule range_eqI)
  1483 apply (rule of_nat_mult [symmetric])
  1484 done
  1485 
  1486 end
  1487 
  1488 
  1489 text {* the lattice order on @{typ nat} *}
  1490 
  1491 instantiation nat :: distrib_lattice
  1492 begin
  1493 
  1494 definition
  1495   "(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min"
  1496 
  1497 definition
  1498   "(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max"
  1499 
  1500 instance by intro_classes
  1501   (simp_all add: inf_nat_def sup_nat_def)
  1502 
  1503 end
  1504 
  1505 
  1506 subsection {* legacy bindings *}
  1507 
  1508 ML
  1509 {*
  1510 val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
  1511 val nat_diff_split = thm "nat_diff_split";
  1512 val nat_diff_split_asm = thm "nat_diff_split_asm";
  1513 val le_square = thm "le_square";
  1514 val le_cube = thm "le_cube";
  1515 val diff_less_mono = thm "diff_less_mono";
  1516 val less_diff_conv = thm "less_diff_conv";
  1517 val le_diff_conv = thm "le_diff_conv";
  1518 val le_diff_conv2 = thm "le_diff_conv2";
  1519 val diff_diff_cancel = thm "diff_diff_cancel";
  1520 val le_add_diff = thm "le_add_diff";
  1521 val diff_less = thm "diff_less";
  1522 val diff_diff_eq = thm "diff_diff_eq";
  1523 val eq_diff_iff = thm "eq_diff_iff";
  1524 val less_diff_iff = thm "less_diff_iff";
  1525 val le_diff_iff = thm "le_diff_iff";
  1526 val diff_le_mono = thm "diff_le_mono";
  1527 val diff_le_mono2 = thm "diff_le_mono2";
  1528 val diff_less_mono2 = thm "diff_less_mono2";
  1529 val diffs0_imp_equal = thm "diffs0_imp_equal";
  1530 val one_less_mult = thm "one_less_mult";
  1531 val n_less_m_mult_n = thm "n_less_m_mult_n";
  1532 val n_less_n_mult_m = thm "n_less_n_mult_m";
  1533 val diff_diff_right = thm "diff_diff_right";
  1534 val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
  1535 val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
  1536 *}
  1537 
  1538 end