author  haftmann 
Mon, 09 Oct 2017 19:10:47 +0200  
changeset 66836  4eb431c3f974 
parent 66816  212a3334e7da 
child 66886  960509bfd47e 
permissions  rwrr 
41959  1 
(* Title: HOL/Int.thy 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
41959  3 
Author: Tobias Nipkow, Florian Haftmann, TU Muenchen 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

4 
*) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

5 

60758  6 
section \<open>The Integers as Equivalence Classes over Pairs of Natural Numbers\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

7 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

8 
theory Int 
63652  9 
imports Equiv_Relations Power Quotient Fun_Def 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

10 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

11 

60758  12 
subsection \<open>Definition of integers as a quotient type\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

13 

63652  14 
definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
15 
where "intrel = (\<lambda>(x, y) (u, v). x + v = u + y)" 

48045  16 

17 
lemma intrel_iff [simp]: "intrel (x, y) (u, v) \<longleftrightarrow> x + v = u + y" 

18 
by (simp add: intrel_def) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

19 

48045  20 
quotient_type int = "nat \<times> nat" / "intrel" 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

21 
morphisms Rep_Integ Abs_Integ 
48045  22 
proof (rule equivpI) 
63652  23 
show "reflp intrel" by (auto simp: reflp_def) 
24 
show "symp intrel" by (auto simp: symp_def) 

25 
show "transp intrel" by (auto simp: transp_def) 

48045  26 
qed 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

27 

48045  28 
lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: 
63652  29 
"(\<And>x y. z = Abs_Integ (x, y) \<Longrightarrow> P) \<Longrightarrow> P" 
30 
by (induct z) auto 

31 

48045  32 

60758  33 
subsection \<open>Integers form a commutative ring\<close> 
48045  34 

35 
instantiation int :: comm_ring_1 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

36 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

37 

51994  38 
lift_definition zero_int :: "int" is "(0, 0)" . 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

39 

51994  40 
lift_definition one_int :: "int" is "(1, 0)" . 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

41 

48045  42 
lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int" 
43 
is "\<lambda>(x, y) (u, v). (x + u, y + v)" 

44 
by clarsimp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

45 

48045  46 
lift_definition uminus_int :: "int \<Rightarrow> int" 
47 
is "\<lambda>(x, y). (y, x)" 

48 
by clarsimp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

49 

48045  50 
lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int" 
51 
is "\<lambda>(x, y) (u, v). (x + v, y + u)" 

52 
by clarsimp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

53 

48045  54 
lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int" 
55 
is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)" 

56 
proof (clarsimp) 

57 
fix s t u v w x y z :: nat 

58 
assume "s + v = u + t" and "w + z = y + x" 

63652  59 
then have "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) = 
60 
(u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)" 

48045  61 
by simp 
63652  62 
then show "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)" 
48045  63 
by (simp add: algebra_simps) 
64 
qed 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

65 

48045  66 
instance 
63652  67 
by standard (transfer; clarsimp simp: algebra_simps)+ 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

68 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

69 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

70 

63652  71 
abbreviation int :: "nat \<Rightarrow> int" 
72 
where "int \<equiv> of_nat" 

44709  73 

48045  74 
lemma int_def: "int n = Abs_Integ (n, 0)" 
63652  75 
by (induct n) (simp add: zero_int.abs_eq, simp add: one_int.abs_eq plus_int.abs_eq) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

76 

63652  77 
lemma int_transfer [transfer_rule]: "(rel_fun (op =) pcr_int) (\<lambda>n. (n, 0)) int" 
78 
by (simp add: rel_fun_def int.pcr_cr_eq cr_int_def int_def) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

79 

63652  80 
lemma int_diff_cases: obtains (diff) m n where "z = int m  int n" 
48045  81 
by transfer clarsimp 
82 

63652  83 

60758  84 
subsection \<open>Integers are totally ordered\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

85 

48045  86 
instantiation int :: linorder 
87 
begin 

88 

89 
lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool" 

90 
is "\<lambda>(x, y) (u, v). x + v \<le> u + y" 

91 
by auto 

92 

93 
lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool" 

94 
is "\<lambda>(x, y) (u, v). x + v < u + y" 

95 
by auto 

96 

97 
instance 

61169  98 
by standard (transfer, force)+ 
48045  99 

100 
end 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

101 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

102 
instantiation int :: distrib_lattice 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

103 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

104 

63652  105 
definition "(inf :: int \<Rightarrow> int \<Rightarrow> int) = min" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

106 

63652  107 
definition "(sup :: int \<Rightarrow> int \<Rightarrow> int) = max" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

108 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

109 
instance 
63652  110 
by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

111 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

112 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

113 

63652  114 

60758  115 
subsection \<open>Ordering properties of arithmetic operations\<close> 
48045  116 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34055
diff
changeset

117 
instance int :: ordered_cancel_ab_semigroup_add 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

118 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

119 
fix i j k :: int 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

120 
show "i \<le> j \<Longrightarrow> k + i \<le> k + j" 
48045  121 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

122 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

123 

63652  124 
text \<open>Strict Monotonicity of Multiplication.\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

125 

63652  126 
text \<open>Strict, in 1st argument; proof is by induction on \<open>k > 0\<close>.\<close> 
127 
lemma zmult_zless_mono2_lemma: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> int k * i < int k * j" 

128 
for i j :: int 

129 
proof (induct k) 

130 
case 0 

131 
then show ?case by simp 

132 
next 

133 
case (Suc k) 

134 
then show ?case 

135 
by (cases "k = 0") (simp_all add: distrib_right add_strict_mono) 

136 
qed 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

137 

63652  138 
lemma zero_le_imp_eq_int: "0 \<le> k \<Longrightarrow> \<exists>n. k = int n" 
139 
for k :: int 

140 
apply transfer 

141 
apply clarsimp 

142 
apply (rule_tac x="a  b" in exI) 

143 
apply simp 

144 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

145 

63652  146 
lemma zero_less_imp_eq_int: "0 < k \<Longrightarrow> \<exists>n>0. k = int n" 
147 
for k :: int 

148 
apply transfer 

149 
apply clarsimp 

150 
apply (rule_tac x="a  b" in exI) 

151 
apply simp 

152 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

153 

63652  154 
lemma zmult_zless_mono2: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" 
155 
for i j k :: int 

