author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 44947  8ae418dfe561 
child 51717  9e7d1c139569 
permissions  rwrr 
23146  1 
(* Title: ZF/int_arith.ML 
2 
Author: Larry Paulson 

3 

4 
Simprocs for linear arithmetic. 

5 
*) 

6 

40312
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

7 
signature INT_NUMERAL_SIMPROCS = 
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

8 
sig 
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

9 
val cancel_numerals: simproc list 
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

10 
val combine_numerals: simproc 
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

11 
val combine_numerals_prod: simproc 
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

12 
end 
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

13 

dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

14 
structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS = 
23146  15 
struct 
16 

35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

17 
(* abstract syntax operations *) 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

18 

ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

19 
fun mk_bit 0 = @{term "0"} 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

20 
 mk_bit 1 = @{term "succ(0)"} 
40312
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

21 
 mk_bit _ = raise TERM ("mk_bit", []); 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

22 

ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

23 
fun dest_bit @{term "0"} = 0 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

24 
 dest_bit @{term "succ(0)"} = 1 
40312
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

25 
 dest_bit t = raise TERM ("dest_bit", [t]); 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

26 

ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

27 
fun mk_bin i = 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

28 
let 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

29 
fun term_of [] = @{term Pls} 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

30 
 term_of [~1] = @{term Min} 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

31 
 term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b; 
35123  32 
in term_of (Numeral_Syntax.make_binary i) end; 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

33 

ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

34 
fun dest_bin tm = 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

35 
let 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

36 
fun bin_of @{term Pls} = [] 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

37 
 bin_of @{term Min} = [~1] 
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

38 
 bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs 
40312
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

39 
 bin_of _ = raise TERM ("dest_bin", [tm]); 
35123  40 
in Numeral_Syntax.dest_binary (bin_of tm) end; 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

41 

ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

42 

23146  43 
(*Utilities*) 
44 

35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
35020
diff
changeset

45 
fun mk_numeral i = @{const integ_of} $ mk_bin i; 
23146  46 

40312
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

47 
fun dest_numeral (Const(@{const_name integ_of}, _) $ w) = dest_bin w 
dff9f73a3763
more conventional exceptions for abstract syntax operations  eliminated ancient SYS_ERROR;
wenzelm
parents:
38715
diff
changeset

48 
 dest_numeral t = raise TERM ("dest_numeral", [t]); 
23146  49 

50 
fun find_first_numeral past (t::terms) = 

51 
((dest_numeral t, rev past @ terms) 

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

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

54 

55 
val zero = mk_numeral 0; 

26059  56 
val mk_plus = FOLogic.mk_binop @{const_name "zadd"}; 
23146  57 

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

59 
fun mk_sum [] = zero 

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

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

62 

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

64 
fun long_mk_sum [] = zero 

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

66 

67 
(*decompose additions AND subtractions as a sum*) 

26059  68 
fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) = 
23146  69 
dest_summing (pos, t, dest_summing (pos, u, ts)) 
26059  70 
 dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) = 
23146  71 
dest_summing (pos, t, dest_summing (not pos, u, ts)) 
72 
 dest_summing (pos, t, ts) = 

27237  73 
if pos then t::ts else @{const zminus} $ t :: ts; 
23146  74 

75 
fun dest_sum t = dest_summing (true, t, []); 

76 

77 
val one = mk_numeral 1; 

26059  78 
val mk_times = FOLogic.mk_binop @{const_name "zmult"}; 
23146  79 

80 
fun mk_prod [] = one 

81 
 mk_prod [t] = t 

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

83 
else mk_times (t, mk_prod ts); 

84 

26190  85 
val dest_times = FOLogic.dest_bin @{const_name "zmult"} @{typ i}; 
23146  86 

87 
fun dest_prod t = 

88 
let val (t,u) = dest_times t 

89 
in dest_prod t @ dest_prod u end 

90 
handle TERM _ => [t]; 

91 

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

93 
fun mk_coeff (k, t) = mk_times (mk_numeral k, t); 

