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