156 
by (drule zero_less_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

157 

63652  158 

159 
text \<open>The integers form an ordered integral domain.\<close> 

160 

48045  161 
instantiation int :: linordered_idom 
162 
begin 

163 

63652  164 
definition zabs_def: "\<bar>i::int\<bar> = (if i < 0 then  i else i)" 
48045  165 

63652  166 
definition zsgn_def: "sgn (i::int) = (if i = 0 then 0 else if 0 < i then 1 else  1)" 
48045  167 

63652  168 
instance 
169 
proof 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

170 
fix i j k :: int 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

171 
show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

172 
by (rule zmult_zless_mono2) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

173 
show "\<bar>i\<bar> = (if i < 0 then i else i)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

174 
by (simp only: zabs_def) 
61076  175 
show "sgn (i::int) = (if i=0 then 0 else if 0<i then 1 else  1)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

176 
by (simp only: zsgn_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

177 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

178 

48045  179 
end 
180 

63652  181 
lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + 1 \<le> z" 
182 
for w z :: int 

48045  183 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

184 

63652  185 
lemma zless_iff_Suc_zadd: "w < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))" 
186 
for w z :: int 

187 
apply transfer 

188 
apply auto 

189 
apply (rename_tac a b c d) 

190 
apply (rule_tac x="c+b  Suc(a+d)" in exI) 

191 
apply arith 

192 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

193 

63652  194 
lemma zabs_less_one_iff [simp]: "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?lhs \<longleftrightarrow> ?rhs") 
195 
for z :: int 

62347  196 
proof 
63652  197 
assume ?rhs 
198 
then show ?lhs by simp 

62347  199 
next 
63652  200 
assume ?lhs 
201 
with zless_imp_add1_zle [of "\<bar>z\<bar>" 1] have "\<bar>z\<bar> + 1 \<le> 1" by simp 

202 
then have "\<bar>z\<bar> \<le> 0" by simp 

203 
then show ?rhs by simp 

62347  204 
qed 
205 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

206 
lemmas int_distrib = 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

207 
distrib_right [of z1 z2 w] 
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

208 
distrib_left [of w z1 z2] 
45607  209 
left_diff_distrib [of z1 z2 w] 
210 
right_diff_distrib [of w z1 z2] 

211 
for z1 z2 w :: int 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

212 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

213 

61799  214 
subsection \<open>Embedding of the Integers into any \<open>ring_1\<close>: \<open>of_int\<close>\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

215 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

216 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

217 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

218 

63652  219 
lift_definition of_int :: "int \<Rightarrow> 'a" 
220 
is "\<lambda>(i, j). of_nat i  of_nat j" 

48045  221 
by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq 
63652  222 
of_nat_add [symmetric] simp del: of_nat_add) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

223 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

224 
lemma of_int_0 [simp]: "of_int 0 = 0" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

225 
by transfer simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

226 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

227 
lemma of_int_1 [simp]: "of_int 1 = 1" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

228 
by transfer simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

229 

63652  230 
lemma of_int_add [simp]: "of_int (w + z) = of_int w + of_int z" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

231 
by transfer (clarsimp simp add: algebra_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

232 

63652  233 
lemma of_int_minus [simp]: "of_int ( z) =  (of_int z)" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

234 
by (transfer fixing: uminus) clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

235 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

236 
lemma of_int_diff [simp]: "of_int (w  z) = of_int w  of_int z" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54223
diff
changeset

237 
using of_int_add [of w " z"] by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

238 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

239 
lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" 
63652  240 
by (transfer fixing: times) (clarsimp simp add: algebra_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

241 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

242 
lemma mult_of_int_commute: "of_int x * y = y * of_int x" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

243 
by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

244 

63652  245 
text \<open>Collapse nested embeddings.\<close> 
44709  246 
lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n" 
63652  247 
by (induct n) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

248 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

249 
lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

250 
by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric]) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

251 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

252 
lemma of_int_neg_numeral [code_post]: "of_int ( numeral k) =  numeral k" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

253 
by simp 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

254 

63652  255 
lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n" 
31015  256 
by (induct n) simp_all 
257 

66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

258 
lemma of_int_of_bool [simp]: 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

259 
"of_int (of_bool P) = of_bool P" 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

260 
by auto 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

261 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

262 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

263 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

264 
context ring_char_0 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

265 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

266 

63652  267 
lemma of_int_eq_iff [simp]: "of_int w = of_int z \<longleftrightarrow> w = z" 
268 
by transfer (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

269 

63652  270 
text \<open>Special cases where either operand is zero.\<close> 
271 
lemma of_int_eq_0_iff [simp]: "of_int z = 0 \<longleftrightarrow> z = 0" 

36424  272 
using of_int_eq_iff [of z 0] by simp 
273 

63652  274 
lemma of_int_0_eq_iff [simp]: "0 = of_int z \<longleftrightarrow> z = 0" 
36424  275 
using of_int_eq_iff [of 0 z] by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

276 

63652  277 
lemma of_int_eq_1_iff [iff]: "of_int z = 1 \<longleftrightarrow> z = 1" 
61234  278 
using of_int_eq_iff [of z 1] by simp 
279 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

280 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

281 

36424  282 
context linordered_idom 
283 
begin 

284 

63652  285 
text \<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close> 
36424  286 
subclass ring_char_0 .. 
287 

63652  288 
lemma of_int_le_iff [simp]: "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z" 
289 
by (transfer fixing: less_eq) 

290 
(clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add) 

36424  291 

63652  292 
lemma of_int_less_iff [simp]: "of_int w < of_int z \<longleftrightarrow> w < z" 
36424  293 
by (simp add: less_le order_less_le) 
294 

63652  295 
lemma of_int_0_le_iff [simp]: "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z" 
36424  296 
using of_int_le_iff [of 0 z] by simp 
297 

63652  298 
lemma of_int_le_0_iff [simp]: "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0" 
36424  299 
using of_int_le_iff [of z 0] by simp 
300 

63652  301 
lemma of_int_0_less_iff [simp]: "0 < of_int z \<longleftrightarrow> 0 < z" 
36424  302 
using of_int_less_iff [of 0 z] by simp 
303 

63652  304 
lemma of_int_less_0_iff [simp]: "of_int z < 0 \<longleftrightarrow> z < 0" 
36424  305 
using of_int_less_iff [of z 0] by simp 
306 

63652  307 
lemma of_int_1_le_iff [simp]: "1 \<le> of_int z \<longleftrightarrow> 1 \<le> z" 
61234  308 
using of_int_le_iff [of 1 z] by simp 
309 

63652  310 
lemma of_int_le_1_iff [simp]: "of_int z \<le> 1 \<longleftrightarrow> z \<le> 1" 
61234  311 
using of_int_le_iff [of z 1] by simp 
312 

63652  313 
lemma of_int_1_less_iff [simp]: "1 < of_int z \<longleftrightarrow> 1 < z" 
61234  314 
using of_int_less_iff [of 1 z] by simp 
315 

63652  316 
lemma of_int_less_1_iff [simp]: "of_int z < 1 \<longleftrightarrow> z < 1" 
61234  317 
using of_int_less_iff [of z 1] by simp 
318 

62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

319 
lemma of_int_pos: "z > 0 \<Longrightarrow> of_int z > 0" 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

320 
by simp 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

321 

3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

322 
lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0" 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

323 
by simp 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

324 

63652  325 
lemma of_int_abs [simp]: "of_int \<bar>x\<bar> = \<bar>of_int x\<bar>" 
62347  326 
by (auto simp add: abs_if) 
327 

328 
lemma of_int_lessD: 

329 
assumes "\<bar>of_int n\<bar> < x" 

330 
shows "n = 0 \<or> x > 1" 

331 
proof (cases "n = 0") 

63652  332 
case True 
333 
then show ?thesis by simp 

62347  334 
next 
335 
case False 

336 
then have "\<bar>n\<bar> \<noteq> 0" by simp 

337 
then have "\<bar>n\<bar> > 0" by simp 

338 
then have "\<bar>n\<bar> \<ge> 1" 

339 
using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp 

340 
then have "\<bar>of_int n\<bar> \<ge> 1" 

341 
unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp 

342 
then have "1 < x" using assms by (rule le_less_trans) 

343 
then show ?thesis .. 

344 
qed 

345 

346 
lemma of_int_leD: 

347 
assumes "\<bar>of_int n\<bar> \<le> x" 

348 
shows "n = 0 \<or> 1 \<le> x" 

349 
proof (cases "n = 0") 

63652  350 
case True 
351 
then show ?thesis by simp 

62347  352 
next 
353 
case False 

354 
then have "\<bar>n\<bar> \<noteq> 0" by simp 

355 
then have "\<bar>n\<bar> > 0" by simp 

356 
then have "\<bar>n\<bar> \<ge> 1" 

357 
using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp 

358 
then have "\<bar>of_int n\<bar> \<ge> 1" 

359 
unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp 

360 
then have "1 \<le> x" using assms by (rule order_trans) 

361 
then show ?thesis .. 

362 
qed 

363 

36424  364 
end 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

365 

61234  366 
text \<open>Comparisons involving @{term of_int}.\<close> 
367 

63652  368 
lemma of_int_eq_numeral_iff [iff]: "of_int z = (numeral n :: 'a::ring_char_0) \<longleftrightarrow> z = numeral n" 
61234  369 
using of_int_eq_iff by fastforce 
370 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

371 
lemma of_int_le_numeral_iff [simp]: 
63652  372 
"of_int z \<le> (numeral n :: 'a::linordered_idom) \<longleftrightarrow> z \<le> numeral n" 
61234  373 
using of_int_le_iff [of z "numeral n"] by simp 
374 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

375 
lemma of_int_numeral_le_iff [simp]: 
63652  376 
"(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z" 
61234  377 
using of_int_le_iff [of "numeral n"] by simp 
378 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

379 
lemma of_int_less_numeral_iff [simp]: 
63652  380 
"of_int z < (numeral n :: 'a::linordered_idom) \<longleftrightarrow> z < numeral n" 
61234  381 
using of_int_less_iff [of z "numeral n"] by simp 
382 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

383 
lemma of_int_numeral_less_iff [simp]: 
63652  384 
"(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z" 
61234  385 
using of_int_less_iff [of "numeral n" z] by simp 
386 

63652  387 
lemma of_nat_less_of_int_iff: "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x" 
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56525
diff
changeset

388 
by (metis of_int_of_nat_eq of_int_less_iff) 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56525
diff
changeset

389 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

390 
lemma of_int_eq_id [simp]: "of_int = id" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

391 
proof 
63652  392 
show "of_int z = id z" for z 
393 
by (cases z rule: int_diff_cases) simp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

394 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

395 

51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

396 
instance int :: no_top 
61169  397 
apply standard 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

398 
apply (rule_tac x="x + 1" in exI) 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

399 
apply simp 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

400 
done 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

401 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

402 
instance int :: no_bot 
61169  403 
apply standard 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

404 
apply (rule_tac x="x  1" in exI) 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

405 
apply simp 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

406 
done 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

407 

63652  408 

61799  409 
subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

410 

48045  411 
lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x  y" 
412 
by auto 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

413 

44709  414 
lemma nat_int [simp]: "nat (int n) = n" 
48045  415 
by transfer simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

416 

44709  417 
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)" 
48045  418 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

