author  haftmann 
Mon, 18 Dec 2006 08:21:28 +0100  
changeset 21872  75ba582dd6e9 
parent 21820  2f2b6a965ccc 
child 21911  e29bcab0c81c 
permissions  rwrr 
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 int :: number_ring 
21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21191
diff
changeset

20 
int_number_of_def: "number_of w \<equiv> of_int w" 
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21191
diff
changeset

21 
by intro_classes (simp only: int_number_of_def) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

22 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset

23 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset

24 
subsection{*Inequality Reasoning for the Arithmetic Simproc*} 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset

25 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

26 
lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

27 
by simp 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

28 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

29 
lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

30 
by simp 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

31 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

32 
lemma mult_numeral_1: "Numeral1 * 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 mult_numeral_1_right: "a * Numeral1 = (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 
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

39 
for 0 and 1 reduces the number of special cases.*} 
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 
lemmas add_0s = add_numeral_0 add_numeral_0_right 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

42 
lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

43 
mult_minus1 mult_minus1_right 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

44 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

45 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

46 
subsection{*Special Arithmetic Rules for Abstract 0 and 1*} 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

47 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

48 
text{*Arithmetic computations are defined for binary literals, which leaves 0 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

49 
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

50 
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

51 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

52 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

53 
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

54 
by simp 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

55 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

56 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

57 
lemmas add_number_of_eq = number_of_add [symmetric] 
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 
text{*Allow 1 on either or both sides*} 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

60 
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

61 
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

62 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

63 
lemmas add_special = 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

64 
one_add_one_is_two 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

65 
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

66 
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

67 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

68 
text{*Allow 1 on either or both sides (11 already simplifies to 0)*} 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

69 
lemmas diff_special = 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

70 
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

71 
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

72 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

73 
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

74 
lemmas eq_special = 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

75 
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

76 
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

77 
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

78 
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

79 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

80 
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

81 
lemmas less_special = 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

82 
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

83 
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

84 
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

85 
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

86 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

87 
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

88 
lemmas le_special = 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

89 
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

90 
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

91 
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

92 
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

93 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

94 
lemmas arith_special = 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

95 
add_special diff_special eq_special less_special le_special 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

96 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

97 

12023  98 
use "int_arith1.ML" 
99 
setup int_arith_setup 

14259  100 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset

101 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

102 
subsection{*Lemmas About Small Numerals*} 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

103 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

104 
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

105 
proof  
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

106 
have "(of_int 1 :: 'a) = of_int ( 1)" by simp 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

107 
also have "... =  of_int 1" by (simp only: of_int_minus) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

108 
also have "... = 1" by simp 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

109 
finally show ?thesis . 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

110 
qed 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

111 

14738  112 
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

113 
by (simp add: abs_if) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

114 

14436  115 
lemma abs_power_minus_one [simp]: 
15003  116 
"abs(1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})" 
14436  117 
by (simp add: power_abs) 
118 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

119 
lemma of_int_number_of_eq: 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

120 
"of_int (number_of v) = (number_of v :: 'a :: number_ring)" 
15013  121 
by (simp add: number_of_eq) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

122 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

123 
text{*Lemmas for specialist use, NOT as default simprules*} 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

124 
lemma mult_2: "2 * z = (z+z::'a::number_ring)" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

125 
proof  
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

126 
have "2*z = (1 + 1)*z" by simp 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

127 
also have "... = z+z" by (simp add: left_distrib) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

128 
finally show ?thesis . 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

129 
qed 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

130 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

131 
lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

132 
by (subst mult_commute, rule mult_2) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

133 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

134 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

135 
subsection{*More Inequality Reasoning*} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset

136 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset

137 
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z  w=z)" 
14259  138 
by arith 
139 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset

140 
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

141 
by arith 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset

142 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

143 
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

144 
by arith 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset

145 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

146 
lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)" 
14259  147 
by arith 
148 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

149 
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

150 
by arith 
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

151 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset

152 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset

153 
subsection{*The Functions @{term nat} and @{term int}*} 
14259  154 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14295
diff
changeset

155 
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

156 
@{term "w +  z"}*} 
14259  157 
declare Zero_int_def [symmetric, simp] 
158 
declare One_int_def [symmetric, simp] 

