author  paulson 
Thu, 15 Jul 1999 10:34:37 +0200  
changeset 7010  63120b6dca50 
parent 6991  500038b6063b 
child 7127  48e235179ffb 
permissions  rwrr 
5508  1 
(* Title: IntDef.ML 
2 
ID: $Id$ 

3 
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
The integers as equivalence classes over nat*nat. 

7 
*) 

8 

9 

10 
(*** Proving that intrel is an equivalence relation ***) 

11 

12 
val eqa::eqb::prems = goal Arith.thy 

13 
"[ (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 ] ==> \ 

14 
\ x1 + y3 = x3 + y1"; 

15 
by (res_inst_tac [("k1","x2")] (add_left_cancel RS iffD1) 1); 

16 
by (rtac (add_left_commute RS trans) 1); 

17 
by (stac eqb 1); 

18 
by (rtac (add_left_commute RS trans) 1); 

19 
by (stac eqa 1); 

20 
by (rtac (add_left_commute) 1); 

21 
qed "integ_trans_lemma"; 

22 

23 
(** Natural deduction for intrel **) 

24 

25 
Goalw [intrel_def] "[ x1+y2 = x2+y1] ==> ((x1,y1),(x2,y2)): intrel"; 

26 
by (Fast_tac 1); 

27 
qed "intrelI"; 

28 

29 
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*) 

30 
Goalw [intrel_def] 

31 
"p: intrel > (EX x1 y1 x2 y2. \ 

32 
\ p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)"; 

33 
by (Fast_tac 1); 

34 
qed "intrelE_lemma"; 

35 

36 
val [major,minor] = Goal 

37 
"[ p: intrel; \ 

38 
\ !!x1 y1 x2 y2. [ p = ((x1,y1),(x2,y2)); x1+y2 = x2+y1] ==> Q ] \ 

39 
\ ==> Q"; 

40 
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1); 

41 
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); 

42 
qed "intrelE"; 

43 

44 
AddSIs [intrelI]; 

45 
AddSEs [intrelE]; 

46 

47 
Goal "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)"; 

48 
by (Fast_tac 1); 

49 
qed "intrel_iff"; 

50 

51 
Goal "(x,x): intrel"; 

52 
by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1); 

53 
qed "intrel_refl"; 

54 

55 
Goalw [equiv_def, refl_def, sym_def, trans_def] 

56 
"equiv {x::(nat*nat).True} intrel"; 

57 
by (fast_tac (claset() addSIs [intrel_refl] 

58 
addSEs [sym, integ_trans_lemma]) 1); 

59 
qed "equiv_intrel"; 

60 

61 
val equiv_intrel_iff = 

62 
[TrueI, TrueI] MRS 

63 
([CollectI, CollectI] MRS 

64 
(equiv_intrel RS eq_equiv_class_iff)); 

65 

66 
Goalw [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ"; 

67 
by (Fast_tac 1); 

68 
qed "intrel_in_integ"; 

69 

70 
Goal "inj_on Abs_Integ Integ"; 

71 
by (rtac inj_on_inverseI 1); 

72 
by (etac Abs_Integ_inverse 1); 

73 
qed "inj_on_Abs_Integ"; 

74 

75 
Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff, 

76 
intrel_iff, intrel_in_integ, Abs_Integ_inverse]; 

77 

78 
Goal "inj(Rep_Integ)"; 

79 
by (rtac inj_inverseI 1); 

80 
by (rtac Rep_Integ_inverse 1); 

81 
qed "inj_Rep_Integ"; 

82 

83 

5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset

84 
(** int: the injection from "nat" to "int" **) 
5508  85 

5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset

86 
Goal "inj int"; 
5508  87 
by (rtac injI 1); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset

88 
by (rewtac int_def); 
5508  89 
by (dtac (inj_on_Abs_Integ RS inj_onD) 1); 
90 
by (REPEAT (rtac intrel_in_integ 1)); 

91 
by (dtac eq_equiv_class 1); 

92 
by (rtac equiv_intrel 1); 

