author | paulson |
Thu, 30 Oct 2003 16:21:50 +0100 | |
changeset 14251 | b91f632a1d37 |
parent 12486 | 0ed8bdd883e0 |
child 14272 | 5efbb548107d |
permissions | -rw-r--r-- |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/NatSimprocs.ML |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
4 |
Copyright 2000 University of Cambridge |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
5 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
6 |
Simprocs for nat numerals (see also nat_simprocs.ML). |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
7 |
*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
8 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
9 |
(** For simplifying Suc m - #n **) |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
10 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
11 |
Goal "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
12 |
by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1] |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
13 |
addsplits [nat_diff_split]) 1); |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
14 |
qed "Suc_diff_eq_diff_pred"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
15 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
16 |
(*Now just instantiating n to (number_of v) does the right simplification, |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
17 |
but with some redundant inequality tests.*) |
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8877
diff
changeset
|
18 |
Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"; |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
19 |
by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0)" 1); |
11468 | 20 |
by (asm_simp_tac (HOL_ss addsimps [less_Suc_eq_le, le_0_eq]) 1); |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
21 |
by (stac less_number_of_Suc 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
22 |
by (Simp_tac 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
23 |
qed "neg_number_of_bin_pred_iff_0"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
24 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
25 |
Goal "neg (number_of (bin_minus v)) ==> \ |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
26 |
\ Suc m - (number_of v) = m - (number_of (bin_pred v))"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
27 |
by (stac Suc_diff_eq_diff_pred 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
28 |
by (Simp_tac 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
29 |
by (Simp_tac 1); |
14251
b91f632a1d37
Got rid of the structure "Int", which was obsolete and which obscured the
paulson
parents:
12486
diff
changeset
|
30 |
by (asm_full_simp_tac (ss_Int addsimps [diff_nat_number_of, |
b91f632a1d37
Got rid of the structure "Int", which was obsolete and which obscured the
paulson
parents:
12486
diff
changeset
|
31 |
less_0_number_of RS sym, neg_number_of_bin_pred_iff_0]) 1); |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
32 |
qed "Suc_diff_number_of"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
33 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
34 |
(* now redundant because of the inverse_fold simproc |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
35 |
Addsimps [Suc_diff_number_of]; *) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
36 |
|
8865 | 37 |
Goal "nat_case a f (number_of v) = \ |
38 |
\ (let pv = number_of (bin_pred v) in \ |
|
39 |
\ if neg pv then a else f (nat pv))"; |
|
40 |
by (simp_tac |
|
41 |
(simpset() addsplits [nat.split] |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
42 |
addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
43 |
qed "nat_case_number_of"; |
8865 | 44 |
|
45 |
Goal "nat_case a f ((number_of v) + n) = \ |
|
46 |
\ (let pv = number_of (bin_pred v) in \ |
|
47 |
\ if neg pv then nat_case a f n else f (nat pv + n))"; |
|
48 |
by (stac add_eq_if 1); |
|
49 |
by (asm_simp_tac |
|
50 |
(simpset() addsplits [nat.split] |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
51 |
addsimps [numeral_1_eq_Suc_0 RS sym, Let_def, |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
52 |
neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1); |
8865 | 53 |
qed "nat_case_add_eq_if"; |
54 |
||
55 |
Addsimps [nat_case_number_of, nat_case_add_eq_if]; |
|
56 |
||
57 |
||
58 |
Goal "nat_rec a f (number_of v) = \ |
|
59 |
\ (let pv = number_of (bin_pred v) in \ |
|
60 |
\ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"; |
|
61 |
by (case_tac "(number_of v)::nat" 1); |
|
62 |
by (ALLGOALS (asm_simp_tac |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
63 |
(simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0]))); |
8865 | 64 |
by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1); |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
65 |
qed "nat_rec_number_of"; |
8865 | 66 |
|
67 |
Goal "nat_rec a f (number_of v + n) = \ |
|
68 |
\ (let pv = number_of (bin_pred v) in \ |
|
69 |
\ if neg pv then nat_rec a f n \ |
|
70 |
\ else f (nat pv + n) (nat_rec a f (nat pv + n)))"; |
|
71 |
by (stac add_eq_if 1); |
|
72 |
by (asm_simp_tac |
|
73 |
(simpset() addsplits [nat.split] |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
74 |
addsimps [numeral_1_eq_Suc_0 RS sym, Let_def, |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
75 |
neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1); |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
76 |
qed "nat_rec_add_eq_if"; |
8865 | 77 |
|
78 |
Addsimps [nat_rec_number_of, nat_rec_add_eq_if]; |
|
79 |
||
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
80 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
81 |
(** For simplifying # m - Suc n **) |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
82 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
83 |
Goal "m - Suc n = (m - 1) - n"; |
8865 | 84 |
by (simp_tac (numeral_ss addsplits [nat_diff_split]) 1); |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
85 |
qed "diff_Suc_eq_diff_pred"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
86 |
|
8877 | 87 |
(*Obsolete because of natdiff_cancel_numerals |
88 |
Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred]; |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11468
diff
changeset
|
89 |
It LOOPS if Numeral1 is being replaced by 1. |
8877 | 90 |
*) |
8776 | 91 |
|
92 |
||
93 |
(** Evens and Odds, for Mutilated Chess Board **) |
|
94 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
95 |
(*Case analysis on b<2*) |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
96 |
Goal "(n::nat) < 2 ==> n = 0 | n = Suc 0"; |
8776 | 97 |
by (arith_tac 1); |
98 |
qed "less_2_cases"; |
|
99 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
100 |
Goal "Suc(Suc(m)) mod 2 = m mod 2"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
101 |
by (subgoal_tac "m mod 2 < 2" 1); |
8776 | 102 |
by (Asm_simp_tac 2); |
12486 | 103 |
by (etac (less_2_cases RS disjE) 1); |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
104 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def, mod_Suc, nat_1]))); |
8776 | 105 |
qed "mod2_Suc_Suc"; |
106 |
Addsimps [mod2_Suc_Suc]; |
|
107 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
108 |
Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"; |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
109 |
by (subgoal_tac "m mod 2 < 2" 1); |
8776 | 110 |
by (Asm_simp_tac 2); |
111 |
by (auto_tac (claset(), simpset() delsimps [mod_less_divisor])); |
|
112 |
qed "mod2_gr_0"; |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
113 |
Addsimps [mod2_gr_0]; |
8776 | 114 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
115 |
(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) 2 **) |
8877 | 116 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
117 |
Goal "2 + n = Suc (Suc n)"; |
8877 | 118 |
by (Simp_tac 1); |
119 |
qed "add_2_eq_Suc"; |
|
120 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
121 |
Goal "n + 2 = Suc (Suc n)"; |
8877 | 122 |
by (Simp_tac 1); |
123 |
qed "add_2_eq_Suc'"; |
|
124 |
||
125 |
Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc']; |
|
126 |
||
127 |
(*Can be used to eliminate long strings of Sucs, but not by default*) |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
128 |
Goal "Suc (Suc (Suc n)) = 3 + n"; |
8877 | 129 |
by (Simp_tac 1); |
130 |
qed "Suc3_eq_add_3"; |
|
9583
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
131 |
|
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
132 |
|
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
133 |
(** To collapse some needless occurrences of Suc |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
134 |
At least three Sucs, since two and fewer are rewritten back to Suc again! |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
135 |
|
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
136 |
We already have some rules to simplify operands smaller than 3. |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
137 |
**) |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
138 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
139 |
Goal "m div (Suc (Suc (Suc n))) = m div (3+n)"; |
9583
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
140 |
by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1); |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
141 |
qed "div_Suc_eq_div_add3"; |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
142 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
143 |
Goal "m mod (Suc (Suc (Suc n))) = m mod (3+n)"; |
9583
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
144 |
by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1); |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
145 |
qed "mod_Suc_eq_mod_add3"; |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
146 |
|
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
147 |
Addsimps [div_Suc_eq_div_add3, mod_Suc_eq_mod_add3]; |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
148 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
149 |
Goal "(Suc (Suc (Suc m))) div n = (3+m) div n"; |
9583
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
150 |
by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1); |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
151 |
qed "Suc_div_eq_add3_div"; |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
152 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
153 |
Goal "(Suc (Suc (Suc m))) mod n = (3+m) mod n"; |
9583
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
154 |
by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1); |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
155 |
qed "Suc_mod_eq_add3_mod"; |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
156 |
|
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
157 |
Addsimps [inst "n" "number_of ?v" Suc_div_eq_add3_div, |
794e26a802c9
some ad-hoc simprules for div and mod to reduce the
paulson
parents:
9436
diff
changeset
|
158 |
inst "n" "number_of ?v" Suc_mod_eq_add3_mod]; |