author | paulson |
Tue, 23 May 2000 18:06:22 +0200 | |
changeset 8935 | 548901d05a0e |
parent 8877 | 9d6514fcd584 |
child 9000 | c20d58286a51 |
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 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
6 |
Simprocs for nat numerals |
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 |
Goal "number_of v + (number_of v' + (k::nat)) = \ |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
10 |
\ (if neg (number_of v) then number_of v' + k \ |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
11 |
\ else if neg (number_of v') then number_of v + k \ |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
12 |
\ else number_of (bin_add v v') + k)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
13 |
by (Simp_tac 1); |
8766 | 14 |
qed "nat_number_of_add_left"; |
8759
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 |
|
8776 | 17 |
(** For combine_numerals **) |
18 |
||
19 |
Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)"; |
|
20 |
by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1); |
|
21 |
qed "left_add_mult_distrib"; |
|
22 |
||
23 |
||
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
24 |
(** For cancel_numerals **) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
25 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
26 |
Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"; |
8865 | 27 |
by (asm_simp_tac (simpset() addsplits [nat_diff_split] |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
28 |
addsimps [add_mult_distrib]) 1); |
8766 | 29 |
qed "nat_diff_add_eq1"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
30 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
31 |
Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))"; |
8865 | 32 |
by (asm_simp_tac (simpset() addsplits [nat_diff_split] |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
33 |
addsimps [add_mult_distrib]) 1); |
8766 | 34 |
qed "nat_diff_add_eq2"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
35 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
36 |
Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)"; |
8865 | 37 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
38 |
addsimps [add_mult_distrib])); |
8766 | 39 |
qed "nat_eq_add_iff1"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
40 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
41 |
Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)"; |
8865 | 42 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
43 |
addsimps [add_mult_distrib])); |
8766 | 44 |
qed "nat_eq_add_iff2"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
45 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
46 |
Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)"; |
8865 | 47 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
48 |
addsimps [add_mult_distrib])); |
8766 | 49 |
qed "nat_less_add_iff1"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
50 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
51 |
Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)"; |
8865 | 52 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
53 |
addsimps [add_mult_distrib])); |
8766 | 54 |
qed "nat_less_add_iff2"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
55 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
56 |
Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; |
8865 | 57 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
58 |
addsimps [add_mult_distrib])); |
8766 | 59 |
qed "nat_le_add_iff1"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
60 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
61 |
Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; |
8865 | 62 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
63 |
addsimps [add_mult_distrib])); |
8766 | 64 |
qed "nat_le_add_iff2"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
65 |
|
8776 | 66 |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
67 |
structure Nat_Numeral_Simprocs = |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
68 |
struct |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
69 |
|
8766 | 70 |
(*Utilities*) |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
71 |
|
8766 | 72 |
fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ |
73 |
NumeralSyntax.mk_bin n; |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
74 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
75 |
(*Decodes a unary or binary numeral to a NATURAL NUMBER*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
76 |
fun dest_numeral (Const ("0", _)) = 0 |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
77 |
| dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
78 |
| dest_numeral (Const("Numeral.number_of", _) $ w) = |
8785 | 79 |
(BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w) |
80 |
handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w])) |
|
81 |
| dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]); |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
82 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
83 |
fun find_first_numeral past (t::terms) = |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
84 |
((dest_numeral t, t, rev past @ terms) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
85 |
handle TERM _ => find_first_numeral (t::past) terms) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
86 |
| find_first_numeral past [] = raise TERM("find_first_numeral", []); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
87 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
88 |
val zero = mk_numeral 0; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
89 |
val mk_plus = HOLogic.mk_binop "op +"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
90 |
|
8766 | 91 |
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
92 |
fun mk_sum [] = zero |
8766 | 93 |
| mk_sum [t,u] = mk_plus (t, u) |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
94 |
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
95 |
|
8776 | 96 |
(*this version ALWAYS includes a trailing zero*) |
97 |
fun long_mk_sum [] = zero |
|
98 |
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
99 |
||
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
100 |
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
101 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
102 |
(*extract the outer Sucs from a term and convert them to a binary numeral*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
103 |
fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
104 |
| dest_Sucs (0, t) = t |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
105 |
| dest_Sucs (k, t) = mk_plus (mk_numeral k, t); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
106 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
107 |
fun dest_sum t = |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
108 |
let val (t,u) = dest_plus t |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
109 |
in dest_sum t @ dest_sum u end |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
110 |
handle TERM _ => [t]; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
111 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
112 |
fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t)); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
113 |
|
8799 | 114 |
val trans_tac = Int_Numeral_Simprocs.trans_tac; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
115 |
|
8776 | 116 |
val prove_conv = Int_Numeral_Simprocs.prove_conv; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
117 |
|
8766 | 118 |
val bin_simps = [add_nat_number_of, nat_number_of_add_left, |
119 |
diff_nat_number_of, le_nat_number_of_eq_not_less, |
|
120 |
less_nat_number_of, Let_number_of, nat_number_of] @ |
|
121 |
bin_arith_simps @ bin_rel_simps; |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
122 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
123 |
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
124 |
fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
125 |
val prep_pats = map prep_pat; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
126 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
127 |
|
8776 | 128 |
(*** CancelNumerals simprocs ***) |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
129 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
130 |
val one = mk_numeral 1; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
131 |
val mk_times = HOLogic.mk_binop "op *"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
132 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
133 |
fun mk_prod [] = one |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
134 |
| mk_prod [t] = t |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
135 |
| mk_prod (t :: ts) = if t = one then mk_prod ts |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
136 |
else mk_times (t, mk_prod ts); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
137 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
138 |
val dest_times = HOLogic.dest_bin "op *" HOLogic.natT; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
139 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
140 |
fun dest_prod t = |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
141 |
let val (t,u) = dest_times t |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
142 |
in dest_prod t @ dest_prod u end |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
143 |
handle TERM _ => [t]; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
144 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
145 |
(*DON'T do the obvious simplifications; that would create special cases*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
146 |
fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
147 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
148 |
(*Express t as a product of (possibly) a numeral with other sorted terms*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
149 |
fun dest_coeff t = |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
150 |
let val ts = sort Term.term_ord (dest_prod t) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
151 |
val (n, _, ts') = find_first_numeral [] ts |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
152 |
handle TERM _ => (1, one, ts) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
153 |
in (n, mk_prod ts') end; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
154 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
155 |
(*Find first coefficient-term THAT MATCHES u*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
156 |
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
157 |
| find_first_coeff past u (t::terms) = |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
158 |
let val (n,u') = dest_coeff t |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
159 |
in if u aconv u' then (n, rev past @ terms) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
160 |
else find_first_coeff (t::past) u terms |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
161 |
end |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
162 |
handle TERM _ => find_first_coeff (t::past) u terms; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
163 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
164 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
165 |
(*Simplify #1*n and n*#1 to n*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
166 |
val add_0s = map (rename_numerals NatBin.thy) [add_0, add_0_right]; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
167 |
val mult_1s = map (rename_numerals NatBin.thy) [mult_1, mult_1_right]; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
168 |
|
8865 | 169 |
(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*) |
170 |
val simplify_meta_eq = |
|
171 |
Int_Numeral_Simprocs.simplify_meta_eq |
|
172 |
[numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right, |
|
173 |
mult_0, mult_0_right, mult_1, mult_1_right]; |
|
174 |
||
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
175 |
structure CancelNumeralsCommon = |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
176 |
struct |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
177 |
val mk_sum = mk_sum |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
178 |
val dest_sum = dest_Sucs_sum |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
179 |
val mk_coeff = mk_coeff |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
180 |
val dest_coeff = dest_coeff |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
181 |
val find_first_coeff = find_first_coeff [] |
8799 | 182 |
val trans_tac = trans_tac |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
183 |
val norm_tac = ALLGOALS |
8785 | 184 |
(simp_tac (HOL_ss addsimps add_0s@mult_1s@ |
8776 | 185 |
[add_0, Suc_eq_add_numeral_1]@add_ac)) |
8785 | 186 |
THEN ALLGOALS (simp_tac |
187 |
(HOL_ss addsimps bin_simps@add_ac@mult_ac)) |
|
8766 | 188 |
val numeral_simp_tac = ALLGOALS |
189 |
(simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps)) |
|
8865 | 190 |
val simplify_meta_eq = simplify_meta_eq |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
191 |
end; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
192 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
193 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
194 |
structure EqCancelNumerals = CancelNumeralsFun |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
195 |
(open CancelNumeralsCommon |
8776 | 196 |
val prove_conv = prove_conv "nateq_cancel_numerals" |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
197 |
val mk_bal = HOLogic.mk_eq |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
198 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT |
8776 | 199 |
val bal_add1 = nat_eq_add_iff1 RS trans |
200 |
val bal_add2 = nat_eq_add_iff2 RS trans |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
201 |
); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
202 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
203 |
structure LessCancelNumerals = CancelNumeralsFun |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
204 |
(open CancelNumeralsCommon |
8776 | 205 |
val prove_conv = prove_conv "natless_cancel_numerals" |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
206 |
val mk_bal = HOLogic.mk_binrel "op <" |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
207 |
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT |
8776 | 208 |
val bal_add1 = nat_less_add_iff1 RS trans |
209 |
val bal_add2 = nat_less_add_iff2 RS trans |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
210 |
); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
211 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
212 |
structure LeCancelNumerals = CancelNumeralsFun |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
213 |
(open CancelNumeralsCommon |
8776 | 214 |
val prove_conv = prove_conv "natle_cancel_numerals" |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
215 |
val mk_bal = HOLogic.mk_binrel "op <=" |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
216 |
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT |
8776 | 217 |
val bal_add1 = nat_le_add_iff1 RS trans |
218 |
val bal_add2 = nat_le_add_iff2 RS trans |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
219 |
); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
220 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
221 |
structure DiffCancelNumerals = CancelNumeralsFun |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
222 |
(open CancelNumeralsCommon |
8776 | 223 |
val prove_conv = prove_conv "natdiff_cancel_numerals" |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
224 |
val mk_bal = HOLogic.mk_binop "op -" |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
225 |
val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT |
8776 | 226 |
val bal_add1 = nat_diff_add_eq1 RS trans |
227 |
val bal_add2 = nat_diff_add_eq2 RS trans |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
228 |
); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
229 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
230 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
231 |
val cancel_numerals = |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
232 |
map prep_simproc |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
233 |
[("nateq_cancel_numerals", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
234 |
prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
235 |
"(l::nat) * m = n", "(l::nat) = m * n", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
236 |
"Suc m = n", "m = Suc n"], |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
237 |
EqCancelNumerals.proc), |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
238 |
("natless_cancel_numerals", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
239 |
prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
240 |
"(l::nat) * m < n", "(l::nat) < m * n", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
241 |
"Suc m < n", "m < Suc n"], |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
242 |
LessCancelNumerals.proc), |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
243 |
("natle_cancel_numerals", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
244 |
prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
245 |
"(l::nat) * m <= n", "(l::nat) <= m * n", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
246 |
"Suc m <= n", "m <= Suc n"], |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
247 |
LeCancelNumerals.proc), |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
248 |
("natdiff_cancel_numerals", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
249 |
prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
250 |
"(l::nat) * m - n", "(l::nat) - m * n", |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
251 |
"Suc m - n", "m - Suc n"], |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
252 |
DiffCancelNumerals.proc)]; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
253 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
254 |
|
8776 | 255 |
structure CombineNumeralsData = |
256 |
struct |
|
257 |
val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) |
|
258 |
val dest_sum = dest_Sucs_sum |
|
259 |
val mk_coeff = mk_coeff |
|
260 |
val dest_coeff = dest_coeff |
|
261 |
val left_distrib = left_add_mult_distrib RS trans |
|
262 |
val prove_conv = prove_conv "nat_combine_numerals" |
|
8799 | 263 |
val trans_tac = trans_tac |
8776 | 264 |
val norm_tac = ALLGOALS |
8785 | 265 |
(simp_tac (HOL_ss addsimps add_0s@mult_1s@ |
8776 | 266 |
[add_0, Suc_eq_add_numeral_1]@add_ac)) |
8785 | 267 |
THEN ALLGOALS (simp_tac |
268 |
(HOL_ss addsimps bin_simps@add_ac@mult_ac)) |
|
8776 | 269 |
val numeral_simp_tac = ALLGOALS |
270 |
(simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps)) |
|
8865 | 271 |
val simplify_meta_eq = simplify_meta_eq |
8776 | 272 |
end; |
273 |
||
274 |
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); |
|
275 |
||
276 |
val combine_numerals = |
|
277 |
prep_simproc ("nat_combine_numerals", |
|
8787 | 278 |
prep_pats ["(i::nat) + j", "Suc (i + j)"], |
8776 | 279 |
CombineNumerals.proc); |
280 |
||
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
281 |
end; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
282 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
283 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
284 |
Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; |
8776 | 285 |
Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
286 |
|
8850
03cb6625c4a5
new default simprule for better compatibility with old setup
paulson
parents:
8799
diff
changeset
|
287 |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
288 |
(*examples: |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
289 |
print_depth 22; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
290 |
set proof_timing; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
291 |
set trace_simp; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
292 |
fun test s = (Goal s; by (Simp_tac 1)); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
293 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
294 |
(*cancel_numerals*) |
8787 | 295 |
test "l +( #2) + (#2) + #2 + (l + #2) + (oo + #2) = (uu::nat)"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
296 |
test "(#2*length xs < #2*length xs + j)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
297 |
test "(#2*length xs < length xs * #2 + j)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
298 |
test "#2*u = (u::nat)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
299 |
test "#2*u = Suc (u)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
300 |
test "(i + j + #12 + (k::nat)) - #15 = y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
301 |
test "(i + j + #12 + (k::nat)) - #5 = y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
302 |
test "Suc u - #2 = y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
303 |
test "Suc (Suc (Suc u)) - #2 = y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
304 |
test "(i + j + #2 + (k::nat)) - 1 = y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
305 |
test "(i + j + #1 + (k::nat)) - 2 = y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
306 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
307 |
test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)"; |
8865 | 308 |
test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
309 |
test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
310 |
test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
311 |
test "Suc ((u*v)*#4) - v*#3*u = w"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
312 |
test "Suc (Suc ((u*v)*#3)) - v*#3*u = w"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
313 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
314 |
test "(i + j + #12 + (k::nat)) = u + #15 + y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
315 |
test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
316 |
test "(i + j + #12 + (k::nat)) = u + #5 + y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
317 |
(*Suc*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
318 |
test "(i + j + #12 + k) = Suc (u + y)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
319 |
test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
320 |
test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
321 |
test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
322 |
test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
323 |
test "#2*y + #3*z + #2*u = Suc (u)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
324 |
test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
325 |
test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = #2*y' + #3*z' + #6*w' + #2*y' + #3*z' + u + (vv::nat)"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
326 |
test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)"; |
8776 | 327 |
test "(#2*n*m) < (#3*(m*n)) + (u::nat)"; |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
328 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
329 |
(*negative numerals: FAIL*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
330 |
test "(i + j + #-23 + (k::nat)) < u + #15 + y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
331 |
test "(i + j + #3 + (k::nat)) < u + #-15 + y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
332 |
test "(i + j + #-12 + (k::nat)) - #15 = y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
333 |
test "(i + j + #12 + (k::nat)) - #-15 = y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
334 |
test "(i + j + #-12 + (k::nat)) - #-15 = y"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
335 |
|
8776 | 336 |
(*combine_numerals*) |
337 |
test "k + #3*k = (u::nat)"; |
|
338 |
test "Suc (i + #3) = u"; |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
339 |
test "Suc (i + j + #3 + k) = u"; |
8776 | 340 |
test "k + j + #3*k + j = (u::nat)"; |
341 |
test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)"; |
|
342 |
test "(#2*n*m) + (#3*(m*n)) = (u::nat)"; |
|
343 |
(*negative numerals: FAIL*) |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
344 |
test "Suc (i + j + #-3 + k) = u"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
345 |
*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
346 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
347 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
348 |
(*** Prepare linear arithmetic for nat numerals ***) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
349 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
350 |
let |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
351 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
352 |
(* reduce contradictory <= to False *) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
353 |
val add_rules = |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
354 |
[add_nat_number_of, diff_nat_number_of, mult_nat_number_of, |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
355 |
eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less, |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
356 |
le_Suc_number_of,le_number_of_Suc, |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
357 |
less_Suc_number_of,less_number_of_Suc, |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
358 |
Suc_eq_number_of,eq_number_of_Suc, |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
359 |
eq_number_of_0, eq_0_number_of, less_0_number_of, |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
360 |
nat_number_of, Let_number_of, if_True, if_False]; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
361 |
|
8776 | 362 |
val simprocs = [Nat_Times_Assoc.conv, |
363 |
Nat_Numeral_Simprocs.combine_numerals]@ |
|
364 |
Nat_Numeral_Simprocs.cancel_numerals; |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
365 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
366 |
in |
8776 | 367 |
LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules |
368 |
addsimps basic_renamed_arith_simps |
|
369 |
addsimprocs simprocs |
|
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
370 |
end; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
371 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
372 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
373 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
374 |
(** For simplifying Suc m - #n **) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
375 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
376 |
Goal "#0 < n ==> Suc m - n = m - (n - #1)"; |
8865 | 377 |
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
378 |
qed "Suc_diff_eq_diff_pred"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
379 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
380 |
(*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
|
381 |
but with some redundant inequality tests.*) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
382 |
|
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8877
diff
changeset
|
383 |
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
|
384 |
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
|
385 |
by (Asm_simp_tac 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
386 |
by (stac less_number_of_Suc 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
387 |
by (Simp_tac 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
388 |
qed "neg_number_of_bin_pred_iff_0"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
389 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
390 |
Goal "neg (number_of (bin_minus v)) ==> \ |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
391 |
\ Suc m - (number_of v) = m - (number_of (bin_pred v))"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
392 |
by (stac Suc_diff_eq_diff_pred 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
393 |
by (Simp_tac 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
394 |
by (Simp_tac 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
395 |
by (asm_full_simp_tac |
8865 | 396 |
(simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym, |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
397 |
neg_number_of_bin_pred_iff_0]) 1); |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
398 |
qed "Suc_diff_number_of"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
399 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
400 |
(* now redundant because of the inverse_fold simproc |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
401 |
Addsimps [Suc_diff_number_of]; *) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
402 |
|
8865 | 403 |
Goal "nat_case a f (number_of v) = \ |
404 |
\ (let pv = number_of (bin_pred v) in \ |
|
405 |
\ if neg pv then a else f (nat pv))"; |
|
406 |
by (simp_tac |
|
407 |
(simpset() addsplits [nat.split] |
|
408 |
addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1); |
|
409 |
qed "nat_case_number_of"; |
|
410 |
||
411 |
Goal "nat_case a f ((number_of v) + n) = \ |
|
412 |
\ (let pv = number_of (bin_pred v) in \ |
|
413 |
\ if neg pv then nat_case a f n else f (nat pv + n))"; |
|
414 |
by (stac add_eq_if 1); |
|
415 |
by (asm_simp_tac |
|
416 |
(simpset() addsplits [nat.split] |
|
417 |
addsimps [Let_def, neg_imp_number_of_eq_0, |
|
418 |
neg_number_of_bin_pred_iff_0]) 1); |
|
419 |
qed "nat_case_add_eq_if"; |
|
420 |
||
421 |
Addsimps [nat_case_number_of, nat_case_add_eq_if]; |
|
422 |
||
423 |
||
424 |
Goal "nat_rec a f (number_of v) = \ |
|
425 |
\ (let pv = number_of (bin_pred v) in \ |
|
426 |
\ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"; |
|
427 |
by (case_tac "(number_of v)::nat" 1); |
|
428 |
by (ALLGOALS (asm_simp_tac |
|
429 |
(simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0]))); |
|
430 |
by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1); |
|
431 |
qed "nat_rec_number_of"; |
|
432 |
||
433 |
Goal "nat_rec a f (number_of v + n) = \ |
|
434 |
\ (let pv = number_of (bin_pred v) in \ |
|
435 |
\ if neg pv then nat_rec a f n \ |
|
436 |
\ else f (nat pv + n) (nat_rec a f (nat pv + n)))"; |
|
437 |
by (stac add_eq_if 1); |
|
438 |
by (asm_simp_tac |
|
439 |
(simpset() addsplits [nat.split] |
|
440 |
addsimps [Let_def, neg_imp_number_of_eq_0, |
|
441 |
neg_number_of_bin_pred_iff_0]) 1); |
|
442 |
qed "nat_rec_add_eq_if"; |
|
443 |
||
444 |
Addsimps [nat_rec_number_of, nat_rec_add_eq_if]; |
|
445 |
||
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
446 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
447 |
(** For simplifying #m - Suc n **) |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
448 |
|
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
449 |
Goal "m - Suc n = (m - #1) - n"; |
8865 | 450 |
by (simp_tac (numeral_ss addsplits [nat_diff_split]) 1); |
8759
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
451 |
qed "diff_Suc_eq_diff_pred"; |
49154c960140
new file containing simproc invocations, from NatBin.ML
paulson
parents:
diff
changeset
|
452 |
|
8877 | 453 |
(*Obsolete because of natdiff_cancel_numerals |
454 |
Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred]; |
|
455 |
It LOOPS if #1 is being replaced by 1. |
|
456 |
*) |
|
8776 | 457 |
|
458 |
||
459 |
(** Evens and Odds, for Mutilated Chess Board **) |
|
460 |
||
461 |
(*Case analysis on b<#2*) |
|
462 |
Goal "(n::nat) < #2 ==> n = #0 | n = #1"; |
|
463 |
by (arith_tac 1); |
|
464 |
qed "less_2_cases"; |
|
465 |
||
466 |
Goal "Suc(Suc(m)) mod #2 = m mod #2"; |
|
467 |
by (subgoal_tac "m mod #2 < #2" 1); |
|
468 |
by (Asm_simp_tac 2); |
|
469 |
be (less_2_cases RS disjE) 1; |
|
470 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc]))); |
|
471 |
qed "mod2_Suc_Suc"; |
|
472 |
Addsimps [mod2_Suc_Suc]; |
|
473 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8877
diff
changeset
|
474 |
Goal "!!m::nat. (0 < m mod #2) = (m mod #2 = #1)"; |
8776 | 475 |
by (subgoal_tac "m mod #2 < #2" 1); |
476 |
by (Asm_simp_tac 2); |
|
477 |
by (auto_tac (claset(), simpset() delsimps [mod_less_divisor])); |
|
478 |
qed "mod2_gr_0"; |
|
479 |
Addsimps [mod2_gr_0, rename_numerals thy mod2_gr_0]; |
|
480 |
||
8877 | 481 |
(** Removal of small numerals: #0, #1 and (in additive positions) #2 **) |
482 |
||
483 |
Goal "#2 + n = Suc (Suc n)"; |
|
484 |
by (Simp_tac 1); |
|
485 |
qed "add_2_eq_Suc"; |
|
486 |
||
487 |
Goal "n + #2 = Suc (Suc n)"; |
|
488 |
by (Simp_tac 1); |
|
489 |
qed "add_2_eq_Suc'"; |
|
490 |
||
491 |
Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc']; |
|
492 |
||
493 |
(*Can be used to eliminate long strings of Sucs, but not by default*) |
|
494 |
Goal "Suc (Suc (Suc n)) = #3 + n"; |
|
495 |
by (Simp_tac 1); |
|
496 |
qed "Suc3_eq_add_3"; |