93 
by (Fast_tac 1); 

94 
by Safe_tac; 

95 
by (Asm_full_simp_tac 1); 

6991  96 
qed "inj_int"; 
5508  97 

98 

99 
(**** zminus: unary negation on Integ ****) 

100 

101 
Goalw [congruent_def] 

102 
"congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)"; 

103 
by Safe_tac; 

104 
by (asm_simp_tac (simpset() addsimps add_ac) 1); 

105 
qed "zminus_congruent"; 

106 

107 

108 
(*Resolve th against the corresponding facts for zminus*) 

109 
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent]; 

110 

111 
Goalw [zminus_def] 

112 
" Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})"; 

113 
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); 

114 
by (simp_tac (simpset() addsimps 

115 
[intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1); 

116 
qed "zminus"; 

117 

118 
(*by lcp*) 

119 
val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P"; 

120 
by (res_inst_tac [("x1","z")] 

121 
(rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1); 

122 
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1); 

123 
by (res_inst_tac [("p","x")] PairE 1); 

124 
by (rtac prem 1); 

125 
by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1); 

126 
qed "eq_Abs_Integ"; 

127 

128 
Goal " ( z) = (z::int)"; 

129 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 

130 
by (asm_simp_tac (simpset() addsimps [zminus]) 1); 

131 
qed "zminus_zminus"; 

132 
Addsimps [zminus_zminus]; 

133 

5594  134 
Goal "inj(%z::int. z)"; 
5508  135 
by (rtac injI 1); 
136 
by (dres_inst_tac [("f","uminus")] arg_cong 1); 

137 
by (Asm_full_simp_tac 1); 

138 
qed "inj_zminus"; 

139 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

140 
Goalw [int_def] " (int 0) = int 0"; 
5508  141 
by (simp_tac (simpset() addsimps [zminus]) 1); 
6917  142 
qed "zminus_int0"; 
5508  143 

6917  144 
Addsimps [zminus_int0]; 
5508  145 

146 

5540  147 
(**** neg: the test for negative integers ****) 
5508  148 

149 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

150 
Goalw [neg_def, int_def] "~ neg(int n)"; 
5508  151 
by (Simp_tac 1); 
7010
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset

152 
qed "not_neg_int"; 
5508  153 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

154 
Goalw [neg_def, int_def] "neg( (int (Suc n)))"; 
5508  155 
by (simp_tac (simpset() addsimps [zminus]) 1); 
7010
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset

156 
qed "neg_zminus_int"; 
5508  157 

7010
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset

158 
Addsimps [neg_zminus_int, not_neg_int]; 
5508  159 

160 

161 
(**** zadd: addition on Integ ****) 

162 

163 
(** Congruence property for addition **) 

164 

165 
Goalw [congruent2_def] 

166 
"congruent2 intrel (%p1 p2. \ 

167 
\ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"; 

168 
(*Proof via congruent2_commuteI seems longer*) 

169 
by Safe_tac; 

5983  170 
by (Asm_simp_tac 1); 
5508  171 
qed "zadd_congruent2"; 
172 

173 
(*Resolve th against the corresponding facts for zadd*) 

174 
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; 

175 

176 
Goalw [zadd_def] 

177 
"Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \ 

178 
\ Abs_Integ(intrel^^{(x1+x2, y1+y2)})"; 

179 
by (asm_simp_tac 

180 
(simpset() addsimps [zadd_ize UN_equiv_class2]) 1); 

181 
qed "zadd"; 

182 

183 
Goal " (z + w) =  z +  (w::int)"; 

184 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 

185 
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); 

186 
by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1); 

187 
qed "zminus_zadd_distrib"; 

188 
Addsimps [zminus_zadd_distrib]; 

189 

190 
Goal "(z::int) + w = w + z"; 

191 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 

192 
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); 

5540  193 
by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1); 
5508  194 
qed "zadd_commute"; 
195 

196 
Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)"; 

197 
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); 

198 
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); 

199 
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); 

200 
by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1); 

201 
qed "zadd_assoc"; 

202 

