author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37388  793618618f78 
child 38864  4abe644fcea5 
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 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

8 
val combine_numerals: simproc 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

9 
val cancel_numerals: simproc list 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

10 
val cancel_factors: simproc list 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

11 
val cancel_numeral_factors: simproc list 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
30685
diff
changeset

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

13 

23164  14 
structure Nat_Numeral_Simprocs = 
15 
struct 

16 

17 
(*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

18 
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  19 
val numeral_sym_ss = HOL_ss addsimps numeral_syms; 
20 

21 
fun rename_numerals th = 

32010  22 
simplify numeral_sym_ss (Thm.transfer @{theory} th); 
23164  23 

24 
(*Utilities*) 

25 

26 
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

27 
fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); 
23164  28 

29 
fun find_first_numeral past (t::terms) = 

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

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

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

33 

34 
val zero = mk_number 0; 

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

35 
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus}; 
23164  36 

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

38 
fun mk_sum [] = zero 

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

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

41 

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

43 
fun long_mk_sum [] = HOLogic.zero 

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

45 

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

46 
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; 
23164  47 

48 

49 
(** Other simproc items **) 

50 

51 
val bin_simps = 

23471  52 
[@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, 
53 
@{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 

54 
@{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, 

55 
@{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 

56 
@{thm less_nat_number_of}, 

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

29039  58 
@{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps}; 
23164  59 

60 

61 
(*** CancelNumerals simprocs ***) 

62 

63 
val one = mk_number 1; 

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

64 
val mk_times = HOLogic.mk_binop @{const_name Groups.times}; 
23164  65 

66 
fun mk_prod [] = one 

67 
 mk_prod [t] = t 

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

69 
else mk_times (t, mk_prod ts); 

70 

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

71 
val dest_times = HOLogic.dest_bin @{const_name Groups.times} HOLogic.natT; 
23164  72 

73 
fun dest_prod t = 

74 
let val (t,u) = dest_times t 

75 
in dest_prod t @ dest_prod u end 

76 
handle TERM _ => [t]; 

77 

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

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

80 

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

82 
fun dest_coeff t = 

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

86 
in (n, mk_prod ts') end; 

87 

88 
(*Find first coefficientterm THAT MATCHES u*) 

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

90 
 find_first_coeff past u (t::terms) = 

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

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

93 
else find_first_coeff (t::past) u terms 

94 
end 

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

96 

97 

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

99 
Sucs and counting them.*) 

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

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

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

105 

106 
(*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

107 
fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true 
23164  108 
 is_numeral _ = false; 
109 

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

111 

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

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

114 
numeral in a coefficient position. This prevents nat_combine_numerals from 

115 
introducing numerals to goals.*) 

116 
fun dest_Sucs_sum relaxed t = 

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

118 
in 

119 
if relaxed orelse exists prod_has_numeral ts then 

120 
if k=0 then ts 

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

121 
else mk_number k :: ts 
23164  122 
else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t]) 
123 
end; 

124 

125 

126 
(*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

127 
val add_0s = map rename_numerals [@{thm Nat.add_0}, @{thm Nat.add_0_right}]; 
23164  128 
val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}]; 
129 

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

131 

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

133 
the arith prover.*) 

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

23164  136 

137 
val simplify_meta_eq = 

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