419 

63652  420 
lemma nat_0_le: "0 \<le> z \<Longrightarrow> int (nat z) = z" 
421 
by simp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

422 

63652  423 
lemma nat_le_0 [simp]: "z \<le> 0 \<Longrightarrow> nat z = 0" 
48045  424 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

425 

63652  426 
lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> nat w \<le> nat z \<longleftrightarrow> w \<le> z" 
48045  427 
by transfer (clarsimp, arith) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

428 

63652  429 
text \<open>An alternative condition is @{term "0 \<le> w"}.\<close> 
430 
lemma nat_mono_iff: "0 < z \<Longrightarrow> nat w < nat z \<longleftrightarrow> w < z" 

431 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

432 

63652  433 
lemma nat_less_eq_zless: "0 \<le> w \<Longrightarrow> nat w < nat z \<longleftrightarrow> w < z" 
434 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

435 

63652  436 
lemma zless_nat_conj [simp]: "nat w < nat z \<longleftrightarrow> 0 < z \<and> w < z" 
48045  437 
by transfer (clarsimp, arith) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

438 

64714
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

439 
lemma nonneg_int_cases: 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

440 
assumes "0 \<le> k" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

441 
obtains n where "k = int n" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

442 
proof  
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

443 
from assms have "k = int (nat k)" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

444 
by simp 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

445 
then show thesis 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

446 
by (rule that) 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

447 
qed 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

448 

53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

449 
lemma pos_int_cases: 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

450 
assumes "0 < k" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

451 
obtains n where "k = int n" and "n > 0" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

452 
proof  
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

453 
from assms have "0 \<le> k" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

454 
by simp 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

455 
then obtain n where "k = int n" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

456 
by (rule nonneg_int_cases) 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

457 
moreover have "n > 0" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

458 
using \<open>k = int n\<close> assms by simp 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

459 
ultimately show thesis 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

460 
by (rule that) 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

461 
qed 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

462 

53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

463 
lemma nonpos_int_cases: 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

464 
assumes "k \<le> 0" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

465 
obtains n where "k =  int n" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

466 
proof  
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

467 
from assms have " k \<ge> 0" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

468 
by simp 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

469 
then obtain n where " k = int n" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

470 
by (rule nonneg_int_cases) 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

471 
then have "k =  int n" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

472 
by simp 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

473 
then show thesis 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

474 
by (rule that) 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

475 
qed 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

476 

53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

477 
lemma neg_int_cases: 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

478 
assumes "k < 0" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

479 
obtains n where "k =  int n" and "n > 0" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

480 
proof  
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

481 
from assms have " k > 0" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

482 
by simp 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

483 
then obtain n where " k = int n" and " k > 0" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

484 
by (blast elim: pos_int_cases) 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

485 
then have "k =  int n" and "n > 0" 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

486 
by simp_all 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

487 
then show thesis 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

488 
by (rule that) 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

489 
qed 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

490 

63652  491 
lemma nat_eq_iff: "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)" 
48045  492 
by transfer (clarsimp simp add: le_imp_diff_is_add) 
60162  493 

63652  494 
lemma nat_eq_iff2: "m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)" 
54223  495 
using nat_eq_iff [of w m] by auto 
496 

63652  497 
lemma nat_0 [simp]: "nat 0 = 0" 
54223  498 
by (simp add: nat_eq_iff) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

499 

63652  500 
lemma nat_1 [simp]: "nat 1 = Suc 0" 
54223  501 
by (simp add: nat_eq_iff) 
502 

63652  503 
lemma nat_numeral [simp]: "nat (numeral k) = numeral k" 
54223  504 
by (simp add: nat_eq_iff) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

505 

63652  506 
lemma nat_neg_numeral [simp]: "nat ( numeral k) = 0" 
54223  507 
by simp 
508 

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

510 
by simp 

60162  511 

63652  512 
lemma nat_less_iff: "0 \<le> w \<Longrightarrow> nat w < m \<longleftrightarrow> w < of_nat m" 
48045  513 
by transfer (clarsimp, arith) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

514 

44709  515 
lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n" 
48045  516 
by transfer (clarsimp simp add: le_diff_conv) 
44707  517 

518 
lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y" 

48045  519 
by transfer auto 
44707  520 

