author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
child 51112  da97167e03f7 
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 
48045  9 
imports Equiv_Relations Wellfounded Quotient 
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 

48045  40 
lift_definition zero_int :: "int" is "(0, 0)" 
41 
by simp 

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

42 

48045  43 
lift_definition one_int :: "int" is "(1, 0)" 
44 
by simp 

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

45 

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

48 
by clarsimp 

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

49 

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

52 
by clarsimp 

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

53 

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

56 
by clarsimp 

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

57 

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

60 
proof (clarsimp) 

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

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

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

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

65 
by simp 

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

67 
by (simp add: algebra_simps) 

68 
qed 

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

69 

48045  70 
instance 
71 
by default (transfer, clarsimp simp: algebra_simps)+ 

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

72 

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

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

74 

44709  75 
abbreviation int :: "nat \<Rightarrow> int" where 
76 
"int \<equiv> of_nat" 

77 

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

80 
simp add: one_int.abs_eq plus_int.abs_eq) 

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

81 

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

84 
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

85 

48045  86 
lemma int_diff_cases: 
87 
obtains (diff) m n where "z = int m  int n" 

88 
by transfer clarsimp 

89 

90 
subsection {* Integers are totally ordered *} 

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

91 

48045  92 
instantiation int :: linorder 
93 
begin 

94 

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

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

97 
by auto 

98 

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

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

101 
by auto 

102 

103 
instance 

104 
by default (transfer, force)+ 

105 

106 
end 

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

107 

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

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

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

110 

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

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

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

113 

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

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

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

116 

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

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

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

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

120 

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

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

122 

48045  123 
subsection {* Ordering properties of arithmetic operations *} 
124 

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

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

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

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

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

130 
qed 
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 Monotonicity of Multiplication*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

133 

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

134 
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

135 
lemma zmult_zless_mono2_lemma: 
44709  136 
"(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

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

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

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

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

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

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

143 

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

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

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

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

149 

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

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

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

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

155 

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

156 
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

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

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

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

160 

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

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

164 

165 
definition 

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

167 

168 
definition 

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

170 

171 
instance proof 

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

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

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

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

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

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

177 
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

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

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

180 

48045  181 
end 
182 

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

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

185 

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

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

190 
apply (rename_tac a b c d) 

191 
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

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

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

194 

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

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

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

197 
distrib_left [of w z1 z2] 
45607  198 
left_diff_distrib [of z1 z2 w] 
199 
right_diff_distrib [of w z1 z2] 

200 
for z1 z2 w :: int 

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

201 

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

204 

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

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

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

207 

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

210 
of_nat_add [symmetric] simp del: of_nat_add) 

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

211 

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

212 
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

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

214 

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

215 
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

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

217 

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

218 
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

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

220 

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

221 
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

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

223 

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

224 
lemma of_int_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

225 
by (simp add: diff_minus Groups.diff_minus) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

226 

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

227 
lemma of_int_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

228 
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

229 

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

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

233 

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

234 
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

235 
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

236 

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

237 
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

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

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

240 

31015  241 
lemma of_int_power: 
242 
"of_int (z ^ n) = of_int z ^ n" 

243 
by (induct n) simp_all 

244 

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

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

246 

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

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

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

249 

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

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

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

252 
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

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

254 

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

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

258 
using of_int_eq_iff [of z 0] by simp 

259 

260 
lemma of_int_0_eq_iff [simp]: 

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

262 
using of_int_eq_iff [of 0 z] by simp 

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

263 

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

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

265 

36424  266 
context linordered_idom 
267 
begin 

268 

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

269 
text{*Every @{text linordered_idom} has characteristic zero.*} 
36424  270 
subclass ring_char_0 .. 
271 

272 
lemma of_int_le_iff [simp]: 

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

274 
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

275 
of_nat_add [symmetric] simp del: of_nat_add) 
36424  276 

277 
lemma of_int_less_iff [simp]: 

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

279 
by (simp add: less_le order_less_le) 

280 

281 
lemma of_int_0_le_iff [simp]: 

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

283 
using of_int_le_iff [of 0 z] by simp 

284 

285 
lemma of_int_le_0_iff [simp]: 

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

287 
using of_int_le_iff [of z 0] by simp 

288 

289 
lemma of_int_0_less_iff [simp]: 

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

291 
using of_int_less_iff [of 0 z] by simp 

292 

293 
lemma of_int_less_0_iff [simp]: 

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

295 
using of_int_less_iff [of z 0] by simp 

296 

297 
end 

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

298 

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

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

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

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

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

304 

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

305 

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

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

307 

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

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

310 

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

313 

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

316 

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

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

319 

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

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

322 

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

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

325 

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

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

327 
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

328 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
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 
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

331 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
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 zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < 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 
lemma nonneg_eq_int: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

337 
fixes z :: int 
44709  338 
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

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

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

