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