author  paulson 
Tue, 13 Jul 1999 10:43:31 +0200  
changeset 6989  dd3e8bd86cc6 
parent 6973  52f70b76a8b5 
child 6997  1833bdd83ebf 
permissions  rwrr 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

1 
(* Title: HOL/Integ/Bin.ML 
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

2 
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory 
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

3 
David Spelt, University of Twente 
6060  4 
Tobias Nipkow, Technical University Munich 
1632  5 
Copyright 1994 University of Cambridge 
6060  6 
Copyright 1996 University of Twente 
7 
Copyright 1999 TU Munich 

1632  8 

6060  9 
Arithmetic on binary integers; 
10 
decision procedure for linear arithmetic. 

1632  11 
*) 
12 

13 
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) 

14 

6910  15 
qed_goal "NCons_Pls_0" thy 
5512  16 
"NCons Pls False = Pls" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

17 
(fn _ => [(Simp_tac 1)]); 
1632  18 

6910  19 
qed_goal "NCons_Pls_1" thy 
5512  20 
"NCons Pls True = Pls BIT True" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

21 
(fn _ => [(Simp_tac 1)]); 
1632  22 

6910  23 
qed_goal "NCons_Min_0" thy 
5512  24 
"NCons Min False = Min BIT False" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

25 
(fn _ => [(Simp_tac 1)]); 
1632  26 

6910  27 
qed_goal "NCons_Min_1" thy 
5512  28 
"NCons Min True = Min" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

29 
(fn _ => [(Simp_tac 1)]); 
1632  30 

6910  31 
qed_goal "bin_succ_1" thy 
5512  32 
"bin_succ(w BIT True) = (bin_succ w) BIT False" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

33 
(fn _ => [(Simp_tac 1)]); 
1632  34 

6910  35 
qed_goal "bin_succ_0" thy 
5512  36 
"bin_succ(w BIT False) = NCons w True" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

37 
(fn _ => [(Simp_tac 1)]); 
1632  38 

6910  39 
qed_goal "bin_pred_1" thy 
5512  40 
"bin_pred(w BIT True) = NCons w False" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

41 
(fn _ => [(Simp_tac 1)]); 
1632  42 

6910  43 
qed_goal "bin_pred_0" thy 
5512  44 
"bin_pred(w BIT False) = (bin_pred w) BIT True" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

45 
(fn _ => [(Simp_tac 1)]); 
1632  46 

6910  47 
qed_goal "bin_minus_1" thy 
5512  48 
"bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

49 
(fn _ => [(Simp_tac 1)]); 
1632  50 

6910  51 
qed_goal "bin_minus_0" thy 
5512  52 
"bin_minus(w BIT False) = (bin_minus w) BIT False" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

53 
(fn _ => [(Simp_tac 1)]); 
1632  54 

5491  55 

1632  56 
(*** bin_add: binary addition ***) 
57 

6910  58 
qed_goal "bin_add_BIT_11" thy 
5512  59 
"bin_add (v BIT True) (w BIT True) = \ 
60 
\ NCons (bin_add v (bin_succ w)) False" 

2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

61 
(fn _ => [(Simp_tac 1)]); 
1632  62 

6910  63 
qed_goal "bin_add_BIT_10" thy 
5512  64 
"bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

65 
(fn _ => [(Simp_tac 1)]); 
1632  66 

6910  67 
qed_goal "bin_add_BIT_0" thy 
5512  68 
"bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y" 
5491  69 
(fn _ => [Auto_tac]); 
1632  70 

5551  71 
Goal "bin_add w Pls = w"; 
72 
by (induct_tac "w" 1); 

73 
by Auto_tac; 

74 
qed "bin_add_Pls_right"; 

1632  75 

6910  76 
qed_goal "bin_add_BIT_Min" thy 
5512  77 
"bin_add (v BIT x) Min = bin_pred (v BIT x)" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

78 
(fn _ => [(Simp_tac 1)]); 
1632  79 

6910  80 
qed_goal "bin_add_BIT_BIT" thy 
5512  81 
"bin_add (v BIT x) (w BIT y) = \ 
82 
\ NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)" 

2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

83 
(fn _ => [(Simp_tac 1)]); 
1632  84 

85 

6036  86 
(*** bin_mult: binary multiplication ***) 
1632  87 