341 

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

344 

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

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

347 

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

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

350 

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

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

48045  355 
by transfer auto 
44707  356 

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

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

360 
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

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

362 

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

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

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

365 

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

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

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

369 

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

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

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

373 

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

376 

44709  377 
lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" 
48045  378 
by transfer (clarsimp simp add: less_diff_conv) 
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 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

382 

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

383 
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

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

385 

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

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

387 

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

390 

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

391 

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

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

393 

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

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

396 

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

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

399 

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

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

402 

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

404 
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

405 

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

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

408 

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

411 

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

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

414 

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

416 
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

417 

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

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

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

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

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

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

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

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

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

428 

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

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

431 

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

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

434 

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

435 
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

436 
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

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

438 
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

439 
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

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

441 
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

442 

44709  443 
lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x =  (int (Suc n))" 
48045  444 
apply transfer 
445 
apply clarsimp 

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

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

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

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

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

451 

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

452 
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

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

454 

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

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

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

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

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

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

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

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

463 

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

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

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

467 

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

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

469 
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

470 
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

471 

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

472 
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

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

474 
unfolding Let_def .. 
37767  475 

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

476 
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

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

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

479 

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

480 
text {* Unfold @{text min} and @{text max} on numerals. *} 
28958  481 

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

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

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

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

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

486 
max_def [of "neg_numeral u" "neg_numeral v"] for u v 
28958  487 

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

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

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

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

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

492 
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

493 

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

494 

28958  495 
subsubsection {* Binary comparisons *} 
496 

497 
text {* Preliminaries *} 

498 

499 
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

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

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

505 
order_less_not_sym [OF zero_less_two]) 

506 
finally show ?thesis . 

507 
qed 

508 

509 
lemma le_imp_0_less: 

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

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

512 
proof  

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

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

514 
also have "... < z + 1" by (rule less_add_one) 
28958  515 
also have "... = 1 + z" by (simp add: add_ac) 
516 
finally show "0 < 1 + z" . 

517 
qed 

518 

519 
lemma odd_less_0_iff: 

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

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

521 
proof (cases z) 
28958  522 
case (nonneg n) 
523 
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing 

524 
le_imp_0_less [THEN order_less_imp_le]) 

525 
next 

526 
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

527 
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

528 
add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) 
28958  529 
qed 
530 

531 
subsubsection {* Comparisons, for Ordered Rings *} 

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

532 

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

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

534 

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

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

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

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

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

539 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

556 

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

557 

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

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

559 

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

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

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

562 

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

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

565 

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

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

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

568 

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

571 

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

45533  573 
using Ints_of_int [of "of_nat n"] by simp 
35634  574 

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

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

577 

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

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

580 

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

581 
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

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

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

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

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

586 

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

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

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

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

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

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

592 

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

595 
apply (rule range_eqI) 

596 
apply (rule of_int_diff [symmetric]) 

597 
done 

598 

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

599 
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

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

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

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

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

604 

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

607 

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

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

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

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

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

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

613 
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

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

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

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

617 

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

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

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

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

621 

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

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

623 

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

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

625 

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

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

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

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

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

630 
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

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

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

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

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

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

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

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

638 
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

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

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

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

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

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

644 

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

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

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

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

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

649 
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

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

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

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

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

654 
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

655 
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

656 
with odd_nonzero show False by blast 
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 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

659 

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

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

661 
using of_nat_in_Nats [of "numeral w"] by simp 
35634  662 

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

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

664 
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

665 
shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" 
25919
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 
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

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

669 
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

670 
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

671 
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

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

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

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

675 

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

676 

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

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

678 

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

679 
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

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

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

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

683 

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

684 
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

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

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

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

688 

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

689 
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

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

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

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

693 

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

694 
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

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

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

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

698 

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

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

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

701 

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 
text {* Legacy theorems *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

704 

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

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

706 
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

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

708 

30802  709 
subsection {* Setting up simplification procedures *} 
710 

711 
lemmas int_arith_rules = 

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

712 
neg_le_iff_le numeral_One 
30802  713 
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

714 
mult_zero_left mult_zero_right mult_1_left mult_1_right 
30802  715 
mult_minus_left mult_minus_right 
716 
minus_add_distrib minus_minus mult_assoc 

717 
of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult 

718 
of_int_0 of_int_1 of_int_add of_int_mult 

719 

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

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

722 

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

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

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

725 
"(m::'a::linordered_idom) = n") = 
43595  726 
{* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *} 
727 

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

728 

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

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

730 

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

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

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

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

734 

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

735 

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

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

737 

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

738 
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

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

740 

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

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

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

743 

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

744 
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

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

746 

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

747 
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

748 
by arith 
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 
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

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

752 

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

753 

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

755 

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

756 
text{*Simplify the term @{term "w +  z"}*} 
48045  757 
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

