src/HOL/NatArith.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17688 91d3604ec4b5
child 21238 c46bc715bdfd
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/NatArith.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel
     4 *)
     5 
     6 header {*Further Arithmetic Facts Concerning the Natural Numbers*}
     7 
     8 theory NatArith
     9 imports Nat
    10 uses "arith_data.ML"
    11 begin
    12 
    13 setup arith_setup
    14 
    15 text{*The following proofs may rely on the arithmetic proof procedures.*}
    16 
    17 lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
    18   by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add)
    19 
    20 lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
    21 by (simp add: less_eq reflcl_trancl [symmetric]
    22             del: reflcl_trancl, arith)
    23 
    24 lemma nat_diff_split:
    25     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
    26     -- {* elimination of @{text -} on @{text nat} *}
    27   by (cases "a<b" rule: case_split)
    28      (auto simp add: diff_is_0_eq [THEN iffD2])
    29 
    30 lemma nat_diff_split_asm:
    31     "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
    32     -- {* elimination of @{text -} on @{text nat} in assumptions *}
    33   by (simp split: nat_diff_split)
    34 
    35 lemmas [arith_split] = nat_diff_split split_min split_max
    36 
    37 
    38 
    39 lemma le_square: "m \<le> m*(m::nat)"
    40 by (induct_tac "m", auto)
    41 
    42 lemma le_cube: "(m::nat) \<le> m*(m*m)"
    43 by (induct_tac "m", auto)
    44 
    45 
    46 text{*Subtraction laws, mostly by Clemens Ballarin*}
    47 
    48 lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
    49 by arith
    50 
    51 lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
    52 by arith
    53 
    54 lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
    55 by arith
    56 
    57 lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
    58 by arith
    59 
    60 lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
    61 by arith
    62 
    63 lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
    64 by arith
    65 
    66 (*Replaces the previous diff_less and le_diff_less, which had the stronger
    67   second premise n\<le>m*)
    68 lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
    69 by arith
    70 
    71 
    72 (** Simplification of relational expressions involving subtraction **)
    73 
    74 lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
    75 by (simp split add: nat_diff_split)
    76 
    77 lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
    78 by (auto split add: nat_diff_split)
    79 
    80 lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
    81 by (auto split add: nat_diff_split)
    82 
    83 lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
    84 by (auto split add: nat_diff_split)
    85 
    86 
    87 text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
    88 
    89 (* Monotonicity of subtraction in first argument *)
    90 lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
    91 by (simp split add: nat_diff_split)
    92 
    93 lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
    94 by (simp split add: nat_diff_split)
    95 
    96 lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
    97 by (simp split add: nat_diff_split)
    98 
    99 lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
   100 by (simp split add: nat_diff_split)
   101 
   102 text{*Lemmas for ex/Factorization*}
   103 
   104 lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
   105 by (case_tac "m", auto)
   106 
   107 lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
   108 by (case_tac "m", auto)
   109 
   110 lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
   111 by (case_tac "m", auto)
   112 
   113 
   114 text{*Rewriting to pull differences out*}
   115 
   116 lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
   117 by arith
   118 
   119 lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
   120 by arith
   121 
   122 lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
   123 by arith
   124 
   125 (*The others are
   126       i - j - k = i - (j + k),
   127       k \<le> j ==> j - k + i = j + i - k,
   128       k \<le> j ==> i + (j - k) = i + j - k *)
   129 lemmas add_diff_assoc = diff_add_assoc [symmetric]
   130 lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
   131 declare diff_diff_left [simp]  add_diff_assoc [simp]  add_diff_assoc2[simp]
   132 
   133 text{*At present we prove no analogue of @{text not_less_Least} or @{text
   134 Least_Suc}, since there appears to be no need.*}
   135 
   136 ML
   137 {*
   138 val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
   139 val nat_diff_split = thm "nat_diff_split";
   140 val nat_diff_split_asm = thm "nat_diff_split_asm";
   141 val le_square = thm "le_square";
   142 val le_cube = thm "le_cube";
   143 val diff_less_mono = thm "diff_less_mono";
   144 val less_diff_conv = thm "less_diff_conv";
   145 val le_diff_conv = thm "le_diff_conv";
   146 val le_diff_conv2 = thm "le_diff_conv2";
   147 val diff_diff_cancel = thm "diff_diff_cancel";
   148 val le_add_diff = thm "le_add_diff";
   149 val diff_less = thm "diff_less";
   150 val diff_diff_eq = thm "diff_diff_eq";
   151 val eq_diff_iff = thm "eq_diff_iff";
   152 val less_diff_iff = thm "less_diff_iff";
   153 val le_diff_iff = thm "le_diff_iff";
   154 val diff_le_mono = thm "diff_le_mono";
   155 val diff_le_mono2 = thm "diff_le_mono2";
   156 val diff_less_mono2 = thm "diff_less_mono2";
   157 val diffs0_imp_equal = thm "diffs0_imp_equal";
   158 val one_less_mult = thm "one_less_mult";
   159 val n_less_m_mult_n = thm "n_less_m_mult_n";
   160 val n_less_n_mult_m = thm "n_less_n_mult_m";
   161 val diff_diff_right = thm "diff_diff_right";
   162 val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
   163 val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
   164 *}
   165 
   166 subsection{*Embedding of the Naturals into any @{text
   167 comm_semiring_1_cancel}: @{term of_nat}*}
   168 
   169 consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
   170 
   171 primrec
   172   of_nat_0:   "of_nat 0 = 0"
   173   of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
   174 
   175 lemma of_nat_1 [simp]: "of_nat 1 = 1"
   176 by simp
   177 
   178 lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
   179 apply (induct m)
   180 apply (simp_all add: add_ac)
   181 done
   182 
   183 lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
   184 apply (induct m)
   185 apply (simp_all add: mult_ac add_ac right_distrib)
   186 done
   187 
   188 lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
   189 apply (induct m, simp_all)
   190 apply (erule order_trans)
   191 apply (rule less_add_one [THEN order_less_imp_le])
   192 done
   193 
   194 lemma less_imp_of_nat_less:
   195      "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
   196 apply (induct m n rule: diff_induct, simp_all)
   197 apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
   198 done
   199 
   200 lemma of_nat_less_imp_less:
   201      "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
   202 apply (induct m n rule: diff_induct, simp_all)
   203 apply (insert zero_le_imp_of_nat)
   204 apply (force simp add: linorder_not_less [symmetric])
   205 done
   206 
   207 lemma of_nat_less_iff [simp]:
   208      "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
   209 by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
   210 
   211 text{*Special cases where either operand is zero*}
   212 lemmas of_nat_0_less_iff = of_nat_less_iff [of 0, simplified]
   213 lemmas of_nat_less_0_iff = of_nat_less_iff [of _ 0, simplified]
   214 declare of_nat_0_less_iff [simp]
   215 declare of_nat_less_0_iff [simp]
   216 
   217 lemma of_nat_le_iff [simp]:
   218      "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
   219 by (simp add: linorder_not_less [symmetric])
   220 
   221 text{*Special cases where either operand is zero*}
   222 lemmas of_nat_0_le_iff = of_nat_le_iff [of 0, simplified]
   223 lemmas of_nat_le_0_iff = of_nat_le_iff [of _ 0, simplified]
   224 declare of_nat_0_le_iff [simp]
   225 declare of_nat_le_0_iff [simp]
   226 
   227 text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
   228 to exclude the possibility of a finite field, which indeed wraps back to
   229 zero.*}
   230 lemma of_nat_eq_iff [simp]:
   231      "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
   232 by (simp add: order_eq_iff)
   233 
   234 text{*Special cases where either operand is zero*}
   235 lemmas of_nat_0_eq_iff = of_nat_eq_iff [of 0, simplified]
   236 lemmas of_nat_eq_0_iff = of_nat_eq_iff [of _ 0, simplified]
   237 declare of_nat_0_eq_iff [simp]
   238 declare of_nat_eq_0_iff [simp]
   239 
   240 lemma of_nat_diff [simp]:
   241      "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
   242 by (simp del: of_nat_add
   243 	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
   244 
   245 
   246 end