203 
(*For AC rewriting*) 

204 
Goal "(x::int)+(y+z)=y+(x+z)"; 

205 
by (rtac (zadd_commute RS trans) 1); 

206 
by (rtac (zadd_assoc RS trans) 1); 

207 
by (rtac (zadd_commute RS arg_cong) 1); 

208 
qed "zadd_left_commute"; 

209 

210 
(*Integer addition is an AC operator*) 

211 
val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute]; 

212 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

213 
Goalw [int_def] "(int m) + (int n) = int (m + n)"; 
5508  214 
by (simp_tac (simpset() addsimps [zadd]) 1); 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

215 
qed "zadd_int"; 
5508  216 

5594  217 
Goal "(int m) + (int n + z) = int (m + n) + z"; 
218 
by (simp_tac (simpset() addsimps [zadd_int, zadd_assoc RS sym]) 1); 

219 
qed "zadd_int_left"; 

220 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

221 
Goal "int (Suc m) = int 1 + (int m)"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

222 
by (simp_tac (simpset() addsimps [zadd_int]) 1); 
6717
70b251dc7055
int_Suc>int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc
paulson
parents:
6674
diff
changeset

223 
qed "int_Suc_int_1"; 
5508  224 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

225 
Goalw [int_def] "int 0 + z = z"; 
5508  226 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 
227 
by (asm_simp_tac (simpset() addsimps [zadd]) 1); 

6917  228 
qed "zadd_int0"; 
5508  229 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

230 
Goal "z + int 0 = z"; 
5508  231 
by (rtac (zadd_commute RS trans) 1); 
6917  232 
by (rtac zadd_int0 1); 
233 
qed "zadd_int0_right"; 

5508  234 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

235 
Goalw [int_def] "z + ( z) = int 0"; 
5508  236 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 
237 
by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1); 

5594  238 
qed "zadd_zminus_inverse"; 
5508  239 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

240 
Goal "( z) + z = int 0"; 
5508  241 
by (rtac (zadd_commute RS trans) 1); 
5594  242 
by (rtac zadd_zminus_inverse 1); 
243 
qed "zadd_zminus_inverse2"; 

5508  244 

6917  245 
Addsimps [zadd_int0, zadd_int0_right, 
5594  246 
zadd_zminus_inverse, zadd_zminus_inverse2]; 
5508  247 

248 
Goal "z + ( z + w) = (w::int)"; 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

249 
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); 
5508  250 
qed "zadd_zminus_cancel"; 
251 

252 
Goal "(z) + (z + w) = (w::int)"; 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

253 
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); 
5508  254 
qed "zminus_zadd_cancel"; 
255 

256 
Addsimps [zadd_zminus_cancel, zminus_zadd_cancel]; 

257 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

258 
Goal "int 0  x = x"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

259 
by (simp_tac (simpset() addsimps [zdiff_def]) 1); 
6917  260 
qed "zdiff_int0"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

261 

a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

262 
Goal "x  int 0 = x"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

263 
by (simp_tac (simpset() addsimps [zdiff_def]) 1); 
6917  264 
qed "zdiff_int0_right"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

265 

5594  266 
Goal "x  x = int 0"; 
267 
by (simp_tac (simpset() addsimps [zdiff_def]) 1); 

268 
qed "zdiff_self"; 

269 

6917  270 
Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self]; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

271 

5508  272 

273 
(** Lemmas **) 

274 

275 
Goal "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"; 

276 
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); 

277 
qed "zadd_assoc_cong"; 

278 

279 
Goal "(z::int) + (v + w) = v + (z + w)"; 

280 
by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1)); 

281 
qed "zadd_assoc_swap"; 

282 

283 

284 
(*Need properties of subtraction? Or use $ just as an abbreviation!*) 

285 

286 
(**** zmult: multiplication on Integ ****) 

287 

288 
(** Congruence property for multiplication **) 

289 

290 
Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)"; 

291 
by (simp_tac (simpset() addsimps add_ac) 1); 

292 
qed "zmult_congruent_lemma"; 

293 