139 
([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right}, 
23471  140 
@{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules); 
23164  141 

142 

143 
(*** Applying CancelNumeralsFun ***) 

144 

145 
structure CancelNumeralsCommon = 

146 
struct 

147 
val mk_sum = (fn T:typ => mk_sum) 

148 
val dest_sum = dest_Sucs_sum true 

149 
val mk_coeff = mk_coeff 

150 
val dest_coeff = dest_coeff 

151 
val find_first_coeff = find_first_coeff [] 

31368  152 
fun trans_tac _ = Arith_Data.trans_tac 
23164  153 

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

154 
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ 
31790  155 
[@{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

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

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

160 

161 
val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; 

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

163 
val simplify_meta_eq = simplify_meta_eq 

164 
end; 

165 

166 

167 
structure EqCancelNumerals = CancelNumeralsFun 

168 
(open CancelNumeralsCommon 

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

169 
val prove_conv = Arith_Data.prove_conv 
23164  170 
val mk_bal = HOLogic.mk_eq 
171 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT 

23471  172 
val bal_add1 = @{thm nat_eq_add_iff1} RS trans 
173 
val bal_add2 = @{thm nat_eq_add_iff2} RS trans 

23164  174 
); 
175 

176 
structure LessCancelNumerals = CancelNumeralsFun 

177 
(open CancelNumeralsCommon 

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

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

179 
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

180 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT 
23471  181 
val bal_add1 = @{thm nat_less_add_iff1} RS trans 
182 
val bal_add2 = @{thm nat_less_add_iff2} RS trans 

23164  183 
); 
184 

185 
structure LeCancelNumerals = CancelNumeralsFun 

186 
(open CancelNumeralsCommon 

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

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

188 
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

189 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT 
23471  190 
val bal_add1 = @{thm nat_le_add_iff1} RS trans 
191 
val bal_add2 = @{thm nat_le_add_iff2} RS trans 

23164  192 
); 
193 

194 
structure DiffCancelNumerals = CancelNumeralsFun 

195 
(open CancelNumeralsCommon 

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

196 
val prove_conv = Arith_Data.prove_conv 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

197 
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

198 
val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT 
23471  199 
val bal_add1 = @{thm nat_diff_add_eq1} RS trans 
200 
val bal_add2 = @{thm nat_diff_add_eq2} RS trans 

23164  201 
); 
202 

203 

204 
val cancel_numerals = 

32155  205 
map (Arith_Data.prep_simproc @{theory}) 
23164  206 
[("nateq_cancel_numerals", 
207 
["(l::nat) + m = n", "(l::nat) = m + n", 

208 
"(l::nat) * m = n", "(l::nat) = m * n", 

209 
"Suc m = n", "m = Suc n"], 

210 
K EqCancelNumerals.proc), 

211 
("natless_cancel_numerals", 

212 
["(l::nat) + m < n", "(l::nat) < m + n", 

213 
"(l::nat) * m < n", "(l::nat) < m * n", 

214 
"Suc m < n", "m < Suc n"], 

215 
K LessCancelNumerals.proc), 

216 
("natle_cancel_numerals", 

217 
["(l::nat) + m <= n", "(l::nat) <= m + n", 

218 
"(l::nat) * m <= n", "(l::nat) <= m * n", 

219 
"Suc m <= n", "m <= Suc n"], 

220 
K LeCancelNumerals.proc), 

221 
("natdiff_cancel_numerals", 

222 
["((l::nat) + m)  n", "(l::nat)  (m + n)", 

223 
"(l::nat) * m  n", "(l::nat)  m * n", 

224 
"Suc m  n", "m  Suc n"], 

225 
K DiffCancelNumerals.proc)]; 

226 

227 

228 
(*** Applying CombineNumeralsFun ***) 

229 

230 
structure CombineNumeralsData = 

231 
struct 

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

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

233 
val iszero = (fn x => x = 0) 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24431
diff
changeset

234 
val add = op + 
23164  235 
val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *) 
236 
val dest_sum = dest_Sucs_sum false 

237 
val mk_coeff = mk_coeff 

238 
val dest_coeff = dest_coeff 

23471  239 
val left_distrib = @{thm left_add_mult_distrib} RS trans 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
29269
diff
changeset

240 
val prove_conv = Arith_Data.prove_conv_nohyps 
31368  241 
fun trans_tac _ = Arith_Data.trans_tac 
23164  242 

31790  243 
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

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

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

248 

249 
val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps; 

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

251 
val simplify_meta_eq = simplify_meta_eq 

252 
end; 

253 

254 
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); 

255 

256 
val combine_numerals = 

32155  257 
Arith_Data.prep_simproc @{theory} 
258 
("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc); 

23164  259 

260 

261 
(*** Applying CancelNumeralFactorFun ***) 

262 

263 
structure CancelNumeralFactorCommon = 

264 
struct 

265 
val mk_coeff = mk_coeff 

266 
val dest_coeff = dest_coeff 

31368  267 
fun trans_tac _ = Arith_Data.trans_tac 
23164  268 

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

269 
val norm_ss1 = Numeral_Simprocs.num_ss addsimps 
31790  270 
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

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

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

275 

276 
val numeral_simp_ss = HOL_ss addsimps bin_simps 

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

278 
val simplify_meta_eq = simplify_meta_eq 

279 
end 

280 

281 
structure DivCancelNumeralFactor = CancelNumeralFactorFun 

282 
(open CancelNumeralFactorCommon 

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

283 
val prove_conv = Arith_Data.prove_conv 
23164  284 
val mk_bal = HOLogic.mk_binop @{const_name Divides.div} 
285 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT 

23471  286 
val cancel = @{thm nat_mult_div_cancel1} RS trans 
23164  287 
val neg_exchanges = false 
288 
) 

289 

23969  290 
structure DvdCancelNumeralFactor = CancelNumeralFactorFun 
291 
(open CancelNumeralFactorCommon 

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

292 
val prove_conv = Arith_Data.prove_conv 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

293 
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

294 
val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT 
23969  295 
val cancel = @{thm nat_mult_dvd_cancel1} RS trans 
296 
val neg_exchanges = false 

297 
) 

298 

23164  299 
structure EqCancelNumeralFactor = CancelNumeralFactorFun 
300 
(open CancelNumeralFactorCommon 

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

301 
val prove_conv = Arith_Data.prove_conv 
23164  302 
val mk_bal = HOLogic.mk_eq 
303 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT 

23471  304 
val cancel = @{thm nat_mult_eq_cancel1} RS trans 
23164  305 
val neg_exchanges = false 
306 
) 

307 

308 
structure LessCancelNumeralFactor = CancelNumeralFactorFun 

309 
(open CancelNumeralFactorCommon 

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

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

311 
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

312 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT 
23471  313 
val cancel = @{thm nat_mult_less_cancel1} RS trans 
23164  314 
val neg_exchanges = true 
315 
) 

316 

317 
structure LeCancelNumeralFactor = CancelNumeralFactorFun 

318 
(open CancelNumeralFactorCommon 

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

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

320 
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

321 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT 
23471  322 
val cancel = @{thm nat_mult_le_cancel1} RS trans 
23164  323 
val neg_exchanges = true 
324 
) 

325 

326 
val cancel_numeral_factors = 

32155  327 
map (Arith_Data.prep_simproc @{theory}) 
23164  328 
[("nateq_cancel_numeral_factors", 
329 
["(l::nat) * m = n", "(l::nat) = m * n"], 

330 
K EqCancelNumeralFactor.proc), 

331 
("natless_cancel_numeral_factors", 

332 
["(l::nat) * m < n", "(l::nat) < m * n"], 

333 
K LessCancelNumeralFactor.proc), 

334 
("natle_cancel_numeral_factors", 

335 
["(l::nat) * m <= n", "(l::nat) <= m * n"], 

336 
K LeCancelNumeralFactor.proc), 

337 
("natdiv_cancel_numeral_factors", 

338 
["((l::nat) * m) div n", "(l::nat) div (m * n)"], 

23969  339 
K DivCancelNumeralFactor.proc), 
340 
("natdvd_cancel_numeral_factors", 

341 
["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], 

342 
K DvdCancelNumeralFactor.proc)]; 

23164  343 

344 

345 

346 
(*** Applying ExtractCommonTermFun ***) 

347 

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

349 
fun long_mk_prod [] = one 

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

351 

352 
(*Find first term that matches u*) 

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

354 
 find_first_t past u (t::terms) = 

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

356 
else find_first_t (t::past) u terms 

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

358 

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

30518  360 
val simplify_one = Arith_Data.simplify_meta_eq 
23164  361 
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}]; 
362 

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

363 
fun cancel_simplify_meta_eq ss cancel_th th = 
23164  364 
simplify_one ss (([th, cancel_th]) MRS trans); 
365 

366 
structure CancelFactorCommon = 

367 
struct 

368 
val mk_sum = (fn T:typ => long_mk_prod) 

369 
val dest_sum = dest_prod 

370 
val mk_coeff = mk_coeff 

371 
val dest_coeff = dest_coeff 

372 
val find_first = find_first_t [] 

31368  373 
fun trans_tac _ = Arith_Data.trans_tac 
23881  374 
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} 
23164  375 
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

