author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 16413 | 47ffc49c7d7b |
child 17085 | 5b57f995a179 |
permissions | -rw-r--r-- |
14259 | 1 |
(* Title: HOL/Integ/IntArith.thy |
2 |
ID: $Id$ |
|
3 |
Authors: Larry Paulson and Tobias Nipkow |
|
4 |
*) |
|
12023 | 5 |
|
6 |
header {* Integer arithmetic *} |
|
7 |
||
15131 | 8 |
theory IntArith |
15140 | 9 |
imports Numeral |
16417 | 10 |
uses ("int_arith1.ML") |
15131 | 11 |
begin |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9214
diff
changeset
|
12 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
13 |
text{*Duplicate: can't understand why it's necessary*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
14 |
declare numeral_0_eq_0 [simp] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
15 |
|
16413 | 16 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
17 |
subsection{*Instantiating Binary Arithmetic for the Integers*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
18 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
19 |
instance |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
20 |
int :: number .. |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
21 |
|
15013 | 22 |
defs (overloaded) |
23 |
int_number_of_def: "(number_of w :: int) == of_int (Rep_Bin w)" |
|
24 |
--{*the type constraint is essential!*} |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
25 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
26 |
instance int :: number_ring |
15013 | 27 |
by (intro_classes, simp add: int_number_of_def) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
28 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset
|
29 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
30 |
subsection{*Inequality Reasoning for the Arithmetic Simproc*} |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
31 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
32 |
lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
33 |
by simp |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
34 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
35 |
lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
36 |
by simp |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
37 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
38 |
lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
39 |
by simp |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
40 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
41 |
lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
42 |
by simp |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
43 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
44 |
text{*Theorem lists for the cancellation simprocs. The use of binary numerals |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
45 |
for 0 and 1 reduces the number of special cases.*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
46 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
47 |
lemmas add_0s = add_numeral_0 add_numeral_0_right |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
48 |
lemmas mult_1s = mult_numeral_1 mult_numeral_1_right |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
49 |
mult_minus1 mult_minus1_right |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
50 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
51 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
52 |
subsection{*Special Arithmetic Rules for Abstract 0 and 1*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
53 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
54 |
text{*Arithmetic computations are defined for binary literals, which leaves 0 |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
55 |
and 1 as special cases. Addition already has rules for 0, but not 1. |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
56 |
Multiplication and unary minus already have rules for both 0 and 1.*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
57 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
58 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
59 |
lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
60 |
by simp |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
61 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
62 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
63 |
lemmas add_number_of_eq = number_of_add [symmetric] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
64 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
65 |
text{*Allow 1 on either or both sides*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
66 |
lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
67 |
by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
68 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
69 |
lemmas add_special = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
70 |
one_add_one_is_two |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
71 |
binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
72 |
binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
73 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
74 |
text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
75 |
lemmas diff_special = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
76 |
binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
77 |
binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
78 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
79 |
text{*Allow 0 or 1 on either side with a binary numeral on the other*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
80 |
lemmas eq_special = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
81 |
binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
82 |
binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
83 |
binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
84 |
binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
85 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
86 |
text{*Allow 0 or 1 on either side with a binary numeral on the other*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
87 |
lemmas less_special = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
88 |
binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
89 |
binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
90 |
binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
91 |
binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
92 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
93 |
text{*Allow 0 or 1 on either side with a binary numeral on the other*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
94 |
lemmas le_special = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
95 |
binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
96 |
binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
97 |
binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
98 |
binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard] |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
99 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
100 |
lemmas arith_special = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
101 |
add_special diff_special eq_special less_special le_special |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
102 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
103 |
|
12023 | 104 |
use "int_arith1.ML" |
105 |
setup int_arith_setup |
|
14259 | 106 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset
|
107 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
108 |
subsection{*Lemmas About Small Numerals*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
109 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
110 |
lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
111 |
proof - |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
112 |
have "(of_int -1 :: 'a) = of_int (- 1)" by simp |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
113 |
also have "... = - of_int 1" by (simp only: of_int_minus) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
114 |
also have "... = -1" by simp |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
115 |
finally show ?thesis . |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
116 |
qed |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
117 |
|
14738 | 118 |
lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
119 |
by (simp add: abs_if) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
120 |
|
14436 | 121 |
lemma abs_power_minus_one [simp]: |
15003 | 122 |
"abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})" |
14436 | 123 |
by (simp add: power_abs) |
124 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
125 |
lemma of_int_number_of_eq: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
126 |
"of_int (number_of v) = (number_of v :: 'a :: number_ring)" |
15013 | 127 |
by (simp add: number_of_eq) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
128 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
129 |
text{*Lemmas for specialist use, NOT as default simprules*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
130 |
lemma mult_2: "2 * z = (z+z::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
131 |
proof - |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
132 |
have "2*z = (1 + 1)*z" by simp |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
133 |
also have "... = z+z" by (simp add: left_distrib) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
134 |
finally show ?thesis . |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
135 |
qed |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
136 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
137 |
lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
138 |
by (subst mult_commute, rule mult_2) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
139 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
140 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
141 |
subsection{*More Inequality Reasoning*} |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
142 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
143 |
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)" |
14259 | 144 |
by arith |
145 |
||
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
146 |
lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
147 |
by arith |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
148 |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
149 |
lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)" |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
150 |
by arith |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
151 |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
152 |
lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)" |
14259 | 153 |
by arith |
154 |
||
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
155 |
lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
156 |
by arith |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
157 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset
|
158 |
|
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset
|
159 |
subsection{*The Functions @{term nat} and @{term int}*} |
14259 | 160 |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset
|
161 |
text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset
|
162 |
@{term "w + - z"}*} |
14259 | 163 |
declare Zero_int_def [symmetric, simp] |
164 |
declare One_int_def [symmetric, simp] |
|
165 |
||
166 |
text{*cooper.ML refers to this theorem*} |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
167 |
lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp] |
14259 | 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 |
||
16413 | 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 |
||
14259 | 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] |
|
13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13685
diff
changeset
|
186 |
|
14295 | 187 |
lemma split_nat [arith_split]: |
14259 | 188 |
"P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" |
13575 | 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 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
203 |
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
204 |
(*Analogous to zadd_int*) |
15013 | 205 |
lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)" |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
206 |
by (induct m n rule: diff_induct, simp_all) |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
207 |
|
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
208 |
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'" |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
209 |
apply (case_tac "0 \<le> z'") |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
210 |
apply (rule inj_int [THEN injD]) |
16413 | 211 |
apply (simp add: int_mult zero_le_mult_iff) |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
212 |
apply (simp add: mult_le_0_iff) |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
213 |
done |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
214 |
|
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
215 |
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')" |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
216 |
apply (rule trans) |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
217 |
apply (rule_tac [2] nat_mult_distrib, auto) |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
218 |
done |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
219 |
|
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
220 |
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)" |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
221 |
apply (case_tac "z=0 | w=0") |
15003 | 222 |
apply (auto simp add: abs_if nat_mult_distrib [symmetric] |
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
223 |
nat_mult_distrib_neg [symmetric] mult_less_0_iff) |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
224 |
done |
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
225 |
|
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset
|
226 |
|
13685 | 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 - |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
236 |
{ fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" |
13685 | 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 |
} |
|
14473 | 251 |
with ge show ?thesis by fast |
13685 | 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) |
|
14259 | 263 |
apply (rule step, simp+) |
13685 | 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 - |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset
|
272 |
{ fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" |
13685 | 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 |
} |
|
14473 | 287 |
with le show ?thesis by fast |
13685 | 288 |
qed |
289 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
290 |
theorem int_less_induct [consumes 1,case_names base step]: |
13685 | 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) |
|
14259 | 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))" |
|
14271 | 306 |
apply (induct_tac "n", simp) |
14259 | 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) |
|
15003 | 313 |
apply (simp add: abs_if split add: split_if_asm) |
14259 | 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 |
||
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
335 |
lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))" |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
336 |
by arith |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
337 |
|
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
338 |
lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)" |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
339 |
apply (case_tac "\<bar>n\<bar>=1") |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
340 |
apply (simp add: abs_mult) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
341 |
apply (rule ccontr) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
342 |
apply (auto simp add: linorder_neq_iff abs_mult) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
343 |
apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>") |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
344 |
prefer 2 apply arith |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
345 |
apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
346 |
apply (rule mult_mono, auto) |
13685 | 347 |
done |
348 |
||
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
349 |
lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1" |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
350 |
by (insert abs_zmult_eq_1 [of m n], arith) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
351 |
|
14259 | 352 |
lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)" |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
353 |
apply (auto dest: pos_zmult_eq_1_iff_lemma) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
354 |
apply (simp add: mult_commute [of m]) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
355 |
apply (frule pos_zmult_eq_1_iff_lemma, auto) |
14259 | 356 |
done |
357 |
||
358 |
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))" |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
359 |
apply (rule iffI) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
360 |
apply (frule pos_zmult_eq_1_iff_lemma) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
361 |
apply (simp add: mult_commute [of m]) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset
|
362 |
apply (frule pos_zmult_eq_1_iff_lemma, auto) |
14259 | 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"; |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
370 |
val abs_minus_one = thm "abs_minus_one"; |
14390 | 371 |
val of_int_number_of_eq = thm"of_int_number_of_eq"; |
14259 | 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 |
||
7707 | 392 |
end |