159 

160 
text{*cooper.ML refers to this theorem*} 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

161 
lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp] 
14259  162 

163 
lemma nat_0: "nat 0 = 0" 

164 
by (simp add: nat_eq_iff) 

165 

166 
lemma nat_1: "nat 1 = Suc 0" 

167 
by (subst nat_eq_iff, simp) 

168 

169 
lemma nat_2: "nat 2 = Suc (Suc 0)" 

170 
by (subst nat_eq_iff, simp) 

171 

16413  172 
lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)" 
173 
apply (insert zless_nat_conj [of 1 z]) 

174 
apply (auto simp add: nat_1) 

175 
done 

176 

14259  177 
text{*This simplifies expressions of the form @{term "int n = z"} where 
178 
z is an integer literal.*} 

17085  179 
lemmas int_eq_iff_number_of = int_eq_iff [of _ "number_of v", standard] 
180 
declare int_eq_iff_number_of [simp] 

181 

13837
8dd150d36c65
Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents:
13685
diff
changeset

182 

14295  183 
lemma split_nat [arith_split]: 
14259  184 
"P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" 
13575  185 
(is "?P = (?L & ?R)") 
186 
proof (cases "i < 0") 

187 
case True thus ?thesis by simp 

188 
next 

189 
case False 

190 
have "?P = ?L" 

191 
proof 

192 
assume ?P thus ?L using False by clarsimp 

193 
next 

194 
assume ?L thus ?P using False by simp 

195 
qed 

196 
with False show ?thesis by simp 

197 
qed 

198 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

199 

14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

200 
(*Analogous to zadd_int*) 
15013  201 
lemma zdiff_int: "n \<le> m ==> int m  int n = int (mn)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

202 
by (induct m n rule: diff_induct, simp_all) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

203 

0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

204 
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

205 
apply (case_tac "0 \<le> z'") 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

206 
apply (rule inj_int [THEN injD]) 
16413  207 
apply (simp add: int_mult zero_le_mult_iff) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

208 
apply (simp add: mult_le_0_iff) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

209 
done 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

210 

0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

211 
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

212 
apply (rule trans) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

213 
apply (rule_tac [2] nat_mult_distrib, auto) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

214 
done 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

215 

0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

216 
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

217 
apply (case_tac "z=0  w=0") 
15003  218 
apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

219 
nat_mult_distrib_neg [symmetric] mult_less_0_iff) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

220 
done 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

221 

0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14473
diff
changeset

222 

17472  223 
subsection "Induction principles for int" 
13685  224 

225 
(* `set:int': dummy construction *) 

226 
theorem int_ge_induct[case_names base step,induct set:int]: 

227 
assumes ge: "k \<le> (i::int)" and 

228 
base: "P(k)" and 

229 
step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" 

230 
shows "P i" 

231 
proof  

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset

232 
{ fix n have "\<And>i::int. n = nat(ik) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" 
13685  233 
proof (induct n) 
234 
case 0 

235 
hence "i = k" by arith 

236 
thus "P i" using base by simp 

237 
next 

238 
case (Suc n) 

239 
hence "n = nat((i  1)  k)" by arith 

240 
moreover 

241 
have ki1: "k \<le> i  1" using Suc.prems by arith 

242 
ultimately 

243 
have "P(i  1)" by(rule Suc.hyps) 

244 
from step[OF ki1 this] show ?case by simp 

245 
qed 

246 
} 

14473  247 
with ge show ?thesis by fast 
13685  248 
qed 
249 

250 
(* `set:int': dummy construction *) 

251 
theorem int_gr_induct[case_names base step,induct set:int]: 

252 
assumes gr: "k < (i::int)" and 

253 
base: "P(k+1)" and 

254 
step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)" 

255 
shows "P i" 

256 
apply(rule int_ge_induct[of "k + 1"]) 

257 
using gr apply arith 

258 
apply(rule base) 

14259  259 
apply (rule step, simp+) 
13685  260 
done 
261 

262 
theorem int_le_induct[consumes 1,case_names base step]: 

263 
assumes le: "i \<le> (k::int)" and 

