# HG changeset patch # User obua # Date 1084867370 -7200 # Node ID 5cc6e6b9e27a7f0b7793e83cc5352422a8fe5552 # Parent a080eeeaec14d30b6ceba46d401650b022f86aa2 simplification for abelian groups diff -r a080eeeaec14 -r 5cc6e6b9e27a src/HOL/OrderedGroup.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/OrderedGroup.ML Tue May 18 10:02:50 2004 +0200 @@ -0,0 +1,42 @@ +(* Title: HOL/OrderedGroup.ML + ID: $Id$ + Author: Steven Obua, Technische Universität München +*) + +structure ab_group_add_cancel_data :> ABEL_CANCEL = +struct + val ss = simpset_of HOL.thy + val eq_reflection = thm "eq_reflection" + + val sg_ref = Sign.self_ref (sign_of (theory "OrderedGroup")) + + val T = TFree("'a", ["OrderedGroup.ab_group_add"]) + + val restrict_to_left = thm "restrict_to_left" + val add_cancel_21 = thm "add_cancel_21" + val add_cancel_end = thm "add_cancel_end" + val add_left_cancel = thm "add_left_cancel" + val add_assoc = thm "add_assoc" + val add_commute = thm "add_commute" + val add_left_commute = thm "add_left_commute" + val add_0 = thm "add_0" + val add_0_right = thm "add_0_right" + + val eq_diff_eq = thm "eq_diff_eq" + + val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"] + fun dest_eqI th = + #1 (HOLogic.dest_bin "op =" HOLogic.boolT + (HOLogic.dest_Trueprop (concl_of th))) + + val diff_def = thm "diff_def" + val minus_add_distrib = thm "minus_add_distrib" + val minus_minus = thm "minus_minus" + val minus_0 = thm "minus_zero" + val add_inverses = [thm "right_minus", thm "left_minus"] + val cancel_simps = [thm "add_minus_cancel", thm "minus_add_cancel"] +end; + +structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data); + +Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];