6910  88 
qed_goal "bin_mult_1" thy 
5512  89 
"bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

90 
(fn _ => [(Simp_tac 1)]); 
1632  91 

6910  92 
qed_goal "bin_mult_0" thy 
5512  93 
"bin_mult (v BIT False) w = NCons (bin_mult v w) False" 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

94 
(fn _ => [(Simp_tac 1)]); 
1632  95 

96 

97 
(**** The carry/borrow functions, bin_succ and bin_pred ****) 

98 

99 

6910  100 
(**** number_of ****) 
1632  101 

6910  102 
qed_goal "number_of_NCons" thy 
103 
"number_of(NCons w b) = (number_of(w BIT b)::int)" 

5184  104 
(fn _ =>[(induct_tac "w" 1), 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

105 
(ALLGOALS Asm_simp_tac) ]); 
1632  106 

6910  107 
Addsimps [number_of_NCons]; 
1632  108 

6910  109 
qed_goal "number_of_succ" thy 
110 
"number_of(bin_succ w) = int 1 + number_of w" 

111 
(fn _ =>[induct_tac "w" 1, 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

112 
(ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]); 
5491  113 

6910  114 
qed_goal "number_of_pred" thy 
115 
"number_of(bin_pred w) =  (int 1) + number_of w" 

116 
(fn _ =>[induct_tac "w" 1, 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

117 
(ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]); 
1632  118 

6910  119 
Goal "number_of(bin_minus w) = ( (number_of w)::int)"; 
120 
by (induct_tac "w" 1); 

5491  121 
by (Simp_tac 1); 
122 
by (Simp_tac 1); 

123 
by (asm_simp_tac (simpset() 

5551  124 
delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT] 
6910  125 
addsimps [number_of_succ,number_of_pred, 
5491  126 
zadd_assoc]) 1); 
6910  127 
qed "number_of_minus"; 
1632  128 

129 

6910  130 
val bin_add_simps = [bin_add_BIT_BIT, number_of_succ, number_of_pred]; 
1632  131 

6036  132 
(*This proof is complicated by the mutual recursion*) 
6910  133 
Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)"; 
5184  134 
by (induct_tac "v" 1); 
4686  135 
by (simp_tac (simpset() addsimps bin_add_simps) 1); 
136 
by (simp_tac (simpset() addsimps bin_add_simps) 1); 

1632  137 
by (rtac allI 1); 
5184  138 
by (induct_tac "w" 1); 
5540  139 
by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac))); 
6910  140 
qed_spec_mp "number_of_add"; 
1632  141 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

142 

5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

143 
(*Subtraction*) 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

144 
Goalw [zdiff_def] 
6910  145 
"number_of v  number_of w = (number_of(bin_add v (bin_minus w))::int)"; 
146 
by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1); 

147 
qed "diff_number_of_eq"; 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

148 

6910  149 
val bin_mult_simps = [zmult_zminus, number_of_minus, number_of_add]; 
1632  150 

6910  151 
Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)"; 
5184  152 
by (induct_tac "v" 1); 
4686  153 
by (simp_tac (simpset() addsimps bin_mult_simps) 1); 
154 
by (simp_tac (simpset() addsimps bin_mult_simps) 1); 