758 

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

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

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

761 

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

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

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

764 

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

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

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

767 

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

768 
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

769 
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

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

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

772 

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

773 
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

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

775 
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

776 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

792 

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

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

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

795 

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

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

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

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

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

800 
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

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

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

803 
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

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

805 

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

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

807 

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

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

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

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

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

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

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

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

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

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

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

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

819 
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

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

821 
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

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

823 
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

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

825 

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

826 
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

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

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

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

830 

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

831 
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

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

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

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

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

836 

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

837 
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

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

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

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

841 

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

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

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

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

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

846 
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

847 
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

848 

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

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

850 
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

851 
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

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

853 
apply (rule nat_mono, simp_all) 
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 nat_numeral [simp, code_abbrev]: 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

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

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

859 

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

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

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

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

863 

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

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

865 
"(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

866 
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

867 

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

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

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

870 
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

871 

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

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

873 

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

874 

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

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

876 

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

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

878 

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

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

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

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

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

883 

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

884 
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

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

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

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

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

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

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

891 

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

892 
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

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

894 

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

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

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

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

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

899 

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

900 
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

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

902 
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

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

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

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

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

907 

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

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

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

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

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

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

913 
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

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

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

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

917 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

934 

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

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

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

939 
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

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

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

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

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

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

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

946 

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

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

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

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

950 
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

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

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

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

954 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

971 

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

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

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

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

975 
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

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

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

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

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

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

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

982 

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

983 
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

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

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

986 
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

987 
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

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

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

990 
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

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

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

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

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

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

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

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

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

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

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

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

1002 

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

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

1004 

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

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

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

1007 
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

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

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

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

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

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

1013 
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

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

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

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

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

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

1020 

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

1021 
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

1022 

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

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

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

1025 
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

1026 
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

1027 
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

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

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

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

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

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

1033 

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 
subsection{*Products and 1, by T. M. Rasmussen*} 
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 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

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

1039 

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

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

1043 
proof  

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

1045 
by auto 

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

1047 
proof 

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

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

1050 
by (simp add: mult_mono 0) 

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

1052 
by (simp add: abs_mult) 

1053 
also have "... = 1" 

1054 
by (simp add: mn) 

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

1056 
thus "False" using 0 

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

1057 
by arith 
34055  1058 
qed 
1059 
thus ?thesis using 0 

1060 
by auto 

1061 
qed 

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

1062 

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

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

1064 

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

1065 
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

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

1067 

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

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

1069 
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

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

1071 
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

1072 
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

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

1074 

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

1075 
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

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

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

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

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

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

1081 

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

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

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

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

1085 
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

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

1087 
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

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

1089 
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

1090 
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

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

1092 

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

1093 

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

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

1095 

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

1096 
subsubsection{*Special Simplification for Constants*} 
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1097 

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

1098 
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

1099 

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

1100 
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

1101 
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

1102 
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

1103 
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

1104 

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

1105 
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

1106 

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

1107 
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

1108 
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

1109 
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

1110 
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

1111 

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

1112 

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

1113 
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

1114 
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

1115 

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

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

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

1118 

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

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

1120 
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

1121 

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

1122 
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

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

1124 

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

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

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

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

1128 

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

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

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

1131 
equation_minus_iff [of "neg_numeral v"] for v 
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 minus_less_iff_numeral [simp, no_atp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

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

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

1136 

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

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

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

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

1140 

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

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

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

1143 
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

1144 

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

1145 
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

1146 

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

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

1148 
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

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

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

1151 

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

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

1153 
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

1154 
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

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

1156 

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

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

1158 
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

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

1160 
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

1161 

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

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

1163 
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

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

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

1166 

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

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

1168 
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

1169 
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

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

1171 

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

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

1173 
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

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

1175 
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

1176 

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

1177 

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

1178 
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

1179 

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

1180 
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

1181 
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

1182 
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

1183 
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

1184 

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

1185 

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

1186 
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

1187 

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

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

1189 
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

1190 
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

1191 

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

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

1193 
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

1194 
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

1195 

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

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

1197 
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

1198 
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

1199 

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

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

1201 
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

1202 
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

1203 

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

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

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

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

1207 

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

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

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

1210 
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

1211 

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

1212 
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

1213 

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

1214 
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

1215 

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

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

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

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

1219 

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

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

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

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

1223 

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

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

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

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

1227 

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

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

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

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

1231 

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

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

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

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

1235 

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

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

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

1238 
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

1239 

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

1240 

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

1241 
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

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

1243 
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

1244 
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

1245 
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

1246 

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

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

1248 

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

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

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

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

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

1253 

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

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

1255 
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

1256 

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

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

1258 
"(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

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

1260 

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

1262 

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

1263 
lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x" 
36719  1264 
by simp 
1265 

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

1266 

33320  1267 
subsection {* The divides relation *} 
1268 

33657  1269 
lemma zdvd_antisym_nonneg: 
1270 
"0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)" 

33320  1271 
apply (simp add: dvd_def, auto) 
33657  1272 
apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff) 
33320  1273 
done 
1274 

