author | paulson |
Thu, 15 Jul 1999 10:34:37 +0200 | |
changeset 7010 | 63120b6dca50 |
parent 7008 | 6def5ce146e2 |
child 7033 | c7479ae352b1 |
permissions | -rw-r--r-- |
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 |
||
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
15 |
Goal "NCons Pls False = Pls"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
16 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
17 |
qed "NCons_Pls_0"; |
1632 | 18 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
19 |
Goal "NCons Pls True = Pls BIT True"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
20 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
21 |
qed "NCons_Pls_1"; |
1632 | 22 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
23 |
Goal "NCons Min False = Min BIT False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
24 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
25 |
qed "NCons_Min_0"; |
1632 | 26 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
27 |
Goal "NCons Min True = Min"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
28 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
29 |
qed "NCons_Min_1"; |
1632 | 30 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
31 |
Goal "bin_succ(w BIT True) = (bin_succ w) BIT False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
32 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
33 |
qed "bin_succ_1"; |
1632 | 34 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
35 |
Goal "bin_succ(w BIT False) = NCons w True"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
36 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
37 |
qed "bin_succ_0"; |
1632 | 38 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
39 |
Goal "bin_pred(w BIT True) = NCons w False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
40 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
41 |
qed "bin_pred_1"; |
1632 | 42 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
43 |
Goal "bin_pred(w BIT False) = (bin_pred w) BIT True"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
44 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
45 |
qed "bin_pred_0"; |
1632 | 46 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
47 |
Goal "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
48 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
49 |
qed "bin_minus_1"; |
1632 | 50 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
51 |
Goal "bin_minus(w BIT False) = (bin_minus w) BIT False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
52 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
53 |
qed "bin_minus_0"; |
1632 | 54 |
|
5491 | 55 |
|
1632 | 56 |
(*** bin_add: binary addition ***) |
57 |
||
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
58 |
Goal "bin_add (v BIT True) (w BIT True) = \ |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
59 |
\ NCons (bin_add v (bin_succ w)) False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
60 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
61 |
qed "bin_add_BIT_11"; |
1632 | 62 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
63 |
Goal "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
64 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
65 |
qed "bin_add_BIT_10"; |
1632 | 66 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
67 |
Goal "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
68 |
by Auto_tac; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
69 |
qed "bin_add_BIT_0"; |
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 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
76 |
Goal "bin_add (v BIT x) Min = bin_pred (v BIT x)"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
77 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
78 |
qed "bin_add_BIT_Min"; |
1632 | 79 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
80 |
Goal "bin_add (v BIT x) (w BIT y) = \ |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
81 |
\ NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
82 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
83 |
qed "bin_add_BIT_BIT"; |
1632 | 84 |
|
85 |
||
6036 | 86 |
(*** bin_mult: binary multiplication ***) |
1632 | 87 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
88 |
Goal "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
89 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
90 |
qed "bin_mult_1"; |
1632 | 91 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
92 |
Goal "bin_mult (v BIT False) w = NCons (bin_mult v w) False"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
93 |
by (Simp_tac 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
94 |
qed "bin_mult_0"; |
1632 | 95 |
|
96 |
||
97 |
(**** The carry/borrow functions, bin_succ and bin_pred ****) |
|
98 |
||
99 |
||
6910 | 100 |
(**** number_of ****) |
1632 | 101 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
102 |
Goal "number_of(NCons w b) = (number_of(w BIT b)::int)"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
103 |
by (induct_tac "w" 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
104 |
by (ALLGOALS Asm_simp_tac); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
105 |
qed "number_of_NCons"; |
1632 | 106 |
|
6910 | 107 |
Addsimps [number_of_NCons]; |
1632 | 108 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
109 |
Goal "number_of(bin_succ w) = int 1 + number_of w"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
110 |
by (induct_tac "w" 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
111 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
112 |
qed "number_of_succ"; |
5491 | 113 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
114 |
Goal "number_of(bin_pred w) = - (int 1) + number_of w"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
115 |
by (induct_tac "w" 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
116 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
117 |
qed "number_of_pred"; |
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 |
speed-up.*) |
|
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 |
(** Special-case 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"; |
6997 | 281 |
|
282 |
Goal "((#1::int) + w <= z) = (w<z)"; |
|
283 |
by (stac zadd_commute 1); |
|
284 |
by (rtac add1_zle_eq 1); |
|
285 |
qed "add1_left_zle_eq"; |
|
5491 | 286 |
|
5540 | 287 |
Goal "neg x = (x < #0)"; |
6917 | 288 |
by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); |
5540 | 289 |
qed "neg_eq_less_0"; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
290 |
|
6989 | 291 |
Goal "(~neg x) = (#0 <= x)"; |
6917 | 292 |
by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1); |
5540 | 293 |
qed "not_neg_eq_ge_0"; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
294 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
295 |
Goal "#0 <= int m"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
296 |
by (Simp_tac 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
297 |
qed "zero_zle_int"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
298 |
AddIffs [zero_zle_int]; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
299 |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
300 |
|
5747 | 301 |
(** Needed because (int 0) rewrites to #0. |
302 |
Can these be generalized without evaluating large numbers?**) |
|
303 |
||
304 |
Goal "~ (int k < #0)"; |
|
305 |
by (Simp_tac 1); |
|
306 |
qed "int_less_0_conv"; |
|
307 |
||
308 |
Goal "(int k <= #0) = (k=0)"; |
|
309 |
by (Simp_tac 1); |
|
310 |
qed "int_le_0_conv"; |
|
311 |
||
312 |
Goal "(int k = #0) = (k=0)"; |
|
313 |
by (Simp_tac 1); |
|
314 |
qed "int_eq_0_conv"; |
|
315 |
||
316 |
Goal "(#0 = int k) = (k=0)"; |
|
317 |
by Auto_tac; |
|
318 |
qed "int_eq_0_conv'"; |
|
319 |
||
320 |
Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv']; |
|
321 |
||
322 |
||
5491 | 323 |
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
324 |
||
325 |
(** Equals (=) **) |
|
1632 | 326 |
|
5491 | 327 |
Goalw [iszero_def] |
6997 | 328 |
"((number_of x::int) = number_of y) = \ |
329 |
\ iszero (number_of (bin_add x (bin_minus y)))"; |
|
5491 | 330 |
by (simp_tac (simpset() addsimps |
6910 | 331 |
(zcompare_rls @ [number_of_add, number_of_minus])) 1); |
332 |
qed "eq_number_of_eq"; |
|
5491 | 333 |
|
6910 | 334 |
Goalw [iszero_def] "iszero ((number_of Pls)::int)"; |
5491 | 335 |
by (Simp_tac 1); |
6910 | 336 |
qed "iszero_number_of_Pls"; |
5491 | 337 |
|
6910 | 338 |
Goalw [iszero_def] "~ iszero ((number_of Min)::int)"; |
5491 | 339 |
by (Simp_tac 1); |
6910 | 340 |
qed "nonzero_number_of_Min"; |
5491 | 341 |
|
342 |
Goalw [iszero_def] |
|
6910 | 343 |
"iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; |
5491 | 344 |
by (Simp_tac 1); |
6910 | 345 |
by (int_case_tac "number_of w" 1); |
5491 | 346 |
by (ALLGOALS (asm_simp_tac |
5540 | 347 |
(simpset() addsimps zcompare_rls @ |
348 |
[zminus_zadd_distrib RS sym, |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
349 |
zadd_int]))); |
6910 | 350 |
qed "iszero_number_of_BIT"; |
5491 | 351 |
|
6910 | 352 |
Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)"; |
353 |
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); |
|
354 |
qed "iszero_number_of_0"; |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
355 |
|
6910 | 356 |
Goal "~ iszero (number_of (w BIT True)::int)"; |
357 |
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); |
|
358 |
qed "iszero_number_of_1"; |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
359 |
|
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
360 |
|
5491 | 361 |
|
362 |
(** Less-than (<) **) |
|
363 |
||
364 |
Goalw [zless_def,zdiff_def] |
|
6910 | 365 |
"(number_of x::int) < number_of y \ |
366 |
\ = neg (number_of (bin_add x (bin_minus y)))"; |
|
5491 | 367 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
6910 | 368 |
qed "less_number_of_eq_neg"; |
5491 | 369 |
|
6910 | 370 |
Goal "~ neg (number_of Pls)"; |
5491 | 371 |
by (Simp_tac 1); |
6910 | 372 |
qed "not_neg_number_of_Pls"; |
5491 | 373 |
|
6910 | 374 |
Goal "neg (number_of Min)"; |
5491 | 375 |
by (Simp_tac 1); |
6910 | 376 |
qed "neg_number_of_Min"; |
5491 | 377 |
|
6910 | 378 |
Goal "neg (number_of (w BIT x)) = neg (number_of w)"; |
5491 | 379 |
by (Asm_simp_tac 1); |
6910 | 380 |
by (int_case_tac "number_of w" 1); |
5491 | 381 |
by (ALLGOALS (asm_simp_tac |
6917 | 382 |
(simpset() addsimps [zadd_int, neg_eq_less_int0, |
5540 | 383 |
symmetric zdiff_def] @ zcompare_rls))); |
6910 | 384 |
qed "neg_number_of_BIT"; |
5491 | 385 |
|
386 |
||
387 |
(** Less-than-or-equals (<=) **) |
|
388 |
||
6910 | 389 |
Goal "(number_of x <= (number_of y::int)) = (~ number_of y < (number_of x::int))"; |
5491 | 390 |
by (simp_tac (simpset() addsimps [zle_def]) 1); |
6910 | 391 |
qed "le_number_of_eq_not_less"; |
5491 | 392 |
|
5540 | 393 |
(*Delete the original rewrites, with their clumsy conditional expressions*) |
5551 | 394 |
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, |
395 |
NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT]; |
|
5491 | 396 |
|
397 |
(*Hide the binary representation of integer constants*) |
|
6910 | 398 |
Delsimps [number_of_Pls, number_of_Min, number_of_BIT]; |
5491 | 399 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
400 |
(*simplification of arithmetic operations on integer constants*) |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
401 |
val bin_arith_extra_simps = |
6910 | 402 |
[number_of_add RS sym, |
403 |
number_of_minus RS sym, |
|
404 |
number_of_mult RS sym, |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
405 |
bin_succ_1, bin_succ_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
406 |
bin_pred_1, bin_pred_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
407 |
bin_minus_1, bin_minus_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
408 |
bin_add_Pls_right, bin_add_BIT_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
409 |
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11, |
6910 | 410 |
diff_number_of_eq, |
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
411 |
bin_mult_1, bin_mult_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
412 |
NCons_Pls_0, NCons_Pls_1, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
413 |
NCons_Min_0, NCons_Min_1, NCons_BIT]; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
414 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
415 |
(*For making a minimal simpset, one must include these default simprules |
6910 | 416 |
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
|
417 |
val bin_arith_simps = |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
418 |
[bin_pred_Pls, bin_pred_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
419 |
bin_succ_Pls, bin_succ_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
420 |
bin_add_Pls, bin_add_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
421 |
bin_minus_Pls, bin_minus_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
422 |
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
|
423 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
424 |
(*Simplification of relational operations*) |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
425 |
val bin_rel_simps = |
6910 | 426 |
[eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min, |
427 |
iszero_number_of_0, iszero_number_of_1, |
|
428 |
less_number_of_eq_neg, |
|
429 |
not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT, |
|
430 |
le_number_of_eq_not_less]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
431 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
432 |
Addsimps bin_arith_extra_simps; |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
433 |
Addsimps bin_rel_simps; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
434 |
|
6997 | 435 |
|
436 |
(** Constant folding inside parentheses **) |
|
437 |
||
438 |
Goal "number_of v + (number_of w + c) = number_of(bin_add v w) + (c::int)"; |
|
439 |
by (stac (zadd_assoc RS sym) 1); |
|
440 |
by (stac number_of_add 1); |
|
441 |
by Auto_tac; |
|
442 |
qed "nested_number_of_add"; |
|
443 |
||
444 |
Goalw [zdiff_def] |
|
445 |
"number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)"; |
|
446 |
by (rtac nested_number_of_add 1); |
|
447 |
qed "nested_diff1_number_of_add"; |
|
448 |
||
449 |
Goal "number_of v + (c - number_of w) = \ |
|
450 |
\ number_of (bin_add v (bin_minus w)) + (c::int)"; |
|
451 |
by (stac (diff_number_of_eq RS sym) 1); |
|
452 |
by Auto_tac; |
|
453 |
qed "nested_diff2_number_of_add"; |
|
454 |
||
455 |
Goal "number_of v * (number_of w * c) = number_of(bin_mult v w) * (c::int)"; |
|
456 |
by (stac (zmult_assoc RS sym) 1); |
|
457 |
by (stac number_of_mult 1); |
|
458 |
by Auto_tac; |
|
459 |
qed "nested_number_of_mult"; |
|
460 |
Addsimps [nested_number_of_add, nested_diff1_number_of_add, |
|
461 |
nested_diff2_number_of_add, nested_number_of_mult]; |
|
462 |
||
463 |
||
464 |
||
6060 | 465 |
(*---------------------------------------------------------------------------*) |
466 |
(* Linear arithmetic *) |
|
467 |
(*---------------------------------------------------------------------------*) |
|
468 |
||
469 |
(* |
|
470 |
Instantiation of the generic linear arithmetic package for int. |
|
471 |
FIXME: multiplication with constants (eg #2 * i) does not work yet. |
|
472 |
Solution: the cancellation simprocs in Int_Cancel should be able to deal with |
|
473 |
it (eg simplify #3 * i <= 2 * i to i <= #0) or `add_rules' below should |
|
474 |
include rules for turning multiplication with constants into addition. |
|
475 |
(The latter option is very inefficient!) |
|
476 |
*) |
|
477 |
||
6128 | 478 |
structure Int_LA_Data(*: LIN_ARITH_DATA*) = |
6060 | 479 |
struct |
6101 | 480 |
|
6128 | 481 |
val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2]; |
6060 | 482 |
|
483 |
fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i) |
|
484 |
| Some n => (overwrite(p,(t,n+m:int)), i)); |
|
485 |
||
486 |
(* Turn term into list of summand * multiplicity plus a constant *) |
|
487 |
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) |
|
488 |
| poly(Const("op -",_) $ s $ t, m, pi) = poly(s,m,poly(t,~1*m,pi)) |
|
489 |
| poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi) |
|
6910 | 490 |
| poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi) = |
491 |
(poly(t,m*NumeralSyntax.dest_bin c,pi) handle Match => add_atom(all,m,pi)) |
|
492 |
| poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) = |
|
493 |
((p,i + m*NumeralSyntax.dest_bin t) handle Match => add_atom(all,m,(p,i))) |
|
6060 | 494 |
| poly x = add_atom x; |
495 |
||
6128 | 496 |
fun decomp2(rel,lhs,rhs) = |
6060 | 497 |
let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0)) |
498 |
in case rel of |
|
499 |
"op <" => Some(p,i,"<",q,j) |
|
500 |
| "op <=" => Some(p,i,"<=",q,j) |
|
501 |
| "op =" => Some(p,i,"=",q,j) |
|
502 |
| _ => None |
|
503 |
end; |
|
504 |
||
6128 | 505 |
val intT = Type("IntDef.int",[]); |
506 |
fun iib T = T = ([intT,intT] ---> HOLogic.boolT); |
|
6060 | 507 |
|
6128 | 508 |
fun decomp1(T,xxx) = |
509 |
if iib T then decomp2 xxx else Nat_LA_Data.decomp1(T,xxx); |
|
510 |
||
511 |
fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs)) |
|
6060 | 512 |
| decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = |
6128 | 513 |
Nat_LA_Data.negate(decomp1(T,(rel,lhs,rhs))) |
6060 | 514 |
| decomp _ = None |
515 |
||
516 |
(* reduce contradictory <= to False *) |
|
517 |
val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0]; |
|
518 |
||
6128 | 519 |
val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules |
6060 | 520 |
addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; |
521 |
||
522 |
val simp = simplify cancel_sums_ss; |
|
523 |
||
6128 | 524 |
val add_mono_thms = Nat_LA_Data.add_mono_thms @ |
525 |
map (fn s => prove_goal Int.thy s |
|
526 |
(fn prems => [cut_facts_tac prems 1, |
|
527 |
asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) |
|
528 |
["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", |
|
529 |
"(i = j) & (k <= l) ==> i + k <= j + (l::int)", |
|
530 |
"(i <= j) & (k = l) ==> i + k <= j + (l::int)", |
|
531 |
"(i = j) & (k = l) ==> i + k = j + (l::int)" |
|
532 |
]; |
|
6060 | 533 |
|
534 |
end; |
|
535 |
||
6128 | 536 |
(* Update parameters of arithmetic prover *) |
537 |
LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms; |
|
538 |
LA_Data_Ref.lessD := Int_LA_Data.lessD; |
|
539 |
LA_Data_Ref.decomp := Int_LA_Data.decomp; |
|
540 |
LA_Data_Ref.simp := Int_LA_Data.simp; |
|
541 |
||
6060 | 542 |
|
6128 | 543 |
val int_arith_simproc_pats = |
6394 | 544 |
map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT)) |
6128 | 545 |
["(m::int) < n","(m::int) <= n", "(m::int) = n"]; |
6060 | 546 |
|
6128 | 547 |
val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats |
548 |
Fast_Arith.lin_arith_prover; |
|
549 |
||
550 |
Addsimprocs [fast_int_arith_simproc]; |
|
6060 | 551 |
|
552 |
(* FIXME: K true should be replaced by a sensible test to speed things up |
|
553 |
in case there are lots of irrelevant terms involved. |
|
6157 | 554 |
|
6128 | 555 |
val arith_tac = |
556 |
refute_tac (K true) (REPEAT o split_tac[nat_diff_split]) |
|
557 |
((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac); |
|
6157 | 558 |
*) |
6060 | 559 |
|
560 |
(* Some test data |
|
561 |
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
|
6301 | 562 |
by (fast_arith_tac 1); |
6060 | 563 |
Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)"; |
6301 | 564 |
by (fast_arith_tac 1); |
6060 | 565 |
Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d"; |
6301 | 566 |
by (fast_arith_tac 1); |
6060 | 567 |
Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; |
6301 | 568 |
by (fast_arith_tac 1); |
6060 | 569 |
Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ |
570 |
\ ==> a+a <= j+j"; |
|
6301 | 571 |
by (fast_arith_tac 1); |
6060 | 572 |
Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \ |
573 |
\ ==> a+a - - #-1 < j+j - #3"; |
|
6301 | 574 |
by (fast_arith_tac 1); |
6060 | 575 |
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; |
6301 | 576 |
by (arith_tac 1); |
6060 | 577 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
578 |
\ ==> a <= l"; |
|
6301 | 579 |
by (fast_arith_tac 1); |
6060 | 580 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
581 |
\ ==> a+a+a+a <= l+l+l+l"; |
|
6301 | 582 |
by (fast_arith_tac 1); |
6060 | 583 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
584 |
\ ==> a+a+a+a+a <= l+l+l+l+i"; |
|
6301 | 585 |
by (fast_arith_tac 1); |
6060 | 586 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
587 |
\ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; |
|
6301 | 588 |
by (fast_arith_tac 1); |
6060 | 589 |
*) |
590 |
||
591 |
(*---------------------------------------------------------------------------*) |
|
592 |
(* End of linear arithmetic *) |
|
593 |
(*---------------------------------------------------------------------------*) |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
594 |
|
5592 | 595 |
(** Simplification of arithmetic when nested to the right **) |
596 |
||
6910 | 597 |
Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)"; |
5592 | 598 |
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
6910 | 599 |
qed "add_number_of_left"; |
5592 | 600 |
|
6910 | 601 |
Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)"; |
5592 | 602 |
by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1); |
6910 | 603 |
qed "mult_number_of_left"; |
5592 | 604 |
|
6910 | 605 |
Addsimps [add_number_of_left, mult_number_of_left]; |
5592 | 606 |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
607 |
(** Simplification of inequalities involving numerical constants **) |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
608 |
|
6910 | 609 |
Goal "(w <= z + (#1::int)) = (w<=z | w = z + (#1::int))"; |
6301 | 610 |
by (arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
611 |
qed "zle_add1_eq"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
612 |
|
6910 | 613 |
Goal "(w <= z - (#1::int)) = (w<(z::int))"; |
6301 | 614 |
by (arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
615 |
qed "zle_diff1_eq"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
616 |
Addsimps [zle_diff1_eq]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
617 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
618 |
(*2nd premise can be proved automatically if v is a literal*) |
6910 | 619 |
Goal "[| w <= z; #0 <= v |] ==> w <= z + (v::int)"; |
6301 | 620 |
by (fast_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
621 |
qed "zle_imp_zle_zadd"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
622 |
|
6910 | 623 |
Goal "w <= z ==> w <= z + (#1::int)"; |
6301 | 624 |
by (fast_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
625 |
qed "zle_imp_zle_zadd1"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
626 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
627 |
(*2nd premise can be proved automatically if v is a literal*) |
6910 | 628 |
Goal "[| w < z; #0 <= v |] ==> w < z + (v::int)"; |
6301 | 629 |
by (fast_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
630 |
qed "zless_imp_zless_zadd"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
631 |
|
6910 | 632 |
Goal "w < z ==> w < z + (#1::int)"; |
6301 | 633 |
by (fast_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
634 |
qed "zless_imp_zless_zadd1"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
635 |
|
6910 | 636 |
Goal "(w < z + #1) = (w<=(z::int))"; |
6301 | 637 |
by (arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
638 |
qed "zle_add1_eq_le"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
639 |
Addsimps [zle_add1_eq_le]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
640 |
|
6910 | 641 |
Goal "(z = z + w) = (w = (#0::int))"; |
6301 | 642 |
by (arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
643 |
qed "zadd_left_cancel0"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
644 |
Addsimps [zadd_left_cancel0]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
645 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
646 |
(*LOOPS as a simprule!*) |
6910 | 647 |
Goal "[| w + v < z; #0 <= v |] ==> w < (z::int)"; |
6301 | 648 |
by (fast_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
649 |
qed "zless_zadd_imp_zless"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
650 |
|
5540 | 651 |
(*LOOPS as a simprule! Analogous to Suc_lessD*) |
6910 | 652 |
Goal "w + #1 < z ==> w < (z::int)"; |
6301 | 653 |
by (fast_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
654 |
qed "zless_zadd1_imp_zless"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
655 |
|
6910 | 656 |
Goal "w + #-1 = w - (#1::int)"; |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
657 |
by (Simp_tac 1); |
5551 | 658 |
qed "zplus_minus1_conv"; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
659 |
|
5551 | 660 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
661 |
(*** nat ***) |
5551 | 662 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
663 |
Goal "#0 <= z ==> int (nat z) = z"; |
5551 | 664 |
by (asm_full_simp_tac |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
665 |
(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
|
666 |
qed "nat_0_le"; |
5551 | 667 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
668 |
Goal "z <= #0 ==> nat z = 0"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
669 |
by (case_tac "z = #0" 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
670 |
by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
671 |
by (asm_full_simp_tac |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
672 |
(simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
673 |
qed "nat_le_0"; |
5551 | 674 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
675 |
Addsimps [nat_0_le, nat_le_0]; |
5551 | 676 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
677 |
Goal "#0 <= w ==> (nat w = m) = (w = int m)"; |
5551 | 678 |
by Auto_tac; |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
679 |
qed "nat_eq_iff"; |
5551 | 680 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
681 |
Goal "#0 <= w ==> (nat w < m) = (w < int m)"; |
5551 | 682 |
by (rtac iffI 1); |
683 |
by (asm_full_simp_tac |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
684 |
(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
|
685 |
by (etac (nat_0_le RS subst) 1); |
5551 | 686 |
by (Simp_tac 1); |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
687 |
qed "nat_less_iff"; |
5551 | 688 |
|
5747 | 689 |
|
6716
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
690 |
(*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
|
691 |
Addsimps [int_0, int_Suc, symmetric zdiff_def]; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
692 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
693 |
Goal "nat #0 = 0"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
694 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
695 |
qed "nat_0"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
696 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
697 |
Goal "nat #1 = 1"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
698 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
699 |
qed "nat_1"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
700 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
701 |
Goal "nat #2 = 2"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
702 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
703 |
qed "nat_2"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
704 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
705 |
Goal "nat #3 = Suc 2"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
706 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
707 |
qed "nat_3"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
708 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
709 |
Goal "nat #4 = Suc (Suc 2)"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
710 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
711 |
qed "nat_4"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
712 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
713 |
Goal "nat #5 = Suc (Suc (Suc 2))"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
714 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
715 |
qed "nat_5"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
716 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
717 |
Goal "nat #6 = Suc (Suc (Suc (Suc 2)))"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
718 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
719 |
qed "nat_6"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
720 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
721 |
Goal "nat #7 = Suc (Suc (Suc (Suc (Suc 2))))"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
722 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
723 |
qed "nat_7"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
724 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
725 |
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
|
726 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
727 |
qed "nat_8"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
728 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
729 |
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
|
730 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
731 |
qed "nat_9"; |
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
732 |
|
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset
|
733 |
(*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
|
734 |
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
|
735 |
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
|
736 |
|
5747 | 737 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
738 |
Goal "#0 <= w ==> (nat w < nat z) = (w<z)"; |
5551 | 739 |
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
|
740 |
by (auto_tac (claset(), simpset() addsimps [nat_less_iff])); |
5551 | 741 |
by (auto_tac (claset() addIs [zless_trans], |
5747 | 742 |
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
|
743 |
qed "nat_less_eq_zless"; |
5747 | 744 |
|
7008
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
745 |
Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
746 |
by (auto_tac (claset(), |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
747 |
simpset() addsimps [linorder_not_less RS sym, |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
748 |
zless_nat_conj])); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
749 |
qed "nat_le_eq_zle"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
750 |
|
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
751 |
(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*) |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
752 |
Goal "n<=m --> int m - int n = int (m-n)"; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
753 |
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
754 |
by Auto_tac; |
6def5ce146e2
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset
|
755 |
qed_spec_mp "zdiff_int"; |
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
756 |
|
6917 | 757 |
(*Towards canonical simplification*) |
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
758 |
Addsimps zadd_ac; |
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset
|
759 |
Addsimps zmult_ac; |
6917 | 760 |
Addsimps [zmult_zminus, zmult_zminus_right]; |
6941 | 761 |
|
762 |
||
763 |
||
764 |
(** Products of signs **) |
|
765 |
||
766 |
Goal "(m::int) < #0 ==> (#0 < m*n) = (n < #0)"; |
|
767 |
by Auto_tac; |
|
768 |
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2); |
|
769 |
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1); |
|
770 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); |
|
771 |
by (force_tac (claset() addDs [zmult_zless_mono1_neg], |
|
772 |
simpset() addsimps [order_le_less]) 1); |
|
773 |
qed "neg_imp_zmult_pos_iff"; |
|
774 |
||
775 |
Goal "(m::int) < #0 ==> (m*n < #0) = (#0 < n)"; |
|
776 |
by Auto_tac; |
|
777 |
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2); |
|
778 |
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1); |
|
779 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); |
|
780 |
by (force_tac (claset() addDs [zmult_zless_mono1_neg], |
|
781 |
simpset() addsimps [order_le_less]) 1); |
|
782 |
qed "neg_imp_zmult_neg_iff"; |
|
783 |
||
784 |
Goal "#0 < (m::int) ==> (m*n < #0) = (n < #0)"; |
|
785 |
by Auto_tac; |
|
786 |
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2); |
|
787 |
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1); |
|
788 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); |
|
789 |
by (force_tac (claset() addDs [zmult_zless_mono1], |
|
790 |
simpset() addsimps [order_le_less]) 1); |
|
791 |
qed "pos_imp_zmult_neg_iff"; |
|
792 |
||
793 |
Goal "#0 < (m::int) ==> (#0 < m*n) = (#0 < n)"; |
|
794 |
by Auto_tac; |
|
795 |
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2); |
|
796 |
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1); |
|
797 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); |
|
798 |
by (force_tac (claset() addDs [zmult_zless_mono1], |
|
799 |
simpset() addsimps [order_le_less]) 1); |
|
800 |
qed "pos_imp_zmult_pos_iff"; |
|
6973 | 801 |
|
802 |
(** <= versions of the theorems above **) |
|
803 |
||
804 |
Goal "(m::int) < #0 ==> (m*n <= #0) = (#0 <= n)"; |
|
805 |
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, |
|
806 |
neg_imp_zmult_pos_iff]) 1); |
|
807 |
qed "neg_imp_zmult_nonpos_iff"; |
|
808 |
||
809 |
Goal "(m::int) < #0 ==> (#0 <= m*n) = (n <= #0)"; |
|
810 |
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, |
|
811 |
neg_imp_zmult_neg_iff]) 1); |
|
812 |
qed "neg_imp_zmult_nonneg_iff"; |
|
813 |
||
814 |
Goal "#0 < (m::int) ==> (m*n <= #0) = (n <= #0)"; |
|
815 |
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, |
|
816 |
pos_imp_zmult_pos_iff]) 1); |
|
817 |
qed "pos_imp_zmult_nonpos_iff"; |
|
818 |
||
819 |
Goal "#0 < (m::int) ==> (#0 <= m*n) = (#0 <= n)"; |
|
820 |
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, |
|
821 |
pos_imp_zmult_neg_iff]) 1); |
|
822 |
qed "pos_imp_zmult_nonneg_iff"; |