5491  155 
by (asm_simp_tac 
5540  156 
(simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1); 
6910  157 
qed "number_of_mult"; 
5491  158 

1632  159 

6941  160 
(*The correctness of shifting. But it doesn't seem to give a measurable 
161 
speedup.*) 

162 
Goal "(#2::int) * number_of w = number_of (w BIT False)"; 

163 
by (induct_tac "w" 1); 

164 
by (ALLGOALS (asm_simp_tac 

165 
(simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac))); 

166 
qed "double_number_of_BIT"; 

167 

168 

5491  169 
(** Simplification rules with integer constants **) 
170 

6910  171 
Goal "#0 + z = (z::int)"; 
5491  172 
by (Simp_tac 1); 
173 
qed "zadd_0"; 

174 

6910  175 
Goal "z + #0 = (z::int)"; 
5491  176 
by (Simp_tac 1); 
177 
qed "zadd_0_right"; 

178 

5592  179 
Addsimps [zadd_0, zadd_0_right]; 
180 

181 

182 
(** Converting simple cases of (int n) to numerals **) 

5491  183 

5592  184 
(*int 0 = #0 *) 
6910  185 
bind_thm ("int_0", number_of_Pls RS sym); 
5491  186 

5592  187 
Goal "int (Suc n) = #1 + int n"; 
188 
by (simp_tac (simpset() addsimps [zadd_int]) 1); 

189 
qed "int_Suc"; 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

190 

6910  191 
Goal " (#0) = (#0::int)"; 
5491  192 
by (Simp_tac 1); 
193 
qed "zminus_0"; 

194 

195 
Addsimps [zminus_0]; 

196 

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

197 

6910  198 
Goal "(#0::int)  x = x"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

199 
by (simp_tac (simpset() addsimps [zdiff_def]) 1); 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

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

201 

6910  202 
Goal "x  (#0::int) = x"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

203 
by (simp_tac (simpset() addsimps [zdiff_def]) 1); 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

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

205 

6910  206 
Goal "x  x = (#0::int)"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

207 
by (simp_tac (simpset() addsimps [zdiff_def]) 1); 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

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

209 

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

210 
Addsimps [zdiff0, zdiff0_right, zdiff_self]; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

211 

6917  212 

213 
(** Special simplification, for constants only **) 

6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

214 

6917  215 
fun inst x t = read_instantiate_sg (sign_of Bin.thy) [(x,t)]; 
216 

217 
(*Distributive laws*) 

218 
Addsimps (map (inst "w" "number_of ?v") 

6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

219 
[zadd_zmult_distrib, zadd_zmult_distrib2, 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

220 
zdiff_zmult_distrib, zdiff_zmult_distrib2]); 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

221 

6917  222 
Addsimps (map (inst "x" "number_of ?v") 
223 
[zless_zminus, zle_zminus, equation_zminus]); 

224 
Addsimps (map (inst "y" "number_of ?v") 

225 
[zminus_zless, zminus_zle, zminus_equation]); 

226 

227 

6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

228 
(** Specialcase simplification for small constants **) 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

229 

6910  230 
Goal "#0 * z = (#0::int)"; 
5491  231 
by (Simp_tac 1); 
232 
qed "zmult_0"; 

233 

6910  234 
Goal "z * #0 = (#0::int)"; 
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

235 
by (Simp_tac 1); 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

236 
qed "zmult_0_right"; 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

237 

6910  238 
Goal "#1 * z = (z::int)"; 
5491  239 
by (Simp_tac 1); 
240 
qed "zmult_1"; 

241 

6910  242 
Goal "z * #1 = (z::int)"; 
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

243 
by (Simp_tac 1); 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

244 
qed "zmult_1_right"; 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

245 

6917  246 
Goal "#1 * z = (z::int)"; 
247 
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1); 

248 
qed "zmult_minus1"; 

249 

250 
Goal "z * #1 = (z::int)"; 

251 
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1); 

252 
qed "zmult_minus1_right"; 

253 

254 
Addsimps [zmult_0, zmult_0_right, 

255 
zmult_1, zmult_1_right, 

256 
zmult_minus1, zmult_minus1_right]; 

257 

258 
(*For specialist use: NOT as default simprules*) 

6910  259 
Goal "#2 * z = (z+z::int)"; 
5491  260 
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); 
261 
qed "zmult_2"; 

262 

6910  263 
Goal "z * #2 = (z+z::int)"; 
5491  264 
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); 
265 
qed "zmult_2_right"; 

266 

6917  267 

268 
(** Inequality reasoning **) 

5491  269 

6989  270 
Goal "(m*n = (#0::int)) = (m = #0  n = #0)"; 
271 
by (stac (int_0 RS sym) 1 THEN rtac zmult_eq_int0_iff 1); 

272 
qed "zmult_eq_0_iff"; 

273 

6910  274 
Goal "(w < z + (#1::int)) = (w<z  w=z)"; 
5592  275 
by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1); 
5491  276 
qed "zless_add1_eq"; 
277 

6910  278 
Goal "(w + (#1::int) <= z) = (w<z)"; 
5592  279 
by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1); 
5491  280 
qed "add1_zle_eq"; 
281 
Addsimps [add1_zle_eq]; 

282 

5540  283 
Goal "neg x = (x < #0)"; 
6917  284 
by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); 
5540  285 
qed "neg_eq_less_0"; 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

286 

6989  287 
Goal "(~neg x) = (#0 <= x)"; 
6917  288 
by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1); 
5540  289 
qed "not_neg_eq_ge_0"; 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

