324 val hypreal_mult_less_0_iff = thm"hypreal_mult_less_0_iff"; |
324 val hypreal_mult_less_0_iff = thm"hypreal_mult_less_0_iff"; |
325 val hypreal_mult_le_0_iff = thm"hypreal_mult_le_0_iff"; |
325 val hypreal_mult_le_0_iff = thm"hypreal_mult_le_0_iff"; |
326 val hypreal_mult_self_sum_ge_zero = thm "hypreal_mult_self_sum_ge_zero"; |
326 val hypreal_mult_self_sum_ge_zero = thm "hypreal_mult_self_sum_ge_zero"; |
327 *} |
327 *} |
328 |
328 |
329 (**** The simproc abel_cancel ****) |
|
330 |
|
331 (*** Two lemmas needed for the simprocs ***) |
|
332 |
|
333 (*Deletion of other terms in the formula, seeking the -x at the front of z*) |
|
334 lemma hypreal_add_cancel_21: "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)" |
|
335 apply (subst hypreal_add_left_commute) |
|
336 apply (rule hypreal_add_left_cancel) |
|
337 done |
|
338 |
|
339 (*A further rule to deal with the case that |
|
340 everything gets cancelled on the right.*) |
|
341 lemma hypreal_add_cancel_end: "((x::hypreal) + (y + z) = y) = (x = -z)" |
|
342 apply (subst hypreal_add_left_commute) |
|
343 apply (rule_tac t = y in hypreal_add_zero_right [THEN subst], subst hypreal_add_left_cancel) |
|
344 apply (simp (no_asm) add: hypreal_eq_diff_eq [symmetric]) |
|
345 done |
|
346 |
|
347 ML{* |
|
348 val hypreal_add_cancel_21 = thm "hypreal_add_cancel_21"; |
|
349 val hypreal_add_cancel_end = thm "hypreal_add_cancel_end"; |
|
350 |
|
351 structure Hyperreal_Cancel_Data = |
|
352 struct |
|
353 val ss = HOL_ss |
|
354 val eq_reflection = eq_reflection |
|
355 |
|
356 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) |
|
357 val T = Type("HyperDef.hypreal",[]) |
|
358 val zero = Const ("0", T) |
|
359 val restrict_to_left = restrict_to_left |
|
360 val add_cancel_21 = hypreal_add_cancel_21 |
|
361 val add_cancel_end = hypreal_add_cancel_end |
|
362 val add_left_cancel = hypreal_add_left_cancel |
|
363 val add_assoc = hypreal_add_assoc |
|
364 val add_commute = hypreal_add_commute |
|
365 val add_left_commute = hypreal_add_left_commute |
|
366 val add_0 = hypreal_add_zero_left |
|
367 val add_0_right = hypreal_add_zero_right |
|
368 |
|
369 val eq_diff_eq = hypreal_eq_diff_eq |
|
370 val eqI_rules = [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI] |
|
371 fun dest_eqI th = |
|
372 #1 (HOLogic.dest_bin "op =" HOLogic.boolT |
|
373 (HOLogic.dest_Trueprop (concl_of th))) |
|
374 |
|
375 val diff_def = hypreal_diff_def |
|
376 val minus_add_distrib = hypreal_minus_add_distrib |
|
377 val minus_minus = hypreal_minus_minus |
|
378 val minus_0 = hypreal_minus_zero |
|
379 val add_inverses = [hypreal_add_minus, hypreal_add_minus_left] |
|
380 val cancel_simps = [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA] |
|
381 end; |
|
382 |
|
383 structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data); |
|
384 |
|
385 Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv]; |
|
386 *} |
|
387 |
|
388 end |
329 end |