94 

95 
(*Express t as a product of (possibly) a numeral with other sorted terms*) 

26059  96 
fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t 
23146  97 
 dest_coeff sign t = 
35408  98 
let val ts = sort Term_Ord.term_ord (dest_prod t) 
23146  99 
val (n, ts') = find_first_numeral [] ts 
100 
handle TERM _ => (1, ts) 

101 
in (sign*n, mk_prod ts') end; 

102 

103 
(*Find first coefficientterm THAT MATCHES u*) 

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

105 
 find_first_coeff past u (t::terms) = 

106 
let val (n,u') = dest_coeff 1 t 

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

108 
else find_first_coeff (t::past) u terms 

109 
end 

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

111 

112 

113 
(*Simplify #1*n and n*#1 to n*) 

24893  114 
val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}]; 
23146  115 

24893  116 
val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify}, 
117 
@{thm zmult_minus1}, @{thm zmult_minus1_right}]; 

23146  118 

24893  119 
val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int}, 
120 
@{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @ 

121 
@{thms bin.intros}; 

122 
val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2}, 

123 
@{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2}, 

124 
@{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}]; 

23146  125 

126 
(*To perform binary arithmetic*) 

24893  127 
val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps}; 
23146  128 

129 
(*To evaluate binary negations of coefficients*) 

24893  130 
val zminus_simps = @{thms NCons_simps} @ 
35409  131 
[@{thm integ_of_minus} RS @{thm sym}, 
24893  132 
@{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min}, 
133 
@{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}]; 

23146  134 

135 
(*To let us treat subtraction as addition*) 

24893  136 
val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}]; 
23146  137 

35020
862a20ffa8e2
prefer explicit @{lemma} over adhoc forward reasoning;
wenzelm
parents:
32957
diff
changeset

138 
(*push the unary minus down*) 
862a20ffa8e2
prefer explicit @{lemma} over adhoc forward reasoning;
wenzelm
parents:
32957
diff
changeset

139 
val int_minus_mult_eq_1_to_2 = @{lemma "$ w $* z = w $* $ z" by simp}; 
23146  140 

141 
(*to extract again any uncancelled minuses*) 

142 
val int_minus_from_mult_simps = 

24893  143 
[@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}]; 
23146  144 

145 
(*combine unary minus with numeric literals, however nested within a product*) 

146 
val int_mult_minus_simps = 

35409  147 
[@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2]; 
23146  148 

32155  149 
fun prep_simproc thy (name, pats, proc) = 
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
35409
diff
changeset

150 
Simplifier.simproc_global thy name pats proc; 
23146  151 

152 
structure CancelNumeralsCommon = 

153 
struct 

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

155 
val dest_sum = dest_sum 

156 
val mk_coeff = mk_coeff 

157 
val dest_coeff = dest_coeff 1 

158 
val find_first_coeff = find_first_coeff [] 

44947
8ae418dfe561
dropped unused argument â€“ avoids problem with SML/NJ
haftmann
parents:
40878
diff
changeset

159 
val trans_tac = ArithData.gen_trans_tac @{thm iff_trans} 
23146  160 

24893  161 
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} 
23146  162 
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys 
24893  163 
val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys 
23146  164 
fun norm_tac ss = 
165 
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) 

166 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) 

167 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) 

168 

169 
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys 

170 
fun numeral_simp_tac ss = 

171 
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 

32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
30607
diff
changeset

172 
THEN ALLGOALS (asm_simp_tac (simpset_of (Simplifier.the_context ss))) 
23146  173 
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) 
174 
end; 

175 

176 

177 
structure EqCancelNumerals = CancelNumeralsFun 

178 
(open CancelNumeralsCommon 

179 
val prove_conv = ArithData.prove_conv "inteq_cancel_numerals" 

180 
val mk_bal = FOLogic.mk_eq 

181 
val dest_bal = FOLogic.dest_eq 

35409  182 
val bal_add1 = @{thm eq_add_iff1} RS @{thm iff_trans} 
183 
val bal_add2 = @{thm eq_add_iff2} RS @{thm iff_trans} 

23146  184 
); 
185 