63652  521 
lemma nat_0_iff[simp]: "nat i = 0 \<longleftrightarrow> i \<le> 0" 
522 
for i :: int 

48045  523 
by transfer clarsimp 
29700  524 

63652  525 
lemma int_eq_iff: "of_nat m = z \<longleftrightarrow> m = nat z \<and> 0 \<le> z" 
526 
by (auto simp add: nat_eq_iff2) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

527 

63652  528 
lemma zero_less_nat_eq [simp]: "0 < nat z \<longleftrightarrow> 0 < z" 
529 
using zless_nat_conj [of 0] by auto 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

530 

63652  531 
lemma nat_add_distrib: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat (z + z') = nat z + nat z'" 
48045  532 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

533 

63652  534 
lemma nat_diff_distrib': "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x  y) = nat x  nat y" 
54223  535 
by transfer clarsimp 
60162  536 

63652  537 
lemma nat_diff_distrib: "0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z  z') = nat z  nat z'" 
54223  538 
by (rule nat_diff_distrib') auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

539 

44709  540 
lemma nat_zminus_int [simp]: "nat ( int n) = 0" 
48045  541 
by transfer simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

542 

63652  543 
lemma le_nat_iff: "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k" 
53065  544 
by transfer auto 
60162  545 

63652  546 
lemma zless_nat_eq_int_zless: "m < nat z \<longleftrightarrow> int m < z" 
48045  547 
by transfer (clarsimp simp add: less_diff_conv) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

548 

63652  549 
lemma (in ring_1) of_nat_nat [simp]: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

550 
by transfer (clarsimp simp add: of_nat_diff) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

551 

63652  552 
lemma diff_nat_numeral [simp]: "(numeral v :: nat)  numeral v' = nat (numeral v  numeral v')" 
54249  553 
by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) 
554 

66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

555 
lemma nat_of_bool [simp]: 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

556 
"nat (of_bool P) = of_bool P" 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

557 
by auto 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

558 

66836  559 
lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))" 
560 
(is "?P = (?L \<and> ?R)") 

561 
for i :: int 

562 
proof (cases "i < 0") 

563 
case True 

564 
then show ?thesis 

565 
by auto 

566 
next 

567 
case False 

568 
have "?P = ?L" 

569 
proof 

570 
assume ?P 

571 
then show ?L using False by auto 

572 
next 

573 
assume ?L 

574 
moreover from False have "int (nat i) = i" 

575 
by (simp add: not_less) 

576 
ultimately show ?P 

577 
by simp 

578 
qed 

579 
with False show ?thesis by simp 

580 
qed 

581 

582 
lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))" 

583 
by (auto split: split_nat) 

584 

585 
lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))" 

586 
proof 

587 
assume "\<exists>x. P x" 

588 
then obtain x where "P x" .. 

589 
then have "int x \<ge> 0 \<and> P (nat (int x))" by simp 

590 
then show "\<exists>x\<ge>0. P (nat x)" .. 

591 
next 

592 
assume "\<exists>x\<ge>0. P (nat x)" 

593 
then show "\<exists>x. P x" by auto 

594 
qed 

595 

54249  596 

60758  597 
text \<open>For termination proofs:\<close> 
63652  598 
lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" .. 
29779  599 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

600 

63652  601 
subsection \<open>Lemmas about the Function @{term of_nat} and Orderings\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

602 

61076  603 
lemma negative_zless_0: " (int (Suc n)) < (0 :: int)" 
63652  604 
by (simp add: order_less_le del: of_nat_Suc) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

605 

44709  606 
lemma negative_zless [iff]: " (int (Suc n)) < int m" 
63652  607 
by (rule negative_zless_0 [THEN order_less_le_trans], simp) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

608 

44709  609 
lemma negative_zle_0: " int n \<le> 0" 
63652  610 
by (simp add: minus_le_iff) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

611 

44709  612 
lemma negative_zle [iff]: " int n \<le> int m" 
63652  613 
by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

614 

63652  615 
lemma not_zle_0_negative [simp]: "\<not> 0 \<le>  int (Suc n)" 
616 
by (subst le_minus_iff) (simp del: of_nat_Suc) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

617 

63652  618 
lemma int_zle_neg: "int n \<le>  int m \<longleftrightarrow> n = 0 \<and> m = 0" 
48045  619 
by transfer simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

620 

63652  621 
lemma not_int_zless_negative [simp]: "\<not> int n <  int m" 
622 
by (simp add: linorder_not_less) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

623 

63652  624 
lemma negative_eq_positive [simp]: " int n = of_nat m \<longleftrightarrow> n = 0 \<and> m = 0" 
625 
by (force simp add: order_eq_iff [of " of_nat n"] int_zle_neg) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

626 

63652  627 
lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)" 
628 
(is "?lhs \<longleftrightarrow> ?rhs") 

62348  629 
proof 
63652  630 
assume ?rhs 
631 
then show ?lhs by auto 

62348  632 
next 
63652  633 
assume ?lhs 
62348  634 
then have "0 \<le> z  w" by simp 
635 
then obtain n where "z  w = int n" 

636 
using zero_le_imp_eq_int [of "z  w"] by blast 

63652  637 
then have "z = w + int n" by simp 
638 
then show ?rhs .. 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

639 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

640 

44709  641 
lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z" 
63652  642 
by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

643 

63652  644 
text \<open> 
645 
This version is proved for all ordered rings, not just integers! 

646 
It is proved here because attribute \<open>arith_split\<close> is not available 

647 
in theory \<open>Rings\<close>. 

648 
But is it really better than just rewriting with \<open>abs_if\<close>? 

649 
\<close> 

650 
lemma abs_split [arith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P ( a))" 

651 
for a :: "'a::linordered_idom" 

652 
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

653 

44709  654 
lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x =  (int (Suc n))" 
63652  655 
apply transfer 
656 
apply clarsimp 

657 
apply (rule_tac x="b  Suc a" in exI) 

658 
apply arith 

659 
done 

660 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

661 

60758  662 
subsection \<open>Cases and induction\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

663 

63652  664 
text \<open> 
665 
Now we replace the case analysis rule by a more conventional one: 

666 
whether an integer is negative or not. 

667 
\<close> 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

668 

63652  669 
text \<open>This version is symmetric in the two subgoals.\<close> 
670 
lemma int_cases2 [case_names nonneg nonpos, cases type: int]: 

671 
"(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z =  (int n) \<Longrightarrow> P) \<Longrightarrow> P" 

672 
by (cases "z < 0") (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym]) 

59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59582
diff
changeset

673 

63652  674 
text \<open>This is the default, with a negative case.\<close> 
675 
lemma int_cases [case_names nonneg neg, cases type: int]: 

676 
"(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z =  (int (Suc n)) \<Longrightarrow> P) \<Longrightarrow> P" 

677 
apply (cases "z < 0") 

678 
apply (blast dest!: negD) 

679 
apply (simp add: linorder_not_less del: of_nat_Suc) 

680 
apply auto 

681 
apply (blast dest: nat_0_le [THEN sym]) 

682 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

683 

60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

684 
lemma int_cases3 [case_names zero pos neg]: 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

685 
fixes k :: int 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

686 
assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P" 
61204  687 
and "\<And>n. k =  int n \<Longrightarrow> n > 0 \<Longrightarrow> P" 
60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

688 
shows "P" 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

