author  haftmann 
Wed, 25 Dec 2013 17:39:06 +0100  
changeset 54863  82acc20ded73 
parent 54489  03ff4d1e6784 
child 55085  0e8e4dc55866 
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 

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

6 
header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
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 
51112  9 
imports Equiv_Relations Wellfounded Quotient FunDef 
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 

48045  12 
subsection {* Definition of integers as a quotient type *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

13 

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

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) 
23 
show "reflp intrel" 

24 
unfolding reflp_def by auto 

25 
show "symp intrel" 

26 
unfolding symp_def by auto 

27 
show "transp intrel" 

28 
unfolding transp_def by auto 

29 
qed 

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

30 

48045  31 
lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: 
32 
"(!!x y. z = Abs_Integ (x, y) ==> P) ==> P" 

33 
by (induct z) auto 

34 

35 
subsection {* Integers form a commutative ring *} 

36 

37 
instantiation int :: comm_ring_1 

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

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

39 

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

41 

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

43 

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

46 
by clarsimp 

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

47 

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

50 
by clarsimp 

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

51 

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

54 
by clarsimp 

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

55 

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

58 
proof (clarsimp) 

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

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

61 
hence "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) 

62 
= (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)" 

63 
by simp 

64 
thus "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)" 

65 
by (simp add: algebra_simps) 

66 
qed 

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

67 

48045  68 
instance 
69 
by default (transfer, clarsimp simp: algebra_simps)+ 

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

70 

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

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

72 

44709  73 
abbreviation int :: "nat \<Rightarrow> int" where 
74 
"int \<equiv> of_nat" 

75 

48045  76 
lemma int_def: "int n = Abs_Integ (n, 0)" 
77 
by (induct n, simp add: zero_int.abs_eq, 

78 
simp add: one_int.abs_eq plus_int.abs_eq) 

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

79 

48045  80 
lemma int_transfer [transfer_rule]: 
81 
"(fun_rel (op =) cr_int) (\<lambda>n. (n, 0)) int" 

82 
unfolding fun_rel_def cr_int_def int_def by simp 

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

83 

48045  84 
lemma int_diff_cases: 
85 
obtains (diff) m n where "z = int m  int n" 

86 
by transfer clarsimp 

87 

88 
subsection {* Integers are totally ordered *} 

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

89 

48045  90 
instantiation int :: linorder 
91 
begin 

92 

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

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

95 
by auto 

96 

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

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

99 
by auto 

100 

101 
instance 

102 
by default (transfer, force)+ 

103 

104 
end 

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

105 

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

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

107 
begin 
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 
definition 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

110 
"(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min" 
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 
definition 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

114 

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

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

116 
by intro_classes 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54489
diff
changeset

117 
(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

118 

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

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

120 

48045  121 
subsection {* Ordering properties of arithmetic operations *} 
122 

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

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

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

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

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

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

129 

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

130 
text{*Strict Monotonicity of Multiplication*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

131 

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

132 
text{*strict, in 1st argument; proof is by induction on k>0*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

133 
lemma zmult_zless_mono2_lemma: 
44709  134 
"(i::int)<j ==> 0<k ==> int k * i < int k * j" 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

135 
apply (induct k) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

136 
apply simp 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

137 
apply (simp add: distrib_right) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

138 
apply (case_tac "k=0") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

139 
apply (simp_all add: add_strict_mono) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

141 

44709  142 
lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n" 
48045  143 
apply transfer 
144 
apply clarsimp 

145 
apply (rule_tac x="a  b" in exI, simp) 

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

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

147 

44709  148 
lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n" 
48045  149 
apply transfer 
150 
apply clarsimp 

151 
apply (rule_tac x="a  b" in exI, simp) 

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

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

153 

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

154 
lemma zmult_zless_mono2: "[ i<j; (0::int) < k ] ==> k*i < k*j" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

155 
apply (drule zero_less_imp_eq_int) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

156 
apply (auto simp add: zmult_zless_mono2_lemma) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

158 

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

159 
text{*The integers form an ordered integral domain*} 
48045  160 
instantiation int :: linordered_idom 
161 
begin 

162 

163 
definition 

164 
zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then  i else i)" 

165 

166 
definition 

167 
zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else  1)" 

168 

169 
instance 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) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

175 
show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else  1)" 
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 

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

181 
lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z" 
48045  182 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

183 

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

184 
lemma zless_iff_Suc_zadd: 
44709  185 
"(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))" 
48045  186 
apply transfer 
187 
apply auto 

188 
apply (rename_tac a b c d) 

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

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

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

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

192 

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

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

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

195 
distrib_left [of w z1 z2] 
45607  196 
left_diff_distrib [of z1 z2 w] 
197 
right_diff_distrib [of w z1 z2] 

198 
for z1 z2 w :: int 

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

199 

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

200 

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

201 
subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

202 

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

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

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

205 

48045  206 
lift_definition of_int :: "int \<Rightarrow> 'a" is "\<lambda>(i, j). of_nat i  of_nat j" 
207 
by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq 

208 
of_nat_add [symmetric] simp del: of_nat_add) 

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

209 

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

210 
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