294 
Goal "congruent2 intrel (%p1 p2. \ 

295 
\ split (%x1 y1. split (%x2 y2. \ 

296 
\ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"; 

297 
by (rtac (equiv_intrel RS congruent2_commuteI) 1); 

298 
by (pair_tac "w" 2); 

299 
by (rename_tac "z1 z2" 2); 

300 
by Safe_tac; 

301 
by (rewtac split_def); 

302 
by (simp_tac (simpset() addsimps add_ac@mult_ac) 1); 

303 
by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff] 

304 
addsimps add_ac@mult_ac) 1); 

305 
by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1); 

306 
by (rtac (zmult_congruent_lemma RS trans) 1); 

307 
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); 

308 
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); 

309 
by (rtac (zmult_congruent_lemma RS trans RS sym) 1); 

310 
by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 1); 

311 
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1); 

312 
qed "zmult_congruent2"; 

313 

314 
(*Resolve th against the corresponding facts for zmult*) 

315 
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; 

316 

317 
Goalw [zmult_def] 

318 
"Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ 

319 
\ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; 

320 
by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1); 

321 
qed "zmult"; 

322 

323 
Goal "( z) * w =  (z * (w::int))"; 

324 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 

325 
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); 

5540  326 
by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1); 
5508  327 
qed "zmult_zminus"; 
328 

329 
Goal "(z::int) * w = w * z"; 

330 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 

331 
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); 

5540  332 
by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1); 
5508  333 
qed "zmult_commute"; 
334 

335 
Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)"; 

336 
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); 

337 
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); 

338 
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); 

5540  339 
by (asm_simp_tac (simpset() addsimps [add_mult_distrib2,zmult] @ 
340 
add_ac @ mult_ac) 1); 

5508  341 
qed "zmult_assoc"; 
342 

343 
(*For AC rewriting*) 

344 
Goal "(z1::int)*(z2*z3) = z2*(z1*z3)"; 

345 
by (rtac (zmult_commute RS trans) 1); 

346 
by (rtac (zmult_assoc RS trans) 1); 

347 
by (rtac (zmult_commute RS arg_cong) 1); 

348 
qed "zmult_left_commute"; 

349 

350 
(*Integer multiplication is an AC operator*) 

351 
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute]; 

352 

353 
Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"; 

354 
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); 

355 
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); 

356 
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); 

357 
by (asm_simp_tac 

5540  358 
(simpset() addsimps [add_mult_distrib2, zadd, zmult] @ 
359 
add_ac @ mult_ac) 1); 

5508  360 
qed "zadd_zmult_distrib"; 
361 

362 
val zmult_commute'= read_instantiate [("z","w")] zmult_commute; 

363 

364 
Goal "w * ( z) =  (w * (z::int))"; 

365 
by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1); 

366 
qed "zmult_zminus_right"; 

367 

368 
Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"; 

369 
by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1); 

370 
qed "zadd_zmult_distrib2"; 

371 

6839  372 
Goalw [zdiff_def] "((z1::int)  z2) * w = (z1 * w)  (z2 * w)"; 
373 
by (stac zadd_zmult_distrib 1); 

374 
by (simp_tac (simpset() addsimps [zmult_zminus]) 1); 

375 
qed "zdiff_zmult_distrib"; 

376 

377 
Goal "(w::int) * (z1  z2) = (w * z1)  (w * z2)"; 

378 
by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1); 

379 
qed "zdiff_zmult_distrib2"; 

380 

7010
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset

381 
Goalw [int_def] "(int m) * (int n) = int (m * n)"; 
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset

382 
by (simp_tac (simpset() addsimps [zmult]) 1); 
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset

383 
qed "zmult_int"; 
63120b6dca50
more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents:
6991
diff
changeset

384 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

385 
Goalw [int_def] "int 0 * z = int 0"; 
5508  386 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 
387 
by (asm_simp_tac (simpset() addsimps [zmult]) 1); 

6917  388 
qed "zmult_int0"; 
5508  389 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