689 
proof (cases k "0::int" rule: linorder_cases) 
63652  690 
case equal 
691 
with assms(1) show P by simp 

60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

692 
next 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

693 
case greater 
63539  694 
then have *: "nat k > 0" by simp 
695 
moreover from * have "k = int (nat k)" by auto 

60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

696 
ultimately show P using assms(2) by blast 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

697 
next 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

698 
case less 
63539  699 
then have *: "nat ( k) > 0" by simp 
700 
moreover from * have "k =  int (nat ( k))" by auto 

60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

701 
ultimately show P using assms(3) by blast 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

702 
qed 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

703 

63652  704 
lemma int_of_nat_induct [case_names nonneg neg, induct type: int]: 
705 
"(\<And>n. P (int n)) \<Longrightarrow> (\<And>n. P ( (int (Suc n)))) \<Longrightarrow> P z" 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

706 
by (cases z) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

707 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

708 
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)" 
61799  709 
\<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close> 
710 
by (fact Let_numeral) \<comment> \<open>FIXME drop\<close> 

37767  711 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

712 
lemma Let_neg_numeral [simp]: "Let ( numeral v) f = f ( numeral v)" 
61799  713 
\<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close> 
714 
by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close> 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

715 

66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

716 
lemma sgn_mult_dvd_iff [simp]: 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

717 
"sgn r * l dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

718 
by (cases r rule: int_cases3) auto 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

719 

212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

720 
lemma mult_sgn_dvd_iff [simp]: 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

721 
"l * sgn r dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

722 
using sgn_mult_dvd_iff [of r l k] by (simp add: ac_simps) 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

723 

212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

724 
lemma dvd_sgn_mult_iff [simp]: 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

725 
"l dvd sgn r * k \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

726 
by (cases r rule: int_cases3) simp_all 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

727 

212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

728 
lemma dvd_mult_sgn_iff [simp]: 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

729 
"l dvd k * sgn r \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

730 
using dvd_sgn_mult_iff [of l r k] by (simp add: ac_simps) 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

731 

212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

732 
lemma int_sgnE: 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

733 
fixes k :: int 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

734 
obtains n and l where "k = sgn l * int n" 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

735 
proof  
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

736 
have "k = sgn k * int (nat \<bar>k\<bar>)" 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

737 
by (simp add: sgn_mult_abs) 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

738 
then show ?thesis .. 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

739 
qed 
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66035
diff
changeset

740 

61799  741 
text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close> 
28958  742 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

