author  haftmann 
Sun, 18 Aug 2013 15:29:50 +0200  
changeset 53065  de1816a7293e 
parent 52435  6646bb548c6b 
child 53652  18fbca265e2e 
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 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

117 
(auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) 
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" 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35032
diff
changeset

223 
by (simp add: diff_minus Groups.diff_minus) 
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 

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

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

236 
unfolding neg_numeral_def neg_numeral_class.neg_numeral_def 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

237 
by (simp only: of_int_minus of_int_numeral) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

238 

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

241 
by (induct n) simp_all 

242 

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

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

244 

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

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

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

247 

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

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

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

250 
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

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

252 

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

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

256 
using of_int_eq_iff [of z 0] by simp 

257 

258 
lemma of_int_0_eq_iff [simp]: 

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

260 
using of_int_eq_iff [of 0 z] by simp 

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

261 

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

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

263 

36424  264 
context linordered_idom 
265 
begin 

266 

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

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

270 
lemma of_int_le_iff [simp]: 

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

272 
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

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

275 
lemma of_int_less_iff [simp]: 

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

277 
by (simp add: less_le order_less_le) 

278 

279 
lemma of_int_0_le_iff [simp]: 

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

281 
using of_int_le_iff [of 0 z] by simp 

282 

283 
lemma of_int_le_0_iff [simp]: 

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

285 
using of_int_le_iff [of z 0] by simp 

286 

287 
lemma of_int_0_less_iff [simp]: 

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

289 
using of_int_less_iff [of 0 z] by simp 

290 

291 
lemma of_int_less_0_iff [simp]: 

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

293 
using of_int_less_iff [of z 0] by simp 

294 

295 
end 

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

296 

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

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

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

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

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

302 

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

303 

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

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

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

306 
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

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

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

309 

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

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

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

312 
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

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

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

315 

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

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

317 

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

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

320 

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

323 

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

326 

44709  327 
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

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

329 

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

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

332 

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

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

335 

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

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

337 
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

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

339 

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

340 
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

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

342 

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

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

345 

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

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

347 
fixes z :: int 
44709  348 
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

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

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

351 

44709  352 
lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)" 
48045  353 
by transfer (clarsimp simp add: le_imp_diff_is_add) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

354 

44709  355 
corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

356 
by (simp only: eq_commute [of m] nat_eq_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

357 

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

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

360 

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

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

48045  365 
by transfer auto 
44707  366 

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

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

370 
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

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

372 

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

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

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

375 

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

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

377 
"[ (0::int) \<le> z; 0 \<le> z' ] ==> nat (z+z') = nat z + nat z'" 
48045  378 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

379 

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

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

381 
"[ (0::int) \<le> z'; z' \<le> z ] ==> nat (zz') = nat z  nat z'" 
48045  382 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

383 

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

386 

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

389 
by transfer auto 

390 

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

393 

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

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

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

396 

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

397 
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

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

399 

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

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

401 

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

404 

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

405 

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

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

407 

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

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

410 

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

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

413 

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

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

416 

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

418 
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

419 

44709  420 
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

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

422 

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

425 

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

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

428 

44709  429 
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

430 
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

431 

44709  432 
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

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

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

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

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

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

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

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

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

442 

44709  443 
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

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

445 

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

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

448 

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

449 
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

450 
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

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

452 
But is it really better than just rewriting with @{text abs_if}?*} 
35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35634
diff
changeset

453 
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

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

455 
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

456 

44709  457 
lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x =  (int (Suc n))" 
48045  458 
apply transfer 
459 
apply clarsimp 

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

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

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

462 

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

463 

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

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

465 

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

466 
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

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

468 

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

469 
theorem int_cases [case_names nonneg neg, cases type: int]: 
44709  470 
"[!! 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

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

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

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

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

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

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

477 

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

478 
theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: 
44709  479 
"[!! 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

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

481 

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

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

483 
assumes "0 \<le> k" obtains n where "k = int n" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

484 
using assms by (cases k, simp, simp del: of_nat_Suc) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

485 

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

486 
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

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

488 
unfolding Let_def .. 
37767  489 

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

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

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

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

493 

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

494 
text {* Unfold @{text min} and @{text max} on numerals. *} 
28958  495 

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

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

