src/HOL/IntArith.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24195 7d1a16c77f7c
child 25162 ad4d5365d9d8
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/IntArith.thy
     2     ID:         $Id$
     3     Authors:    Larry Paulson and Tobias Nipkow
     4 *)
     5 
     6 header {* Integer arithmetic *}
     7 
     8 theory IntArith
     9 imports Numeral Wellfounded_Relations
    10 uses
    11   "~~/src/Provers/Arith/assoc_fold.ML"
    12   "~~/src/Provers/Arith/cancel_numerals.ML"
    13   "~~/src/Provers/Arith/combine_numerals.ML"
    14   ("int_arith1.ML")
    15 begin
    16 
    17 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
    18 
    19 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
    20 by simp 
    21 
    22 lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
    23 by simp
    24 
    25 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
    26 by simp 
    27 
    28 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
    29 by simp
    30 
    31 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
    32 by simp
    33 
    34 lemma inverse_numeral_1:
    35   "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
    36 by simp
    37 
    38 text{*Theorem lists for the cancellation simprocs. The use of binary numerals
    39 for 0 and 1 reduces the number of special cases.*}
    40 
    41 lemmas add_0s = add_numeral_0 add_numeral_0_right
    42 lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
    43                  mult_minus1 mult_minus1_right
    44 
    45 
    46 subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
    47 
    48 text{*Arithmetic computations are defined for binary literals, which leaves 0
    49 and 1 as special cases. Addition already has rules for 0, but not 1.
    50 Multiplication and unary minus already have rules for both 0 and 1.*}
    51 
    52 
    53 lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
    54 by simp
    55 
    56 
    57 lemmas add_number_of_eq = number_of_add [symmetric]
    58 
    59 text{*Allow 1 on either or both sides*}
    60 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
    61 by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
    62 
    63 lemmas add_special =
    64     one_add_one_is_two
    65     binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
    66     binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
    67 
    68 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
    69 lemmas diff_special =
    70     binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
    71     binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
    72 
    73 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
    74 lemmas eq_special =
    75     binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
    76     binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
    77     binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
    78     binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
    79 
    80 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
    81 lemmas less_special =
    82   binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
    83   binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
    84   binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
    85   binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
    86 
    87 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
    88 lemmas le_special =
    89     binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
    90     binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
    91     binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
    92     binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
    93 
    94 lemmas arith_special[simp] = 
    95        add_special diff_special eq_special less_special le_special
    96 
    97 
    98 lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
    99                    max (0::int) 1 = 1 & max (1::int) 0 = 1"
   100 by(simp add:min_def max_def)
   101 
   102 lemmas min_max_special[simp] =
   103  min_max_01
   104  max_def[of "0::int" "number_of v", standard, simp]
   105  min_def[of "0::int" "number_of v", standard, simp]
   106  max_def[of "number_of u" "0::int", standard, simp]
   107  min_def[of "number_of u" "0::int", standard, simp]
   108  max_def[of "1::int" "number_of v", standard, simp]
   109  min_def[of "1::int" "number_of v", standard, simp]
   110  max_def[of "number_of u" "1::int", standard, simp]
   111  min_def[of "number_of u" "1::int", standard, simp]
   112 
   113 use "int_arith1.ML"
   114 declaration {* K int_arith_setup *}
   115 
   116 
   117 subsection{*Lemmas About Small Numerals*}
   118 
   119 lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
   120 proof -
   121   have "(of_int -1 :: 'a) = of_int (- 1)" by simp
   122   also have "... = - of_int 1" by (simp only: of_int_minus)
   123   also have "... = -1" by simp
   124   finally show ?thesis .
   125 qed
   126 
   127 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
   128 by (simp add: abs_if)
   129 
   130 lemma abs_power_minus_one [simp]:
   131      "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
   132 by (simp add: power_abs)
   133 
   134 lemma of_int_number_of_eq:
   135      "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
   136 by (simp add: number_of_eq) 
   137 
   138 text{*Lemmas for specialist use, NOT as default simprules*}
   139 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
   140 proof -
   141   have "2*z = (1 + 1)*z" by simp
   142   also have "... = z+z" by (simp add: left_distrib)
   143   finally show ?thesis .
   144 qed
   145 
   146 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
   147 by (subst mult_commute, rule mult_2)
   148 
   149 
   150 subsection{*More Inequality Reasoning*}
   151 
   152 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
   153 by arith
   154 
   155 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
   156 by arith
   157 
   158 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
   159 by arith
   160 
   161 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
   162 by arith
   163 
   164 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
   165 by arith
   166 
   167 
   168 subsection{*The Functions @{term nat} and @{term int}*}
   169 
   170 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
   171   @{term "w + - z"}*}
   172 declare Zero_int_def [symmetric, simp]
   173 declare One_int_def [symmetric, simp]
   174 
   175 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
   176 
   177 lemma nat_0: "nat 0 = 0"
   178 by (simp add: nat_eq_iff)
   179 
   180 lemma nat_1: "nat 1 = Suc 0"
   181 by (subst nat_eq_iff, simp)
   182 
   183 lemma nat_2: "nat 2 = Suc (Suc 0)"
   184 by (subst nat_eq_iff, simp)
   185 
   186 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
   187 apply (insert zless_nat_conj [of 1 z])
   188 apply (auto simp add: nat_1)
   189 done
   190 
   191 text{*This simplifies expressions of the form @{term "int n = z"} where
   192       z is an integer literal.*}
   193 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
   194 
   195 lemma split_nat [arith_split]:
   196   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   197   (is "?P = (?L & ?R)")
   198 proof (cases "i < 0")
   199   case True thus ?thesis by auto
   200 next
   201   case False
   202   have "?P = ?L"
   203   proof
   204     assume ?P thus ?L using False by clarsimp
   205   next
   206     assume ?L thus ?P using False by simp
   207   qed
   208   with False show ?thesis by simp
   209 qed
   210 
   211 lemma of_int_of_nat: "of_int k = (if k < 0 then - of_nat (nat (- k))
   212   else of_nat (nat k))"
   213   by (auto simp add: of_nat_nat)
   214 
   215 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
   216 apply (cases "0 \<le> z'")
   217 apply (rule inj_int [THEN injD])
   218 apply (simp add: int_mult zero_le_mult_iff)
   219 apply (simp add: mult_le_0_iff)
   220 done
   221 
   222 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
   223 apply (rule trans)
   224 apply (rule_tac [2] nat_mult_distrib, auto)
   225 done
   226 
   227 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
   228 apply (cases "z=0 | w=0")
   229 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
   230                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
   231 done
   232 
   233 
   234 subsection "Induction principles for int"
   235 
   236 text{*Well-founded segments of the integers*}
   237 
   238 definition
   239   int_ge_less_than  ::  "int => (int * int) set"
   240 where
   241   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
   242 
   243 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
   244 proof -
   245   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
   246     by (auto simp add: int_ge_less_than_def)
   247   thus ?thesis 
   248     by (rule wf_subset [OF wf_measure]) 
   249 qed
   250 
   251 text{*This variant looks odd, but is typical of the relations suggested
   252 by RankFinder.*}
   253 
   254 definition
   255   int_ge_less_than2 ::  "int => (int * int) set"
   256 where
   257   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
   258 
   259 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
   260 proof -
   261   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))" 
   262     by (auto simp add: int_ge_less_than2_def)
   263   thus ?thesis 
   264     by (rule wf_subset [OF wf_measure]) 
   265 qed
   266 
   267 (* `set:int': dummy construction *)
   268 theorem int_ge_induct [case_names base step, induct set:int]:
   269   fixes i :: int
   270   assumes ge: "k \<le> i" and
   271     base: "P k" and
   272     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
   273   shows "P i"
   274 proof -
   275   { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
   276     proof (induct n)
   277       case 0
   278       hence "i = k" by arith
   279       thus "P i" using base by simp
   280     next
   281       case (Suc n)
   282       then have "n = nat((i - 1) - k)" by arith
   283       moreover
   284       have ki1: "k \<le> i - 1" using Suc.prems by arith
   285       ultimately
   286       have "P(i - 1)" by(rule Suc.hyps)
   287       from step[OF ki1 this] show ?case by simp
   288     qed
   289   }
   290   with ge show ?thesis by fast
   291 qed
   292 
   293                      (* `set:int': dummy construction *)
   294 theorem int_gr_induct[case_names base step,induct set:int]:
   295   assumes gr: "k < (i::int)" and
   296         base: "P(k+1)" and
   297         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
   298   shows "P i"
   299 apply(rule int_ge_induct[of "k + 1"])
   300   using gr apply arith
   301  apply(rule base)
   302 apply (rule step, simp+)
   303 done
   304 
   305 theorem int_le_induct[consumes 1,case_names base step]:
   306   assumes le: "i \<le> (k::int)" and
   307         base: "P(k)" and
   308         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   309   shows "P i"
   310 proof -
   311   { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
   312     proof (induct n)
   313       case 0
   314       hence "i = k" by arith
   315       thus "P i" using base by simp
   316     next
   317       case (Suc n)
   318       hence "n = nat(k - (i+1))" by arith
   319       moreover
   320       have ki1: "i + 1 \<le> k" using Suc.prems by arith
   321       ultimately
   322       have "P(i+1)" by(rule Suc.hyps)
   323       from step[OF ki1 this] show ?case by simp
   324     qed
   325   }
   326   with le show ?thesis by fast
   327 qed
   328 
   329 theorem int_less_induct [consumes 1,case_names base step]:
   330   assumes less: "(i::int) < k" and
   331         base: "P(k - 1)" and
   332         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   333   shows "P i"
   334 apply(rule int_le_induct[of _ "k - 1"])
   335   using less apply arith
   336  apply(rule base)
   337 apply (rule step, simp+)
   338 done
   339 
   340 subsection{*Intermediate value theorems*}
   341 
   342 lemma int_val_lemma:
   343      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
   344       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
   345 apply (induct_tac "n", simp)
   346 apply (intro strip)
   347 apply (erule impE, simp)
   348 apply (erule_tac x = n in allE, simp)
   349 apply (case_tac "k = f (n+1) ")
   350  apply force
   351 apply (erule impE)
   352  apply (simp add: abs_if split add: split_if_asm)
   353 apply (blast intro: le_SucI)
   354 done
   355 
   356 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
   357 
   358 lemma nat_intermed_int_val:
   359      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
   360          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
   361 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
   362        in int_val_lemma)
   363 apply simp
   364 apply (erule exE)
   365 apply (rule_tac x = "i+m" in exI, arith)
   366 done
   367 
   368 
   369 subsection{*Products and 1, by T. M. Rasmussen*}
   370 
   371 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
   372 by arith
   373 
   374 lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
   375 apply (cases "\<bar>n\<bar>=1") 
   376 apply (simp add: abs_mult) 
   377 apply (rule ccontr) 
   378 apply (auto simp add: linorder_neq_iff abs_mult) 
   379 apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
   380  prefer 2 apply arith 
   381 apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) 
   382 apply (rule mult_mono, auto) 
   383 done
   384 
   385 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
   386 by (insert abs_zmult_eq_1 [of m n], arith)
   387 
   388 lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
   389 apply (auto dest: pos_zmult_eq_1_iff_lemma) 
   390 apply (simp add: mult_commute [of m]) 
   391 apply (frule pos_zmult_eq_1_iff_lemma, auto) 
   392 done
   393 
   394 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
   395 apply (rule iffI) 
   396  apply (frule pos_zmult_eq_1_iff_lemma)
   397  apply (simp add: mult_commute [of m]) 
   398  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
   399 done
   400 
   401 
   402 subsection {* Legacy ML bindings *}
   403 
   404 ML {*
   405 val of_int_number_of_eq = @{thm of_int_number_of_eq};
   406 val nat_0 = @{thm nat_0};
   407 val nat_1 = @{thm nat_1};
   408 *}
   409 
   410 end