186 
structure LessCancelNumerals = CancelNumeralsFun 

187 
(open CancelNumeralsCommon 

188 
val prove_conv = ArithData.prove_conv "intless_cancel_numerals" 

26059  189 
val mk_bal = FOLogic.mk_binrel @{const_name "zless"} 
26190  190 
val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i} 
35409  191 
val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans} 
192 
val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans} 

23146  193 
); 
194 

195 
structure LeCancelNumerals = CancelNumeralsFun 

196 
(open CancelNumeralsCommon 

197 
val prove_conv = ArithData.prove_conv "intle_cancel_numerals" 

26059  198 
val mk_bal = FOLogic.mk_binrel @{const_name "zle"} 
26190  199 
val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i} 
35409  200 
val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans} 
201 
val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans} 

23146  202 
); 
203 

204 
val cancel_numerals = 

32155  205 
map (prep_simproc @{theory}) 
23146  206 
[("inteq_cancel_numerals", 
207 
["l $+ m = n", "l = m $+ n", 

208 
"l $ m = n", "l = m $ n", 

209 
"l $* m = n", "l = m $* n"], 

210 
K EqCancelNumerals.proc), 

211 
("intless_cancel_numerals", 

212 
["l $+ m $< n", "l $< m $+ n", 

213 
"l $ m $< n", "l $< m $ n", 

214 
"l $* m $< n", "l $< m $* n"], 

215 
K LessCancelNumerals.proc), 

216 
("intle_cancel_numerals", 

217 
["l $+ m $<= n", "l $<= m $+ n", 

218 
"l $ m $<= n", "l $<= m $ n", 

219 
"l $* m $<= n", "l $<= m $* n"], 

220 
K LeCancelNumerals.proc)]; 

221 

222 

223 
(*version without the hyps argument*) 

224 
fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg []; 

225 

226 
structure CombineNumeralsData = 

227 
struct 

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

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

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

230 
val add = op + 
23146  231 
val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *) 
232 
val dest_sum = dest_sum 

233 
val mk_coeff = mk_coeff 

234 
val dest_coeff = dest_coeff 1 

35409  235 
val left_distrib = @{thm left_zadd_zmult_distrib} RS @{thm trans} 
23146  236 
val prove_conv = prove_conv_nohyps "int_combine_numerals" 
44947
8ae418dfe561
dropped unused argument â€“ avoids problem with SML/NJ
haftmann
parents:
40878
diff
changeset

237 
val trans_tac = ArithData.gen_trans_tac @{thm trans} 
23146  238 

24893  239 
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys 
23146  240 
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys 
24893  241 
val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys 
23146  242 
fun norm_tac ss = 
243 
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) 

244 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) 

245 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) 

246 

247 
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys 

248 
fun numeral_simp_tac ss = 

249 
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 

250 
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) 

251 
end; 

252 

253 
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); 

254 

255 
val combine_numerals = 

32155  256 
prep_simproc @{theory} 
257 
("int_combine_numerals", ["i $+ j", "i $ j"], K CombineNumerals.proc); 

23146  258 

259 

260 

261 
(** Constant folding for integer multiplication **) 

262 

263 
(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as 

264 
the "sum" of #3, x, #4; the literals are then multiplied*) 

265 

266 

267 
structure CombineNumeralsProdData = 

268 
struct 

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

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

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

271 
val add = op * 
23146  272 
val mk_sum = (fn T:typ => mk_prod) 
273 
val dest_sum = dest_prod 

274 
fun mk_coeff(k,t) = if t=one then mk_numeral k 

275 
else raise TERM("mk_coeff", []) 

276 
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*) 

35409  277 
val left_distrib = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans} 
23146  278 
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" 
44947
8ae418dfe561
dropped unused argument â€“ avoids problem with SML/NJ
haftmann
parents:
40878
diff
changeset

