161 K DiffCancelSums.proc)]; |
161 K DiffCancelSums.proc)]; |
162 |
162 |
163 val arith_data_setup = |
163 val arith_data_setup = |
164 Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums); |
164 Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums); |
165 |
165 |
166 |
|
167 (* FIXME dead code *) |
|
168 (* antisymmetry: |
|
169 combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y |
|
170 |
|
171 local |
|
172 val antisym = mk_meta_eq order_antisym |
|
173 val not_lessD = @{thm linorder_not_less} RS iffD1 |
|
174 fun prp t thm = (#prop(rep_thm thm) = t) |
|
175 in |
|
176 fun antisym_eq prems thm = |
|
177 let |
|
178 val r = #prop(rep_thm thm); |
|
179 in |
|
180 case r of |
|
181 Tr $ ((c as Const(@{const_name HOL.less_eq},T)) $ s $ t) => |
|
182 let val r' = Tr $ (c $ t $ s) |
|
183 in |
|
184 case Library.find_first (prp r') prems of |
|
185 NONE => |
|
186 let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ s $ t)) |
|
187 in case Library.find_first (prp r') prems of |
|
188 NONE => [] |
|
189 | SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)] |
|
190 end |
|
191 | SOME thm' => [thm' RS (thm RS antisym)] |
|
192 end |
|
193 | Tr $ (Const("Not",_) $ (Const(@{const_name HOL.less},T) $ s $ t)) => |
|
194 let val r' = Tr $ (Const(@{const_name HOL.less_eq},T) $ s $ t) |
|
195 in |
|
196 case Library.find_first (prp r') prems of |
|
197 NONE => |
|
198 let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ t $ s)) |
|
199 in case Library.find_first (prp r') prems of |
|
200 NONE => [] |
|
201 | SOME thm' => |
|
202 [(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)] |
|
203 end |
|
204 | SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)] |
|
205 end |
|
206 | _ => [] |
|
207 end |
|
208 handle THM _ => [] |
|
209 end; |
|
210 *) |
|
211 |
|
212 end; |
166 end; |
213 |
167 |
214 open ArithData; |
168 open ArithData; |