author  huffman 
Fri, 11 Nov 2011 11:30:31 +0100  
changeset 45463  9a588a835c1e 
parent 45462  aba629d6cee5 
child 45668  0ea1c705eebb 
permissions  rwrr 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

1 
(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
23164  2 

3 
Simprocs for nat numerals. 

4 
*) 

5 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

6 
signature NAT_NUMERAL_SIMPROCS = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

7 
sig 
45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

8 
val combine_numerals: simpset > cterm > thm option 
45436
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45306
diff
changeset

9 
val eq_cancel_numerals: simpset > cterm > thm option 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45306
diff
changeset

10 
val less_cancel_numerals: simpset > cterm > thm option 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45306
diff
changeset

11 
val le_cancel_numerals: simpset > cterm > thm option 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45306
diff
changeset

12 
val diff_cancel_numerals: simpset > cterm > thm option 
45463
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

13 
val eq_cancel_numeral_factor: simpset > cterm > thm option 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

14 
val less_cancel_numeral_factor: simpset > cterm > thm option 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

15 
val le_cancel_numeral_factor: simpset > cterm > thm option 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

16 
val div_cancel_numeral_factor: simpset > cterm > thm option 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

17 
val dvd_cancel_numeral_factor: simpset > cterm > thm option 
45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

18 
val eq_cancel_factor: simpset > cterm > thm option 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

19 
val less_cancel_factor: simpset > cterm > thm option 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

20 
val le_cancel_factor: simpset > cterm > thm option 
45463
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

21 
val div_cancel_factor: simpset > cterm > thm option 
45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

22 
val dvd_cancel_factor: simpset > cterm > thm option 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

23 
end; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

24 

45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

25 
structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS = 
23164  26 
struct 
27 

28 
(*Maps n to #n for n = 0, 1, 2*) 

30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29269
diff
changeset

29 
val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym]; 
23164  30 
val numeral_sym_ss = HOL_ss addsimps numeral_syms; 
31 

44945  32 
val rename_numerals = simplify numeral_sym_ss o Thm.transfer @{theory}; 
23164  33 

34 
(*Utilities*) 

35 

36 
fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n; 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24431
diff
changeset

37 
fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); 
23164  38 

39 
fun find_first_numeral past (t::terms) = 

40 
((dest_number t, t, rev past @ terms) 

41 
handle TERM _ => find_first_numeral (t::past) terms) 

42 
 find_first_numeral past [] = raise TERM("find_first_numeral", []); 

43 

44 
val zero = mk_number 0; 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

45 
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; 
23164  46 

47 
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) 

48 
fun mk_sum [] = zero 

49 
 mk_sum [t,u] = mk_plus (t, u) 

50 
 mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 

51 

52 
(*this version ALWAYS includes a trailing zero*) 

53 
fun long_mk_sum [] = HOLogic.zero 

54 
 long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 

55 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

56 
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; 
23164  57 

58 

59 
(** Other simproc items **) 

60 

61 
val bin_simps = 