33657  1275 
lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" 
33320  1276 
shows "\<bar>a\<bar> = \<bar>b\<bar>" 
33657  1277 
proof cases 
1278 
assume "a = 0" with assms show ?thesis by simp 

1279 
next 

1280 
assume "a \<noteq> 0" 

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

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

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

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

1286 
hence "k = 1 \<and> k' = 1 \<or> k = 1 \<and> k' = 1" by (simp add: zmult_eq_1_iff) 

1287 
thus ?thesis using k k' by auto 

1288 
qed 

1289 

1290 
lemma zdvd_zdiffD: "k dvd m  n ==> k dvd n ==> k dvd (m::int)" 

1291 
apply (subgoal_tac "m = n + (m  n)") 

1292 
apply (erule ssubst) 

1293 
apply (blast intro: dvd_add, simp) 

1294 
done 

1295 

1296 
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" 

1297 
apply (rule iffI) 

1298 
apply (erule_tac [2] dvd_add) 

1299 
apply (subgoal_tac "n = (n + k * m)  k * m") 

1300 
apply (erule ssubst) 

1301 
apply (erule dvd_diff) 

1302 
apply(simp_all) 

1303 
done 

1304 

1305 
lemma dvd_imp_le_int: 

1306 
fixes d i :: int 

1307 
assumes "i \<noteq> 0" and "d dvd i" 

1308 
shows "\<bar>d\<bar> \<le> \<bar>i\<bar>" 

1309 
proof  

1310 
from `d dvd i` obtain k where "i = d * k" .. 

1311 
with `i \<noteq> 0` have "k \<noteq> 0" by auto 

1312 
then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto 

1313 
then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono) 

1314 
with `i = d * k` show ?thesis by (simp add: abs_mult) 

1315 
qed 

1316 

1317 
lemma zdvd_not_zless: 

1318 
fixes m n :: int 

1319 
assumes "0 < m" and "m < n" 

1320 
shows "\<not> n dvd m" 

1321 
proof 

1322 
from assms have "0 < n" by auto 

1323 
assume "n dvd m" then obtain k where k: "m = n * k" .. 

1324 
with `0 < m` have "0 < n * k" by auto 

1325 
with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff) 

1326 
with k `0 < n` `m < n` have "n * k < n * 1" by simp 

1327 
with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto 

1328 
qed 

1329 

1330 
lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)" 

1331 
shows "m dvd n" 

1332 
proof 

1333 
from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast 

1334 
{assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp 

1335 
with h have False by (simp add: mult_assoc)} 

1336 
hence "n = m * h" by blast 

1337 
thus ?thesis by simp 

1338 
qed 

1339 

1340 
theorem zdvd_int: "(x dvd y) = (int x dvd int y)" 

1341 
proof  

1342 
have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y" 

1343 
proof  

1344 
fix k 

1345 
assume A: "int y = int x * k" 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1346 
then show "x dvd y" 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1347 
proof (cases k) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1348 
case (nonneg n) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1349 
with A have "y = x * n" by (simp add: of_nat_mult [symmetric]) 
33320  1350 
then show ?thesis .. 
1351 
next 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1352 
case (neg n) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1353 
with A have "int y = int x * ( int (Suc n))" by simp 
33320  1354 
also have "\<dots> =  (int x * int (Suc n))" by (simp only: mult_minus_right) 
1355 
also have "\<dots> =  int (x * Suc n)" by (simp only: of_nat_mult [symmetric]) 

1356 
finally have " int (x * Suc n) = int y" .. 

1357 
then show ?thesis by (simp only: negative_eq_positive) auto 

1358 
qed 

1359 
qed 

1360 
then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) 

1361 
qed 

1362 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1363 
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)" 
33320  1364 
proof 
1365 
assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp 

1366 
hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int) 

1367 
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

1368 
thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto 
33320  1369 
next 
1370 
assume "\<bar>x\<bar>=1" 

1371 
then have "x = 1 \<or> x = 1" by auto 

1372 
then show "x dvd 1" by (auto intro: dvdI) 

1373 
qed 

1374 

1375 
lemma zdvd_mult_cancel1: 

1376 
assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)" 

1377 
proof 

1378 
assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1379 
by (cases "n >0") (auto simp add: minus_equation_iff) 
33320  1380 
next 
1381 
assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp 

1382 
from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq) 

1383 
qed 

1384 

1385 
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" 

1386 
unfolding zdvd_int by (cases "z \<ge> 0") simp_all 

1387 

1388 
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" 

73998ef6ea91
moved some dv 