290 

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

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

292 
by (Simp_tac 1); 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

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

294 
AddIffs [zero_zle_int]; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

295 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

296 

5747  297 
(** Needed because (int 0) rewrites to #0. 
298 
Can these be generalized without evaluating large numbers?**) 

299 

300 
Goal "~ (int k < #0)"; 

301 
by (Simp_tac 1); 

302 
qed "int_less_0_conv"; 

303 

304 
Goal "(int k <= #0) = (k=0)"; 

305 
by (Simp_tac 1); 

306 
qed "int_le_0_conv"; 

307 

308 
Goal "(int k = #0) = (k=0)"; 

309 
by (Simp_tac 1); 

310 
qed "int_eq_0_conv"; 

311 

312 
Goal "(#0 = int k) = (k=0)"; 

313 
by Auto_tac; 

314 
qed "int_eq_0_conv'"; 

315 

316 
Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv']; 

317 

318 

5491  319 
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) 
320 

321 
(** Equals (=) **) 

1632  322 

5491  323 
Goalw [iszero_def] 
6910  324 
"((number_of x::int) = number_of y) = iszero(number_of (bin_add x (bin_minus y)))"; 
5491  325 
by (simp_tac (simpset() addsimps 
6910  326 
(zcompare_rls @ [number_of_add, number_of_minus])) 1); 
327 
qed "eq_number_of_eq"; 

5491  328 

6910  329 
Goalw [iszero_def] "iszero ((number_of Pls)::int)"; 
5491  330 
by (Simp_tac 1); 
6910  331 
qed "iszero_number_of_Pls"; 
5491  332 

6910  333 
Goalw [iszero_def] "~ iszero ((number_of Min)::int)"; 
5491  334 
by (Simp_tac 1); 
6910  335 
qed "nonzero_number_of_Min"; 
5491  336 

337 
Goalw [iszero_def] 

6910  338 
"iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; 
5491  339 
by (Simp_tac 1); 
6910  340 
by (int_case_tac "number_of w" 1); 
5491  341 
by (ALLGOALS (asm_simp_tac 
5540  342 
(simpset() addsimps zcompare_rls @ 
343 
[zminus_zadd_distrib RS sym, 

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

344 
zadd_int]))); 
6910  345 
qed "iszero_number_of_BIT"; 
5491  346 

6910  347 
Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)"; 
348 
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 

349 
qed "iszero_number_of_0"; 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

350 

6910  351 
Goal "~ iszero (number_of (w BIT True)::int)"; 
352 
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 

353 
qed "iszero_number_of_1"; 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

354 

5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

355 

5491  356 

357 
(** Lessthan (<) **) 

358 

359 
Goalw [zless_def,zdiff_def] 

6910  360 
"(number_of x::int) < number_of y \ 
361 
\ = neg (number_of (bin_add x (bin_minus y)))"; 

5491  362 
by (simp_tac (simpset() addsimps bin_mult_simps) 1); 
6910  363 
qed "less_number_of_eq_neg"; 
5491  364 

6910  365 
Goal "~ neg (number_of Pls)"; 
5491  366 
by (Simp_tac 1); 
6910  367 
qed "not_neg_number_of_Pls"; 
5491  368 

6910  369 
Goal "neg (number_of Min)"; 
5491  370 
by (Simp_tac 1); 
6910  371 
qed "neg_number_of_Min"; 
5491  372 

6910  373 
Goal "neg (number_of (w BIT x)) = neg (number_of w)"; 
5491  374 
by (Asm_simp_tac 1); 
6910  375 
by (int_case_tac "number_of w" 1); 
5491  376 
by (ALLGOALS (asm_simp_tac 
6917  377 
(simpset() addsimps [zadd_int, neg_eq_less_int0, 
5540  378 
symmetric zdiff_def] @ zcompare_rls))); 
6910  379 
qed "neg_number_of_BIT"; 
5491  380 

381 

382 
(** Lessthanorequals (<=) **) 

383 

6910  384 
Goal "(number_of x <= (number_of y::int)) = (~ number_of y < (number_of x::int))"; 
5491  385 
by (simp_tac (simpset() addsimps [zle_def]) 1); 
6910  386 
qed "le_number_of_eq_not_less"; 
5491  387 

