author  berghofe 
Tue, 27 Sep 2005 12:14:39 +0200  
changeset 17667  2beb71c0f92e 
parent 17551  2a747fc49a8c 
child 18114  a36a9b2921e9 
permissions  rwrr 
5508  1 
(* Title: IntDef.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
*) 

7 

14271  8 
header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} 
9 

15131  10 
theory IntDef 
15300  11 
imports Equiv_Relations NatArith 
15131  12 
begin 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

13 

5508  14 
constdefs 
14271  15 
intrel :: "((nat * nat) * (nat * nat)) set" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

16 
{*the equivalence relation underlying the integers*} 
14496  17 
"intrel == {((x,y),(u,v))  x y u v. x+v = u+y}" 
5508  18 

19 
typedef (Integ) 

14259  20 
int = "UNIV//intrel" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

21 
by (auto simp add: quotient_def) 
5508  22 

14691  23 
instance int :: "{ord, zero, one, plus, times, minus}" .. 
5508  24 

25 
constdefs 

14259  26 
int :: "nat => int" 
10834  27 
"int m == Abs_Integ(intrel `` {(m,0)})" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

28 

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

29 

14269  30 
defs (overloaded) 
14271  31 

14259  32 
Zero_int_def: "0 == int 0" 
14271  33 
One_int_def: "1 == int 1" 
8937  34 

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

35 
minus_int_def: 
14532  36 
" z == Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. intrel``{(y,x)})" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

37 

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

38 
add_int_def: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

39 
"z + w == 
14532  40 
Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w. 
41 
intrel``{(x+u, y+v)})" 

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

42 

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

43 
diff_int_def: "z  (w::int) == z + (w)" 
5508  44 

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

45 
mult_int_def: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

46 
"z * w == 
14532  47 
Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w. 
48 
intrel``{(x*u + y*v, x*v + y*u)})" 

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

49 

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

50 
le_int_def: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

51 
"z \<le> (w::int) == 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

52 
\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Integ z & (u,v) \<in> Rep_Integ w" 
5508  53 

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

54 
less_int_def: "(z < (w::int)) == (z \<le> w & z \<noteq> w)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

55 

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

56 

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

57 
subsection{*Construction of the Integers*} 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

58 

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

59 
subsubsection{*Preliminary Lemmas about the Equivalence Relation*} 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

60 

14496  61 
lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

62 
by (simp add: intrel_def) 
14259  63 

64 
lemma equiv_intrel: "equiv UNIV intrel" 

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

65 
by (simp add: intrel_def equiv_def refl_def sym_def trans_def) 
14259  66 

14496  67 
text{*Reduces equality of equivalence classes to the @{term intrel} relation: 
68 
@{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *} 

69 
lemmas equiv_intrel_iff = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I] 

14259  70 

14496  71 
declare equiv_intrel_iff [simp] 
72 

73 

74 
text{*All equivalence classes belong to set of representatives*} 

14532  75 
lemma [simp]: "intrel``{(x,y)} \<in> Integ" 
14496  76 
by (auto simp add: Integ_def intrel_def quotient_def) 
14259  77 

15413  78 
text{*Reduces equality on abstractions to equality on representatives: 
14496  79 
@{term "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *} 
15413  80 
declare Abs_Integ_inject [simp] Abs_Integ_inverse [simp] 
14259  81 

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

82 
text{*Case analysis on the representation of an integer as an equivalence 
14485  83 
class of pairs of naturals.*} 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

84 
lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

85 
"(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P" 
15413  86 
apply (rule Abs_Integ_cases [of z]) 
87 
apply (auto simp add: Integ_def quotient_def) 

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

88 
done 
14259  89 

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

90 

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

91 
subsubsection{*@{term int}: Embedding the Naturals into the Integers*} 
14259  92 

93 
lemma inj_int: "inj int" 

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

94 
by (simp add: inj_on_def int_def) 
14259  95 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

96 
lemma int_int_eq [iff]: "(int m = int n) = (m = n)" 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

97 
by (fast elim!: inj_int [THEN injD]) 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

98 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

99 

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

100 
subsubsection{*Integer Unary Negation*} 
14259  101 

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

102 
lemma minus: " Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

103 
proof  
15169  104 
have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

105 
by (simp add: congruent_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

106 
thus ?thesis 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

107 
by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel]) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

108 
qed 
14259  109 

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

110 
lemma zminus_zminus: " ( z) = (z::int)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

111 
by (cases z, simp add: minus) 
14259  112 

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

113 
lemma zminus_0: " 0 = (0::int)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

114 
by (simp add: int_def Zero_int_def minus) 
14259  115 

116 

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

117 
subsection{*Integer Addition*} 
14259  118 

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

119 
lemma add: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

120 
"Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) = 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

121 
Abs_Integ (intrel``{(x+u, y+v)})" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

122 
proof  
15169  123 
have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
124 
respects2 intrel" 

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

125 
by (simp add: congruent2_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

126 
thus ?thesis 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

127 
by (simp add: add_int_def UN_UN_split_split_eq 
14658  128 
UN_equiv_class2 [OF equiv_intrel equiv_intrel]) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

129 
qed 
14259  130 

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

131 
lemma zminus_zadd_distrib: " (z + w) = ( z) + ( w::int)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

132 
by (cases z, cases w, simp add: minus add) 
14259  133 

134 
lemma zadd_commute: "(z::int) + w = w + z" 

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

135 
by (cases z, cases w, simp add: add_ac add) 
14259  136 

137 
lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)" 

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

138 
by (cases z1, cases z2, cases z3, simp add: add add_assoc) 
14259  139 

140 
(*For AC rewriting*) 

14271  141 
lemma zadd_left_commute: "x + (y + z) = y + ((x + z) ::int)" 
14259  142 
apply (rule mk_left_commute [of "op +"]) 
143 
apply (rule zadd_assoc) 

144 
apply (rule zadd_commute) 

145 
done 

146 

147 
lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute 

148 

14738  149 
lemmas zmult_ac = OrderedGroup.mult_ac 
14271  150 

14259  151 
lemma zadd_int: "(int m) + (int n) = int (m + n)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

152 
by (simp add: int_def add) 
14259  153 

154 
lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z" 

155 
by (simp add: zadd_int zadd_assoc [symmetric]) 

156 

157 
lemma int_Suc: "int (Suc m) = 1 + (int m)" 

158 
by (simp add: One_int_def zadd_int) 

159 

14738  160 
(*also for the instance declaration int :: comm_monoid_add*) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

161 
lemma zadd_0: "(0::int) + z = z" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

162 
apply (simp add: Zero_int_def int_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

163 
apply (cases z, simp add: add) 
14259  164 
done 
165 

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

166 
lemma zadd_0_right: "z + (0::int) = z" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

167 
by (rule trans [OF zadd_commute zadd_0]) 
14259  168 

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

169 
lemma zadd_zminus_inverse2: "( z) + z = (0::int)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

170 
by (cases z, simp add: int_def Zero_int_def minus add) 
14259  171 

172 

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

173 
subsection{*Integer Multiplication*} 
14259  174 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

175 
text{*Congruence property for multiplication*} 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

176 
lemma mult_congruent2: 
15169  177 
"(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1) 
178 
respects2 intrel" 

14259  179 
apply (rule equiv_intrel [THEN congruent2_commuteI]) 
14532  180 
apply (force simp add: mult_ac, clarify) 
181 
apply (simp add: congruent_def mult_ac) 

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

182 
apply (rename_tac u v w x y z) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

183 
apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16642
diff
changeset

184 
apply (simp add: mult_ac) 
14259  185 
apply (simp add: add_mult_distrib [symmetric]) 
186 
done 

187 

14532  188 

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

189 
lemma mult: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

190 
"Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) = 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

191 
Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

192 
by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2 
14658  193 
UN_equiv_class2 [OF equiv_intrel equiv_intrel]) 
14259  194 

195 
lemma zmult_zminus: "( z) * w =  (z * (w::int))" 

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

196 
by (cases z, cases w, simp add: minus mult add_ac) 
14259  197 

198 
lemma zmult_commute: "(z::int) * w = w * z" 

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

199 
by (cases z, cases w, simp add: mult add_ac mult_ac) 
14259  200 

201 
lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)" 

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