264 
base: "P(k)" and 

265 
step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i  1)" 

266 
shows "P i" 

267 
proof  

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14271
diff
changeset

268 
{ fix n have "\<And>i::int. n = nat(ki) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" 
13685  269 
proof (induct n) 
270 
case 0 

271 
hence "i = k" by arith 

272 
thus "P i" using base by simp 

273 
next 

274 
case (Suc n) 

275 
hence "n = nat(k  (i+1))" by arith 

276 
moreover 

277 
have ki1: "i + 1 \<le> k" using Suc.prems by arith 

278 
ultimately 

279 
have "P(i+1)" by(rule Suc.hyps) 

280 
from step[OF ki1 this] show ?case by simp 

281 
qed 

282 
} 

14473  283 
with le show ?thesis by fast 
13685  284 
qed 
285 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

286 
theorem int_less_induct [consumes 1,case_names base step]: 
13685  287 
assumes less: "(i::int) < k" and 
288 
base: "P(k  1)" and 

289 
step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i  1)" 

290 
shows "P i" 

291 
apply(rule int_le_induct[of _ "k  1"]) 

292 
using less apply arith 

293 
apply(rule base) 

14259  294 
apply (rule step, simp+) 
295 
done 

296 

297 
subsection{*Intermediate value theorems*} 

298 

299 
lemma int_val_lemma: 

300 
"(\<forall>i<n::nat. abs(f(i+1)  f i) \<le> 1) > 

301 
f 0 \<le> k > k \<le> f n > (\<exists>i \<le> n. f i = (k::int))" 

14271  302 
apply (induct_tac "n", simp) 
14259  303 
apply (intro strip) 
304 
apply (erule impE, simp) 

305 
apply (erule_tac x = n in allE, simp) 

306 
apply (case_tac "k = f (n+1) ") 

307 
apply force 

308 
apply (erule impE) 

15003  309 
apply (simp add: abs_if split add: split_if_asm) 
14259  310 
apply (blast intro: le_SucI) 
311 
done 

312 

313 
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)] 

314 

315 
lemma nat_intermed_int_val: 

316 
"[ \<forall>i. m \<le> i & i < n > abs(f(i + 1::nat)  f i) \<le> 1; m < n; 

317 
f m \<le> k; k \<le> f n ] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)" 

318 
apply (cut_tac n = "nm" and f = "%i. f (i+m) " and k = k 

319 
in int_val_lemma) 

320 
apply simp 

321 
apply (erule exE) 

322 
apply (rule_tac x = "i+m" in exI, arith) 

323 
done 

324 

325 

326 
subsection{*Products and 1, by T. M. Rasmussen*} 

327 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

328 
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

329 
by arith 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

330 

ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

331 
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

332 
apply (case_tac "\<bar>n\<bar>=1") 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

333 
apply (simp add: abs_mult) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

334 
apply (rule ccontr) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

335 
apply (auto simp add: linorder_neq_iff abs_mult) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

336 
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

337 
prefer 2 apply arith 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

338 
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

339 
apply (rule mult_mono, auto) 
13685  340 
done 
341 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

342 
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

343 
by (insert abs_zmult_eq_1 [of m n], arith) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

344 

14259  345 
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

346 
apply (auto dest: pos_zmult_eq_1_iff_lemma) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

347 
apply (simp add: mult_commute [of m]) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

348 
apply (frule pos_zmult_eq_1_iff_lemma, auto) 
14259  349 
done 
350 

351 
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

352 
apply (rule iffI) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