5540  388 
(*Delete the original rewrites, with their clumsy conditional expressions*) 
5551  389 
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
390 
NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT]; 

5491  391 

392 
(*Hide the binary representation of integer constants*) 

6910  393 
Delsimps [number_of_Pls, number_of_Min, number_of_BIT]; 
5491  394 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

395 
(*simplification of arithmetic operations on integer constants*) 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

396 
val bin_arith_extra_simps = 
6910  397 
[number_of_add RS sym, 
398 
number_of_minus RS sym, 

399 
number_of_mult RS sym, 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

400 
bin_succ_1, bin_succ_0, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

401 
bin_pred_1, bin_pred_0, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

402 
bin_minus_1, bin_minus_0, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

403 
bin_add_Pls_right, bin_add_BIT_Min, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

404 
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11, 
6910  405 
diff_number_of_eq, 
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

406 
bin_mult_1, bin_mult_0, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

407 
NCons_Pls_0, NCons_Pls_1, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

408 
NCons_Min_0, NCons_Min_1, NCons_BIT]; 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

409 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

410 
(*For making a minimal simpset, one must include these default simprules 
6910  411 
of thy. Also include simp_thms, or at least (~False)=True*) 
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

412 
val bin_arith_simps = 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

413 
[bin_pred_Pls, bin_pred_Min, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

414 
bin_succ_Pls, bin_succ_Min, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

415 
bin_add_Pls, bin_add_Min, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

416 
bin_minus_Pls, bin_minus_Min, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

417 
bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps; 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

418 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

419 
(*Simplification of relational operations*) 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

420 
val bin_rel_simps = 
6910  421 
[eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min, 
422 
iszero_number_of_0, iszero_number_of_1, 

423 
less_number_of_eq_neg, 

424 
not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT, 

425 
le_number_of_eq_not_less]; 

2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

426 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

427 
Addsimps bin_arith_extra_simps; 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

428 
Addsimps bin_rel_simps; 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

429 

6060  430 
(**) 
431 
(* Linear arithmetic *) 

432 
(**) 

433 

434 
(* 

435 
Instantiation of the generic linear arithmetic package for int. 

436 
FIXME: multiplication with constants (eg #2 * i) does not work yet. 

437 
Solution: the cancellation simprocs in Int_Cancel should be able to deal with 

438 
it (eg simplify #3 * i <= 2 * i to i <= #0) or `add_rules' below should 

439 
include rules for turning multiplication with constants into addition. 

440 
(The latter option is very inefficient!) 

441 
*) 

442 

6128  443 
structure Int_LA_Data(*: LIN_ARITH_DATA*) = 
6060  444 
struct 
6101  445 

6128  446 
val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2]; 
6060  447 

448 
fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i) 

449 
 Some n => (overwrite(p,(t,n+m:int)), i)); 

450 

451 
(* Turn term into list of summand * multiplicity plus a constant *) 

452 
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) 

453 
 poly(Const("op ",_) $ s $ t, m, pi) = poly(s,m,poly(t,~1*m,pi)) 

454 
 poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi) 

6910  455 
 poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi) = 
456 
(poly(t,m*NumeralSyntax.dest_bin c,pi) handle Match => add_atom(all,m,pi)) 

457 
 poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) = 

458 
((p,i + m*NumeralSyntax.dest_bin t) handle Match => add_atom(all,m,(p,i))) 

6060  459 
 poly x = add_atom x; 
460 

6128  461 
fun decomp2(rel,lhs,rhs) = 
6060  462 
let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0)) 
463 
in case rel of 

464 
"op <" => Some(p,i,"<",q,j) 

465 
 "op <=" => Some(p,i,"<=",q,j) 

466 
 "op =" => Some(p,i,"=",q,j) 

467 
 _ => None 

468 
end; 

469 

6128  470 
val intT = Type("IntDef.int",[]); 
471 
fun iib T = T = ([intT,intT] > HOLogic.boolT); 

6060  472 

6128  473 
fun decomp1(T,xxx) = 
474 
if iib T then decomp2 xxx else Nat_LA_Data.decomp1(T,xxx); 

475 

476 
fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs)) 

6060  477 
 decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = 
6128  478 
Nat_LA_Data.negate(decomp1(T,(rel,lhs,rhs))) 
6060  479 
 decomp _ = None 
480 

481 
(* reduce contradictory <= to False *) 

