author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 45620  f2a587696afb 
child 51717  9e7d1c139569 
permissions  rwrr 
9548  1 
(* Title: ZF/arith_data.ML 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 

4 
Arithmetic simplification: cancellation of common terms 

5 
*) 

6 

7 
signature ARITH_DATA = 

8 
sig 

9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

9 
(*the main outcome*) 
9548  10 
val nat_cancel: simproc list 
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

11 
(*tools for use in similar applications*) 
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

12 
val gen_trans_tac: thm > thm option > tactic 
20113  13 
val prove_conv: string > tactic list > Proof.context > thm list > term * term > thm option 
16973  14 
val simplify_meta_eq: thm list > simpset > thm > thm 
9874  15 
(*debugging*) 
16 
structure EqCancelNumeralsData : CANCEL_NUMERALS_DATA 

17 
structure LessCancelNumeralsData : CANCEL_NUMERALS_DATA 

18 
structure DiffCancelNumeralsData : CANCEL_NUMERALS_DATA 

9548  19 
end; 
20 

9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

21 

9548  22 
structure ArithData: ARITH_DATA = 
23 
struct 

24 

25 
val iT = Ind_Syntax.iT; 

26 

41310  27 
val zero = Const(@{const_name zero}, iT); 
38513  28 
val succ = Const(@{const_name succ}, iT > iT); 
9548  29 
fun mk_succ t = succ $ t; 
30 
val one = mk_succ zero; 

31 

38513  32 
val mk_plus = FOLogic.mk_binop @{const_name Arith.add}; 
9548  33 

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

35 
fun mk_sum [] = zero 

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

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

38 

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

40 
fun long_mk_sum [] = zero 

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

42 

38513  43 
val dest_plus = FOLogic.dest_bin @{const_name Arith.add} iT; 
9548  44 

45 
(* dest_sum *) 

46 

41310  47 
fun dest_sum (Const(@{const_name zero},_)) = [] 
38513  48 
 dest_sum (Const(@{const_name succ},_) $ t) = one :: dest_sum t 
49 
 dest_sum (Const(@{const_name Arith.add},_) $ t $ u) = dest_sum t @ dest_sum u 

9548  50 
 dest_sum tm = [tm]; 
51 

52 
(*Apply the given rewrite (if present) just once*) 

15531  53 
fun gen_trans_tac th2 NONE = all_tac 
54 
 gen_trans_tac th2 (SOME th) = ALLGOALS (rtac (th RS th2)); 

9548  55 

56 
(*Use <> or = depending on the type of t*) 

57 
fun mk_eq_iff(t,u) = 

58 
if fastype_of t = iT then FOLogic.mk_eq(t,u) 

59 
else FOLogic.mk_iff(t,u); 

60 

9874  61 
(*We remove equality assumptions because they confuse the simplifier and 
62 
because only typechecking assumptions are necessary.*) 

13462  63 
fun is_eq_thm th = 
44058  64 
can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th)); 
9649
89155e48fa53
simproc bug fix: only TYPING assumptions are given to the simplifier
paulson
parents:
9570
diff
changeset

65 

9548  66 
fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct); 
67 

20113  68 
fun prove_conv name tacs ctxt prems (t,u) = 
15531  69 
if t aconv u then NONE 
9548  70 
else 
33317  71 
let val prems' = filter_out is_eq_thm prems 
44058  72 
val goal = Logic.list_implies (map Thm.prop_of prems', 
12134  73 
FOLogic.mk_Trueprop (mk_eq_iff (t, u))); 
20113  74 
in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs))) 
18678  75 
handle ERROR msg => 
15531  76 
(warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE) 
9548  77 
end; 
78 

32155  79 
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:
38513
diff
changeset

80 
Simplifier.simproc_global thy name pats proc; 
9548  81 

82 

13462  83 
(*** Use CancelNumerals simproc without binary numerals, 
9548  84 
just for cancellation ***) 
85 

38513  86 
val mk_times = FOLogic.mk_binop @{const_name Arith.mult}; 
9548  87 

88 
fun mk_prod [] = one 

89 
 mk_prod [t] = t 

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

91 
else mk_times (t, mk_prod ts); 

92 

38513  93 
val dest_times = FOLogic.dest_bin @{const_name Arith.mult} iT; 
9548  94 

95 
fun dest_prod t = 

96 
let val (t,u) = dest_times t 

97 
in dest_prod t @ dest_prod u end 

98 
handle TERM _ => [t]; 

99 

100 
(*Dummy version: the only arguments are 0 and 1*) 

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