353 
apply (frule 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 

20355  358 

359 
subsection {* code generator setup *} 

360 

21191  361 
code_modulename SML 
362 
Numeral Integer 

20355  363 

20595  364 
lemma Numeral_Pls_refl [code func]: 
365 
"Numeral.Pls = Numeral.Pls" .. 

20402
e2c6d096af01
more concise preprocessing of numerals for code generation
haftmann
parents:
20380
diff
changeset

366 

20595  367 
lemma Numeral_Min_refl [code func]: 
368 
"Numeral.Min = Numeral.Min" .. 

20402
e2c6d096af01
more concise preprocessing of numerals for code generation
haftmann
parents:
20380
diff
changeset

369 

20595  370 
lemma zero_int_refl [code func]: 
371 
"(0\<Colon>int) = 0" .. 

20355  372 

20595  373 
lemma one_int_refl [code func]: 
374 
"(1\<Colon>int) = 1" .. 

20355  375 

20595  376 
lemma number_of_int_refl [code func]: 
377 
"(number_of \<Colon> int \<Rightarrow> int) = number_of" .. 

378 

379 
lemma number_of_is_id: 

20485  380 
"number_of (k::int) = k" 
381 
unfolding int_number_of_def by simp 

20355  382 

21060  383 
lemma zero_is_num_zero [code inline, symmetric, normal post]: 
20595  384 
"(0::int) = number_of Numeral.Pls" 
385 
by simp 

386 

21060  387 
lemma one_is_num_one [code inline, symmetric, normal post]: 
20595  388 
"(1::int) = number_of (Numeral.Pls BIT bit.B1)" 
389 
by simp 

390 

391 
lemmas int_code_rewrites = 

392 
arith_simps(527) 

20900  393 
arith_extra_simps(15) [where 'a = int] 
20595  394 

395 
declare int_code_rewrites [code func] 

20355  396 

20699  397 
code_type bit 
21113  398 
(SML "bool") 
399 
(Haskell "Bool") 

20699  400 
code_const "Numeral.bit.B0" and "Numeral.bit.B1" 
21113  401 
(SML "false" and "true") 
402 
(Haskell "False" and "True") 

20699  403 

404 
code_const "number_of \<Colon> int \<Rightarrow> int" 

405 
and "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit" 

406 
and "Numeral.succ" and "Numeral.pred" 

20595  407 
(SML "_" 
21113  408 
and "0/ :/ IntInf.int" 
409 
and "~1/ :/ IntInf.int" 

21872  410 
and "(_; _; raise Fail \"BIT\")" 
21113  411 
and "IntInf.+/ (_,/ 1)" 
412 
and "IntInf./ (_,/ 1))") 

20595  413 
(Haskell "_" 
21113  414 
and "0" 
415 
and "negate/ 1" 

416 
and "error/ \"BIT\"" 

417 
and "(+)/ 1" 

418 
and "()/ _/ 1") 

20485  419 

20355  420 
setup {* 
21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21191
diff
changeset

421 
CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral (try HOLogic.dest_numeral)) 
20355  422 
*} 
423 

424 

19601  425 
subsection {* legacy ML bindings *} 
426 

14259  427 
ML 
428 
{* 

429 
val zle_diff1_eq = thm "zle_diff1_eq"; 

430 
val zle_add1_eq_le = thm "zle_add1_eq_le"; 

431 
val nonneg_eq_int = thm "nonneg_eq_int"; 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

432 
val abs_minus_one = thm "abs_minus_one"; 
14390  433 
val of_int_number_of_eq = thm"of_int_number_of_eq"; 
14259  434 
val nat_eq_iff = thm "nat_eq_iff"; 
435 
val nat_eq_iff2 = thm "nat_eq_iff2"; 

436 
val nat_less_iff = thm "nat_less_iff"; 

437 
val int_eq_iff = thm "int_eq_iff"; 

438 
val nat_0 = thm "nat_0"; 

439 
val nat_1 = thm "nat_1"; 

440 
val nat_2 = thm "nat_2"; 

441 
val nat_less_eq_zless = thm "nat_less_eq_zless"; 

442 
val nat_le_eq_zle = thm "nat_le_eq_zle"; 

443 

444 
val nat_intermed_int_val = thm "nat_intermed_int_val"; 

445 
val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff"; 

446 
val zmult_eq_1_iff = thm "zmult_eq_1_iff"; 

447 
val nat_add_distrib = thm "nat_add_distrib"; 

448 
val nat_diff_distrib = thm "nat_diff_distrib"; 

449 
val nat_mult_distrib = thm "nat_mult_distrib"; 

450 
val nat_mult_distrib_neg = thm "nat_mult_distrib_neg"; 

451 
val nat_abs_mult_distrib = thm "nat_abs_mult_distrib"; 

452 
*} 

453 

7707  454 
end 