390 
Goalw [int_def] "int 1 * z = z"; 
5508  391 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 
392 
by (asm_simp_tac (simpset() addsimps [zmult]) 1); 

6917  393 
qed "zmult_int1"; 
5508  394 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

395 
Goal "z * int 0 = int 0"; 
6917  396 
by (rtac ([zmult_commute, zmult_int0] MRS trans) 1); 
397 
qed "zmult_int0_right"; 

5508  398 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

399 
Goal "z * int 1 = z"; 
6917  400 
by (rtac ([zmult_commute, zmult_int1] MRS trans) 1); 
401 
qed "zmult_int1_right"; 

5508  402 

6917  403 
Addsimps [zmult_int0, zmult_int0_right, zmult_int1, zmult_int1_right]; 
5508  404 

405 

406 
(* Theorems about less and less_equal *) 

407 

408 
(*This lemma allows direct proofs of other <properties*) 

5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset

409 
Goalw [zless_def, neg_def, zdiff_def, int_def] 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

410 
"(w < z) = (EX n. z = w + int(Suc n))"; 
5508  411 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 
412 
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); 

413 
by (Clarify_tac 1); 

414 
by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1); 

415 
by (safe_tac (claset() addSDs [less_eq_Suc_add])); 

416 
by (res_inst_tac [("x","k")] exI 1); 

417 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac))); 

418 
qed "zless_iff_Suc_zadd"; 

419 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

420 
Goal "z < z + int (Suc n)"; 
5508  421 
by (auto_tac (claset(), 
422 
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

423 
zadd_int])); 
5508  424 
qed "zless_zadd_Suc"; 
425 

426 
Goal "[ z1<z2; z2<z3 ] ==> z1 < (z3::int)"; 

427 
by (auto_tac (claset(), 

428 
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

429 
zadd_int])); 
5508  430 
qed "zless_trans"; 
431 

432 
Goal "!!w::int. z<w ==> ~w<z"; 

433 
by (safe_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1])); 

434 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 

435 
by Safe_tac; 

5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset

436 
by (asm_full_simp_tac (simpset() addsimps [int_def, zadd]) 1); 
5508  437 
qed "zless_not_sym"; 
438 

439 
(* [ n<m; ~P ==> m<n ] ==> P *) 

5540  440 
bind_thm ("zless_asym", zless_not_sym RS swap); 
5508  441 

442 
Goal "!!z::int. ~ z<z"; 

443 
by (resolve_tac [zless_asym RS notI] 1); 

444 
by (REPEAT (assume_tac 1)); 

445 
qed "zless_not_refl"; 

446 

447 
(* z<z ==> R *) 

5594  448 
bind_thm ("zless_irrefl", zless_not_refl RS notE); 
5508  449 
AddSEs [zless_irrefl]; 
450 

451 
Goal "z<w ==> w ~= (z::int)"; 

452 
by (Blast_tac 1); 

453 
qed "zless_not_refl2"; 

454 

455 
(* s < t ==> s ~= t *) 

456 
bind_thm ("zless_not_refl3", zless_not_refl2 RS not_sym); 

457 

458 

459 
(*"Less than" is a linear ordering*) 

5540  460 
Goalw [zless_def, neg_def, zdiff_def] 
5508  461 
"z<w  z=w  w<(z::int)"; 
462 
by (res_inst_tac [("z","z")] eq_Abs_Integ 1); 

463 
by (res_inst_tac [("z","w")] eq_Abs_Integ 1); 

464 
by Safe_tac; 

465 
by (asm_full_simp_tac 

466 
(simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1); 

467 
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1); 

5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5594
diff
changeset

468 
by (ALLGOALS (force_tac (claset(), simpset() addsimps add_ac))); 
5508  469 
qed "zless_linear"; 
470 

471 
Goal "!!w::int. (w ~= z) = (w<z  z<w)"; 

472 
by (cut_facts_tac [zless_linear] 1); 

473 
by (Blast_tac 1); 

474 
qed "int_neq_iff"; 

475 

476 
(*** eliminates ~= in premises ***) 

477 
bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE); 

