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
```