497 
max_def [of "numeral u" "numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

498 
max_def [of "numeral u" "neg_numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

499 
max_def [of "neg_numeral u" "numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

500 
max_def [of "neg_numeral u" "neg_numeral v"] for u v 
28958  501 

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

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

503 
min_def [of "numeral u" "numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

504 
min_def [of "numeral u" "neg_numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

505 
min_def [of "neg_numeral u" "numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

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

507 

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

508 

28958  509 
subsubsection {* Binary comparisons *} 
510 

511 
text {* Preliminaries *} 

512 

513 
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

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

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

519 
order_less_not_sym [OF zero_less_two]) 

520 
finally show ?thesis . 

521 
qed 

522 

523 
lemma le_imp_0_less: 

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

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

526 
proof  

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

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

528 
also have "... < z + 1" by (rule less_add_one) 
28958  529 
also have "... = 1 + z" by (simp add: add_ac) 
530 
finally show "0 < 1 + z" . 

531 
qed 

532 

533 
lemma odd_less_0_iff: 

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

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

535 
proof (cases z) 
28958  536 
case (nonneg n) 
537 
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing 

538 
le_imp_0_less [THEN order_less_imp_le]) 

539 
next 

540 
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

541 
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

542 
add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) 
28958  543 
qed 
544 

545 
subsubsection {* Comparisons, for Ordered Rings *} 

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

546 

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

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

548 

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

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

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

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

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

553 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

570 

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

571 

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

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

573 

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

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

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

576 

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

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

579 

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

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

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

582 

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

585 

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

45533  587 
using Ints_of_int [of "of_nat n"] by simp 
35634  588 

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

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

591 

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

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

594 

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

595 
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

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

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

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

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

600 

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

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

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

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

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

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

606 

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

609 
apply (rule range_eqI) 

610 
apply (rule of_int_diff [symmetric]) 

611 
done 

612 

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

613 
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

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

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

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

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

618 

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

621 

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

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

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

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

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

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

627 
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

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

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

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

631 

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

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

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

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

635 

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

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

637 

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

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

639 

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

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

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

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

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

644 
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

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

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

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

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

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

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

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

652 
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

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

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

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

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

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

658 

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

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

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

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

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

663 
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

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

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

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

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

668 
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

669 
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

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

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

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

673 

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

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

675 
using of_nat_in_Nats [of "numeral w"] by simp 
35634  676 

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

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

678 
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

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

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

681 
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

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

683 
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

684 
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

685 
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

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

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

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

689 

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

690 

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

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

692 

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

693 
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

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

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

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

697 

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

698 
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

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

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

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

702 

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

703 
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

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

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

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

707 

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

708 
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

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

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

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

712 

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

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

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

715 

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

716 

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

717 
text {* Legacy theorems *} 
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 
lemmas zle_int = of_nat_le_iff [where 'a=int] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

720 
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

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

722 

30802  723 
subsection {* Setting up simplification procedures *} 
724 

725 
lemmas int_arith_rules = 

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

726 
neg_le_iff_le numeral_One 
30802  727 
minus_zero diff_minus left_minus right_minus 
45219
29f6e990674d
removed mult_Bit1 from int_arith_rules (cf. 882403378a41 and 3078fd2eec7b, where mult_num1 erroneously replaced mult_1)
huffman
parents:
45196
diff
changeset

728 
mult_zero_left mult_zero_right mult_1_left mult_1_right 
30802  729 
mult_minus_left mult_minus_right 
730 
minus_add_distrib minus_minus mult_assoc 

731 
of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult 

732 
of_int_0 of_int_1 of_int_add of_int_mult 

733 

48891  734 
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

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

736 

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

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

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

739 
"(m::'a::linordered_idom) = n") = 
43595  740 
{* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *} 
741 

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

742 

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

743 
subsection{*Lemmas About Small Numerals*} 
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 
lemma abs_power_minus_one [simp]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

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

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

748 

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

749 

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

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

751 

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

752 
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

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

754 

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

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

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

757 

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

758 
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

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

760 

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

761 
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

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

763 

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

764 
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

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

766 

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

767 

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

769 

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

770 
text{*Simplify the term @{term "w +  z"}*} 
48045  771 
lemmas diff_int_def_symmetric = diff_def [where 'a=int, symmetric, simp] 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

772 

44695
075327b8e841
remove duplicate lemma nat_zero in favor of nat_0
huffman
parents:
43595
diff
changeset

773 
lemma nat_0 [simp]: "nat 0 = 0" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

775 

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

776 
lemma nat_1 [simp]: "nat 1 = Suc 0" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

777 
by (subst nat_eq_iff, simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

778 

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

779 
lemma nat_2: "nat 2 = Suc (Suc 0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

780 
by (subst nat_eq_iff, simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

781 

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

782 
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

783 
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

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

785 
done 
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 
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

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

789 
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

790 

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

791 
lemma split_nat [arith_split]: 
44709  792 
"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

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

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

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

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

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

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

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

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

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

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

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

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

805 
qed 
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 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

809 

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

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

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

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

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

814 
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

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

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

817 
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

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

819 

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

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

821 

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

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

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

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

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

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

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

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

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

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

831 
ultimately 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 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

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

835 
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

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

837 
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

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

839 

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

840 
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

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

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

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

844 

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

845 
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

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

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

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

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

850 

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

851 
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

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

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

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

855 

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

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

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

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

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

860 
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

861 
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

862 

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

863 
(* nat_diff_distrib has toostrong premises *) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

864 
lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x  y) = nat x  nat y" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

865 
apply (rule int_int_eq [THEN iffD1], clarsimp) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

866 
apply (subst of_nat_diff) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

867 
apply (rule nat_mono, simp_all) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

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

869 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51112
diff
changeset

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

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

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

873 

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

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

875 
"nat (neg_numeral k) = 0" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

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

877 

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

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

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

880 
by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

881 

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

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

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

884 
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

885 

47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

886 
lemmas nat_arith = diff_nat_numeral 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset

887 

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

888 

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

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

890 

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

891 
text{*Wellfounded segments of the integers*} 
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 
definition 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

897 

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

898 
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

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

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

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

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

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

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

905 

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

906 
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

907 
by RankFinder.*} 
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 
definition 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

913 

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

914 
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

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

916 
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

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

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

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

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

921 

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

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

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

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

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

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

927 
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

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

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

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

931 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

948 

25928  949 
(* `set:int': dummy construction *) 
950 
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

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

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

953 
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

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

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

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

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

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

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

960 

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

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

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

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

964 
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

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

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

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

968 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

985 

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

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

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

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

989 
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

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

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

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

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

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

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

996 

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

997 
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

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

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

1000 
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

1001 
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

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

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

1004 
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

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

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

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

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

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

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

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

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

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

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

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

1016 

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

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

1018 

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

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

1020 
"(\<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

1021 
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

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

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

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

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

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

1027 
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

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

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

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

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

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

1034 

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

1035 
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

1036 

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

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

1038 
"[ \<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

1039 
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

1040 
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

1041 
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

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

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

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

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

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

1047 

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

1048 

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

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

1050 

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

1051 
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

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

1053 

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

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

1057 
proof  

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

1059 
by auto 

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

1061 
proof 

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

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

1064 
by (simp add: mult_mono 0) 

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

1066 
by (simp add: abs_mult) 

1067 
also have "... = 1" 

1068 
by (simp add: mn) 

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

1070 
thus "False" using 0 

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

1071 
by arith 
34055  1072 
qed 
1073 
thus ?thesis using 0 

1074 
by auto 

1075 
qed 

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

1076 

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

1077 
ML_val {* @{const_name neg_numeral} *} 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1078 

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

1079 
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

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

1081 

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

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

1083 
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

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

1085 
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

1086 
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

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

1088 

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

1089 
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

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

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

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

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

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

1095 

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

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

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

1098 
assume "finite (UNIV::int set)" 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1099 
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

1100 
by (rule injI) simp 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1101 
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

1102 
by (rule finite_UNIV_inj_surj) 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1103 
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

1104 
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

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

1106 

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

1107 

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

1108 
subsection {* Further theorems on numerals *} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1109 

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

1110 
subsubsection{*Special Simplification for Constants*} 
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 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

1113 

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

1114 
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

1115 
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

1116 
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

1117 
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

1118 

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

1119 
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

1120 

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

1121 
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

1122 
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

1123 
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

1124 
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

1125 

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

1126 

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

1127 
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

1128 
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

1129 

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

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

1131 
inverse_eq_divide [of "numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1132 

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

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

1134 
inverse_eq_divide [of "neg_numeral w"] for w 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1135 

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

1136 
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

1137 
into the literal.*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1138 

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

1139 
lemmas le_minus_iff_numeral [simp, no_atp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1140 
le_minus_iff [of "numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1141 
le_minus_iff [of "neg_numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1142 

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

1143 
lemmas equation_minus_iff_numeral [simp, no_atp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1144 
equation_minus_iff [of "numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1145 
equation_minus_iff [of "neg_numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1146 

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

1147 
lemmas minus_less_iff_numeral [simp, no_atp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1148 
minus_less_iff [of _ "numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1149 
minus_less_iff [of _ "neg_numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1150 

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

1151 
lemmas minus_le_iff_numeral [simp, no_atp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1152 
minus_le_iff [of _ "numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1153 
minus_le_iff [of _ "neg_numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1154 

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

1155 
lemmas minus_equation_iff_numeral [simp, no_atp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1156 
minus_equation_iff [of _ "numeral v"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1157 
minus_equation_iff [of _ "neg_numeral v"] for v 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1158 

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

1159 
text{*To Simplify Inequalities Where One Side is the Constant 1*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1160 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35634
diff
changeset

1161 
lemma less_minus_iff_1 [simp,no_atp]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1162 
fixes b::"'b::linordered_idom" 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1163 
shows "(1 <  b) = (b < 1)" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

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

1165 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35634
diff
changeset

1166 
lemma le_minus_iff_1 [simp,no_atp]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1167 
fixes b::"'b::linordered_idom" 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1168 
shows "(1 \<le>  b) = (b \<le> 1)" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

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

1170 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35634
diff
changeset

1171 
lemma equation_minus_iff_1 [simp,no_atp]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1172 
fixes b::"'b::ring_1" 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1173 
shows "(1 =  b) = (b = 1)" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1174 
by (subst equation_minus_iff, auto) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1175 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35634
diff
changeset

1176 
lemma minus_less_iff_1 [simp,no_atp]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1177 
fixes a::"'b::linordered_idom" 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1178 
shows "( a < 1) = (1 < a)" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

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

1180 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35634
diff
changeset

1181 
lemma minus_le_iff_1 [simp,no_atp]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1182 
fixes a::"'b::linordered_idom" 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1183 
shows "( a \<le> 1) = (1 \<le> a)" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

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

1185 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35634
diff
changeset

1186 
lemma minus_equation_iff_1 [simp,no_atp]: 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1187 
fixes a::"'b::ring_1" 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1188 
shows "( a = 1) = (a = 1)" 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1189 
by (subst minus_equation_iff, auto) 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1190 

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

1191 

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

1192 
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

1193 

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

1194 
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

1195 
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

1196 
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

1197 
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

1198 

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

1199 

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

1200 
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

1201 

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

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

1203 
pos_le_divide_eq [of "numeral w", OF zero_less_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1204 
neg_le_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1205 

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

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

1207 
pos_divide_le_eq [of "numeral w", OF zero_less_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1208 
neg_divide_le_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1209 

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

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

1211 
pos_less_divide_eq [of "numeral w", OF zero_less_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1212 
neg_less_divide_eq [of "neg_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

1213 

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

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

1215 
pos_divide_less_eq [of "numeral w", OF zero_less_numeral] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1216 
neg_divide_less_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1217 

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

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

1219 
eq_divide_eq [of _ _ "numeral w"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1220 
eq_divide_eq [of _ _ "neg_numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1221 

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

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

1223 
divide_eq_eq [of _ "numeral w"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1224 
divide_eq_eq [of _ "neg_numeral w"] for w 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1225 

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

1226 
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

1227 

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

1228 
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

1229 

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

1230 
lemmas le_divide_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1231 
le_divide_eq [of "numeral w"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1232 
le_divide_eq [of "neg_numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1233 

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

1234 
lemmas divide_le_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1235 
divide_le_eq [of _ _ "numeral w"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1236 
divide_le_eq [of _ _ "neg_numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1237 

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

1238 
lemmas less_divide_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1239 
less_divide_eq [of "numeral w"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1240 
less_divide_eq [of "neg_numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1241 

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

1242 
lemmas divide_less_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1243 
divide_less_eq [of _ _ "numeral w"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1244 
divide_less_eq [of _ _ "neg_numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1245 

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

1246 
lemmas eq_divide_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1247 
eq_divide_eq [of "numeral w"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1248 
eq_divide_eq [of "neg_numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1249 

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

1250 
lemmas divide_eq_eq_numeral = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1251 
divide_eq_eq [of _ _ "numeral w"] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1252 
divide_eq_eq [of _ _ "neg_numeral w"] for w 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1253 

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

1254 

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

1255 
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

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

1257 
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

1258 
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

1259 
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

1260 

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

1261 
text{*Division By @{text "1"}*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1262 

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

1263 
lemma divide_minus1 [simp]: "(x::'a::field) / 1 =  x" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1264 
unfolding minus_one [symmetric] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1265 
unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric] 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

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

1267 

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

1268 
lemma minus1_divide [simp]: "1 / (x::'a::field) =  (1 / x)" 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1269 
unfolding minus_one [symmetric] by (rule divide_minus_left) 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1270 

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

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

1272 
"(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))" 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

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

1274 

45607  1275 
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

1276 

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

1277 
lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x" 
36719  1278 
by simp 
1279 

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

1280 

33320  1281 
subsection {* The divides relation *} 
1282 

33657  1283 
lemma zdvd_antisym_nonneg: 
1284 
"0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)" 

33320  1285 
apply (simp add: dvd_def, auto) 
33657  1286 
apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff) 
33320  1287 
done 
1288 

33657  1289 
lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" 
33320  1290 
shows "\<bar>a\<bar> = \<bar>b\<bar>" 
33657  1291 
proof cases 
1292 
assume "a = 0" with assms show ?thesis by simp 

1293 
next 

1294 
assume "a \<noteq> 0" 

33320  1295 
from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
1296 
from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 

1297 
from k k' have "a = a*k*k'" by simp 

1298 
with mult_cancel_left1[where c="a" and b="k*k'"] 

1299 
have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc) 

1300 
hence "k = 1 \<and> k' = 1 \<or> k = 1 \<and> k' = 1" by (simp add: zmult_eq_1_iff) 

1301 
thus ?thesis using k k' by auto 

1302 
qed 

1303 

1304 
lemma zdvd_zdiffD: "k dvd m  n ==> k dvd n ==> k dvd (m::int)" 

1305 
apply (subgoal_tac "m = n + (m  n)") 

1306 
apply (erule ssubst) 

1307 
apply (blast intro: dvd_add, simp) 

1308 
done 

1309 

1310 
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" 

1311 
apply (rule iffI) 

1312 
apply (erule_tac [2] dvd_add) 

1313 
apply (subgoal_tac "n = (n + k * m)  k * m") 

1314 
apply (erule ssubst) 

1315 
apply (erule dvd_diff) 

1316 
apply(simp_all) 

1317 
done 

1318 

1319 
lemma dvd_imp_le_int: 

1320 
fixes d i :: int 

1321 
assumes "i \<noteq> 0" and "d dvd i" 

1322 
shows "\<bar>d\<bar> \<le> \<bar>i\<bar>" 

1323 
proof  

1324 
from `d dvd i` obtain k where "i = d * k" .. 

1325 
with `i \<noteq> 0` have "k \<noteq> 0" by auto 

1326 
then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto 

1327 
then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono) 

1328 
with `i = d * k` show ?thesis by (simp add: abs_mult) 

1329 
qed 

1330 

1331 
lemma zdvd_not_zless: 

1332 
fixes m n :: int 

1333 
assumes "0 < m" and "m < n" 

1334 
shows "\<not> n dvd m" 

1335 
proof 

1336 
from assms have "0 < n" by auto 

1337 
assume "n dvd m" then obtain k where k: "m = n * k" .. 

1338 
with `0 < m` have "0 < n * k" by auto 

1339 
with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff) 

1340 
with k `0 < n` `m < n` have "n * k < n * 1" by simp 

1341 
with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto 

1342 
qed 

1343 

1344 
lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)" 

1345 
shows "m dvd n" 

1346 
proof 

1347 
from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast 

1348 
{assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp 

1349 
with h have False by (simp add: mult_assoc)} 

1350 
hence "n = m * h" by blast 

1351 
thus ?thesis by simp 

1352 
qed 

1353 

1354 
theorem zdvd_int: "(x dvd y) = (int x dvd int y)" 

1355 
proof  

1356 
have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y" 

1357 
proof  

1358 
fix k 

1359 
assume A: "int y = int x * k" 

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

1360 
then show "x dvd y" 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1361 
proof (cases k) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1362 
case (nonneg n) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1363 
with A have "y = x * n" by (simp add: of_nat_mult [symmetric]) 
33320  1364 
then show ?thesis .. 
1365 
next 

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

1366 
case (neg n) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1367 
with A have "int y = int x * ( int (Suc n))" by simp 
33320  1368 
also have "\<dots> =  (int x * int (Suc n))" by (simp only: mult_minus_right) 
1369 
also have "\<dots> =  int (x * Suc n)" by (simp only: of_nat_mult [symmetric]) 

1370 
finally have " int (x * Suc n) = int y" .. 

1371 
then show ?thesis by (simp only: negative_eq_positive) auto 

1372 
qed 

1373 
qed 

1374 
then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) 

1375 
qed 

1376 

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

1377 
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)" 
33320  1378 
proof 
1379 
assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp 

1380 
hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) 

1381 
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

1382 
thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto 
33320  1383 
next 
1384 
assume "\<bar>x\<bar>=1" 

1385 
then have "x = 1 \<or> x = 1" by auto 

1386 
then show "x dvd 1" by (auto intro: dvdI) 

1387 
qed 

1388 
