author | wenzelm |
Tue, 25 Jul 2000 00:06:46 +0200 | |
changeset 9436 | 62bb04ab4b01 |
parent 9000 | c20d58286a51 |
child 9583 | 794e26a802c9 |
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 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
9 |
(** For simplifying Suc m - #n **) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
10 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
11 |
Goal "#0 < n ==> Suc m - n = m - (n - #1)"; |
8865 | 12 |
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
13 |
qed "Suc_diff_eq_diff_pred"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
14 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
15 |
(*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
|
16 |
but with some redundant inequality tests.*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
17 |
|
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))"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
19 |
by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
20 |
by (Asm_simp_tac 1); |
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); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
30 |
by (asm_full_simp_tac |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
31 |
(simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym, |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
32 |
neg_number_of_bin_pred_iff_0]) 1); |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
33 |
qed "Suc_diff_number_of"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
34 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
35 |
(* now redundant because of the inverse_fold simproc |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
36 |
Addsimps [Suc_diff_number_of]; *) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
37 |
|
8865 | 38 |
Goal "nat_case a f (number_of v) = \ |
39 |
\ (let pv = number_of (bin_pred v) in \ |
|
40 |
\ if neg pv then a else f (nat pv))"; |
|
41 |
by (simp_tac |
|
42 |
(simpset() addsplits [nat.split] |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
43 |
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
|
44 |
qed "nat_case_number_of"; |
8865 | 45 |
|
46 |
Goal "nat_case a f ((number_of v) + n) = \ |
|
47 |
\ (let pv = number_of (bin_pred v) in \ |
|
48 |
\ if neg pv then nat_case a f n else f (nat pv + n))"; |
|
49 |
by (stac add_eq_if 1); |
|
50 |
by (asm_simp_tac |
|
51 |
(simpset() addsplits [nat.split] |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
52 |
addsimps [Let_def, neg_imp_number_of_eq_0, |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
53 |
neg_number_of_bin_pred_iff_0]) 1); |
8865 | 54 |
qed "nat_case_add_eq_if"; |
55 |
||
56 |
Addsimps [nat_case_number_of, nat_case_add_eq_if]; |
|
57 |
||
58 |
||
59 |
Goal "nat_rec a f (number_of v) = \ |
|
60 |
\ (let pv = number_of (bin_pred v) in \ |
|
61 |
\ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"; |
|
62 |
by (case_tac "(number_of v)::nat" 1); |
|
63 |
by (ALLGOALS (asm_simp_tac |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
64 |
(simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0]))); |
8865 | 65 |
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
|
66 |
qed "nat_rec_number_of"; |
8865 | 67 |
|
68 |
Goal "nat_rec a f (number_of v + n) = \ |
|
69 |
\ (let pv = number_of (bin_pred v) in \ |
|
70 |
\ if neg pv then nat_rec a f n \ |
|
71 |
\ else f (nat pv + n) (nat_rec a f (nat pv + n)))"; |
|
72 |
by (stac add_eq_if 1); |
|
73 |
by (asm_simp_tac |
|
74 |
(simpset() addsplits [nat.split] |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
75 |
addsimps [Let_def, neg_imp_number_of_eq_0, |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
76 |
neg_number_of_bin_pred_iff_0]) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
77 |
qed "nat_rec_add_eq_if"; |
8865 | 78 |
|
79 |
Addsimps [nat_rec_number_of, nat_rec_add_eq_if]; |
|
80 |
||
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
81 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
82 |
(** For simplifying #m - Suc n **) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
83 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
84 |
Goal "m - Suc n = (m - #1) - n"; |
8865 | 85 |
by (simp_tac (numeral_ss addsplits [nat_diff_split]) 1); |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
86 |
qed "diff_Suc_eq_diff_pred"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
87 |
|
8877 | 88 |
(*Obsolete because of natdiff_cancel_numerals |
89 |
Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred]; |
|
90 |
It LOOPS if #1 is being replaced by 1. |
|
91 |
*) |
|
8776 | 92 |
|
93 |
||
94 |
(** Evens and Odds, for Mutilated Chess Board **) |
|
95 |
||
96 |
(*Case analysis on b<#2*) |
|
97 |
Goal "(n::nat) < #2 ==> n = #0 | n = #1"; |
|
98 |
by (arith_tac 1); |
|
99 |
qed "less_2_cases"; |
|
100 |
||
101 |
Goal "Suc(Suc(m)) mod #2 = m mod #2"; |
|
102 |
by (subgoal_tac "m mod #2 < #2" 1); |
|
103 |
by (Asm_simp_tac 2); |
|
104 |
be (less_2_cases RS disjE) 1; |
|
105 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc]))); |
|
106 |
qed "mod2_Suc_Suc"; |
|
107 |
Addsimps [mod2_Suc_Suc]; |
|
108 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8877
diff
changeset
|
109 |
Goal "!!m::nat. (0 < m mod #2) = (m mod #2 = #1)"; |
8776 | 110 |
by (subgoal_tac "m mod #2 < #2" 1); |
111 |
by (Asm_simp_tac 2); |
|
112 |
by (auto_tac (claset(), simpset() delsimps [mod_less_divisor])); |
|
113 |
qed "mod2_gr_0"; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9000
diff
changeset
|
114 |
Addsimps [mod2_gr_0, rename_numerals mod2_gr_0]; |
8776 | 115 |
|
8877 | 116 |
(** Removal of small numerals: #0, #1 and (in additive positions) #2 **) |
117 |
||
118 |
Goal "#2 + n = Suc (Suc n)"; |
|
119 |
by (Simp_tac 1); |
|
120 |
qed "add_2_eq_Suc"; |
|
121 |
||
122 |
Goal "n + #2 = Suc (Suc n)"; |
|
123 |
by (Simp_tac 1); |
|
124 |
qed "add_2_eq_Suc'"; |
|
125 |
||
126 |
Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc']; |
|
127 |
||
128 |
(*Can be used to eliminate long strings of Sucs, but not by default*) |
|
129 |
Goal "Suc (Suc (Suc n)) = #3 + n"; |
|
130 |
by (Simp_tac 1); |
|
131 |
qed "Suc3_eq_add_3"; |