src/HOL/OrderedGroup.ML
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14755 5cc6e6b9e27a
child 16423 24abe4c0e4b4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
obua@14755
     1
(*  Title:      HOL/OrderedGroup.ML
obua@14755
     2
    ID:         $Id$
obua@14755
     3
    Author:     Steven Obua, 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
obua@14755
     8
  val ss = simpset_of HOL.thy
obua@14755
     9
  val eq_reflection = thm "eq_reflection"
obua@14755
    10
  
obua@14755
    11
  val sg_ref = Sign.self_ref (sign_of (theory "OrderedGroup"))
obua@14755
    12
obua@14755
    13
  val T = TFree("'a", ["OrderedGroup.ab_group_add"])
obua@14755
    14
  
obua@14755
    15
  val restrict_to_left = thm "restrict_to_left"
obua@14755
    16
  val add_cancel_21 = thm "add_cancel_21"
obua@14755
    17
  val add_cancel_end = thm "add_cancel_end"
obua@14755
    18
  val add_left_cancel = thm "add_left_cancel"
obua@14755
    19
  val add_assoc = thm "add_assoc"
obua@14755
    20
  val add_commute = thm "add_commute"
obua@14755
    21
  val add_left_commute = thm "add_left_commute"
obua@14755
    22
  val add_0 = thm "add_0"
obua@14755
    23
  val add_0_right = thm "add_0_right"
obua@14755
    24
  
obua@14755
    25
  val eq_diff_eq = thm "eq_diff_eq"
obua@14755
    26
  
obua@14755
    27
  val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
obua@14755
    28
  fun dest_eqI th = 
obua@14755
    29
      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
obua@14755
    30
	      (HOLogic.dest_Trueprop (concl_of th)))  
obua@14755
    31
obua@14755
    32
  val diff_def		= thm "diff_def"
obua@14755
    33
  val minus_add_distrib	= thm "minus_add_distrib"
obua@14755
    34
  val minus_minus	= thm "minus_minus"
obua@14755
    35
  val minus_0		= thm "minus_zero"
obua@14755
    36
  val add_inverses	= [thm "right_minus", thm "left_minus"]
obua@14755
    37
  val cancel_simps	= [thm "add_minus_cancel", thm "minus_add_cancel"]
obua@14755
    38
end;
obua@14755
    39
obua@14755
    40
structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
obua@14755
    41
obua@14755
    42
Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];