src/HOL/OrderedGroup.ML
changeset 16568 e02fe7ae212b
parent 16423 24abe4c0e4b4
child 18925 2e3d508ba8dc
     1.1 --- a/src/HOL/OrderedGroup.ML	Sat Jun 25 12:37:07 2005 +0200
     1.2 +++ b/src/HOL/OrderedGroup.ML	Sat Jun 25 16:06:17 2005 +0200
     1.3 @@ -1,40 +1,35 @@
     1.4  (*  Title:      HOL/OrderedGroup.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Steven Obua, Technische Universität München
     1.7 +    Author:     Steven Obua, Tobias Nipkow, Technische Universität München
     1.8  *)
     1.9  
    1.10  structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
    1.11  struct
    1.12 -  val ss = simpset_of HOL.thy
    1.13 +
    1.14 +(*** Term order for abelian groups ***)
    1.15 +
    1.16 +fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"];
    1.17 +
    1.18 +fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    1.19 +
    1.20 +val cancel_ss = HOL_basic_ss settermless termless_agrp addsimps
    1.21 +  [thm "add_assoc", thm "add_commute", thm "add_left_commute",
    1.22 +   thm "add_0", thm "add_0_right",
    1.23 +   thm "diff_def", thm "minus_add_distrib",
    1.24 +   thm "minus_minus", thm "minus_zero",
    1.25 +   thm "right_minus", thm "left_minus",
    1.26 +   thm "add_minus_cancel", thm "minus_add_cancel"];
    1.27 +  
    1.28    val eq_reflection = thm "eq_reflection"
    1.29    
    1.30    val thy_ref = Theory.self_ref (theory "OrderedGroup")
    1.31  
    1.32    val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    1.33 -  
    1.34 -  val restrict_to_left = thm "restrict_to_left"
    1.35 -  val add_cancel_21 = thm "add_cancel_21"
    1.36 -  val add_cancel_end = thm "add_cancel_end"
    1.37 -  val add_left_cancel = thm "add_left_cancel"
    1.38 -  val add_assoc = thm "add_assoc"
    1.39 -  val add_commute = thm "add_commute"
    1.40 -  val add_left_commute = thm "add_left_commute"
    1.41 -  val add_0 = thm "add_0"
    1.42 -  val add_0_right = thm "add_0_right"
    1.43 -  
    1.44 -  val eq_diff_eq = thm "eq_diff_eq"
    1.45 -  
    1.46 +
    1.47    val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
    1.48    fun dest_eqI th = 
    1.49        #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
    1.50  	      (HOLogic.dest_Trueprop (concl_of th)))  
    1.51 -
    1.52 -  val diff_def		= thm "diff_def"
    1.53 -  val minus_add_distrib	= thm "minus_add_distrib"
    1.54 -  val minus_minus	= thm "minus_minus"
    1.55 -  val minus_0		= thm "minus_zero"
    1.56 -  val add_inverses	= [thm "right_minus", thm "left_minus"]
    1.57 -  val cancel_simps	= [thm "add_minus_cancel", thm "minus_add_cancel"]
    1.58  end;
    1.59  
    1.60  structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);