102 necessary. Rewriting is faster if the formula is already |
102 necessary. Rewriting is faster if the formula is already |
103 in that form. |
103 in that form. |
104 *) |
104 *) |
105 |
105 |
106 fun sum_proc sg _ lhs = |
106 fun sum_proc sg _ lhs = |
107 let val _ = if !trace then writeln ("cancel_sums: LHS = " ^ |
107 let val _ = if !trace then tracing ("cancel_sums: LHS = " ^ |
108 string_of_cterm (cterm_of sg lhs)) |
108 string_of_cterm (cterm_of sg lhs)) |
109 else () |
109 else () |
110 val (head::tail) = terms lhs |
110 val (head::tail) = terms lhs |
111 val head' = negate head |
111 val head' = negate head |
112 val rhs = mk_sum (cancelled (head',tail)) |
112 val rhs = mk_sum (cancelled (head',tail)) |
113 and chead' = Thm.cterm_of sg head' |
113 and chead' = Thm.cterm_of sg head' |
114 val _ = if !trace then |
114 val _ = if !trace then |
115 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
115 tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
116 else () |
116 else () |
117 val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)) |
117 val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)) |
118 val thm = prove ct |
118 val thm = prove ct |
119 (fn _ => [rtac eq_reflection 1, |
119 (fn _ => [rtac eq_reflection 1, |
120 simp_tac prepare_ss 1, |
120 simp_tac prepare_ss 1, |
151 addsimps [add_0, add_0_right]; |
151 addsimps [add_0, add_0_right]; |
152 |
152 |
153 val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute]; |
153 val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute]; |
154 |
154 |
155 fun rel_proc sg _ (lhs as (rel$lt$rt)) = |
155 fun rel_proc sg _ (lhs as (rel$lt$rt)) = |
156 let val _ = if !trace then writeln ("cancel_relations: LHS = " ^ |
156 let val _ = if !trace then tracing ("cancel_relations: LHS = " ^ |
157 string_of_cterm (cterm_of sg lhs)) |
157 string_of_cterm (cterm_of sg lhs)) |
158 else () |
158 else () |
159 val ltms = terms lt |
159 val ltms = terms lt |
160 and rtms = terms rt |
160 and rtms = terms rt |
161 val common = (*inter_term miscounts repetitions, so squash them*) |
161 val common = (*inter_term miscounts repetitions, so squash them*) |
168 val lt' = cancelled ltms |
168 val lt' = cancelled ltms |
169 and rt' = cancelled rtms |
169 and rt' = cancelled rtms |
170 |
170 |
171 val rhs = rel$lt'$rt' |
171 val rhs = rel$lt'$rt' |
172 val _ = if !trace then |
172 val _ = if !trace then |
173 writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
173 tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs)) |
174 else () |
174 else () |
175 val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs)) |
175 val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs)) |
176 |
176 |
177 val thm = prove ct |
177 val thm = prove ct |
178 (fn _ => [rtac eq_reflection 1, |
178 (fn _ => [rtac eq_reflection 1, |