101 
fun mk_coeff (0, t) = zero 
9548  102 
 mk_coeff (1, t) = t 
103 
 mk_coeff _ = raise TERM("mk_coeff", []); 

104 

105 
(*Dummy version: the "coefficient" is always 1. 

106 
In the result, the factors are sorted terms*) 

35408  107 
fun dest_coeff t = (1, mk_prod (sort Term_Ord.term_ord (dest_prod t))); 
9548  108 

109 
(*Find first coefficientterm THAT MATCHES u*) 

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

111 
 find_first_coeff past u (t::terms) = 

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

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

114 
else find_first_coeff (t::past) u terms 

115 
end 

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

117 

118 

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

24893  120 
val add_0s = [@{thm add_0_natify}, @{thm add_0_right_natify}]; 
121 
val add_succs = [@{thm add_succ}, @{thm add_succ_right}]; 

122 
val mult_1s = [@{thm mult_1_natify}, @{thm mult_1_right_natify}]; 

123 
val tc_rules = [@{thm natify_in_nat}, @{thm add_type}, @{thm diff_type}, @{thm mult_type}]; 

124 
val natifys = [@{thm natify_0}, @{thm natify_ident}, @{thm add_natify1}, @{thm add_natify2}, 

125 
@{thm diff_natify1}, @{thm diff_natify2}]; 

9548  126 

127 
(*Final simplification: cancel + and **) 

18328  128 
fun simplify_meta_eq rules = 
129 
let val ss0 = 

45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
44947
diff
changeset

130 
FOL_ss 
26287  131 
delsimps @{thms iff_simps} (*these could erase the whole rule!*) 
18328  132 
addsimps rules 
45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
44947
diff
changeset

133 
> fold Simplifier.add_eqcong [@{thm eq_cong2}, @{thm iff_cong2}] 
18328  134 
in fn ss => mk_meta_eq o simplify (Simplifier.inherit_context ss ss0) end; 
9548  135 

24893  136 
val final_rules = add_0s @ mult_1s @ [@{thm mult_0}, @{thm mult_0_right}]; 
9548  137 

138 
structure CancelNumeralsCommon = 

139 
struct 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13487
diff
changeset

140 
val mk_sum = (fn T:typ => mk_sum) 
9548  141 
val dest_sum = dest_sum 
142 
val mk_coeff = mk_coeff 

143 
val dest_coeff = dest_coeff 

144 
val find_first_coeff = find_first_coeff [] 

18328  145 

24893  146 
val norm_ss1 = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ @{thms add_ac} 
147 
val norm_ss2 = ZF_ss addsimps add_0s @ mult_1s @ @{thms add_ac} @ 

148 
@{thms mult_ac} @ tc_rules @ natifys 

16973  149 
fun norm_tac ss = 
18328  150 
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) 
151 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) 

152 
val numeral_simp_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys 

16973  153 
fun numeral_simp_tac ss = 
18328  154 
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 
9548  155 
val simplify_meta_eq = simplify_meta_eq final_rules 
156 
end; 

157 

9874  158 
(** The functor argumnets are declared as separate structures 
159 
so that they can be exported to ease debugging. **) 

9548  160 

13462  161 
structure EqCancelNumeralsData = 
9874  162 
struct 
163 
open CancelNumeralsCommon 

9548  164 
val prove_conv = prove_conv "nateq_cancel_numerals" 
165 
val mk_bal = FOLogic.mk_eq 

9649
89155e48fa53
simproc bug fix: only TYPING assumptions are given to the simplifier
paulson
parents:
9570
diff
changeset

166 
val dest_bal = FOLogic.dest_eq 
35409  167 
val bal_add1 = @{thm eq_add_iff} RS @{thm iff_trans} 
168 
val bal_add2 = @{thm eq_add_iff} RS @{thm iff_trans} 

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

169 
val trans_tac = gen_trans_tac @{thm iff_trans} 
9874  170 
end; 
171 

172 
structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData); 

9548  173 

13462  174 
structure LessCancelNumeralsData = 
9874  175 
struct 
176 
open CancelNumeralsCommon 

9548  177 
val prove_conv = prove_conv "natless_cancel_numerals" 
38513  178 
val mk_bal = FOLogic.mk_binrel @{const_name Ordinal.lt} 
179 
val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT 

35409  180 
val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans} 
181 
val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans} 

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

182 
val trans_tac = gen_trans_tac @{thm iff_trans} 
9874  183 
end; 
184 

185 
structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData); 

9548  186 

