src/HOL/OrderedGroup.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16568 e02fe7ae212b
child 18925 2e3d508ba8dc
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/OrderedGroup.ML
     2     ID:         $Id$
     3     Author:     Steven Obua, Tobias Nipkow, Technische Universität München
     4 *)
     5 
     6 structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
     7 struct
     8 
     9 (*** Term order for abelian groups ***)
    10 
    11 fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"];
    12 
    13 fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    14 
    15 val cancel_ss = HOL_basic_ss settermless termless_agrp addsimps
    16   [thm "add_assoc", thm "add_commute", thm "add_left_commute",
    17    thm "add_0", thm "add_0_right",
    18    thm "diff_def", thm "minus_add_distrib",
    19    thm "minus_minus", thm "minus_zero",
    20    thm "right_minus", thm "left_minus",
    21    thm "add_minus_cancel", thm "minus_add_cancel"];
    22   
    23   val eq_reflection = thm "eq_reflection"
    24   
    25   val thy_ref = Theory.self_ref (theory "OrderedGroup")
    26 
    27   val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    28 
    29   val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
    30   fun dest_eqI th = 
    31       #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
    32 	      (HOLogic.dest_Trueprop (concl_of th)))  
    33 end;
    34 
    35 structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
    36 
    37 Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];