23471  62 
[@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, 
63 
@{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 

64 
@{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, 

65 
@{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 

66 
@{thm less_nat_number_of}, 

67 
@{thm Let_number_of}, @{thm nat_number_of}] @ 

29039  68 
@{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps}; 
23164  69 

70 

71 
(*** CancelNumerals simprocs ***) 

72 

73 
val one = mk_number 1; 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

74 
val mk_times = HOLogic.mk_binop @{const_name Groups.times}; 
23164  75 

76 
fun mk_prod [] = one 

77 
 mk_prod [t] = t 

78 
 mk_prod (t :: ts) = if t = one then mk_prod ts 

79 
else mk_times (t, mk_prod ts); 

80 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

81 
val dest_times = HOLogic.dest_bin @{const_name Groups.times} HOLogic.natT; 
23164  82 

83 
fun dest_prod t = 

84 
let val (t,u) = dest_times t 

85 
in dest_prod t @ dest_prod u end 

86 
handle TERM _ => [t]; 

87 

88 
(*DON'T do the obvious simplifications; that would create special cases*) 

89 
fun mk_coeff (k,t) = mk_times (mk_number k, t); 

90 

91 
(*Express t as a product of (possibly) a numeral with other factors, sorted*) 

92 
fun dest_coeff t = 

35408  93 
let val ts = sort Term_Ord.term_ord (dest_prod t) 
23164  94 
val (n, _, ts') = find_first_numeral [] ts 
95 
handle TERM _ => (1, one, ts) 

96 
in (n, mk_prod ts') end; 

97 

98 
(*Find first coefficientterm THAT MATCHES u*) 

99 
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 

100 
 find_first_coeff past u (t::terms) = 

101 
let val (n,u') = dest_coeff t 

102 
in if u aconv u' then (n, rev past @ terms) 

103 
else find_first_coeff (t::past) u terms 

104 
end 

105 
handle TERM _ => find_first_coeff (t::past) u terms; 

106 

107 

108 
(*Split up a sum into the list of its constituent terms, on the way removing any 

109 
Sucs and counting them.*) 

37388  110 
fun dest_Suc_sum (Const (@{const_name Suc}, _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts)) 
23164  111 
 dest_Suc_sum (t, (k,ts)) = 
112 
let val (t1,t2) = dest_plus t 

113 
in dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts))) end 

114 
handle TERM _ => (k, t::ts); 

115 

116 
(*Code for testing whether numerals are already used in the goal*) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25481
diff
changeset

117 
fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true 
23164  118 
 is_numeral _ = false; 
119 

120 
fun prod_has_numeral t = exists is_numeral (dest_prod t); 

121 

122 
(*The Sucs found in the term are converted to a binary numeral. If relaxed is false, 

123 
an exception is raised unless the original expression contains at least one 

124 
numeral in a coefficient position. This prevents nat_combine_numerals from 

125 
introducing numerals to goals.*) 

126 
fun dest_Sucs_sum relaxed t = 

127 
let val (k,ts) = dest_Suc_sum (t,(0,[])) 

128 
in 

129 
if relaxed orelse exists prod_has_numeral ts then 

130 
if k=0 then ts 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24431
diff
changeset

131 
else mk_number k :: ts 
23164  132 
else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t]) 
133 
end; 

134 

135 

136 
(*Simplify 1*n and n*1 to n*) 

35064
1bdef0c013d3
hide fact names clashing with fact names from Group.thy
haftmann
parents:
35050
diff
changeset

137 
val add_0s = map rename_numerals [@{thm Nat.add_0}, @{thm Nat.add_0_right}]; 
23164  138 
val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}]; 
139 

140 
(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*) 

141 

142 
(*And these help the simproc return False when appropriate, which helps 

143 
the arith prover.*) 

23881  144 
val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc}, 
145 
@{thm Suc_not_Zero}, @{thm le_0_eq}]; 

23164  146 

147 
val simplify_meta_eq = 

30518  148 
Arith_Data.simplify_meta_eq 
35064
1bdef0c013d3
hide fact names clashing with fact names from Group.thy
haftmann
parents:
35050
diff
changeset

149 
([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right}, 
23471  150 
@{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules); 
23164  151 

152 

153 
(*** Applying CancelNumeralsFun ***) 

154 

155 
structure CancelNumeralsCommon = 

44945  156 
struct 
157 
val mk_sum = (fn T : typ => mk_sum) 

158 
val dest_sum = dest_Sucs_sum true 

159 
val mk_coeff = mk_coeff 

160 
val dest_coeff = dest_coeff 

161 
val find_first_coeff = find_first_coeff [] 

44947
8ae418dfe561
dropped unused argument – avoids problem with SML/NJ
haftmann
parents:
44945
diff
changeset

162 
val trans_tac = Numeral_Simprocs.trans_tac 
23164  163 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

164 
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ 
31790  165 
[@{thm Suc_eq_plus1_left}] @ @{thms add_ac} 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

166 
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} 
23164  167 
fun norm_tac ss = 
168 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 

169 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) 

170 

171 
val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; 

172 
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)); 

173 
val simplify_meta_eq = simplify_meta_eq 

44945  174 
val prove_conv = Arith_Data.prove_conv 
175 
end; 

23164  176 

177 
structure EqCancelNumerals = CancelNumeralsFun 

178 
(open CancelNumeralsCommon 

179 
val mk_bal = HOLogic.mk_eq 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
37388
diff
changeset

180 
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT 
23471  181 
val bal_add1 = @{thm nat_eq_add_iff1} RS trans 
182 
val bal_add2 = @{thm nat_eq_add_iff2} RS trans 

23164  183 
); 
184 

185 
structure LessCancelNumerals = CancelNumeralsFun 