478 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

479 
Goal "(int m = int n) = (m = n)"; 
6991  480 
by (fast_tac (claset() addSEs [inj_int RS injD]) 1); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset

481 
qed "int_int_eq"; 
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5540
diff
changeset

482 
AddIffs [int_int_eq]; 
5508  483 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

484 
Goal "(int m < int n) = (m<n)"; 
5508  485 
by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

486 
zadd_int]) 1); 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

487 
qed "zless_int"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

488 
Addsimps [zless_int]; 
5508  489 

490 

491 
(*** Properties of <= ***) 

492 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

493 
Goalw [zle_def, le_def] "(int m <= int n) = (m<=n)"; 
5508  494 
by (Simp_tac 1); 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

495 
qed "zle_int"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

496 
Addsimps [zle_int]; 
5508  497 

498 
Goalw [zle_def] "z <= w ==> z < w  z=(w::int)"; 

499 
by (cut_facts_tac [zless_linear] 1); 

500 
by (blast_tac (claset() addEs [zless_asym]) 1); 

501 
qed "zle_imp_zless_or_eq"; 

502 

503 
Goalw [zle_def] "z<w  z=w ==> z <= (w::int)"; 

504 
by (cut_facts_tac [zless_linear] 1); 

505 
by (blast_tac (claset() addEs [zless_asym]) 1); 

506 
qed "zless_or_eq_imp_zle"; 

507 

508 
Goal "(x <= (y::int)) = (x < y  x=y)"; 

509 
by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1)); 

5540  510 
qed "integ_le_less"; 
5508  511 

512 
Goal "w <= (w::int)"; 

5540  513 
by (simp_tac (simpset() addsimps [integ_le_less]) 1); 
5508  514 
qed "zle_refl"; 
515 

516 
Goalw [zle_def] "z < w ==> z <= (w::int)"; 

517 
by (blast_tac (claset() addEs [zless_asym]) 1); 

518 
qed "zless_imp_zle"; 

519 

520 
(* Axiom 'linorder_linear' of class 'linorder': *) 

521 
Goal "(z::int) <= w  w <= z"; 

5540  522 
by (simp_tac (simpset() addsimps [integ_le_less]) 1); 
5508  523 
by (cut_facts_tac [zless_linear] 1); 
524 
by (Blast_tac 1); 

525 
qed "zle_linear"; 

526 

527 
Goal "[ i <= j; j < k ] ==> i < (k::int)"; 

528 
by (dtac zle_imp_zless_or_eq 1); 

529 
by (blast_tac (claset() addIs [zless_trans]) 1); 

530 
qed "zle_zless_trans"; 

531 

532 
Goal "[ i < j; j <= k ] ==> i < (k::int)"; 

533 
by (dtac zle_imp_zless_or_eq 1); 

534 
by (blast_tac (claset() addIs [zless_trans]) 1); 

535 
qed "zless_zle_trans"; 

536 

537 
Goal "[ i <= j; j <= k ] ==> i <= (k::int)"; 

538 
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, 

539 
rtac zless_or_eq_imp_zle, 

540 
blast_tac (claset() addIs [zless_trans])]); 

541 
qed "zle_trans"; 

542 

543 
Goal "[ z <= w; w <= z ] ==> z = (w::int)"; 

544 
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, 

545 
blast_tac (claset() addEs [zless_asym])]); 

546 
qed "zle_anti_sym"; 

547 

548 
(* Axiom 'order_less_le' of class 'order': *) 

549 
Goal "(w::int) < z = (w <= z & w ~= z)"; 

550 
by (simp_tac (simpset() addsimps [zle_def, int_neq_iff]) 1); 

551 
by (blast_tac (claset() addSEs [zless_asym]) 1); 

552 
qed "int_less_le"; 

553 

554 
(* [ w <= z; w ~= z ] ==> w < z *) 

555 
bind_thm ("zle_neq_implies_zless", [int_less_le, conjI] MRS iffD2); 

556 

557 

558 

559 
(*** Subtraction laws ***) 

560 