211 
by transfer simp 
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 
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

214 
by transfer simp 
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 
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

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

218 

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

219 
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

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

221 

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

222 
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

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

224 

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

225 
lemma of_int_mult [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

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

227 

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

228 
text{*Collapse nested embeddings*} 
44709  229 
lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n" 
29667  230 
by (induct n) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

231 

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

232 
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

233 
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

234 

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

235 
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

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

237 

31015  238 
lemma of_int_power: 
239 
"of_int (z ^ n) = of_int z ^ n" 

240 
by (induct n) simp_all 

241 

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

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

243 

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

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

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

246 

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

247 
lemma of_int_eq_iff [simp]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

248 
"of_int w = of_int z \<longleftrightarrow> w = z" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

249 
by transfer (clarsimp simp add: algebra_simps 
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

250 
of_nat_add [symmetric] simp del: of_nat_add) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

251 

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

252 
text{*Special cases where either operand is zero*} 
36424  253 
lemma of_int_eq_0_iff [simp]: 
254 
"of_int z = 0 \<longleftrightarrow> z = 0" 

255 
using of_int_eq_iff [of z 0] by simp 

256 

257 
lemma of_int_0_eq_iff [simp]: 

258 
"0 = of_int z \<longleftrightarrow> z = 0" 

259 
using of_int_eq_iff [of 0 z] by simp 

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

260 

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

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

262 

36424  263 
context linordered_idom 
264 
begin 

265 

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

266 
text{*Every @{text linordered_idom} has characteristic zero.*} 
36424  267 
subclass ring_char_0 .. 
268 

269 
lemma of_int_le_iff [simp]: 

270 
"of_int w \<le> of_int z \<longleftrightarrow> w \<le> z" 

48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

271 
by (transfer fixing: less_eq) (clarsimp simp add: algebra_simps 
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

272 
of_nat_add [symmetric] simp del: of_nat_add) 
36424  273 

274 
lemma of_int_less_iff [simp]: 

275 
"of_int w < of_int z \<longleftrightarrow> w < z" 

276 
by (simp add: less_le order_less_le) 

277 

278 
lemma of_int_0_le_iff [simp]: 

279 
"0 \<le> of_int z \<longleftrightarrow> 0 \<le> z" 

280 
using of_int_le_iff [of 0 z] by simp 

281 

282 
lemma of_int_le_0_iff [simp]: 

283 
"of_int z \<le> 0 \<longleftrightarrow> z \<le> 0" 

284 
using of_int_le_iff [of z 0] by simp 

285 

286 
lemma of_int_0_less_iff [simp]: 

287 
"0 < of_int z \<longleftrightarrow> 0 < z" 

288 
using of_int_less_iff [of 0 z] by simp 

289 

290 
lemma of_int_less_0_iff [simp]: 

291 
"of_int z < 0 \<longleftrightarrow> z < 0" 

292 
using of_int_less_iff [of z 0] by simp 

293 

294 
end 

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

295 

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

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

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

298 
fix z show "of_int z = id z" 
48045  299 
by (cases z rule: int_diff_cases, simp) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

301 

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

302 

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

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

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

305 
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

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

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

308 

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

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

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

311 
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

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

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

314 

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

315 
subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

316 

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

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

319 

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

322 

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

325 

44709  326 
corollary nat_0_le: "0 \<le> z ==> int (nat z) = z" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

328 

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

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

331 

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

332 
lemma nat_le_eq_zle: "0 < w  0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)" 
48045  333 
by transfer (clarsimp, arith) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

334 

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

335 
text{*An alternative condition is @{term "0 \<le> w"} *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

336 
corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

337 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

338 

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

339 
corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

340 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

341 

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

342 
lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)" 
48045  343 
by transfer (clarsimp, arith) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

344 

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

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

346 
fixes z :: int 
44709  347 
assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

349 
using assms by (blast dest: nat_0_le sym) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

350 

54223  351 
lemma nat_eq_iff: 
352 
"nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)" 

48045  353 
by transfer (clarsimp simp add: le_imp_diff_is_add) 
54223  354 

355 
corollary nat_eq_iff2: 

356 
"m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)" 

357 
using nat_eq_iff [of w m] by auto 

358 

359 
lemma nat_0 [simp]: 

360 
"nat 0 = 0" 

361 
by (simp add: nat_eq_iff) 

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

362 

54223  363 
lemma nat_1 [simp]: 
364 
"nat 1 = Suc 0" 

365 
by (simp add: nat_eq_iff) 

366 

367 
lemma nat_numeral [simp]: 

368 
"nat (numeral k) = numeral k" 

369 
by (simp add: nat_eq_iff) 

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

370 

54223  371 
lemma nat_neg_numeral [simp]: 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

372 
"nat ( numeral k) = 0" 
54223  373 
by simp 
374 

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

376 
by simp 

377 

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

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

380 

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

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

48045  385 
by transfer auto 
44707  386 

29700  387 
lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0" 
48045  388 
by transfer clarsimp 
29700  389 

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

390 
lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

392 

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

393 
lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

394 
by (insert zless_nat_conj [of 0], auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

395 

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

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

399 

54223  400 
lemma nat_diff_distrib': 
401 
"0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x  y) = nat x  nat y" 

402 
by transfer clarsimp 

403 

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

404 
lemma nat_diff_distrib: 
54223  405 
"0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z  z') = nat z  nat z'" 
406 
by (rule nat_diff_distrib') auto 

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

407 

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

410 

53065  411 
lemma le_nat_iff: 
412 
"k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k" 

413 
by transfer auto 

414 

44709  415 
lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" 
48045  416 
by transfer (clarsimp simp add: less_diff_conv) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

417 

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

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

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

420 

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

421 
lemma of_nat_nat: "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

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

423 

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

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

425 

54249  426 
lemma diff_nat_numeral [simp]: 
427 
"(numeral v :: nat)  numeral v' = nat (numeral v  numeral v')" 

428 
by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) 

429 

430 

29779  431 
text {* For termination proofs: *} 
432 
lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. 

433 

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

434 

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

435 
subsection{*Lemmas about the Function @{term of_nat} and Orderings*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

436 

44709  437 
lemma negative_zless_0: " (int (Suc n)) < (0 \<Colon> int)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

438 
by (simp add: order_less_le del: of_nat_Suc) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

439 

44709  440 
lemma negative_zless [iff]: " (int (Suc n)) < int m" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

441 
by (rule negative_zless_0 [THEN order_less_le_trans], simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

442 

44709  443 
lemma negative_zle_0: " int n \<le> 0" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

445 

44709  446 
lemma negative_zle [iff]: " int n \<le> int m" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

447 
by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

448 

44709  449 
lemma not_zle_0_negative [simp]: "~ (0 \<le>  (int (Suc n)))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

450 
by (subst le_minus_iff, simp del: of_nat_Suc) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

451 

44709  452 
lemma int_zle_neg: "(int n \<le>  int m) = (n = 0 & m = 0)" 
48045  453 
by transfer simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

454 

44709  455 
lemma not_int_zless_negative [simp]: "~ (int n <  int m)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

457 

44709  458 
lemma negative_eq_positive [simp]: "( int n = of_nat m) = (n = 0 & m = 0)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

459 
by (force simp add: order_eq_iff [of " of_nat n"] int_zle_neg) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

460 

44709  461 
lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

463 
have "(w \<le> z) = (0 \<le> z  w)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

465 
also have "\<dots> = (\<exists>n. z  w = of_nat n)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

466 
by (auto elim: zero_le_imp_eq_int) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

467 
also have "\<dots> = (\<exists>n. z = w + of_nat n)" 
29667  468 
by (simp only: algebra_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

471 

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

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

474 

44709  475 
lemma int_Suc0_eq_1: "int (Suc 0) = 1" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

477 

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

478 
text{*This version is proved for all ordered rings, not just integers! 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

479 
It is proved here because attribute @{text arith_split} is not available 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35032
diff
changeset

480 
in theory @{text Rings}. 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

481 
But is it really better than just rewriting with @{text abs_if}?*} 
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53652
diff
changeset

482 
lemma abs_split [arith_split, no_atp]: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34055
diff
changeset

483 
"P(abs(a::'a::linordered_idom)) = ((0 \<le> a > P a) & (a < 0 > P(a)))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

484 
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

485 

44709  486 
lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x =  (int (Suc n))" 
48045  487 
apply transfer 
488 
apply clarsimp 

489 
apply (rule_tac x="b  Suc a" in exI, arith) 

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

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

491 

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

492 

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

493 
subsection {* Cases and induction *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

494 

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

495 
text{*Now we replace the case analysis rule by a more conventional one: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

496 
whether an integer is negative or not.*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

497 

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

498 
theorem int_cases [case_names nonneg neg, cases type: int]: 
44709  499 
"[!! n. z = int n ==> P; !! n. z =  (int (Suc n)) ==> P ] ==> P" 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

500 
apply (cases "z < 0") 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

501 
apply (blast dest!: negD) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

502 
apply (simp add: linorder_not_less del: of_nat_Suc) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

504 
apply (blast dest: nat_0_le [THEN sym]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

506 

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

507 
theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: 
44709  508 
"[!! n. P (int n); !!n. P ( (int (Suc n))) ] ==> P z" 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

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

510 

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

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

512 
assumes "0 \<le> k" obtains n where "k = int n" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

513 
using assms by (rule nonneg_eq_int) 
47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

514 

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

515 
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

516 
 {* Unfold all @{text let}s involving constants *} 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

517 
unfolding Let_def .. 
37767  518 

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

519 
lemma Let_neg_numeral [simp]: "Let ( numeral v) f = f ( numeral v)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

520 
 {* Unfold all @{text let}s involving constants *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

522 

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

523 
text {* Unfold @{text min} and @{text max} on numerals. *} 
28958  524 

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

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

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

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

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

529 
max_def [of " numeral u" " numeral v"] for u v 
28958  530 

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

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

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

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

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

535 
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

536 

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

537 

28958  538 
subsubsection {* Binary comparisons *} 
539 

540 
text {* Preliminaries *} 

541 

542 
lemma even_less_0_iff: 

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

543 
"a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)" 
28958  544 
proof  
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

545 
have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: distrib_right del: one_add_one) 
28958  546 
also have "(1+1)*a < 0 \<longleftrightarrow> a < 0" 
547 
by (simp add: mult_less_0_iff zero_less_two 

548 
order_less_not_sym [OF zero_less_two]) 

549 
finally show ?thesis . 

550 
qed 

551 

552 
lemma le_imp_0_less: 

553 
assumes le: "0 \<le> z" 

554 
shows "(0::int) < 1 + z" 

555 
proof  

556 
have "0 \<le> z" by fact 

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

557 
also have "... < z + 1" by (rule less_add_one) 
28958  558 
also have "... = 1 + z" by (simp add: add_ac) 
559 
finally show "0 < 1 + z" . 

560 
qed 

561 

562 
lemma odd_less_0_iff: 

563 
"(1 + z + z < 0) = (z < (0::int))" 

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

564 
proof (cases z) 
28958  565 
case (nonneg n) 
566 
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing 

567 
le_imp_0_less [THEN order_less_imp_le]) 

568 
next 

569 
case (neg n) 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

570 
thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

571 
add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) 
28958  572 
qed 
573 

574 
subsubsection {* Comparisons, for Ordered Rings *} 

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

575 

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

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

577 

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

578 
lemma odd_nonzero: 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

579 
"1 + z + z \<noteq> (0::int)" 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

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

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

582 
have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

583 
thus ?thesis using le_imp_0_less [OF le] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

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

589 
assume eq: "1 + z + z = 0" 
44709  590 
have "(0::int) < 1 + (int n + int n)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

592 
also have "... =  (1 + z + z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

593 
by (simp add: neg add_assoc [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

594 
also have "... = 0" by (simp add: eq) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

595 
finally have "0<0" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

596 
thus False by blast 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

599 

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

600 

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

601 
subsection {* The Set of Integers *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

602 

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

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

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

605 

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

606 
definition Ints :: "'a set" where 
37767  607 
"Ints = range of_int" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

608 

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

609 
notation (xsymbols) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

610 
Ints ("\<int>") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

611 

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

614 

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

45533  616 
using Ints_of_int [of "of_nat n"] by simp 
35634  617 

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

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

620 

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

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

623 

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

624 
lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

625 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

626 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

627 
apply (rule of_int_add [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

629 

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

630 
lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> a \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

631 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

632 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

633 
apply (rule of_int_minus [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

635 

35634  636 
lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a  b \<in> \<int>" 
637 
apply (auto simp add: Ints_def) 

638 
apply (rule range_eqI) 

639 
apply (rule of_int_diff [symmetric]) 

640 
done 

641 

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

642 
lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

643 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

644 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

645 
apply (rule of_int_mult [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

647 

35634  648 
lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>" 
649 
by (induct n) simp_all 

650 

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

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

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

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

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

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

656 
from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

660 

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

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

662 
"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

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

664 

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

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

666 

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

667 
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

668 

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

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

670 
assumes in_Ints: "a \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

671 
shows "(a + a = 0) = (a = (0::'a::ring_char_0))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

673 
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

677 
assume "a = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

678 
thus "a + a = 0" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

680 
assume eq: "a + a = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

681 
hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

682 
hence "z + z = 0" by (simp only: of_int_eq_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

683 
hence "z = 0" by (simp only: double_eq_0_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

684 
thus "a = 0" by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

687 

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

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

689 
assumes in_Ints: "a \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

690 
shows "1 + a + a \<noteq> (0::'a::ring_char_0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

692 
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

696 
assume eq: "1 + a + a = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

697 
hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

698 
hence "1 + z + z = 0" by (simp only: of_int_eq_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

702 

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

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

704 
using of_nat_in_Nats [of "numeral w"] by simp 
35634  705 

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

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

707 
assumes in_Ints: "a \<in> Ints" 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34055
diff
changeset

708 
shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

710 
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

712 
hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

713 
by (simp add: a) 
45532
74b17a0881b3
Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead
huffman
parents:
45219
diff
changeset

714 
also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

715 
also have "... = (a < 0)" by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

718 

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

719 

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

720 
subsection {* @{term setsum} and @{term setprod} *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

721 

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

722 
lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

723 
apply (cases "finite A") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

724 
apply (erule finite_induct, auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

726 

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

727 
lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

728 
apply (cases "finite A") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

729 
apply (erule finite_induct, auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

731 

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

732 
lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

733 
apply (cases "finite A") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

734 
apply (erule finite_induct, auto simp add: of_nat_mult) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

736 

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

737 
lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

738 
apply (cases "finite A") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

739 
apply (erule finite_induct, auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

741 

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

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

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

744 

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

745 

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

746 
text {* Legacy theorems *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

747 

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

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

749 
lemmas int_int_eq = of_nat_eq_iff [where 'a=int] 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

750 
lemmas numeral_1_eq_1 = numeral_One 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

751 

30802  752 
subsection {* Setting up simplification procedures *} 
753 

54249  754 
lemmas of_int_simps = 
755 
of_int_0 of_int_1 of_int_add of_int_mult 

756 

30802  757 
lemmas int_arith_rules = 
54249  758 
numeral_One more_arith_simps of_nat_simps of_int_simps 
30802  759 

48891  760 
ML_file "Tools/int_arith.ML" 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30273
diff
changeset

761 
declaration {* K Int_Arith.setup *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

762 

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

763 
simproc_setup fast_arith ("(m::'a::linordered_idom) < n"  
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

764 
"(m::'a::linordered_idom) <= n"  
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

765 
"(m::'a::linordered_idom) = n") = 
43595  766 
{* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *} 
767 

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

768 

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

769 
subsection{*Lemmas About Small Numerals*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

770 

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

771 
lemma abs_power_minus_one [simp]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

772 
"abs(1 ^ n) = (1::'a::linordered_idom)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

774 

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

775 

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

776 
subsection{*More Inequality Reasoning*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

777 

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

778 
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z  w=z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

780 

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

781 
lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

783 

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

784 
lemma zle_diff1_eq [simp]: "(w \<le> z  (1::int)) = (w<z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

785 
by arith 
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 
lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

789 

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

790 
lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

792 

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

793 

28958  794 
subsection{*The functions @{term nat} and @{term int}*} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

795 

48044
fea6f3060b65
remove unnecessary simp rules involving Abs_Integ
huffman
parents:
47255
diff
changeset

796 
text{*Simplify the term @{term "w +  z"}*} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

797 

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

798 
lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

799 
apply (insert zless_nat_conj [of 1 z]) 
47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

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

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

802 

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

803 
text{*This simplifies expressions of the form @{term "int n = z"} where 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

804 
z is an integer literal.*} 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

805 
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

806 

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

807 
lemma split_nat [arith_split]: 
44709  808 
"P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

809 
(is "?P = (?L & ?R)") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

810 
proof (cases "i < 0") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

811 
case True thus ?thesis by auto 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

814 
have "?P = ?L" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

816 
assume ?P thus ?L using False by clarsimp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

818 
assume ?L thus ?P using False by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

822 

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

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

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

825 

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

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

827 
"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

828 
proof (cases "k < 0") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

829 
case True then have "0 \<le>  k" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

830 
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

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

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

833 
case False then show ?thesis by (simp add: not_less of_nat_nat) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

835 

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

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

837 

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

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

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

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

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

842 
proof (cases "0 \<le> z'") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

843 
case False with assms have "z * z' \<le> 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

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

849 
case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

851 
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

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

853 
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

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

855 

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

856 
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(z) * nat(z')" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

857 
apply (rule trans) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

858 
apply (rule_tac [2] nat_mult_distrib, auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

860 

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

861 
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

862 
apply (cases "z=0  w=0") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

863 
apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

864 
nat_mult_distrib_neg [symmetric] mult_less_0_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

866 

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

867 
lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

868 
apply (rule sym) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

869 
apply (simp add: nat_eq_iff) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

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

871 

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

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

873 
"nat z  nat z' = 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

874 
(if z' < 0 then nat z 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

875 
else let d = zz' in 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

876 
if d < 0 then 0 else nat d)" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

877 
by (simp add: Let_def nat_diff_distrib [symmetric]) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

878 

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

879 
lemma nat_numeral_diff_1 [simp]: 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

880 
"numeral v  (1::nat) = nat (numeral v  1)" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

881 
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

882 

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

883 

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

884 
subsection "Induction principles for int" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

885 

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

886 
text{*Wellfounded segments of the integers*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

887 

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

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

889 
int_ge_less_than :: "int => (int * int) set" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

891 
"int_ge_less_than d = {(z',z). d \<le> z' & z' < z}" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

892 

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

893 
theorem wf_int_ge_less_than: "wf (int_ge_less_than d)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

895 
have "int_ge_less_than d \<subseteq> measure (%z. nat (zd))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

898 
by (rule wf_subset [OF wf_measure]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

900 

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

901 
text{*This variant looks odd, but is typical of the relations suggested 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

902 
by RankFinder.*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

903 

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

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

905 
int_ge_less_than2 :: "int => (int * int) set" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

907 
"int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

908 

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

909 
theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

911 
have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+zd))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

914 
by (rule wf_subset [OF wf_measure]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

916 

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

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

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

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

920 
assumes ge: "k \<le> i" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

921 
base: "P k" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

922 
step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

925 
{ fix n 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

926 
have "\<And>i::int. n = nat (i  k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

927 
proof (induct n) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

929 
hence "i = k" by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

930 
thus "P i" using base by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

933 
then have "n = nat((i  1)  k)" by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

935 
have ki1: "k \<le> i  1" using Suc.prems by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

937 
have "P (i  1)" by (rule Suc.hyps) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

938 
from step [OF ki1 this] show ?case by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

943 

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

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

946 
assumes gr: "k < (i::int)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

947 
base: "P(k+1)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

948 
step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

950 
apply(rule int_ge_induct[of "k + 1"]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

951 
using gr apply arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

952 
apply(rule base) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

953 
apply (rule step, simp+) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

955 

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

956 
theorem int_le_induct [consumes 1, case_names base step]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

957 
assumes le: "i \<le> (k::int)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

958 
base: "P(k)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

959 
step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i  1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

962 
{ fix n 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

963 
have "\<And>i::int. n = nat(ki) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

964 
proof (induct n) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

966 
hence "i = k" by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

967 
thus "P i" using base by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

969 
case (Suc n) 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

970 
hence "n = nat (k  (i + 1))" by arith 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

972 
have ki1: "i + 1 \<le> k" using Suc.prems by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

974 
have "P (i + 1)" by(rule Suc.hyps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

975 
from step[OF ki1 this] show ?case by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

980 

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

981 
theorem int_less_induct [consumes 1, case_names base step]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

982 
assumes less: "(i::int) < k" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

983 
base: "P(k  1)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

984 
step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i  1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

986 
apply(rule int_le_induct[of _ "k  1"]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

987 
using less apply arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

988 
apply(rule base) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

989 
apply (rule step, simp+) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

991 

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

992 
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

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

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

995 
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

996 
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

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

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

999 
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

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

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

1002 
assume "i \<ge> k" 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1003 
then show ?thesis using base 
36801
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1004 
by (rule int_ge_induct) (fact step1) 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

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

1006 
assume "i \<le> k" 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1007 
then show ?thesis using base 
36801
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1008 
by (rule int_le_induct) (fact step2) 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

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

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

1011 

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

1012 
subsection{*Intermediate value theorems*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1013 

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

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

1015 
"(\<forall>i<n::nat. abs(f(i+1)  f i) \<le> 1) > 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1016 
f 0 \<le> k > k \<le> f n > (\<exists>i \<le> n. f i = (k::int))" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

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

1018 
apply (induct n) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

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

1020 
apply (intro strip) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1021 
apply (erule impE, simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1022 
apply (erule_tac x = n in allE, simp) 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

1023 
apply (case_tac "k = f (Suc n)") 
27106  1024 
apply force 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1025 
apply (erule impE) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1026 
apply (simp add: abs_if split add: split_if_asm) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1027 
apply (blast intro: le_SucI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1029 

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

1030 
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

1031 

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

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

1033 
"[ \<forall>i. m \<le> i & i < n > abs(f(i + 1::nat)  f i) \<le> 1; m < n; 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1034 
f m \<le> k; k \<le> f n ] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1035 
apply (cut_tac n = "nm" and f = "%i. f (i+m) " and k = k 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1036 
in int_val_lemma) 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

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

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

1039 
apply (erule exE) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1040 
apply (rule_tac x = "i+m" in exI, arith) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1042 

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

1043 

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

1044 
subsection{*Products and 1, by T. M. Rasmussen*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1045 

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

1046 
lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1048 

34055  1049 
lemma abs_zmult_eq_1: 
1050 
assumes mn: "\<bar>m * n\<bar> = 1" 

1051 
shows "\<bar>m\<bar> = (1::int)" 

1052 
proof  

1053 
have 0: "m \<noteq> 0 & n \<noteq> 0" using mn 

1054 
by auto 

1055 
have "~ (2 \<le> \<bar>m\<bar>)" 

1056 
proof 

1057 
assume "2 \<le> \<bar>m\<bar>" 

1058 
hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>" 

1059 
by (simp add: mult_mono 0) 

1060 
also have "... = \<bar>m*n\<bar>" 

1061 
by (simp add: abs_mult) 

1062 
also have "... = 1" 

1063 
by (simp add: mn) 

1064 
finally have "2*\<bar>n\<bar> \<le> 1" . 

1065 
thus "False" using 0 

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

1066 
by arith 
34055  1067 
qed 
1068 
thus ?thesis using 0 

1069 
by auto 

1070 
qed 

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

1071 

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

1072 
lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int)  m = 1" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1073 
by (insert abs_zmult_eq_1 [of m n], arith) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1074 

35815
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1075 
lemma pos_zmult_eq_1_iff: 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1076 
assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)" 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1077 
proof  
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1078 
from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma) 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1079 
thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma) 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

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

1081 

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

1082 
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1)  (m = 1 & n = 1))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1083 
apply (rule iffI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1084 
apply (frule pos_zmult_eq_1_iff_lemma) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1085 
apply (simp add: mult_commute [of m]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1086 
apply (frule pos_zmult_eq_1_iff_lemma, auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1088 

33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1089 
lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1090 
proof 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1091 
assume "finite (UNIV::int set)" 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1092 
moreover have "inj (\<lambda>i\<Colon>int. 2 * i)" 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1093 
by (rule injI) simp 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1094 
ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)" 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1095 
by (rule finite_UNIV_inj_surj) 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1096 
then obtain i :: int where "1 = 2 * i" by (rule surjE) 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1097 
then show False by (simp add: pos_zmult_eq_1_iff) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1099 

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

1100 

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

1101 
subsection {* Further theorems on numerals *} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1102 

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

1103 
subsubsection{*Special Simplification for Constants*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1104 

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

1105 
text{*These distributive laws move literals inside sums and differences.*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1106 

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

1107 
lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v 
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

1108 
lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1109 
lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1110 
lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1111 

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

1112 
text{*These are actually for fields, like real: but where else to put them?*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1113 

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

1114 
lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1115 
lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1116 
lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1117 
lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1118 

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

1119 

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

1120 
text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1121 
strange, but then other simprocs simplify the quotient.*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1122 

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

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

1124 
inverse_eq_divide [of "numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1125 

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

1126 
lemmas inverse_eq_divide_neg_numeral [simp] = 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1127 
inverse_eq_divide [of " numeral w"] for w 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1128 

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

1129 
text {*These laws simplify inequalities, moving unary minus from a term 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1130 
into the literal.*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1131 

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

1132 
lemmas equation_minus_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1133 
equation_minus_iff [of "numeral v"] for v 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1134 

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

1135 
lemmas minus_equation_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1136 
minus_equation_iff [of _ "numeral v"] for v 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1137 

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

1138 
lemmas le_minus_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1139 
le_minus_iff [of "numeral v"] for v 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1140 

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

1141 
lemmas minus_le_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1142 
minus_le_iff [of _ "numeral v"] for v 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1143 

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

1144 
lemmas less_minus_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1145 
less_minus_iff [of "numeral v"] for v 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1146 

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

1147 
lemmas minus_less_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1148 
minus_less_iff [of _ "numeral v"] for v 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1149 

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

1150 
 {* FIXME maybe simproc *} 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1151 

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

1152 

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

1153 
text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1154 

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

1155 
lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1156 
lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1157 
lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1158 
lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1159 

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

1160 

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

1161 
text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1162 

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

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

1164 
pos_le_divide_eq [of "numeral w", OF zero_less_numeral] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1165 
neg_le_divide_eq [of " numeral w", OF neg_numeral_less_zero] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1166 

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

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

1168 
pos_divide_le_eq [of "numeral w", OF zero_less_numeral] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1169 
neg_divide_le_eq [of " numeral w", OF neg_numeral_less_zero] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1170 

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

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

1172 
pos_less_divide_eq [of "numeral w", OF zero_less_numeral] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1173 
neg_less_divide_eq [of " numeral w", OF neg_numeral_less_zero] for w 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1174 

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

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

1176 
pos_divide_less_eq [of "numeral w", OF zero_less_numeral] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1177 
neg_divide_less_eq [of " numeral w", OF neg_numeral_less_zero] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1178 

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

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

1180 
eq_divide_eq [of _ _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1181 
eq_divide_eq [of _ _ " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1182 

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

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

1184 
divide_eq_eq [of _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1185 
divide_eq_eq [of _ " numeral w"] for w 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1186 

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

1187 

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

1188 
subsubsection{*Optional Simplification Rules Involving Constants*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1189 

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

1190 
text{*Simplify quotients that are compared with a literal constant.*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1191 

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

1192 
lemmas le_divide_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1193 
le_divide_eq [of "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1194 
le_divide_eq [of " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1195 

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

1196 
lemmas divide_le_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1197 
divide_le_eq [of _ _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1198 
divide_le_eq [of _ _ " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1199 

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

1200 
lemmas less_divide_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1201 
less_divide_eq [of "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1202 
less_divide_eq [of " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1203 

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

1204 
lemmas divide_less_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1205 
divide_less_eq [of _ _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1206 
divide_less_eq [of _ _ " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1207 

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

1208 
lemmas eq_divide_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1209 
eq_divide_eq [of "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1210 
eq_divide_eq [of " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1211 

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

1212 
lemmas divide_eq_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1213 
divide_eq_eq [of _ _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1214 
divide_eq_eq [of _ _ " numeral w"] for w 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1215 

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

1216 

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

1217 
text{*Not good as automatic simprules because they cause case splits.*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

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

1219 
le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

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

1221 
le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1222 

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

1223 
text{*Division By @{text "1"}*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1224 

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

1225 
lemma divide_minus1 [simp]: "(x::'a::field) / 1 =  x" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1226 
unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

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

1228 

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

1229 
lemma minus1_divide [simp]: "1 / (x::'a::field) =  (1 / x)" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1230 
by (fact divide_minus_left) 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1231 

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

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

1233 
"(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))" 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

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

1235 

45607  1236 
lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2] 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1237 

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

1238 
lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1239 
by (fact divide_numeral_1) 
36719  1240 

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

1241 

33320  1242 
subsection {* The divides relation *} 
1243 

33657  1244 
lemma zdvd_antisym_nonneg: 
1245 
"0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)" 

33320  1246 
apply (simp add: dvd_def, auto) 
33657  1247 
apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff) 
33320  1248 
done 
1249 

33657  1250 
lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" 
33320  1251 
shows "\<bar>a\<bar> = \<bar>b\<bar>" 
33657  1252 
proof cases 
1253 
assume "a = 0" with assms show ?thesis by simp 

1254 
next 

1255 
assume "a \<noteq> 0" 

33320  1256 
from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
1257 
from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 

1258 
from k k' have "a = a*k*k'" by simp 

1259 
with mult_cancel_left1[where c="a" and b="k*k'"] 

1260 
have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc) 

1261 
hence "k = 1 \<and> k' = 1 \<or> k = 1 \<and> k' = 1" by (simp add: zmult_eq_1_iff) 

1262 
thus ?thesis using k k' by auto 

1263 
qed 

1264 

1265 
lemma zdvd_zdiffD: "k dvd m  n ==> k dvd n ==> k dvd (m::int)" 

1266 
apply (subgoal_tac "m = n + (m  n)") 

1267 
apply (erule ssubst) 

1268 
apply (blast intro: dvd_add, simp) 

1269 
done 

1270 

1271 
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" 

1272 
apply (rule iffI) 

1273 
apply (erule_tac [2] dvd_add) 

1274 
apply (subgoal_tac "n = (n + k * m)  k * m") 

1275 
apply (erule ssubst) 

1276 
apply (erule dvd_diff) 

1277 
apply(simp_all) 

1278 
done 

1279 

1280 
lemma dvd_imp_le_int: 

1281 
fixes d i :: int 

1282 
assumes "i \<noteq> 0" and "d dvd i" 

1283 
shows "\<bar>d\<bar> \<le> \<bar>i\<bar>" 

1284 
proof  

1285 
from `d dvd i` obtain k where "i = d * k" .. 

1286 
with `i \<noteq> 0` have "k \<noteq> 0" by auto 

1287 
then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto 

1288 
then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono) 

1289 
with `i = d * k` show ?thesis by (simp add: abs_mult) 

1290 
qed 

1291 

1292 
lemma zdvd_not_zless: 

1293 
fixes m n :: int 

1294 
assumes "0 < m" and "m < n" 

1295 
shows "\<not> n dvd m" 

1296 
proof 

1297 
from assms have "0 < n" by auto 

1298 
assume "n dvd m" then obtain k where k: "m = n * k" .. 

1299 
with `0 < m` have "0 < n * k" by auto 

1300 
with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff) 

1301 
with k `0 < n` `m < n` have "n * k < n * 1" by simp 

1302 
with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto 

1303 
qed 

1304 

1305 
lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)" 

1306 
shows "m dvd n" 

1307 
proof 

1308 
from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast 

1309 
{assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp 

1310 
with h have False by (simp add: mult_assoc)} 

1311 
hence "n = m * h" by blast 

1312 
thus ?thesis by simp 

1313 
qed 

1314 

1315 
theorem zdvd_int: "(x dvd y) = (int x dvd int y)" 

1316 
proof  

1317 
have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y" 

1318 
proof  

1319 
fix k 

1320 
assume A: "int y = int x * k" 

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

1321 
then show "x dvd y" 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1322 
proof (cases k) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1323 
case (nonneg n) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1324 
with A have "y = x * n" by (simp add: of_nat_mult [symmetric]) 
33320  1325 
then show ?thesis .. 
1326 
next 

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

1327 
case (neg n) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1328 
with A have "int y = int x * ( int (Suc n))" by simp 
33320  1329 
also have "\<dots> =  (int x * int (Suc n))" by (simp only: mult_minus_right) 
1330 
also have "\<dots> =  int (x * Suc n)" by (simp only: of_nat_mult [symmetric]) 

1331 
finally have " int (x * Suc n) = int y" .. 

1332 
then show ?thesis by (simp only: negative_eq_positive) auto 

1333 
qed 

1334 
qed 

1335 
then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) 

1336 
qed 

1337 

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

1338 
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)" 
33320  1339 
proof 
1340 
assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp 

1341 
hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) 

1342 
hence "nat \<bar>x\<bar> = 1" by simp 

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

1343 
thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto 
33320  1344 
next 
1345 
assume "\<bar>x\<bar>=1" 

1346 
then have "x = 1 \<or> x = 1" by auto 

1347 
then show "x dvd 1" by (auto intro: dvdI) 

1348 
qed 

1349 

1350 
lemma zdvd_mult_cancel1: 

1351 
assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)" 

1352 
proof 

1353 
assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 

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

1354 
by (cases "n >0") (auto simp add: minus_equation_iff) 
33320  1355 
next 
1356 
assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp 

1357 
from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq) 

1358 
qed 

1359 

1360 
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" 

1361 
unfolding zdvd_int by (cases "z \<ge> 0") simp_all 

1362 

1363 
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" 

1364 
unfolding zdvd_int by (cases "z \<ge> 0") simp_all 

1365 

1366 
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)" 

1367 
by (auto simp add: dvd_int_iff) 

1368 

33341  1369 
lemma eq_nat_nat_iff: 
1370 
"0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'" 

1371 
by (auto elim!: nonneg_eq_int) 

1372 

1373 
lemma nat_power_eq: 

1374 
"0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n" 

1375 
by (induct n) (simp_all add: nat_mult_distrib) 

1376 

33320  1377 
lemma zdvd_imp_le: "[ z dvd n; 0 < n ] ==> z \<le> (n::int)" 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1378 
apply (cases n) 
33320  1379 
apply (auto simp add: dvd_int_iff) 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1380 
apply (cases z) 
33320  1381 
apply (auto simp add: dvd_imp_le) 
1382 
done 

1383 

36749  1384 
lemma zdvd_period: 
1385 
fixes a d :: int 

1386 
assumes "a dvd d" 

1387 
shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)" 