202 
by (cases z1, cases z2, cases z3, simp add: mult add_mult_distrib2 mult_ac) 
14259  203 

204 
lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)" 

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

205 
by (cases z1, cases z2, cases w, simp add: add mult add_mult_distrib2 mult_ac) 
14259  206 

207 
lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)" 

208 
by (simp add: zmult_commute [of w] zadd_zmult_distrib) 

209 

210 
lemma zdiff_zmult_distrib: "((z1::int)  z2) * w = (z1 * w)  (z2 * w)" 

14496  211 
by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus) 
14259  212 

213 
lemma zdiff_zmult_distrib2: "(w::int) * (z1  z2) = (w * z1)  (w * z2)" 

214 
by (simp add: zmult_commute [of w] zdiff_zmult_distrib) 

215 

216 
lemmas int_distrib = 

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

217 
zadd_zmult_distrib zadd_zmult_distrib2 
14259  218 
zdiff_zmult_distrib zdiff_zmult_distrib2 
219 

16413  220 
lemma int_mult: "int (m * n) = (int m) * (int n)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

221 
by (simp add: int_def mult) 
14259  222 

16413  223 
text{*Compatibility binding*} 
224 
lemmas zmult_int = int_mult [symmetric] 

225 

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

226 
lemma zmult_1: "(1::int) * z = z" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

227 
by (cases z, simp add: One_int_def int_def mult) 
14259  228 

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

229 
lemma zmult_1_right: "z * (1::int) = z" 
14259  230 
by (rule trans [OF zmult_commute zmult_1]) 
231 

232 

14740  233 
text{*The integers form a @{text comm_ring_1}*} 
14738  234 
instance int :: comm_ring_1 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

235 
proof 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

236 
fix i j k :: int 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

237 
show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc) 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

238 
show "i + j = j + i" by (simp add: zadd_commute) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

239 
show "0 + i = i" by (rule zadd_0) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

240 
show " i + i = 0" by (rule zadd_zminus_inverse2) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

241 
show "i  j = i + (j)" by (simp add: diff_int_def) 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

242 
show "(i * j) * k = i * (j * k)" by (rule zmult_assoc) 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

243 
show "i * j = j * i" by (rule zmult_commute) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

244 
show "1 * i = i" by (rule zmult_1) 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

245 
show "(i + j) * k = i * k + j * k" by (simp add: int_distrib) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

246 
show "0 \<noteq> (1::int)" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

247 
by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq) 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

248 
qed 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

249 

a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

250 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