376 
val simplify_meta_eq = cancel_simplify_meta_eq 
23164  377 
end; 
378 

379 
structure EqCancelFactor = ExtractCommonTermFun 

380 
(open CancelFactorCommon 

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

381 
val prove_conv = Arith_Data.prove_conv 
23164  382 
val mk_bal = HOLogic.mk_eq 
383 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT 

31368  384 
fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj} 
23164  385 
); 
386 

387 
structure LessCancelFactor = ExtractCommonTermFun 

388 
(open CancelFactorCommon 

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

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

390 
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

391 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT 
31368  392 
fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj} 
23164  393 
); 
394 

395 
structure LeCancelFactor = ExtractCommonTermFun 

396 
(open CancelFactorCommon 

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

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

398 
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

399 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT 
31368  400 
fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj} 
23164  401 
); 
402 

403 
structure DivideCancelFactor = ExtractCommonTermFun 

404 
(open CancelFactorCommon 

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

405 
val prove_conv = Arith_Data.prove_conv 
23164  406 
val mk_bal = HOLogic.mk_binop @{const_name Divides.div} 
407 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT 

31368  408 
fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj} 
23164  409 
); 
410 

23969  411 
structure DvdCancelFactor = ExtractCommonTermFun 
412 
(open CancelFactorCommon 

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

413 
val prove_conv = Arith_Data.prove_conv 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset

414 
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

415 
val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT 
31368  416 
fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj} 
23969  417 
); 
418 

