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