251 
subsection{*The @{text "\<le>"} Ordering*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

252 

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

253 
lemma le: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

254 
"(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

255 
by (force simp add: le_int_def) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

256 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

257 
lemma zle_refl: "w \<le> (w::int)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

258 
by (cases w, simp add: le) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

259 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

260 
lemma zle_trans: "[ i \<le> j; j \<le> k ] ==> i \<le> (k::int)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

261 
by (cases i, cases j, cases k, simp add: le) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

262 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

263 
lemma zle_anti_sym: "[ z \<le> w; w \<le> z ] ==> z = (w::int)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

264 
by (cases w, cases z, simp add: le) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

265 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

266 
(* Axiom 'order_less_le' of class 'order': *) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

267 
lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

268 
by (simp add: less_int_def) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

269 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

270 
instance int :: order 
14691  271 
by intro_classes 
272 
(assumption  

273 
rule zle_refl zle_trans zle_anti_sym zless_le)+ 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

274 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

275 
(* Axiom 'linorder_linear' of class 'linorder': *) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

276 
lemma zle_linear: "(z::int) \<le> w  w \<le> z" 
14691  277 
by (cases z, cases w) (simp add: le linorder_linear) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

278 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

279 
instance int :: linorder 
14691  280 
by intro_classes (rule zle_linear) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

281 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

282 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

283 
lemmas zless_linear = linorder_less_linear [where 'a = int] 
15921  284 
lemmas linorder_neqE_int = linorder_neqE[where 'a = int] 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

285 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

286 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

287 
lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

288 
by (simp add: Zero_int_def) 
14259  289 

290 
lemma zless_int [simp]: "(int m < int n) = (m<n)" 

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

291 
by (simp add: le add int_def linorder_not_le [symmetric]) 
14259  292 

293 
lemma int_less_0_conv [simp]: "~ (int k < 0)" 

294 
by (simp add: Zero_int_def) 

295 

296 
lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)" 

297 
by (simp add: Zero_int_def) 

298 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

299 
lemma int_0_less_1: "0 < (1::int)" 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

300 
by (simp only: Zero_int_def One_int_def One_nat_def zless_int) 
14259  301 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

302 
lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)" 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

303 
by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq) 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

304 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

305 
lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

306 
by (simp add: linorder_not_less [symmetric]) 
14259  307 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

308 
lemma zero_zle_int [simp]: "(0 \<le> int n)" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

309 
by (simp add: Zero_int_def) 
14259  310 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

311 
lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