23164  419 
val cancel_factor = 
32155  420 
map (Arith_Data.prep_simproc @{theory}) 
23164  421 
[("nat_eq_cancel_factor", 
422 
["(l::nat) * m = n", "(l::nat) = m * n"], 

423 
K EqCancelFactor.proc), 

424 
("nat_less_cancel_factor", 

425 
["(l::nat) * m < n", "(l::nat) < m * n"], 

426 
K LessCancelFactor.proc), 

427 
("nat_le_cancel_factor", 

428 
["(l::nat) * m <= n", "(l::nat) <= m * n"], 

429 
K LeCancelFactor.proc), 

430 
("nat_divide_cancel_factor", 

431 
["((l::nat) * m) div n", "(l::nat) div (m * n)"], 

23969  432 
K DivideCancelFactor.proc), 
433 
("nat_dvd_cancel_factor", 

434 
["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"], 

435 
K DvdCancelFactor.proc)]; 

23164  436 

437 
end; 

438 

439 

440 
Addsimprocs Nat_Numeral_Simprocs.cancel_numerals; 

441 
Addsimprocs [Nat_Numeral_Simprocs.combine_numerals]; 

442 
Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors; 

443 
Addsimprocs Nat_Numeral_Simprocs.cancel_factor; 

444 

445 

