src/HOL/Integ/IntArith.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17472 bcbf48d59059
child 19601 299d4cd2ef51
permissions -rw-r--r--
adaptions to codegen_package
     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 lemmas int_eq_iff_number_of = int_eq_iff [of _ "number_of v", standard]
   186 declare int_eq_iff_number_of [simp]
   187 
   188 
   189 lemma split_nat [arith_split]:
   190   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   191   (is "?P = (?L & ?R)")
   192 proof (cases "i < 0")
   193   case True thus ?thesis by simp
   194 next
   195   case False
   196   have "?P = ?L"
   197   proof
   198     assume ?P thus ?L using False by clarsimp
   199   next
   200     assume ?L thus ?P using False by simp
   201   qed
   202   with False show ?thesis by simp
   203 qed
   204 
   205 
   206 (*Analogous to zadd_int*)
   207 lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)" 
   208 by (induct m n rule: diff_induct, simp_all)
   209 
   210 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
   211 apply (case_tac "0 \<le> z'")
   212 apply (rule inj_int [THEN injD])
   213 apply (simp add: int_mult zero_le_mult_iff)
   214 apply (simp add: mult_le_0_iff)
   215 done
   216 
   217 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
   218 apply (rule trans)
   219 apply (rule_tac [2] nat_mult_distrib, auto)
   220 done
   221 
   222 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
   223 apply (case_tac "z=0 | w=0")
   224 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
   225                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
   226 done
   227 
   228 
   229 subsection "Induction principles for int"
   230 
   231                      (* `set:int': dummy construction *)
   232 theorem int_ge_induct[case_names base step,induct set:int]:
   233   assumes ge: "k \<le> (i::int)" and
   234         base: "P(k)" and
   235         step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
   236   shows "P i"
   237 proof -
   238   { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
   239     proof (induct n)
   240       case 0
   241       hence "i = k" by arith
   242       thus "P i" using base by simp
   243     next
   244       case (Suc n)
   245       hence "n = nat((i - 1) - k)" by arith
   246       moreover
   247       have ki1: "k \<le> i - 1" using Suc.prems by arith
   248       ultimately
   249       have "P(i - 1)" by(rule Suc.hyps)
   250       from step[OF ki1 this] show ?case by simp
   251     qed
   252   }
   253   with ge show ?thesis by fast
   254 qed
   255 
   256                      (* `set:int': dummy construction *)
   257 theorem int_gr_induct[case_names base step,induct set:int]:
   258   assumes gr: "k < (i::int)" and
   259         base: "P(k+1)" and
   260         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
   261   shows "P i"
   262 apply(rule int_ge_induct[of "k + 1"])
   263   using gr apply arith
   264  apply(rule base)
   265 apply (rule step, simp+)
   266 done
   267 
   268 theorem int_le_induct[consumes 1,case_names base step]:
   269   assumes le: "i \<le> (k::int)" and
   270         base: "P(k)" and
   271         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   272   shows "P i"
   273 proof -
   274   { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
   275     proof (induct n)
   276       case 0
   277       hence "i = k" by arith
   278       thus "P i" using base by simp
   279     next
   280       case (Suc n)
   281       hence "n = nat(k - (i+1))" by arith
   282       moreover
   283       have ki1: "i + 1 \<le> k" using Suc.prems by arith
   284       ultimately
   285       have "P(i+1)" by(rule Suc.hyps)
   286       from step[OF ki1 this] show ?case by simp
   287     qed
   288   }
   289   with le show ?thesis by fast
   290 qed
   291 
   292 theorem int_less_induct [consumes 1,case_names base step]:
   293   assumes less: "(i::int) < k" and
   294         base: "P(k - 1)" and
   295         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   296   shows "P i"
   297 apply(rule int_le_induct[of _ "k - 1"])
   298   using less apply arith
   299  apply(rule base)
   300 apply (rule step, simp+)
   301 done
   302 
   303 subsection{*Intermediate value theorems*}
   304 
   305 lemma int_val_lemma:
   306      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
   307       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
   308 apply (induct_tac "n", simp)
   309 apply (intro strip)
   310 apply (erule impE, simp)
   311 apply (erule_tac x = n in allE, simp)
   312 apply (case_tac "k = f (n+1) ")
   313  apply force
   314 apply (erule impE)
   315  apply (simp add: abs_if split add: split_if_asm)
   316 apply (blast intro: le_SucI)
   317 done
   318 
   319 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
   320 
   321 lemma nat_intermed_int_val:
   322      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
   323          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
   324 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
   325        in int_val_lemma)
   326 apply simp
   327 apply (erule impE)
   328  apply (intro strip)
   329  apply (erule_tac x = "i+m" in allE, arith)
   330 apply (erule exE)
   331 apply (rule_tac x = "i+m" in exI, arith)
   332 done
   333 
   334 
   335 subsection{*Products and 1, by T. M. Rasmussen*}
   336 
   337 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
   338 by arith
   339 
   340 lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
   341 apply (case_tac "\<bar>n\<bar>=1") 
   342 apply (simp add: abs_mult) 
   343 apply (rule ccontr) 
   344 apply (auto simp add: linorder_neq_iff abs_mult) 
   345 apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
   346  prefer 2 apply arith 
   347 apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) 
   348 apply (rule mult_mono, auto) 
   349 done
   350 
   351 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
   352 by (insert abs_zmult_eq_1 [of m n], arith)
   353 
   354 lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
   355 apply (auto dest: pos_zmult_eq_1_iff_lemma) 
   356 apply (simp add: mult_commute [of m]) 
   357 apply (frule pos_zmult_eq_1_iff_lemma, auto) 
   358 done
   359 
   360 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
   361 apply (rule iffI) 
   362  apply (frule pos_zmult_eq_1_iff_lemma)
   363  apply (simp add: mult_commute [of m]) 
   364  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
   365 done
   366 
   367 ML
   368 {*
   369 val zle_diff1_eq = thm "zle_diff1_eq";
   370 val zle_add1_eq_le = thm "zle_add1_eq_le";
   371 val nonneg_eq_int = thm "nonneg_eq_int";
   372 val abs_minus_one = thm "abs_minus_one";
   373 val of_int_number_of_eq = thm"of_int_number_of_eq";
   374 val nat_eq_iff = thm "nat_eq_iff";
   375 val nat_eq_iff2 = thm "nat_eq_iff2";
   376 val nat_less_iff = thm "nat_less_iff";
   377 val int_eq_iff = thm "int_eq_iff";
   378 val nat_0 = thm "nat_0";
   379 val nat_1 = thm "nat_1";
   380 val nat_2 = thm "nat_2";
   381 val nat_less_eq_zless = thm "nat_less_eq_zless";
   382 val nat_le_eq_zle = thm "nat_le_eq_zle";
   383 
   384 val nat_intermed_int_val = thm "nat_intermed_int_val";
   385 val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
   386 val zmult_eq_1_iff = thm "zmult_eq_1_iff";
   387 val nat_add_distrib = thm "nat_add_distrib";
   388 val nat_diff_distrib = thm "nat_diff_distrib";
   389 val nat_mult_distrib = thm "nat_mult_distrib";
   390 val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
   391 val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
   392 *}
   393 
   394 end