186 
(open CancelNumeralsCommon 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

187 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

188 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT 
23471  189 
val bal_add1 = @{thm nat_less_add_iff1} RS trans 
190 
val bal_add2 = @{thm nat_less_add_iff2} RS trans 

23164  191 
); 
192 

193 
structure LeCancelNumerals = CancelNumeralsFun 

194 
(open CancelNumeralsCommon 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

195 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

196 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT 
23471  197 
val bal_add1 = @{thm nat_le_add_iff1} RS trans 
198 
val bal_add2 = @{thm nat_le_add_iff2} RS trans 

23164  199 
); 
200 

201 
structure DiffCancelNumerals = CancelNumeralsFun 

202 
(open CancelNumeralsCommon 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

203 
val mk_bal = HOLogic.mk_binop @{const_name Groups.minus} 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

204 
val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT 
23471  205 
val bal_add1 = @{thm nat_diff_add_eq1} RS trans 
206 
val bal_add2 = @{thm nat_diff_add_eq2} RS trans 

23164  207 
); 
208 

45436
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45306
diff
changeset

209 
fun eq_cancel_numerals ss ct = EqCancelNumerals.proc ss (term_of ct) 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45306
diff
changeset

210 
fun less_cancel_numerals ss ct = LessCancelNumerals.proc ss (term_of ct) 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45306
diff
changeset

211 
fun le_cancel_numerals ss ct = LeCancelNumerals.proc ss (term_of ct) 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45306
diff
changeset

212 
fun diff_cancel_numerals ss ct = DiffCancelNumerals.proc ss (term_of ct) 
23164  213 

214 

215 
(*** Applying CombineNumeralsFun ***) 

216 

217 
structure CombineNumeralsData = 

44945  218 
struct 
219 
type coeff = int 

220 
val iszero = (fn x => x = 0) 

221 
val add = op + 

222 
val mk_sum = (fn T : typ => long_mk_sum) (*to work for 2*x + 3*x *) 

223 
val dest_sum = dest_Sucs_sum false 

224 
val mk_coeff = mk_coeff 

225 
val dest_coeff = dest_coeff 

226 
val left_distrib = @{thm left_add_mult_distrib} RS trans 

227 
val prove_conv = Arith_Data.prove_conv_nohyps 

44947
8ae418dfe561
dropped unused argument – avoids problem with SML/NJ
haftmann
parents:
44945
diff
changeset

228 
val trans_tac = Numeral_Simprocs.trans_tac 
23164  229 

31790  230 
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac} 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

231 
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} 
23164  232 
fun norm_tac ss = 
233 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 

234 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) 

235 

236 
val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; 

237 
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 

44945  238 
val simplify_meta_eq = simplify_meta_eq 
239 
end; 

23164  240 

241 
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); 

242 

45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

243 
fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct) 
23164  244 

245 

246 
(*** Applying CancelNumeralFactorFun ***) 

247 

248 
structure CancelNumeralFactorCommon = 

44945  249 
struct 
250 
val mk_coeff = mk_coeff 

251 
val dest_coeff = dest_coeff 

44947
8ae418dfe561
dropped unused argument – avoids problem with SML/NJ
haftmann
parents:
44945
diff
changeset

252 
val trans_tac = Numeral_Simprocs.trans_tac 
23164  253 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

254 
val norm_ss1 = Numeral_Simprocs.num_ss addsimps 
31790  255 
numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac} 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

256 
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} 
23164  257 
fun norm_tac ss = 
258 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 

259 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) 

260 

261 
val numeral_simp_ss = HOL_ss addsimps bin_simps 

262 
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 

44945  263 
val simplify_meta_eq = simplify_meta_eq 
264 
val prove_conv = Arith_Data.prove_conv 

265 
end; 

23164  266 

267 
structure DivCancelNumeralFactor = CancelNumeralFactorFun 

268 
(open CancelNumeralFactorCommon 

269 
val mk_bal = HOLogic.mk_binop @{const_name Divides.div} 

270 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT 

23471  271 
val cancel = @{thm nat_mult_div_cancel1} RS trans 
23164  272 
val neg_exchanges = false 
44945  273 
); 
23164  274 

23969  275 
structure DvdCancelNumeralFactor = CancelNumeralFactorFun 
276 
(open CancelNumeralFactorCommon 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

277 
val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd} 
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

278 
val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT 
23969  279 
val cancel = @{thm nat_mult_dvd_cancel1} RS trans 
280 
val neg_exchanges = false 

44945  281 
); 
23969  282 

