simplification for abelian groups
authorobua
Tue May 18 10:02:50 2004 +0200 (2004-05-18)
changeset 147555cc6e6b9e27a
parent 14754 a080eeeaec14
child 14756 9c8cc63714f4
simplification for abelian groups
src/HOL/OrderedGroup.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/OrderedGroup.ML	Tue May 18 10:02:50 2004 +0200
     1.3 @@ -0,0 +1,42 @@
     1.4 +(*  Title:      HOL/OrderedGroup.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Steven Obua, Technische Universität München
     1.7 +*)
     1.8 +
     1.9 +structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
    1.10 +struct
    1.11 +  val ss = simpset_of HOL.thy
    1.12 +  val eq_reflection = thm "eq_reflection"
    1.13 +  
    1.14 +  val sg_ref = Sign.self_ref (sign_of (theory "OrderedGroup"))
    1.15 +
    1.16 +  val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    1.17 +  
    1.18 +  val restrict_to_left = thm "restrict_to_left"
    1.19 +  val add_cancel_21 = thm "add_cancel_21"
    1.20 +  val add_cancel_end = thm "add_cancel_end"
    1.21 +  val add_left_cancel = thm "add_left_cancel"
    1.22 +  val add_assoc = thm "add_assoc"
    1.23 +  val add_commute = thm "add_commute"
    1.24 +  val add_left_commute = thm "add_left_commute"
    1.25 +  val add_0 = thm "add_0"
    1.26 +  val add_0_right = thm "add_0_right"
    1.27 +  
    1.28 +  val eq_diff_eq = thm "eq_diff_eq"
    1.29 +  
    1.30 +  val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
    1.31 +  fun dest_eqI th = 
    1.32 +      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
    1.33 +	      (HOLogic.dest_Trueprop (concl_of th)))  
    1.34 +
    1.35 +  val diff_def		= thm "diff_def"
    1.36 +  val minus_add_distrib	= thm "minus_add_distrib"
    1.37 +  val minus_minus	= thm "minus_minus"
    1.38 +  val minus_0		= thm "minus_zero"
    1.39 +  val add_inverses	= [thm "right_minus", thm "left_minus"]
    1.40 +  val cancel_simps	= [thm "add_minus_cancel", thm "minus_add_cancel"]
    1.41 +end;
    1.42 +
    1.43 +structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
    1.44 +
    1.45 +Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];