446 
(*examples: 

447 
print_depth 22; 

448 
set timing; 

449 
set trace_simp; 

450 
fun test s = (Goal s; by (Simp_tac 1)); 

451 

452 
(*cancel_numerals*) 

453 
test "l +( 2) + (2) + 2 + (l + 2) + (oo + 2) = (uu::nat)"; 

454 
test "(2*length xs < 2*length xs + j)"; 

455 
test "(2*length xs < length xs * 2 + j)"; 

456 
test "2*u = (u::nat)"; 

457 
test "2*u = Suc (u)"; 

458 
test "(i + j + 12 + (k::nat))  15 = y"; 

459 
test "(i + j + 12 + (k::nat))  5 = y"; 

460 
test "Suc u  2 = y"; 

461 
test "Suc (Suc (Suc u))  2 = y"; 

462 
test "(i + j + 2 + (k::nat))  1 = y"; 

463 
test "(i + j + 1 + (k::nat))  2 = y"; 

464 

465 
test "(2*x + (u*v) + y)  v*3*u = (w::nat)"; 

466 
test "(2*x*u*v + 5 + (u*v)*4 + y)  v*u*4 = (w::nat)"; 

467 
test "(2*x*u*v + (u*v)*4 + y)  v*u = (w::nat)"; 

468 
test "Suc (Suc (2*x*u*v + u*4 + y))  u = w"; 

469 
test "Suc ((u*v)*4)  v*3*u = w"; 

470 
test "Suc (Suc ((u*v)*3))  v*3*u = w"; 

471 

472 
test "(i + j + 12 + (k::nat)) = u + 15 + y"; 

473 
test "(i + j + 32 + (k::nat))  (u + 15 + y) = zz"; 

474 
test "(i + j + 12 + (k::nat)) = u + 5 + y"; 

475 
(*Suc*) 

476 
test "(i + j + 12 + k) = Suc (u + y)"; 

477 
test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)"; 

478 
test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"; 

479 
test "Suc (Suc (Suc (Suc (Suc (u + y)))))  5 = v"; 

480 
test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"; 

481 
test "2*y + 3*z + 2*u = Suc (u)"; 

482 
test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"; 

483 
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)"; 

484 
test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"; 

485 
test "(2*n*m) < (3*(m*n)) + (u::nat)"; 

486 

487 
test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0  Suc k => k)))))) <= Suc 0)"; 

488 

489 
test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1"; 

490 

491 
test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))"; 

492 

493 
test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \<A> e) ST mxr c))))))) <= length (compT P E A ST mxr e))"; 

494 

495 

496 
(*negative numerals: FAIL*) 

497 
test "(i + j + 23 + (k::nat)) < u + 15 + y"; 

498 
test "(i + j + 3 + (k::nat)) < u + 15 + y"; 

499 
test "(i + j + 12 + (k::nat))  15 = y"; 

500 
test "(i + j + 12 + (k::nat))  15 = y"; 

501 
test "(i + j + 12 + (k::nat))  15 = y"; 

502 

503 
(*combine_numerals*) 

504 
test "k + 3*k = (u::nat)"; 

505 
test "Suc (i + 3) = u"; 

506 
test "Suc (i + j + 3 + k) = u"; 

507 
test "k + j + 3*k + j = (u::nat)"; 

508 
test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)"; 

509 
test "(2*n*m) + (3*(m*n)) = (u::nat)"; 

510 
(*negative numerals: FAIL*) 

511 
test "Suc (i + j + 3 + k) = u"; 

512 

513 
(*cancel_numeral_factors*) 

514 
test "9*x = 12 * (y::nat)"; 

515 
test "(9*x) div (12 * (y::nat)) = z"; 

516 
test "9*x < 12 * (y::nat)"; 

517 
test "9*x <= 12 * (y::nat)"; 

518 

519 
(*cancel_factor*) 

520 
test "x*k = k*(y::nat)"; 

521 
test "k = k*(y::nat)"; 

522 
test "a*(b*c) = (b::nat)"; 

523 
test "a*(b*c) = d*(b::nat)*(x*a)"; 

524 

525 
test "x*k < k*(y::nat)"; 

526 
test "k < k*(y::nat)"; 

527 
test "a*(b*c) < (b::nat)"; 

528 
test "a*(b*c) < d*(b::nat)*(x*a)"; 

529 

530 
test "x*k <= k*(y::nat)"; 

531 
test "k <= k*(y::nat)"; 

532 
test "a*(b*c) <= (b::nat)"; 

533 
test "a*(b*c) <= d*(b::nat)*(x*a)"; 

534 

535 
test "(x*k) div (k*(y::nat)) = (uu::nat)"; 

536 
test "(k) div (k*(y::nat)) = (uu::nat)"; 

537 
test "(a*(b*c)) div ((b::nat)) = (uu::nat)"; 

538 
test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)"; 

539 
*) 