279 
val trans_tac = ArithData.gen_trans_tac @{thm trans} 
23146  280 

281 

282 

283 
val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps 

35409  284 
val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @ 
24893  285 
bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys 
23146  286 
fun norm_tac ss = 
287 
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) 

288 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) 

289 

290 
val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys 

291 
fun numeral_simp_tac ss = 

292 
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 

293 
val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s); 

294 
end; 

295 

296 

297 
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); 

298 

299 
val combine_numerals_prod = 

32155  300 
prep_simproc @{theory} 
301 
("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc); 

23146  302 

303 
end; 

304 

305 

306 
Addsimprocs Int_Numeral_Simprocs.cancel_numerals; 

307 
Addsimprocs [Int_Numeral_Simprocs.combine_numerals, 

308 
Int_Numeral_Simprocs.combine_numerals_prod]; 

309 

310 

311 
(*examples:*) 

312 
(* 

313 
print_depth 22; 

314 
set timing; 

40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40313
diff
changeset

315 
set simp_trace; 
23146  316 
fun test s = (Goal s; by (Asm_simp_tac 1)); 
317 
val sg = #sign (rep_thm (topthm())); 

318 
val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1)); 

319 
val (t,_) = FOLogic.dest_eq t; 

320 

321 
(*combine_numerals_prod (products of separate literals) *) 

322 
test "#5 $* x $* #3 = y"; 

323 

324 
test "y2 $+ ?x42 = y $+ y2"; 

325 

326 
test "oo : int ==> l $+ (l $+ #2) $+ oo = oo"; 

327 

328 
test "#9$*x $+ y = x$*#23 $+ z"; 

329 
test "y $+ x = x $+ z"; 

330 

331 
test "x : int ==> x $+ y $+ z = x $+ z"; 

332 
test "x : int ==> y $+ (z $+ x) = z $+ x"; 

333 
test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)"; 

334 
test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)"; 

335 

336 
test "#3 $* x $+ y $<= x $* #2 $+ z"; 

337 
test "y $+ x $<= x $+ z"; 

338 
test "x $+ y $+ z $<= x $+ z"; 

339 

340 
test "y $+ (z $+ x) $< z $+ x"; 

341 
test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)"; 

342 
test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)"; 

343 

344 
test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu"; 

345 
test "u : int ==> #2 $* u = u"; 

346 
test "(i $+ j $+ #12 $+ k) $ #15 = y"; 

347 
test "(i $+ j $+ #12 $+ k) $ #5 = y"; 

348 

349 
test "y $ b $< b"; 

350 
test "y $ (#3 $* b $+ c) $< b $ #2 $* c"; 

351 

352 
test "(#2 $* x $ (u $* v) $+ y) $ v $* #3 $* u = w"; 

353 
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $ v $* u $* #4 = w"; 

354 
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $ v $* u = w"; 

355 
test "u $* v $ (x $* u $* v $+ (u $* v) $* #4 $+ y) = w"; 

356 

357 
test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y"; 

358 
test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y"; 

359 

360 
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"; 

361 

362 
test "a $+ $(b$+c) $+ b = d"; 

363 
test "a $+ $(b$+c) $ b = d"; 

364 

365 
(*negative numerals*) 

366 
test "(i $+ j $+ #2 $+ k) $ (u $+ #5 $+ y) = zz"; 

367 
test "(i $+ j $+ #3 $+ k) $< u $+ #5 $+ y"; 

368 
test "(i $+ j $+ #3 $+ k) $< u $+ #6 $+ y"; 

369 
test "(i $+ j $+ #12 $+ k) $ #15 = y"; 

370 
test "(i $+ j $+ #12 $+ k) $ #15 = y"; 

371 
test "(i $+ j $+ #12 $+ k) $ #15 = y"; 

372 

373 
(*Multiplying separated numerals*) 

374 
Goal "#6 $* ($# x $* #2) = uu"; 

375 
Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) = uu"; 

376 
*) 

377 