482 
val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0]; 

483 

6128  484 
val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules 
6060  485 
addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; 
486 

487 
val simp = simplify cancel_sums_ss; 

488 

6128  489 
val add_mono_thms = Nat_LA_Data.add_mono_thms @ 
490 
map (fn s => prove_goal Int.thy s 

491 
(fn prems => [cut_facts_tac prems 1, 

492 
asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) 

493 
["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", 

494 
"(i = j) & (k <= l) ==> i + k <= j + (l::int)", 

495 
"(i <= j) & (k = l) ==> i + k <= j + (l::int)", 

496 
"(i = j) & (k = l) ==> i + k = j + (l::int)" 

497 
]; 

6060  498 

499 
end; 

500 

6128  501 
(* Update parameters of arithmetic prover *) 
502 
LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms; 

503 
LA_Data_Ref.lessD := Int_LA_Data.lessD; 

504 
LA_Data_Ref.decomp := Int_LA_Data.decomp; 

505 
LA_Data_Ref.simp := Int_LA_Data.simp; 

506 

6060  507 

6128  508 
val int_arith_simproc_pats = 
6394  509 
map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT)) 
6128  510 
["(m::int) < n","(m::int) <= n", "(m::int) = n"]; 
6060  511 

6128  512 
val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats 
513 
Fast_Arith.lin_arith_prover; 

514 

515 
Addsimprocs [fast_int_arith_simproc]; 

6060  516 

517 
(* FIXME: K true should be replaced by a sensible test to speed things up 

518 
in case there are lots of irrelevant terms involved. 

6157  519 

6128  520 
val arith_tac = 
521 
refute_tac (K true) (REPEAT o split_tac[nat_diff_split]) 

522 
((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac); 

6157  523 
*) 
6060  524 

525 
(* Some test data 

526 
Goal "!!a::int. [ a <= b; c <= d; x+y<z ] ==> a+c <= b+d"; 

6301  527 
by (fast_arith_tac 1); 
6060  528 
Goal "!!a::int. [ a < b; c < d ] ==> ad+ #2 <= b+(c)"; 
6301  529 
by (fast_arith_tac 1); 
6060  530 
Goal "!!a::int. [ a < b; c < d ] ==> a+c+ #1 < b+d"; 
6301  531 
by (fast_arith_tac 1); 
6060  532 
Goal "!!a::int. [ a <= b; b+b <= c ] ==> a+a <= c"; 
6301  533 
by (fast_arith_tac 1); 
6060  534 
Goal "!!a::int. [ a+b <= i+j; a<=b; i<=j ] \ 
535 
\ ==> a+a <= j+j"; 

6301  536 
by (fast_arith_tac 1); 
6060  537 
Goal "!!a::int. [ a+b < i+j; a<b; i<j ] \ 
538 
\ ==> a+a   #1 < j+j  #3"; 

6301  539 
by (fast_arith_tac 1); 
6060  540 
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k > a+a+a <= k+k+k"; 
6301  541 
by (arith_tac 1); 
6060  542 
Goal "!!a::int. [ a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l ] \ 
543 
\ ==> a <= l"; 

6301  544 
by (fast_arith_tac 1); 
6060  545 
Goal "!!a::int. [ a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l ] \ 
546 
\ ==> a+a+a+a <= l+l+l+l"; 

6301  547 
by (fast_arith_tac 1); 
6060  548 
Goal "!!a::int. [ a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l ] \ 
549 
\ ==> a+a+a+a+a <= l+l+l+l+i"; 

6301  550 
by (fast_arith_tac 1); 
6060  551 
Goal "!!a::int. [ a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l ] \ 
552 
\ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; 

6301  553 
by (fast_arith_tac 1); 
6060  554 
*) 
555 

556 
(**) 

557 
(* End of linear arithmetic *) 

558 
(**) 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

559 

5592  560 
(** Simplification of arithmetic when nested to the right **) 
561 

6910  562 
Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)"; 
5592  563 
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); 
6910  564 
qed "add_number_of_left"; 
5592  565 

6910  566 
Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)"; 
5592  567 
by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1); 
6910  568 
qed "mult_number_of_left"; 
5592  569 

6910  570 
Addsimps [add_number_of_left, mult_number_of_left]; 
5592  571 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

572 
(** Simplification of inequalities involving numerical constants **) 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

573 