561 
Goal "x + (y  z) = (x + y)  (z::int)"; 

5540  562 
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); 
5508  563 
qed "zadd_zdiff_eq"; 
564 

565 
Goal "(x  y) + z = (x + z)  (y::int)"; 

5540  566 
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); 
5508  567 
qed "zdiff_zadd_eq"; 
568 

569 
Goal "(x  y)  z = x  (y + (z::int))"; 

5540  570 
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); 
5508  571 
qed "zdiff_zdiff_eq"; 
572 

573 
Goal "x  (y  z) = (x + z)  (y::int)"; 

5540  574 
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1); 
5508  575 
qed "zdiff_zdiff_eq2"; 
576 

577 
Goalw [zless_def, zdiff_def] "(xy < z) = (x < z + (y::int))"; 

578 
by (simp_tac (simpset() addsimps zadd_ac) 1); 

579 
qed "zdiff_zless_eq"; 

580 

581 
Goalw [zless_def, zdiff_def] "(x < zy) = (x + (y::int) < z)"; 

582 
by (simp_tac (simpset() addsimps zadd_ac) 1); 

583 
qed "zless_zdiff_eq"; 

584 

585 
Goalw [zle_def] "(xy <= z) = (x <= z + (y::int))"; 

586 
by (simp_tac (simpset() addsimps [zless_zdiff_eq]) 1); 

587 
qed "zdiff_zle_eq"; 

588 

589 
Goalw [zle_def] "(x <= zy) = (x + (y::int) <= z)"; 

590 
by (simp_tac (simpset() addsimps [zdiff_zless_eq]) 1); 

591 
qed "zle_zdiff_eq"; 

592 

593 
Goalw [zdiff_def] "(xy = z) = (x = z + (y::int))"; 

594 
by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); 

595 
qed "zdiff_eq_eq"; 

596 

597 
Goalw [zdiff_def] "(x = zy) = (x + (y::int) = z)"; 

598 
by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); 

599 
qed "eq_zdiff_eq"; 

600 

601 
(*This list of rewrites simplifies (in)equalities by bringing subtractions 

602 
to the top and then moving negative terms to the other side. 

603 
Use with zadd_ac*) 

604 
val zcompare_rls = 

605 
[symmetric zdiff_def, 

606 
zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 

607 
zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq, 

608 
zdiff_eq_eq, eq_zdiff_eq]; 

609 

610 

611 
(** Cancellation laws **) 

612 

613 
Goal "!!w::int. (z + w' = z + w) = (w' = w)"; 

614 
by Safe_tac; 

615 
by (dres_inst_tac [("f", "%x. x + z")] arg_cong 1); 

616 
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); 

617 
qed "zadd_left_cancel"; 

618 

619 
Addsimps [zadd_left_cancel]; 

620 

621 
Goal "!!z::int. (w' + z = w + z) = (w' = w)"; 

622 
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); 

623 
qed "zadd_right_cancel"; 

624 

625 
Addsimps [zadd_right_cancel]; 

626 

627 

5594  628 
(** For the cancellation simproc. 
629 
The idea is to cancel like terms on opposite sides by subtraction **) 

630 

631 
Goal "(x::int)  y = x'  y' ==> (x<y) = (x'<y')"; 

632 
by (asm_simp_tac (simpset() addsimps [zless_def]) 1); 

633 
qed "zless_eqI"; 

5508  634 

5594  635 
Goal "(x::int)  y = x'  y' ==> (y<=x) = (y'<=x')"; 
636 
by (dtac zless_eqI 1); 

637 
by (asm_simp_tac (simpset() addsimps [zle_def]) 1); 

638 
qed "zle_eqI"; 

5508  639 

5594  640 
Goal "(x::int)  y = x'  y' ==> (x=y) = (x'=y')"; 
641 
by Safe_tac; 

642 
by (ALLGOALS 

643 
(asm_full_simp_tac (simpset() addsimps [eq_zdiff_eq, zdiff_eq_eq]))); 

644 
qed "zeq_eqI"; 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

645 