312 
by (simp add: Zero_int_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

313 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

314 
lemma int_0 [simp]: "int 0 = (0::int)" 
14259  315 
by (simp add: Zero_int_def) 
316 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

317 
lemma int_1 [simp]: "int 1 = 1" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

318 
by (simp add: One_int_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

319 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

320 
lemma int_Suc0_eq_1: "int (Suc 0) = 1" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

321 
by (simp add: One_int_def One_nat_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

322 

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

323 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

324 
subsection{*Monotonicity results*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

325 

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

326 
lemma zadd_left_mono: "i \<le> j ==> k + i \<le> k + (j::int)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

327 
by (cases i, cases j, cases k, simp add: le add) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

328 

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

329 
lemma zadd_strict_right_mono: "i < j ==> i + k < j + (k::int)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

330 
apply (cases i, cases j, cases k) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

331 
apply (simp add: linorder_not_le [where 'a = int, symmetric] 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

332 
linorder_not_le [where 'a = nat] le add) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

333 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

334 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

335 
lemma zadd_zless_mono: "[ w'<w; z'\<le>z ] ==> w' + z' < w + (z::int)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

336 
by (rule order_less_le_trans [OF zadd_strict_right_mono zadd_left_mono]) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

337 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

338 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

339 
subsection{*Strict Monotonicity of Multiplication*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

340 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

341 
text{*strict, in 1st argument; proof is by induction on k>0*} 
15251  342 
lemma zmult_zless_mono2_lemma: 
343 
"i<j ==> 0<k ==> int k * i < int k * j" 

344 
apply (induct "k", simp) 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

345 
apply (simp add: int_Suc) 
15251  346 
apply (case_tac "k=0") 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

347 
apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

348 
apply (simp add: zadd_zless_mono int_Suc0_eq_1 order_le_less) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

349 
done 
14259  350 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

351 
lemma zero_le_imp_eq_int: "0 \<le> k ==> \<exists>n. k = int n" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

352 
apply (cases k) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

353 
apply (auto simp add: le add int_def Zero_int_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

354 
apply (rule_tac x="xy" in exI, simp) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

355 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

356 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

357 
lemma zmult_zless_mono2: "[ i<j; (0::int) < k ] ==> k*i < k*j" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

358 
apply (frule order_less_imp_le [THEN zero_le_imp_eq_int]) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

359 
apply (auto simp add: zmult_zless_mono2_lemma) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

360 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

361 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

362 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

363 
defs (overloaded) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

364 
zabs_def: "abs(i::int) == if i < 0 then i else i" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

365 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

366 

14740  367 
text{*The integers form an ordered @{text comm_ring_1}*} 
14738  368 
instance int :: ordered_idom 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

369 
proof 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

370 
fix i j k :: int 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

371 
show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

372 
show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

373 
show "\<bar>i\<bar> = (if i < 0 then i else i)" by (simp only: zabs_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

374 
qed 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

375 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

376 

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

377 
lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

378 
apply (cases w, cases z) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

379 
apply (simp add: linorder_not_le [symmetric] le int_def add One_int_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

380 
done 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

381 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

382 
subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

383 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

384 
constdefs 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

385 
nat :: "int => nat" 
14532  386 
"nat z == contents (\<Union>(x,y) \<in> Rep_Integ z. { xy })" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

387 

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

388 
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = xy" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

389 
proof  
15169  390 
have "(\<lambda>(x,y). {xy}) respects intrel" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

391 
by (simp add: congruent_def, arith) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

392 
thus ?thesis 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

393 
by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

394 
qed 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

395 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

396 
lemma nat_int [simp]: "nat(int n) = n" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

397 
by (simp add: nat int_def) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

398 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

399 
lemma nat_zero [simp]: "nat 0 = 0" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

400 
by (simp only: Zero_int_def nat_int) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

401 

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

402 
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

403 
by (cases z, simp add: nat le int_def Zero_int_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

404 

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

405 
corollary nat_0_le: "0 \<le> z ==> int (nat z) = z" 
15413  406 
by simp 
14259  407 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

408 
lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

409 
by (cases z, simp add: nat le int_def Zero_int_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

410 

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

411 
lemma nat_le_eq_zle: "0 < w  0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

412 
apply (cases w, cases z) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

413 
apply (simp add: nat le linorder_not_le [symmetric] int_def Zero_int_def, arith) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

414 
done 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

415 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

416 
text{*An alternative condition is @{term "0 \<le> w"} *} 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

417 
corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

418 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

419 

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

420 
corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

421 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

422 

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

423 
lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

424 
apply (cases w, cases z) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

425 
apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

426 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

427 

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

428 
lemma nonneg_eq_int: "[ 0 \<le> z; !!m. z = int m ==> P ] ==> P" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

429 
by (blast dest: nat_0_le sym) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

430 

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

431 
lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

432 
by (cases w, simp add: nat le int_def Zero_int_def, arith) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

433 

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

434 
corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

435 
by (simp only: eq_commute [of m] nat_eq_iff) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

436 

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

437 
lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

438 
apply (cases w) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

439 
apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

440 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

441 

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

442 
lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

443 
by (auto simp add: nat_eq_iff2) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

444 

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

445 
lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

446 
by (insert zless_nat_conj [of 0], auto) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

447 

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

448 
lemma nat_add_distrib: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

449 
"[ (0::int) \<le> z; 0 \<le> z' ] ==> nat (z+z') = nat z + nat z'" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

450 
by (cases z, cases z', simp add: nat add le int_def Zero_int_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

451 

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

452 
lemma nat_diff_distrib: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

453 
"[ (0::int) \<le> z'; z' \<le> z ] ==> nat (zz') = nat z  nat z'" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

454 
by (cases z, cases z', 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

455 
simp add: nat add minus diff_minus le int_def Zero_int_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

456 

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

457 

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

458 
lemma nat_zminus_int [simp]: "nat ( (int n)) = 0" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

459 
by (simp add: int_def minus nat Zero_int_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

460 

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

461 
lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

462 
by (cases z, simp add: nat le int_def linorder_not_le [symmetric], arith) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

463 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

464 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

465 
subsection{*Lemmas about the Function @{term int} and Orderings*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

466 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

467 
lemma negative_zless_0: " (int (Suc n)) < 0" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

468 
by (simp add: order_less_le) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

469 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

470 
lemma negative_zless [iff]: " (int (Suc n)) < int m" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

471 
by (rule negative_zless_0 [THEN order_less_le_trans], simp) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

472 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

473 
lemma negative_zle_0: " int n \<le> 0" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

474 
by (simp add: minus_le_iff) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

475 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

476 
lemma negative_zle [iff]: " int n \<le> int m" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

477 
by (rule order_trans [OF negative_zle_0 zero_zle_int]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

478 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

479 
lemma not_zle_0_negative [simp]: "~ (0 \<le>  (int (Suc n)))" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

480 
by (subst le_minus_iff, simp) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

481 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

482 
lemma int_zle_neg: "(int n \<le>  int m) = (n = 0 & m = 0)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

483 
by (simp add: int_def le minus Zero_int_def) 
14259  484 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

485 
lemma not_int_zless_negative [simp]: "~ (int n <  int m)" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

486 
by (simp add: linorder_not_less) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

487 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

488 
lemma negative_eq_positive [simp]: "( int n = int m) = (n = 0 & m = 0)" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

489 
by (force simp add: order_eq_iff [of " int n"] int_zle_neg) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

490 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

491 
lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)" 
15413  492 
proof (cases w, cases z, simp add: le add int_def) 
493 
fix a b c d 

494 
assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})" 

495 
show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)" 

496 
proof 

497 
assume "a + d \<le> c + b" 

498 
thus "\<exists>n. c + b = a + n + d" 

499 
by (auto intro!: exI [where x="c+b  (a+d)"]) 

500 
next 

501 
assume "\<exists>n. c + b = a + n + d" 

502 
then obtain n where "c + b = a + n + d" .. 

503 
thus "a + d \<le> c + b" by arith 

504 
qed 

505 
qed 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

506 

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

507 
lemma abs_int_eq [simp]: "abs (int m) = int m" 
15003  508 
by (simp add: abs_if) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

509 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

510 
text{*This version is proved for all ordered rings, not just integers! 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

511 
It is proved here because attribute @{text arith_split} is not available 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

512 
in theory @{text Ring_and_Field}. 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

513 
But is it really better than just rewriting with @{text abs_if}?*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

514 
lemma abs_split [arith_split]: 
14738  515 
"P(abs(a::'a::ordered_idom)) = ((0 \<le> a > P a) & (a < 0 > P(a)))" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

516 
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

517 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

518 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

519 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

520 
subsection{*The Constants @{term neg} and @{term iszero}*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

521 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

522 
constdefs 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

523 

14738  524 
neg :: "'a::ordered_idom => bool" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

525 
"neg(Z) == Z < 0" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

526 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

527 
(*For simplifying equalities*) 
14738  528 
iszero :: "'a::comm_semiring_1_cancel => bool" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

529 
"iszero z == z = (0)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

530 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

531 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

532 
lemma not_neg_int [simp]: "~ neg(int n)" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

533 
by (simp add: neg_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

534 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

535 
lemma neg_zminus_int [simp]: "neg( (int (Suc n)))" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

536 
by (simp add: neg_def neg_less_0_iff_less) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

537 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

538 
lemmas neg_eq_less_0 = neg_def 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

539 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

540 
lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

541 
by (simp add: neg_def linorder_not_less) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

542 

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

543 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

544 
subsection{*To simplify inequalities when Numeral1 can get simplified to 1*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

545 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

546 
lemma not_neg_0: "~ neg 0" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

547 
by (simp add: One_int_def neg_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

548 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

549 
lemma not_neg_1: "~ neg 1" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

550 
by (simp add: neg_def linorder_not_less zero_le_one) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

551 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

552 
lemma iszero_0: "iszero 0" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

553 
by (simp add: iszero_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

554 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

555 
lemma not_iszero_1: "~ iszero 1" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

556 
by (simp add: iszero_def eq_commute) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

557 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

558 
lemma neg_nat: "neg z ==> nat z = 0" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

559 
by (simp add: neg_def order_less_imp_le) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

560 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

561 
lemma not_neg_nat: "~ neg z ==> int (nat z) = z" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

562 
by (simp add: linorder_not_less neg_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

563 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

564 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

565 
subsection{*The Set of Natural Numbers*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

566 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

567 
constdefs 
14738  568 
Nats :: "'a::comm_semiring_1_cancel set" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

569 
"Nats == range of_nat" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

570 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

571 
syntax (xsymbols) Nats :: "'a set" ("\<nat>") 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

572 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

573 
lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

574 
by (simp add: Nats_def) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

575 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

576 
lemma Nats_0 [simp]: "0 \<in> Nats" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

577 
apply (simp add: Nats_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

578 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

579 
apply (rule of_nat_0 [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

580 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

581 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

582 
lemma Nats_1 [simp]: "1 \<in> Nats" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

583 
apply (simp add: Nats_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

584 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

585 
apply (rule of_nat_1 [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

586 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

587 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

588 
lemma Nats_add [simp]: "[a \<in> Nats; b \<in> Nats] ==> a+b \<in> Nats" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

589 
apply (auto simp add: Nats_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

590 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

591 
apply (rule of_nat_add [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

592 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

593 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

594 
lemma Nats_mult [simp]: "[a \<in> Nats; b \<in> Nats] ==> a*b \<in> Nats" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

595 
apply (auto simp add: Nats_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

596 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

597 
apply (rule of_nat_mult [symmetric]) 
14259  598 
done 
599 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

600 
text{*Agreement with the specific embedding for the integers*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

601 
lemma int_eq_of_nat: "int = (of_nat :: nat => int)" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

602 
proof 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

603 
fix n 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

604 
show "int n = of_nat n" by (induct n, simp_all add: int_Suc add_ac) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

605 
qed 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

606 

14496  607 
lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)" 
608 
proof 

609 
fix n 

610 
show "of_nat n = id n" by (induct n, simp_all) 

611 
qed 

612 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

613 

14740  614 
subsection{*Embedding of the Integers into any @{text comm_ring_1}: 
615 
@{term of_int}*} 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

616 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

617 
constdefs 
14738  618 
of_int :: "int => 'a::comm_ring_1" 
14532  619 
"of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i  of_nat j })" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

620 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

621 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

622 
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i  of_nat j" 
14496  623 
proof  
15169  624 
have "(\<lambda>(i,j). { of_nat i  (of_nat j :: 'a) }) respects intrel" 
14496  625 
by (simp add: congruent_def compare_rls of_nat_add [symmetric] 
626 
del: of_nat_add) 

627 
thus ?thesis 

628 
by (simp add: of_int_def UN_equiv_class [OF equiv_intrel]) 

629 
qed 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

630 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

631 
lemma of_int_0 [simp]: "of_int 0 = 0" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

632 
by (simp add: of_int Zero_int_def int_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

633 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

634 
lemma of_int_1 [simp]: "of_int 1 = 1" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

635 
by (simp add: of_int One_int_def int_def) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

636 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

637 
lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

638 
by (cases w, cases z, simp add: compare_rls of_int add) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

639 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

640 
lemma of_int_minus [simp]: "of_int (z) =  (of_int z)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

641 
by (cases z, simp add: compare_rls of_int minus) 
14259  642 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

643 
lemma of_int_diff [simp]: "of_int (wz) = of_int w  of_int z" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

644 
by (simp add: diff_minus) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

645 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

646 
lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

647 
apply (cases w, cases z) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

648 
apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

649 
mult add_ac) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

650 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

651 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

652 
lemma of_int_le_iff [simp]: 
14738  653 
"(of_int w \<le> (of_int z::'a::ordered_idom)) = (w \<le> z)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

654 
apply (cases w) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

655 
apply (cases z) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

656 
apply (simp add: compare_rls of_int le diff_int_def add minus 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

657 
of_nat_add [symmetric] del: of_nat_add) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

658 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

659 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

660 
text{*Special cases where either operand is zero*} 
17085  661 
lemmas of_int_0_le_iff = of_int_le_iff [of 0, simplified] 
662 
lemmas of_int_le_0_iff = of_int_le_iff [of _ 0, simplified] 

663 
declare of_int_0_le_iff [simp] 

664 
declare of_int_le_0_iff [simp] 

14259  665 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

666 
lemma of_int_less_iff [simp]: 
14738  667 
"(of_int w < (of_int z::'a::ordered_idom)) = (w < z)" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

668 
by (simp add: linorder_not_le [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

669 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

670 
text{*Special cases where either operand is zero*} 
17085  671 
lemmas of_int_0_less_iff = of_int_less_iff [of 0, simplified] 
672 
lemmas of_int_less_0_iff = of_int_less_iff [of _ 0, simplified] 

673 
declare of_int_0_less_iff [simp] 

674 
declare of_int_less_0_iff [simp] 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

675 

14740  676 
text{*The ordering on the @{text comm_ring_1} is necessary. 
677 
See @{text of_nat_eq_iff} above.*} 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

678 
lemma of_int_eq_iff [simp]: 
14738  679 
"(of_int w = (of_int z::'a::ordered_idom)) = (w = z)" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

680 
by (simp add: order_eq_iff) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

681 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

682 
text{*Special cases where either operand is zero*} 
17085  683 
lemmas of_int_0_eq_iff = of_int_eq_iff [of 0, simplified] 
684 
lemmas of_int_eq_0_iff = of_int_eq_iff [of _ 0, simplified] 

685 
declare of_int_0_eq_iff [simp] 

686 
declare of_int_eq_0_iff [simp] 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

687 

14496  688 
lemma of_int_eq_id [simp]: "of_int = (id :: int => int)" 
689 
proof 

690 
fix z 

691 
show "of_int z = id z" 

692 
by (cases z, 

693 
simp add: of_int add minus int_eq_of_nat [symmetric] int_def diff_minus) 

694 
qed 

695 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

696 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

697 
subsection{*The Set of Integers*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

698 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

699 
constdefs 
14738  700 
Ints :: "'a::comm_ring_1 set" 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

701 
"Ints == range of_int" 
14271  702 

14259  703 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

704 
syntax (xsymbols) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

705 
Ints :: "'a set" ("\<int>") 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

706 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

707 
lemma Ints_0 [simp]: "0 \<in> Ints" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

708 
apply (simp add: Ints_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

709 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

710 
apply (rule of_int_0 [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

711 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

712 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

713 
lemma Ints_1 [simp]: "1 \<in> Ints" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

714 
apply (simp add: Ints_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

715 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

716 
apply (rule of_int_1 [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

717 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

718 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

719 
lemma Ints_add [simp]: "[a \<in> Ints; b \<in> Ints] ==> a+b \<in> Ints" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

720 
apply (auto simp add: Ints_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

721 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

722 
apply (rule of_int_add [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

723 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

724 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

725 
lemma Ints_minus [simp]: "a \<in> Ints ==> a \<in> Ints" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

726 
apply (auto simp add: Ints_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

727 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

728 
apply (rule of_int_minus [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

729 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

730 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

731 
lemma Ints_diff [simp]: "[a \<in> Ints; b \<in> Ints] ==> ab \<in> Ints" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

732 
apply (auto simp add: Ints_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

733 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

734 
apply (rule of_int_diff [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

735 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

736 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

737 
lemma Ints_mult [simp]: "[a \<in> Ints; b \<in> Ints] ==> a*b \<in> Ints" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

738 
apply (auto simp add: Ints_def) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

739 
apply (rule range_eqI) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

740 
apply (rule of_int_mult [symmetric]) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

741 
done 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

742 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

743 
text{*Collapse nested embeddings*} 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

744 
lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

745 
by (induct n, auto) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

746 

15013  747 
lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

748 
by (simp add: int_eq_of_nat) 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14271
diff
changeset

749 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

750 
lemma Ints_cases [case_names of_int, cases set: Ints]: 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

751 
"q \<in> \<int> ==> (!!z. q = of_int z ==> C) ==> C" 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

752 
proof (simp add: Ints_def) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

753 
assume "!!z. q = of_int z ==> C" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

754 
assume "q \<in> range of_int" thus C .. 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

755 
qed 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

756 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

757 
lemma Ints_induct [case_names of_int, induct set: Ints]: 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

758 
"q \<in> \<int> ==> (!!z. P (of_int z)) ==> P q" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

759 
by (rule Ints_cases) auto 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

760 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

761 

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

762 
(* int (Suc n) = 1 + int n *) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

763 
declare int_Suc [simp] 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

764 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

765 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

766 
subsection{*More Properties of @{term setsum} and @{term setprod}*} 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

767 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

768 
text{*By Jeremy Avigad*} 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

769 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

770 

15554  771 
lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

772 
apply (case_tac "finite A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

773 
apply (erule finite_induct, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

774 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

775 

15554  776 
lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

777 
apply (case_tac "finite A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

778 
apply (erule finite_induct, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

779 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

780 

15554  781 
lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))" 
782 
by (simp add: int_eq_of_nat of_nat_setsum) 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

783 

15554  784 
lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

785 
apply (case_tac "finite A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

786 
apply (erule finite_induct, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

787 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

788 

15554  789 
lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

790 
apply (case_tac "finite A") 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

791 
apply (erule finite_induct, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

792 
done 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

793 

15554  794 
lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))" 
795 
by (simp add: int_eq_of_nat of_nat_setprod) 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

796 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

797 
lemma setprod_nonzero_nat: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

798 
"finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

799 
by (rule setprod_nonzero, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

800 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

801 
lemma setprod_zero_eq_nat: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

802 
"finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

803 
by (rule setprod_zero_eq, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

804 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

805 
lemma setprod_nonzero_int: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

806 
"finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

807 
by (rule setprod_nonzero, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

808 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

809 
lemma setprod_zero_eq_int: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

810 
"finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

811 
by (rule setprod_zero_eq, auto) 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

812 

5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

813 

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

814 
text{*Now we replace the case analysis rule by a more conventional one: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

815 
whether an integer is negative or not.*} 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

816 

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

817 
lemma zless_iff_Suc_zadd: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

818 
"(w < z) = (\<exists>n. z = w + int(Suc n))" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

819 
apply (cases z, cases w) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

820 
apply (auto simp add: le add int_def linorder_not_le [symmetric]) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

821 
apply (rename_tac a b c d) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

822 
apply (rule_tac x="a+d  Suc(c+b)" in exI) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

823 
apply arith 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

824 
done 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

825 

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

826 
lemma negD: "x<0 ==> \<exists>n. x =  (int (Suc n))" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

827 
apply (cases x) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

828 
apply (auto simp add: le minus Zero_int_def int_def order_less_le) 
14496  829 
apply (rule_tac x="y  Suc x" in exI, arith) 
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

830 
done 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

831 

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

832 
theorem int_cases [cases type: int, case_names nonneg neg]: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

833 
"[!! n. z = int n ==> P; !! n. z =  (int (Suc n)) ==> P ] ==> P" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

834 
apply (case_tac "z < 0", blast dest!: negD) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

835 
apply (simp add: linorder_not_less) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

836 
apply (blast dest: nat_0_le [THEN sym]) 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

837 
done 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

838 

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

839 
theorem int_induct [induct type: int, case_names nonneg neg]: 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

840 
"[!! n. P (int n); !!n. P ( (int (Suc n))) ] ==> P z" 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

841 
by (cases z) auto 
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14430
diff
changeset

842 

15558  843 
text{*Contributed by Brian Huffman*} 
844 
theorem int_diff_cases [case_names diff]: 

845 
assumes prem: "!!m n. z = int m  int n ==> P" shows "P" 

846 
apply (rule_tac z=z in int_cases) 

847 
apply (rule_tac m=n and n=0 in prem, simp) 

848 
apply (rule_tac m=0 and n="Suc n" in prem, simp) 

849 
done 

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

850 

15013  851 
lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z" 
852 
apply (cases z) 

853 
apply (simp_all add: not_zle_0_negative del: int_Suc) 

854 
done 

855 

856 

16642
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

857 
subsection {* Configuration of the code generator *} 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

858 

16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

859 
(*FIXME: the IntInf.fromInt below hides a dependence on fixedprecision ints!*) 
16642
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

860 

849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

861 
types_code 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

862 
"int" ("int") 
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

863 
attach (term_of) {* 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

864 
val term_of_int = HOLogic.mk_int o IntInf.fromInt; 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

865 
*} 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

866 
attach (test) {* 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

867 
fun gen_int i = one_of [~1, 1] * random_range 0 i; 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

868 
*} 
16642
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

869 

849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

870 
constdefs 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

871 
int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

872 
"int_aux i n == (i + int n)" 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

873 
nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

874 
"nat_aux n i == (n + nat i)" 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

875 

849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

876 
lemma [code]: 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

877 
"int_aux i 0 = i" 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

878 
"int_aux i (Suc n) = int_aux (i + 1) n"  {* tail recursive *} 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

879 
"int n = int_aux 0 n" 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

880 
by (simp add: int_aux_def)+ 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

881 

849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

882 
lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i  1))" 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

883 
 {* tail recursive *} 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

884 
by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

885 
dest: zless_imp_add1_zle) 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

886 
lemma [code]: "nat i = nat_aux 0 i" 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

887 
by (simp add: nat_aux_def) 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

888 

849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

889 
consts_code 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

890 
"0" :: "int" ("0") 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

891 
"1" :: "int" ("1") 
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

892 
"uminus" :: "int => int" ("~") 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

893 
"op +" :: "int => int => int" ("(_ +/ _)") 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16733
diff
changeset

894 
"op *" :: "int => int => int" ("(_ */ _)") 
16642
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

895 
"op <" :: "int => int => bool" ("(_ </ _)") 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

896 
"op <=" :: "int => int => bool" ("(_ <=/ _)") 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

897 
"neg" ("(_ < 0)") 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

898 

849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

899 
ML {* 
17551  900 
fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", 
901 
Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) = 

902 
(SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)), 

903 
Pretty.str (IntInf.toString (HOLogic.dest_binum bin))) handle TERM _ => NONE) 

17667
2beb71c0f92e
Inserted clause for nat in number_of_codegen again ("code unfold" turned
berghofe
parents:
17551
diff
changeset

904 
 number_of_codegen thy defs gr s thyname b (Const ("Numeral.number_of", 
2beb71c0f92e
Inserted clause for nat in number_of_codegen again ("code unfold" turned
berghofe
parents:
17551
diff
changeset

905 
Type ("fun", [_, Type ("nat", [])])) $ bin) = 
2beb71c0f92e
Inserted clause for nat in number_of_codegen again ("code unfold" turned
berghofe
parents:
17551
diff
changeset

906 
SOME (Codegen.invoke_codegen thy defs s thyname b (gr, 
2beb71c0f92e
Inserted clause for nat in number_of_codegen again ("code unfold" turned
berghofe
parents:
17551
diff
changeset

907 
Const ("IntDef.nat", HOLogic.intT > HOLogic.natT) $ 
2beb71c0f92e
Inserted clause for nat in number_of_codegen again ("code unfold" turned
berghofe
parents:
17551
diff
changeset

908 
(Const ("Numeral.number_of", HOLogic.binT > HOLogic.intT) $ bin))) 
16642
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

909 
 number_of_codegen _ _ _ _ _ _ _ = NONE; 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

910 
*} 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

911 

849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

912 
setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *} 
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

913 

17464  914 
quickcheck_params [default_type = int] 
915 

16642
849ec3962b55
Moved code generator setup from NatBin to IntDef.
berghofe
parents:
16413
diff
changeset

916 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

917 
(*Legacy ML bindings, but no longer the structure Int.*) 
14259  918 
ML 
919 
{* 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

920 
val zabs_def = thm "zabs_def" 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

921 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

922 
val int_0 = thm "int_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

923 
val int_1 = thm "int_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

924 
val int_Suc0_eq_1 = thm "int_Suc0_eq_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

925 
val neg_eq_less_0 = thm "neg_eq_less_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

926 
val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

927 
val not_neg_0 = thm "not_neg_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

928 
val not_neg_1 = thm "not_neg_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

929 
val iszero_0 = thm "iszero_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

930 
val not_iszero_1 = thm "not_iszero_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

931 
val int_0_less_1 = thm "int_0_less_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

932 
val int_0_neq_1 = thm "int_0_neq_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

933 
val negative_zless = thm "negative_zless"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

934 
val negative_zle = thm "negative_zle"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

935 
val not_zle_0_negative = thm "not_zle_0_negative"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

936 
val not_int_zless_negative = thm "not_int_zless_negative"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

937 
val negative_eq_positive = thm "negative_eq_positive"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

938 
val zle_iff_zadd = thm "zle_iff_zadd"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

939 
val abs_int_eq = thm "abs_int_eq"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

940 
val abs_split = thm"abs_split"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

941 
val nat_int = thm "nat_int"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

942 
val nat_zminus_int = thm "nat_zminus_int"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

943 
val nat_zero = thm "nat_zero"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

944 
val not_neg_nat = thm "not_neg_nat"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

945 
val neg_nat = thm "neg_nat"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

946 
val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

947 
val nat_0_le = thm "nat_0_le"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

948 
val nat_le_0 = thm "nat_le_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

949 
val zless_nat_conj = thm "zless_nat_conj"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

950 
val int_cases = thm "int_cases"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

951 

14259  952 
val int_def = thm "int_def"; 
953 
val Zero_int_def = thm "Zero_int_def"; 

954 
val One_int_def = thm "One_int_def"; 

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

955 
val diff_int_def = thm "diff_int_def"; 
14259  956 

957 
val inj_int = thm "inj_int"; 

958 
val zminus_zminus = thm "zminus_zminus"; 

959 
val zminus_0 = thm "zminus_0"; 

960 
val zminus_zadd_distrib = thm "zminus_zadd_distrib"; 

961 
val zadd_commute = thm "zadd_commute"; 

962 
val zadd_assoc = thm "zadd_assoc"; 

963 
val zadd_left_commute = thm "zadd_left_commute"; 

964 
val zadd_ac = thms "zadd_ac"; 

14271  965 
val zmult_ac = thms "zmult_ac"; 
14259  966 
val zadd_int = thm "zadd_int"; 
967 
val zadd_int_left = thm "zadd_int_left"; 

968 
val int_Suc = thm "int_Suc"; 

969 
val zadd_0 = thm "zadd_0"; 

970 
val zadd_0_right = thm "zadd_0_right"; 

971 
val zmult_zminus = thm "zmult_zminus"; 

972 
val zmult_commute = thm "zmult_commute"; 

973 
val zmult_assoc = thm "zmult_assoc"; 

974 
val zadd_zmult_distrib = thm "zadd_zmult_distrib"; 

975 
val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2"; 

976 
val zdiff_zmult_distrib = thm "zdiff_zmult_distrib"; 

977 
val zdiff_zmult_distrib2 = thm "zdiff_zmult_distrib2"; 

978 
val int_distrib = thms "int_distrib"; 

979 
val zmult_int = thm "zmult_int"; 

980 
val zmult_1 = thm "zmult_1"; 

981 
val zmult_1_right = thm "zmult_1_right"; 

982 
val int_int_eq = thm "int_int_eq"; 

983 
val int_eq_0_conv = thm "int_eq_0_conv"; 

984 
val zless_int = thm "zless_int"; 

985 
val int_less_0_conv = thm "int_less_0_conv"; 

986 
val zero_less_int_conv = thm "zero_less_int_conv"; 

987 
val zle_int = thm "zle_int"; 

988 
val zero_zle_int = thm "zero_zle_int"; 

989 
val int_le_0_conv = thm "int_le_0_conv"; 

990 
val zle_refl = thm "zle_refl"; 

991 
val zle_linear = thm "zle_linear"; 

992 
val zle_trans = thm "zle_trans"; 

993 
val zle_anti_sym = thm "zle_anti_sym"; 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

994 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

995 
val Ints_def = thm "Ints_def"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

996 
val Nats_def = thm "Nats_def"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

997 

69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

998 
val of_nat_0 = thm "of_nat_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

999 
val of_nat_Suc = thm "of_nat_Suc"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1000 
val of_nat_1 = thm "of_nat_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1001 
val of_nat_add = thm "of_nat_add"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1002 
val of_nat_mult = thm "of_nat_mult"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1003 
val zero_le_imp_of_nat = thm "zero_le_imp_of_nat"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1004 
val less_imp_of_nat_less = thm "less_imp_of_nat_less"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1005 
val of_nat_less_imp_less = thm "of_nat_less_imp_less"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1006 
val of_nat_less_iff = thm "of_nat_less_iff"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1007 
val of_nat_le_iff = thm "of_nat_le_iff"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1008 
val of_nat_eq_iff = thm "of_nat_eq_iff"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1009 
val Nats_0 = thm "Nats_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1010 
val Nats_1 = thm "Nats_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1011 
val Nats_add = thm "Nats_add"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1012 
val Nats_mult = thm "Nats_mult"; 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

1013 
val int_eq_of_nat = thm"int_eq_of_nat"; 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1014 
val of_int = thm "of_int"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1015 
val of_int_0 = thm "of_int_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1016 
val of_int_1 = thm "of_int_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1017 
val of_int_add = thm "of_int_add"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1018 
val of_int_minus = thm "of_int_minus"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1019 
val of_int_diff = thm "of_int_diff"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1020 
val of_int_mult = thm "of_int_mult"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1021 
val of_int_le_iff = thm "of_int_le_iff"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1022 
val of_int_less_iff = thm "of_int_less_iff"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1023 
val of_int_eq_iff = thm "of_int_eq_iff"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1024 
val Ints_0 = thm "Ints_0"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1025 
val Ints_1 = thm "Ints_1"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1026 
val Ints_add = thm "Ints_add"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1027 
val Ints_minus = thm "Ints_minus"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1028 
val Ints_diff = thm "Ints_diff"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1029 
val Ints_mult = thm "Ints_mult"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1030 
val of_int_of_nat_eq = thm"of_int_of_nat_eq"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1031 
val Ints_cases = thm "Ints_cases"; 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14348
diff
changeset

1032 
val Ints_induct = thm "Ints_induct"; 
14259  1033 
*} 
1034 

5508  1035 
end 