6910  574 
Goal "(w <= z + (#1::int)) = (w<=z  w = z + (#1::int))"; 
6301  575 
by (arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

576 
qed "zle_add1_eq"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

577 

6910  578 
Goal "(w <= z  (#1::int)) = (w<(z::int))"; 
6301  579 
by (arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

580 
qed "zle_diff1_eq"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

581 
Addsimps [zle_diff1_eq]; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

582 

ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

583 
(*2nd premise can be proved automatically if v is a literal*) 
6910  584 
Goal "[ w <= z; #0 <= v ] ==> w <= z + (v::int)"; 
6301  585 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

586 
qed "zle_imp_zle_zadd"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

587 

6910  588 
Goal "w <= z ==> w <= z + (#1::int)"; 
6301  589 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

590 
qed "zle_imp_zle_zadd1"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

591 

ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

592 
(*2nd premise can be proved automatically if v is a literal*) 
6910  593 
Goal "[ w < z; #0 <= v ] ==> w < z + (v::int)"; 
6301  594 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

595 
qed "zless_imp_zless_zadd"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

596 

6910  597 
Goal "w < z ==> w < z + (#1::int)"; 
6301  598 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

599 
qed "zless_imp_zless_zadd1"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

600 

6910  601 
Goal "(w < z + #1) = (w<=(z::int))"; 
6301  602 
by (arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

603 
qed "zle_add1_eq_le"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

604 
Addsimps [zle_add1_eq_le]; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

605 

6910  606 
Goal "(z = z + w) = (w = (#0::int))"; 
6301  607 
by (arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

608 
qed "zadd_left_cancel0"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

609 
Addsimps [zadd_left_cancel0]; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

610 

ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

611 
(*LOOPS as a simprule!*) 
6910  612 
Goal "[ w + v < z; #0 <= v ] ==> w < (z::int)"; 
6301  613 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

614 
qed "zless_zadd_imp_zless"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

615 

5540  616 
(*LOOPS as a simprule! Analogous to Suc_lessD*) 
6910  617 
Goal "w + #1 < z ==> w < (z::int)"; 
6301  618 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

619 
qed "zless_zadd1_imp_zless"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

620 

6910  621 
Goal "w + #1 = w  (#1::int)"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

622 
by (Simp_tac 1); 
5551  623 
qed "zplus_minus1_conv"; 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

624 

5551  625 

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

626 
(*** nat ***) 
5551  627 

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

628 
Goal "#0 <= z ==> int (nat z) = z"; 
5551  629 
by (asm_full_simp_tac 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

630 
(simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

631 
qed "nat_0_le"; 
5551  632 

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

633 
Goal "z < #0 ==> nat z = 0"; 
5551  634 
by (asm_full_simp_tac 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

635 
(simpset() addsimps [neg_eq_less_0, zle_def, neg_nat]) 1); 
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

636 
qed "nat_less_0"; 
5551  637 

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

638 
Addsimps [nat_0_le, nat_less_0]; 
5551  639 

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

640 
Goal "#0 <= w ==> (nat w = m) = (w = int m)"; 
5551  641 
by Auto_tac; 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

642 
qed "nat_eq_iff"; 
5551  643 

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

644 
Goal "#0 <= w ==> (nat w < m) = (w < int m)"; 
5551  645 
by (rtac iffI 1); 
646 
by (asm_full_simp_tac 

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

647 
(simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

648 
by (etac (nat_0_le RS subst) 1); 
5551  649 
by (Simp_tac 1); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

650 
qed "nat_less_iff"; 
5551  651 

5747  652 

6716
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

653 
(*Users don't want to see (int 0), int(Suc 0) or w +  z*) 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

654 
Addsimps [int_0, int_Suc, symmetric zdiff_def]; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

655 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

656 
Goal "nat #0 = 0"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

657 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

658 
qed "nat_0"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

659 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

660 
Goal "nat #1 = 1"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

661 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

662 
qed "nat_1"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

663 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

664 
Goal "nat #2 = 2"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

665 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

666 
qed "nat_2"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

667 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

668 
Goal "nat #3 = Suc 2"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

669 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

670 
qed "nat_3"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

671 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

672 
Goal "nat #4 = Suc (Suc 2)"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

673 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

674 
qed "nat_4"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

675 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

676 
Goal "nat #5 = Suc (Suc (Suc 2))"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

677 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

678 
qed "nat_5"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

679 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

680 
Goal "nat #6 = Suc (Suc (Suc (Suc 2)))"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

681 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

682 
qed "nat_6"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

683 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

684 
Goal "nat #7 = Suc (Suc (Suc (Suc (Suc 2))))"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

685 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

686 
qed "nat_7"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

687 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

688 
Goal "nat #8 = Suc (Suc (Suc (Suc (Suc (Suc 2)))))"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

689 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

690 
qed "nat_8"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

691 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

692 
Goal "nat #9 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 2))))))"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

693 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

694 
qed "nat_9"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

695 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

696 
(*Users also don't want to see (nat 0), (nat 1), ...*) 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

697 
Addsimps [nat_0, nat_1, nat_2, nat_3, nat_4, 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

698 
nat_5, nat_6, nat_7, nat_8, nat_9]; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

699 

5747  700 

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

701 
Goal "#0 <= w ==> (nat w < nat z) = (w<z)"; 
5551  702 
by (case_tac "neg z" 1); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

703 
by (auto_tac (claset(), simpset() addsimps [nat_less_iff])); 
5551  704 
by (auto_tac (claset() addIs [zless_trans], 
5747  705 
simpset() addsimps [neg_eq_less_0, zle_def])); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

706 
qed "nat_less_eq_zless"; 
5747  707 

6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

708 

6917  709 
(*Towards canonical simplification*) 
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

710 
Addsimps zadd_ac; 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

711 
Addsimps zmult_ac; 
6917  712 
Addsimps [zmult_zminus, zmult_zminus_right]; 
6941  713 

714 

715 

716 
(** Products of signs **) 

717 

718 
Goal "(m::int) < #0 ==> (#0 < m*n) = (n < #0)"; 

719 
by Auto_tac; 

720 
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2); 

721 
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1); 

722 
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 

723 
by (force_tac (claset() addDs [zmult_zless_mono1_neg], 

724 
simpset() addsimps [order_le_less]) 1); 

725 
qed "neg_imp_zmult_pos_iff"; 

726 

727 
Goal "(m::int) < #0 ==> (m*n < #0) = (#0 < n)"; 

728 
by Auto_tac; 

729 
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2); 

730 
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1); 

731 
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 

732 
by (force_tac (claset() addDs [zmult_zless_mono1_neg], 

733 
simpset() addsimps [order_le_less]) 1); 

734 
qed "neg_imp_zmult_neg_iff"; 

735 

736 
Goal "#0 < (m::int) ==> (m*n < #0) = (n < #0)"; 

737 
by Auto_tac; 

738 
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2); 

739 
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1); 

740 
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 

741 
by (force_tac (claset() addDs [zmult_zless_mono1], 

742 
simpset() addsimps [order_le_less]) 1); 

743 
qed "pos_imp_zmult_neg_iff"; 

744 

745 
Goal "#0 < (m::int) ==> (#0 < m*n) = (#0 < n)"; 

746 
by Auto_tac; 

747 
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2); 

748 
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1); 

749 
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 

750 
by (force_tac (claset() addDs [zmult_zless_mono1], 

751 
simpset() addsimps [order_le_less]) 1); 

752 
qed "pos_imp_zmult_pos_iff"; 

6973  753 

754 
(** <= versions of the theorems above **) 

755 

756 
Goal "(m::int) < #0 ==> (m*n <= #0) = (#0 <= n)"; 

757 
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 

758 
neg_imp_zmult_pos_iff]) 1); 

759 
qed "neg_imp_zmult_nonpos_iff"; 

760 

761 
Goal "(m::int) < #0 ==> (#0 <= m*n) = (n <= #0)"; 

762 
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 

763 
neg_imp_zmult_neg_iff]) 1); 

764 
qed "neg_imp_zmult_nonneg_iff"; 

765 

766 
Goal "#0 < (m::int) ==> (m*n <= #0) = (n <= #0)"; 

767 
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 

768 
pos_imp_zmult_pos_iff]) 1); 

769 
qed "pos_imp_zmult_nonpos_iff"; 

770 

771 
Goal "#0 < (m::int) ==> (#0 <= m*n) = (#0 <= n)"; 

772 
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 

773 
pos_imp_zmult_neg_iff]) 1); 

774 
qed "pos_imp_zmult_nonneg_iff"; 