743 
lemmas max_number_of [simp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

744 
max_def [of "numeral u" "numeral v"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

745 
max_def [of "numeral u" " numeral v"] 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

746 
max_def [of " numeral u" "numeral v"] 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

747 
max_def [of " numeral u" " numeral v"] for u v 
28958  748 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

749 
lemmas min_number_of [simp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

750 
min_def [of "numeral u" "numeral v"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

751 
min_def [of "numeral u" " numeral v"] 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

752 
min_def [of " numeral u" "numeral v"] 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

753 
min_def [of " numeral u" " numeral v"] for u v 
26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

754 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

755 

60758  756 
subsubsection \<open>Binary comparisons\<close> 
28958  757 

60758  758 
text \<open>Preliminaries\<close> 
28958  759 

60162  760 
lemma le_imp_0_less: 
63652  761 
fixes z :: int 
28958  762 
assumes le: "0 \<le> z" 
63652  763 
shows "0 < 1 + z" 
28958  764 
proof  
765 
have "0 \<le> z" by fact 

63652  766 
also have "\<dots> < z + 1" by (rule less_add_one) 
767 
also have "\<dots> = 1 + z" by (simp add: ac_simps) 

28958  768 
finally show "0 < 1 + z" . 
769 
qed 

770 

63652  771 
lemma odd_less_0_iff: "1 + z + z < 0 \<longleftrightarrow> z < 0" 
772 
for z :: int 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

773 
proof (cases z) 
28958  774 
case (nonneg n) 
63652  775 
then show ?thesis 
776 
by (simp add: linorder_not_less add.assoc add_increasing le_imp_0_less [THEN order_less_imp_le]) 

28958  777 
next 
778 
case (neg n) 

63652  779 
then show ?thesis 
780 
by (simp del: of_nat_Suc of_nat_add of_nat_1 

781 
add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) 

28958  782 
qed 
783 

63652  784 

60758  785 
subsubsection \<open>Comparisons, for Ordered Rings\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

786 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

787 
lemmas double_eq_0_iff = double_zero 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

788 

63652  789 
lemma odd_nonzero: "1 + z + z \<noteq> 0" 
790 
for z :: int 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

791 
proof (cases z) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

792 
case (nonneg n) 
63652  793 
have le: "0 \<le> z + z" 
794 
by (simp add: nonneg add_increasing) 

795 
then show ?thesis 

796 
using le_imp_0_less [OF le] by (auto simp: add.assoc) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

797 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

798 
case (neg n) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

799 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

800 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

801 
assume eq: "1 + z + z = 0" 
63652  802 
have "0 < 1 + (int n + int n)" 
60162  803 
by (simp add: le_imp_0_less add_increasing) 
63652  804 
also have "\<dots> =  (1 + z + z)" 
60162  805 
by (simp add: neg add.assoc [symmetric]) 
63652  806 
also have "\<dots> = 0" by (simp add: eq) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

807 
finally have "0<0" .. 
63652  808 
then show False by blast 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

809 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

810 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

811 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

812 

60758  813 
subsection \<open>The Set of Integers\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

814 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

815 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

816 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

817 

61070  818 
definition Ints :: "'a set" ("\<int>") 
819 
where "\<int> = range of_int" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

820 

35634  821 
lemma Ints_of_int [simp]: "of_int z \<in> \<int>" 
822 
by (simp add: Ints_def) 

823 

824 
lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>" 

45533  825 
using Ints_of_int [of "of_nat n"] by simp 
35634  826 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

827 
lemma Ints_0 [simp]: "0 \<in> \<int>" 
45533  828 
using Ints_of_int [of "0"] by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

829 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

830 
lemma Ints_1 [simp]: "1 \<in> \<int>" 
45533  831 
using Ints_of_int [of "1"] by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

832 

61552
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

833 
lemma Ints_numeral [simp]: "numeral n \<in> \<int>" 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

834 
by (subst of_nat_numeral [symmetric], rule Ints_of_nat) 
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

835 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

836 
lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>" 
63652  837 
apply (auto simp add: Ints_def) 
838 
apply (rule range_eqI) 

839 
apply (rule of_int_add [symmetric]) 

840 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

841 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

842 
lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> a \<in> \<int>" 
63652  843 
apply (auto simp add: Ints_def) 
844 
apply (rule range_eqI) 

845 
apply (rule of_int_minus [symmetric]) 

846 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

847 

35634  848 
lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a  b \<in> \<int>" 
63652  849 
apply (auto simp add: Ints_def) 
850 
apply (rule range_eqI) 

851 
apply (rule of_int_diff [symmetric]) 

852 
done 

35634  853 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

854 
lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>" 
63652  855 
apply (auto simp add: Ints_def) 
856 
apply (rule range_eqI) 

857 
apply (rule of_int_mult [symmetric]) 

858 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

859 

35634  860 
lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>" 
63652  861 
by (induct n) simp_all 
35634  862 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

863 
lemma Ints_cases [cases set: Ints]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

864 
assumes "q \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

865 
obtains (of_int) z where "q = of_int z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

866 
unfolding Ints_def 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

867 
proof  
60758  868 
from \<open>q \<in> \<int>\<close> have "q \<in> range of_int" unfolding Ints_def . 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

869 
then obtain z where "q = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

870 
then show thesis .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

871 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

872 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

873 
lemma Ints_induct [case_names of_int, induct set: Ints]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

874 
"q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

875 
by (rule Ints_cases) auto 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

876 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

877 
lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

878 
unfolding Nats_def Ints_def 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

879 
by (rule subsetI, elim imageE, hypsubst, subst of_int_of_nat_eq[symmetric], rule imageI) simp_all 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

880 

f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

881 
lemma Nats_altdef1: "\<nat> = {of_int n n. n \<ge> 0}" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

882 
proof (intro subsetI equalityI) 
63652  883 
fix x :: 'a 
884 
assume "x \<in> {of_int n n. n \<ge> 0}" 

885 
then obtain n where "x = of_int n" "n \<ge> 0" 

886 
by (auto elim!: Ints_cases) 

887 
then have "x = of_nat (nat n)" 

888 
by (subst of_nat_nat) simp_all 

889 
then show "x \<in> \<nat>" 

890 
by simp 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

891 
next 
63652  892 
fix x :: 'a 
893 
assume "x \<in> \<nat>" 

894 
then obtain n where "x = of_nat n" 

895 
by (auto elim!: Nats_cases) 

896 
then have "x = of_int (int n)" by simp 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

897 
also have "int n \<ge> 0" by simp 
63652  898 
then have "of_int (int n) \<in> {of_int n n. n \<ge> 0}" by blast 
61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

899 
finally show "x \<in> {of_int n n. n \<ge> 0}" . 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

900 
qed 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

901 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

902 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

903 

64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

904 
lemma (in linordered_idom) Ints_abs [simp]: 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

905 
shows "a \<in> \<int> \<Longrightarrow> abs a \<in> \<int>" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

906 
by (auto simp: abs_if) 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

907 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

908 
lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

909 
proof (intro subsetI equalityI) 
63652  910 
fix x :: 'a 
911 
assume "x \<in> {n \<in> \<int>. n \<ge> 0}" 

912 
then obtain n where "x = of_int n" "n \<ge> 0" 

913 
by (auto elim!: Ints_cases) 

914 
then have "x = of_nat (nat n)" 

915 
by (subst of_nat_nat) simp_all 

916 
then show "x \<in> \<nat>" 

917 
by simp 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

918 
qed (auto elim!: Nats_cases) 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

919 

64849  920 
lemma (in idom_divide) of_int_divide_in_Ints: 
921 
"of_int a div of_int b \<in> \<int>" if "b dvd a" 

922 
proof  

923 
from that obtain c where "a = b * c" .. 

924 
then show ?thesis 

925 
by (cases "of_int b = 0") simp_all 

926 
qed 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

927 

60758  928 
text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

929 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

930 
lemma Ints_double_eq_0_iff: 
63652  931 
fixes a :: "'a::ring_char_0" 
61070  932 
assumes in_Ints: "a \<in> \<int>" 
63652  933 
shows "a + a = 0 \<longleftrightarrow> a = 0" 
934 
(is "?lhs \<longleftrightarrow> ?rhs") 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

935 
proof  
63652  936 
from in_Ints have "a \<in> range of_int" 
937 
unfolding Ints_def [symmetric] . 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

938 
then obtain z where a: "a = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

939 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

940 
proof 
63652  941 
assume ?rhs 
942 
then show ?lhs by simp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

943 
next 
63652  944 
assume ?lhs 
945 
with a have "of_int (z + z) = (of_int 0 :: 'a)" by simp 

946 
then have "z + z = 0" by (simp only: of_int_eq_iff) 

947 
then have "z = 0" by (simp only: double_eq_0_iff) 

948 
with a show ?rhs by simp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

949 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

950 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

951 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

952 
lemma Ints_odd_nonzero: 
63652  953 
fixes a :: "'a::ring_char_0" 
61070  954 
assumes in_Ints: "a \<in> \<int>" 
63652  955 
shows "1 + a + a \<noteq> 0" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

956 
proof  
63652  957 
from in_Ints have "a \<in> range of_int" 
958 
unfolding Ints_def [symmetric] . 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

959 
then obtain z where a: "a = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

960 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

961 
proof 
63652  962 
assume "1 + a + a = 0" 
963 
with a have "of_int (1 + z + z) = (of_int 0 :: 'a)" by simp 

964 
then have "1 + z + z = 0" by (simp only: of_int_eq_iff) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

965 
with odd_nonzero show False by blast 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

966 
qed 
60162  967 
qed 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

968 

61070  969 
lemma Nats_numeral [simp]: "numeral w \<in> \<nat>" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

970 
using of_nat_in_Nats [of "numeral w"] by simp 
35634  971 

60162  972 
lemma Ints_odd_less_0: 
63652  973 
fixes a :: "'a::linordered_idom" 
61070  974 
assumes in_Ints: "a \<in> \<int>" 
63652  975 
shows "1 + a + a < 0 \<longleftrightarrow> a < 0" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

976 
proof  
63652  977 
from in_Ints have "a \<in> range of_int" 
978 
unfolding Ints_def [symmetric] . 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

979 
then obtain z where a: "a = of_int z" .. 
63652  980 
with a have "1 + a + a < 0 \<longleftrightarrow> of_int (1 + z + z) < (of_int 0 :: 'a)" 
981 
by simp 

982 
also have "\<dots> \<longleftrightarrow> z < 0" 

983 
by (simp only: of_int_less_iff odd_less_0_iff) 

984 
also have "\<dots> \<longleftrightarrow> a < 0" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

985 
by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

986 
finally show ?thesis . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

987 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

988 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

989 

64272  990 
subsection \<open>@{term sum} and @{term prod}\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

991 

64267  992 
lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))" 
63652  993 
by (induct A rule: infinite_finite_induct) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

994 

64267  995 
lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))" 
63652  996 
by (induct A rule: infinite_finite_induct) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

997 

64272  998 
lemma of_nat_prod [simp]: "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat(f x))" 
63652  999 
by (induct A rule: infinite_finite_induct) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1000 

64272  1001 
lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))" 
63652  1002 
by (induct A rule: infinite_finite_induct) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1003 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1004 

60758  1005 
text \<open>Legacy theorems\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1006 

64714
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