13462  187 
structure DiffCancelNumeralsData = 
9874  188 
struct 
189 
open CancelNumeralsCommon 

9548  190 
val prove_conv = prove_conv "natdiff_cancel_numerals" 
38513  191 
val mk_bal = FOLogic.mk_binop @{const_name Arith.diff} 
192 
val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT 

35409  193 
val bal_add1 = @{thm diff_add_eq} RS @{thm trans} 
194 
val bal_add2 = @{thm diff_add_eq} RS @{thm trans} 

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

195 
val trans_tac = gen_trans_tac @{thm trans} 
9874  196 
end; 
197 

198 
structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData); 

9548  199 

200 

201 
val nat_cancel = 

32155  202 
map (prep_simproc @{theory}) 
13462  203 
[("nateq_cancel_numerals", 
204 
["l #+ m = n", "l = m #+ n", 

205 
"l #* m = n", "l = m #* n", 

206 
"succ(m) = n", "m = succ(n)"], 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19250
diff
changeset

207 
(K EqCancelNumerals.proc)), 
13462  208 
("natless_cancel_numerals", 
209 
["l #+ m < n", "l < m #+ n", 

210 
"l #* m < n", "l < m #* n", 

211 
"succ(m) < n", "m < succ(n)"], 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19250
diff
changeset

212 
(K LessCancelNumerals.proc)), 
13462  213 
("natdiff_cancel_numerals", 
214 
["(l #+ m) # n", "l # (m #+ n)", 

215 
"(l #* m) # n", "l # (m #* n)", 

216 
"succ(m) # n", "m # succ(n)"], 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19250
diff
changeset

217 
(K DiffCancelNumerals.proc))]; 
9548  218 

219 
end; 

220 

13259  221 
Addsimprocs ArithData.nat_cancel; 
222 

223 

9548  224 
(*examples: 
225 
print_depth 22; 

226 
set timing; 

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

227 
set simp_trace; 
9548  228 
fun test s = (Goal s; by (Asm_simp_tac 1)); 
229 

230 
test "x #+ y = x #+ z"; 

231 
test "y #+ x = x #+ z"; 

232 
test "x #+ y #+ z = x #+ z"; 

233 
test "y #+ (z #+ x) = z #+ x"; 

234 
test "x #+ y #+ z = (z #+ y) #+ (x #+ w)"; 

235 
test "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)"; 

236 

237 
test "x #+ succ(y) = x #+ z"; 

238 
test "x #+ succ(y) = succ(z #+ x)"; 

239 
test "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)"; 

240 

241 
test "(x #+ y) # (x #+ z) = w"; 

242 
test "(y #+ x) # (x #+ z) = dd"; 

243 
test "(x #+ y #+ z) # (x #+ z) = dd"; 

244 
test "(y #+ (z #+ x)) # (z #+ x) = dd"; 

245 
test "(x #+ y #+ z) # ((z #+ y) #+ (x #+ w)) = dd"; 

246 
test "(x#*y #+ z) # ((z #+ y) #+ (y#*x #+ w)) = dd"; 

247 

248 
(*BAD occurrence of natify*) 

249 
test "(x #+ succ(y)) # (x #+ z) = dd"; 

250 

251 
test "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2"; 

252 

253 
test "(x #+ succ(y)) # (succ(z #+ x)) = dd"; 

254 
test "(succ(x) #+ succ(y) #+ z) # (succ(z #+ y) #+ succ(x #+ w)) = dd"; 

255 

256 
(*use of typing information*) 

257 
test "x : nat ==> x #+ y = x"; 

258 
test "x : nat > x #+ y = x"; 

259 
test "x : nat ==> x #+ y < x"; 

260 
test "x : nat ==> x < y#+x"; 

13126  261 
test "x : nat ==> x le succ(x)"; 
9548  262 

263 
(*fails: no typing information isn't visible*) 

264 
test "x #+ y = x"; 

265 

266 
test "x #+ y < x #+ z"; 

267 
test "y #+ x < x #+ z"; 

268 
test "x #+ y #+ z < x #+ z"; 

269 
test "y #+ z #+ x < x #+ z"; 

270 
test "y #+ (z #+ x) < z #+ x"; 

271 
test "x #+ y #+ z < (z #+ y) #+ (x #+ w)"; 

272 
test "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)"; 

273 

274 
test "x #+ succ(y) < x #+ z"; 

275 
test "x #+ succ(y) < succ(z #+ x)"; 

276 
test "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)"; 

277 

278 
test "x #+ succ(y) le succ(z #+ x)"; 

279 
*) 