23164  283 
structure EqCancelNumeralFactor = CancelNumeralFactorFun 
284 
(open CancelNumeralFactorCommon 

285 
val mk_bal = HOLogic.mk_eq 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
37388
diff
changeset

286 
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT 
23471  287 
val cancel = @{thm nat_mult_eq_cancel1} RS trans 
23164  288 
val neg_exchanges = false 
44945  289 
); 
23164  290 

291 
structure LessCancelNumeralFactor = CancelNumeralFactorFun 

292 
(open CancelNumeralFactorCommon 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

293 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

294 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT 
23471  295 
val cancel = @{thm nat_mult_less_cancel1} RS trans 
23164  296 
val neg_exchanges = true 
44945  297 
); 
23164  298 

299 
structure LeCancelNumeralFactor = CancelNumeralFactorFun 

300 
(open CancelNumeralFactorCommon 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

301 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

302 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT 
23471  303 
val cancel = @{thm nat_mult_le_cancel1} RS trans 
23164  304 
val neg_exchanges = true 
305 
) 

306 

45463
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

307 
fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct) 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

308 
fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct) 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

309 
fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct) 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

310 
fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct) 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

311 
fun dvd_cancel_numeral_factor ss ct = DvdCancelNumeralFactor.proc ss (term_of ct) 
23164  312 

313 

314 
(*** Applying ExtractCommonTermFun ***) 

315 

316 
(*this version ALWAYS includes a trailing one*) 

317 
fun long_mk_prod [] = one 

318 
 long_mk_prod (t :: ts) = mk_times (t, mk_prod ts); 

319 

320 
(*Find first term that matches u*) 

321 
fun find_first_t past u [] = raise TERM("find_first_t", []) 

322 
 find_first_t past u (t::terms) = 

323 
if u aconv t then (rev past @ terms) 

324 
else find_first_t (t::past) u terms 

325 
handle TERM _ => find_first_t (t::past) u terms; 

326 

327 
(** Final simplification for the CancelFactor simprocs **) 

30518  328 
val simplify_one = Arith_Data.simplify_meta_eq 
23164  329 
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}]; 
330 

30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

331 
fun cancel_simplify_meta_eq ss cancel_th th = 
23164  332 
simplify_one ss (([th, cancel_th]) MRS trans); 
333 

334 
structure CancelFactorCommon = 

44945  335 
struct 
336 
val mk_sum = (fn T : typ => long_mk_prod) 

337 
val dest_sum = dest_prod 

338 
val mk_coeff = mk_coeff 

339 
val dest_coeff = dest_coeff 

340 
val find_first = find_first_t [] 

44947
8ae418dfe561
dropped unused argument – avoids problem with SML/NJ
haftmann
parents:
44945
diff
changeset

341 
val trans_tac = Numeral_Simprocs.trans_tac 
23881  342 
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} 
23164  343 
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

344 
val simplify_meta_eq = cancel_simplify_meta_eq 
45270
d5b5c9259afd
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents:
44947
diff
changeset

345 
fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) 
44945  346 
end; 
23164  347 

348 
structure EqCancelFactor = ExtractCommonTermFun 

349 
(open CancelFactorCommon 

350 
val mk_bal = HOLogic.mk_eq 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
37388
diff
changeset

351 
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT 
31368  352 
fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj} 
23164  353 
); 
354 

44945  355 
structure LeCancelFactor = ExtractCommonTermFun 
356 
(open CancelFactorCommon 

357 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} 

358 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT 

359 
fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj} 

360 
); 

361 

23164  362 
structure LessCancelFactor = ExtractCommonTermFun 
363 
(open CancelFactorCommon 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

364 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35064
diff
changeset

365 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT 
31368  366 
fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj} 
23164  367 
); 
368 

369 
structure DivideCancelFactor = ExtractCommonTermFun 

370 
(open CancelFactorCommon 

371 
val mk_bal = HOLogic.mk_binop @{const_name Divides.div} 

372 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT 

31368  373 
fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj} 
23164  374 
); 
375 

23969  376 
structure DvdCancelFactor = ExtractCommonTermFun 
377 
(open CancelFactorCommon 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

378 
val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd} 
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

379 
val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT 
31368  380 
fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj} 
23969  381 
); 
382 

45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

383 
fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct) 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

384 
fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct) 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

385 
fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct) 
45463
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

386 
fun div_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct) 
45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45436
diff
changeset

387 
fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct) 
23164  388 

389 
end; 