1007 
lemmas int_sum = of_nat_sum [where 'a=int] 
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

1008 
lemmas int_prod = of_nat_prod [where 'a=int] 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1009 
lemmas zle_int = of_nat_le_iff [where 'a=int] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1010 
lemmas int_int_eq = of_nat_eq_iff [where 'a=int] 
64714
53bab28983f1
complete set of cases rules for integers known to be (non)positive/negative;
haftmann
parents:
64272
diff
changeset

1011 
lemmas nonneg_eq_int = nonneg_int_cases 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1012 

63652  1013 

60758  1014 
subsection \<open>Setting up simplification procedures\<close> 
30802  1015 

54249  1016 
lemmas of_int_simps = 
1017 
of_int_0 of_int_1 of_int_add of_int_mult 

1018 

48891  1019 
ML_file "Tools/int_arith.ML" 
60758  1020 
declaration \<open>K Int_Arith.setup\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1021 

63652  1022 
simproc_setup fast_arith 
1023 
("(m::'a::linordered_idom) < n"  

1024 
"(m::'a::linordered_idom) \<le> n"  

1025 
"(m::'a::linordered_idom) = n") = 

61144  1026 
\<open>K Lin_Arith.simproc\<close> 
43595  1027 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1028 

60758  1029 
subsection\<open>More Inequality Reasoning\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1030 

63652  1031 
lemma zless_add1_eq: "w < z + 1 \<longleftrightarrow> w < z \<or> w = z" 
1032 
for w z :: int 

1033 
by arith 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1034 

63652  1035 
lemma add1_zle_eq: "w + 1 \<le> z \<longleftrightarrow> w < z" 
1036 
for w z :: int 

1037 
by arith 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1038 

63652  1039 
lemma zle_diff1_eq [simp]: "w \<le> z  1 \<longleftrightarrow> w < z" 
1040 
for w z :: int 

1041 
by arith 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1042 

63652  1043 
lemma zle_add1_eq_le [simp]: "w < z + 1 \<longleftrightarrow> w \<le> z" 
1044 
for w z :: int 

1045 
by arith 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1046 

63652  1047 
lemma int_one_le_iff_zero_less: "1 \<le> z \<longleftrightarrow> 0 < z" 
1048 
for z :: int 

1049 
by arith 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1050 

64758
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1051 
lemma Ints_nonzero_abs_ge1: 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1052 
fixes x:: "'a :: linordered_idom" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1053 
assumes "x \<in> Ints" "x \<noteq> 0" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1054 
shows "1 \<le> abs x" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1055 
proof (rule Ints_cases [OF \<open>x \<in> Ints\<close>]) 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1056 
fix z::int 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1057 
assume "x = of_int z" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1058 
with \<open>x \<noteq> 0\<close> 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1059 
show "1 \<le> \<bar>x\<bar>" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1060 
apply (auto simp add: abs_if) 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1061 
by (metis diff_0 of_int_1 of_int_le_iff of_int_minus zle_diff1_eq) 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1062 
qed 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1063 

3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1064 
lemma Ints_nonzero_abs_less1: 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1065 
fixes x:: "'a :: linordered_idom" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1066 
shows "\<lbrakk>x \<in> Ints; abs x < 1\<rbrakk> \<Longrightarrow> x = 0" 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1067 
using Ints_nonzero_abs_ge1 [of x] by auto 
3b33d2fc5fc0
A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents:
64714
diff
changeset

1068 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1069 

63652  1070 
subsection \<open>The functions @{term nat} and @{term int}\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1071 

63652  1072 
text \<open>Simplify the term @{term "w +  z"}.\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1073 

63652  1074 
lemma one_less_nat_eq [simp]: "Suc 0 < nat z \<longleftrightarrow> 1 < z" 
60162  1075 
using zless_nat_conj [of 1 z] by auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1076 

63652  1077 
text \<open> 
1078 
This simplifies expressions of the form @{term "int n = z"} where 

1079 
\<open>z\<close> is an integer literal. 

1080 
\<close> 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1081 
lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1082 

59000  1083 
lemma nat_abs_int_diff: "nat \<bar>int a  int b\<bar> = (if a \<le> b then b  a else a  b)" 
1084 
by auto 

1085 

1086 
lemma nat_int_add: "nat (int a + int b) = a + b" 

1087 
by auto 

1088 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1089 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1090 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1091 

33056
791a4655cae3
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
blanchet
parents:
32437
diff
changeset

1092 
lemma of_int_of_nat [nitpick_simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1093 
"of_int k = (if k < 0 then  of_nat (nat ( k)) else of_nat (nat k))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1094 
proof (cases "k < 0") 
63652  1095 
case True 
1096 
then have "0 \<le>  k" by simp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1097 
then have "of_nat (nat ( k)) = of_int ( k)" by (rule of_nat_nat) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1098 
with True show ?thesis by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1099 
next 
63652  1100 
case False 
1101 
then show ?thesis by (simp add: not_less) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1102 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1103 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1104 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1105 

64014  1106 
lemma transfer_rule_of_int: 
1107 
fixes R :: "'a::ring_1 \<Rightarrow> 'b::ring_1 \<Rightarrow> bool" 

1108 
assumes [transfer_rule]: "R 0 0" "R 1 1" 

1109 
"rel_fun R (rel_fun R R) plus plus" 

1110 
"rel_fun R R uminus uminus" 

1111 
shows "rel_fun HOL.eq R of_int of_int" 

1112 
proof  

1113 
note transfer_rule_of_nat [transfer_rule] 

1114 
have [transfer_rule]: "rel_fun HOL.eq R of_nat of_nat" 

1115 
by transfer_prover 

1116 
show ?thesis 

1117 
by (unfold of_int_of_nat [abs_def]) transfer_prover 

1118 
qed 

1119 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1120 
lemma nat_mult_distrib: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1121 
fixes z z' :: int 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1122 
assumes "0 \<le> z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1123 
shows "nat (z * z') = nat z * nat z'" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1124 
proof (cases "0 \<le> z'") 
63652  1125 
case False 
1126 
with assms have "z * z' \<le> 0" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1127 
by (simp add: not_le mult_le_0_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1128 
then have "nat (z * z') = 0" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1129 
moreover from False have "nat z' = 0" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1130 
ultimately show ?thesis by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1131 
next 
63652  1132 
case True 
1133 
with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1134 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1135 
by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1136 
(simp only: of_nat_mult of_nat_nat [OF True] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1137 
of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1138 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1139 

63652  1140 
lemma nat_mult_distrib_neg: "z \<le> 0 \<Longrightarrow> nat (z * z') = nat ( z) * nat ( z')" 
1141 
for z z' :: int 

1142 
apply (rule trans) 

1143 
apply (rule_tac [2] nat_mult_distrib) 

1144 
apply auto 

1145 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1146 

61944  1147 
lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>" 
63652  1148 
by (cases "z = 0 \<or> w = 0") 
1149 
(auto simp add: abs_if nat_mult_distrib [symmetric] 

1150 
nat_mult_distrib_neg [symmetric] mult_less_0_iff) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1151 

63652  1152 
lemma int_in_range_abs [simp]: "int n \<in> range abs" 
60570  1153 
proof (rule range_eqI) 
63652  1154 
show "int n = \<bar>int n\<bar>" by simp 
60570  1155 
qed 
1156 

63652  1157 
lemma range_abs_Nats [simp]: "range abs = (\<nat> :: int set)" 
60570  1158 
proof  
1159 
have "\<bar>k\<bar> \<in> \<nat>" for k :: int 

1160 
by (cases k) simp_all 

1161 
moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int 

1162 
using that by induct simp 

1163 
ultimately show ?thesis by blast 

61204  1164 
qed 
60570  1165 

63652  1166 
lemma Suc_nat_eq_nat_zadd1: "0 \<le> z \<Longrightarrow> Suc (nat z) = nat (1 + z)" 
1167 
for z :: int 

1168 
by (rule sym) (simp add: nat_eq_iff) 

47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

1169 

9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

1170 
lemma diff_nat_eq_if: 
63652  1171 
"nat z  nat z' = 
1172 
(if z' < 0 then nat z 

1173 
else 

1174 
let d = z  z' 

1175 
in if d < 0 then 0 else nat d)" 

1176 
by (simp add: Let_def nat_diff_distrib [symmetric]) 

47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

1177 

63652  1178 
lemma nat_numeral_diff_1 [simp]: "numeral v  (1::nat) = nat (numeral v  1)" 
47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

1179 
using diff_nat_numeral [of v Num.One] by simp 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

1180 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1181 

63652  1182 
subsection \<open>Induction principles for int\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1183 

63652  1184 
text \<open>Wellfounded segments of the integers.\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1185 

63652  1186 
definition int_ge_less_than :: "int \<Rightarrow> (int \<times> int) set" 
1187 
where "int_ge_less_than d = {(z', z). d \<le> z' \<and> z' < z}" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1188 

63652  1189 
lemma wf_int_ge_less_than: "wf (int_ge_less_than d)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1190 
proof  
63652  1191 
have "int_ge_less_than d \<subseteq> measure (\<lambda>z. nat (z  d))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1192 
by (auto simp add: int_ge_less_than_def) 
63652  1193 
then show ?thesis 
60162  1194 
by (rule wf_subset [OF wf_measure]) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1195 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1196 

63652  1197 
text \<open> 
1198 
This variant looks odd, but is typical of the relations suggested 

1199 
by RankFinder.\<close> 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1200 

63652  1201 
definition int_ge_less_than2 :: "int \<Rightarrow> (int \<times> int) set" 
1202 
where "int_ge_less_than2 d = {(z',z). d \<le> z \<and> z' < z}" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1203 

63652  1204 
lemma wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1205 
proof  
63652  1206 
have "int_ge_less_than2 d \<subseteq> measure (\<lambda>z. nat (1 + z  d))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1207 
by (auto simp add: int_ge_less_than2_def) 
63652  1208 
then show ?thesis 
60162  1209 
by (rule wf_subset [OF wf_measure]) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1210 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1211 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1212 
(* `set:int': dummy construction *) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1213 
theorem int_ge_induct [case_names base step, induct set: int]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1214 
fixes i :: int 
63652  1215 
assumes ge: "k \<le> i" 
1216 
and base: "P k" 

1217 
and step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1218 
shows "P i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1219 
proof  
63652  1220 
have "\<And>i::int. n = nat (i  k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" for n 
1221 
proof (induct n) 

1222 
case 0 

1223 
then have "i = k" by arith 

1224 
with base show "P i" by simp 

1225 
next 

1226 
case (Suc n) 

1227 
then have "n = nat ((i  1)  k)" by arith 

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

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

1230 
from step [OF k this] show ?case by simp 

1231 
qed 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1232 
with ge show ?thesis by fast 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1233 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1234 

25928  1235 
(* `set:int': dummy construction *) 
1236 
theorem int_gr_induct [case_names base step, induct set: int]: 

63652  1237 
fixes i k :: int 
1238 
assumes gr: "k < i" 

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

1240 
and step: "\<And>i. k < i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1241 
shows "P i" 
63652  1242 
apply (rule int_ge_induct[of "k + 1"]) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1243 
using gr apply arith 
63652  1244 
apply (rule base) 
1245 
apply (rule step) 

1246 
apply simp_all 

1247 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1248 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1249 
theorem int_le_induct [consumes 1, case_names base step]: 
63652  1250 
fixes i k :: int 
1251 
assumes le: "i \<le> k" 

1252 
and base: "P k" 

1253 
and step: "\<And>i. i \<le> k \<Longrightarrow> P i \<Longrightarrow> P (i  1)" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1254 
shows "P i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1255 
proof  
63652  1256 
have "\<And>i::int. n = nat(ki) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" for n 
1257 
proof (induct n) 

1258 
case 0 

1259 
then have "i = k" by arith 

1260 
with base show "P i" by simp 

1261 
next 

1262 
case (Suc n) 

1263 
then have "n = nat (k  (i + 1))" by arith 

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

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

1266 
from step[OF k this] show ?case by simp 

1267 
qed 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1268 
with le show ?thesis by fast 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1269 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1270 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1271 
theorem int_less_induct [consumes 1, case_names base step]: 
63652  1272 
fixes i k :: int 
1273 
assumes less: "i < k" 

1274 
and base: "P (k  1)" 

1275 
and step: "\<And>i. i < k \<Longrightarrow> P i \<Longrightarrow> P (i  1)" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1276 
shows "P i" 
63652  1277 
apply (rule int_le_induct[of _ "k  1"]) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1278 
using less apply arith 
63652  1279 
apply (rule base) 
1280 
apply (rule step) 

1281 
apply simp_all 

1282 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1283 

36811
4ab4aa5bee1c
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
haftmann
parents:
36801
diff
changeset

1284 
theorem int_induct [case_names base step1 step2]: 
36801
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1285 
fixes k :: int 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1286 
assumes base: "P k" 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1287 
and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1288 
and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i  1)" 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1289 
shows "P i" 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1290 
proof  
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1291 
have "i \<le> k \<or> i \<ge> k" by arith 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1292 
then show ?thesis 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1293 
proof 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1294 
assume "i \<ge> k" 
63652  1295 
then show ?thesis 
1296 
using base by (rule int_ge_induct) (fact step1) 

36801
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1297 
next 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1298 
assume "i \<le> k" 
63652  1299 
then show ?thesis 
1300 
using base by (rule int_le_induct) (fact step2) 

36801
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1301 
qed 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1302 
qed 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1303 

63652  1304 

1305 
subsection \<open>Intermediate value theorems\<close> 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1306 

63652  1307 
lemma int_val_lemma: "(\<forall>i<n. \<bar>f (i + 1)  f i\<bar> \<le> 1) \<longrightarrow> f 0 \<le> k \<longrightarrow> k \<le> f n \<longrightarrow> (\<exists>i \<le> n. f i = k)" 
1308 
for n :: nat and k :: int 

1309 
unfolding One_nat_def 

1310 
apply (induct n) 

1311 
apply simp 

1312 
apply (intro strip) 

1313 
apply (erule impE) 

1314 
apply simp 

1315 
apply (erule_tac x = n in allE) 

1316 
apply simp 

1317 
apply (case_tac "k = f (Suc n)") 

1318 
apply force 

1319 
apply (erule impE) 

1320 
apply (simp add: abs_if split: if_split_asm) 

1321 
apply (blast intro: le_SucI) 

1322 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1323 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1324 
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1325 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1326 
lemma nat_intermed_int_val: 
63652  1327 
"\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (i + 1)  f i\<bar> \<le> 1 \<Longrightarrow> m < n \<Longrightarrow> 
1328 
f m \<le> k \<Longrightarrow> k \<le> f n \<Longrightarrow> \<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k" 

1329 
for f :: "nat \<Rightarrow> int" and k :: int 

1330 
apply (cut_tac n = "nm" and f = "\<lambda>i. f (i + m)" and k = k in int_val_lemma) 

1331 
unfolding One_nat_def 

1332 
apply simp 

1333 
apply (erule exE) 

1334 
apply (rule_tac x = "i+m" in exI) 

1335 
apply arith 

1336 
done 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1337 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1338 

63652  1339 
subsection \<open>Products and 1, by T. M. Rasmussen\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1340 

34055  1341 
lemma abs_zmult_eq_1: 
63652  1342 
fixes m n :: int 