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)
     1 (*  Title:      HOL/OrderedGroup.ML
     2     ID:         $Id$
     3     Author:     Steven Obua, Technische Universität München
     4 *)
     5 
     6 structure ab_group_add_cancel_data :> ABEL_CANCEL  = 
     7 struct
     8   val ss = simpset_of HOL.thy
     9   val eq_reflection = thm "eq_reflection"
    10   
    11   val sg_ref = Sign.self_ref (sign_of (theory "OrderedGroup"))
    12 
    13   val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    14   
    15   val restrict_to_left = thm "restrict_to_left"
    16   val add_cancel_21 = thm "add_cancel_21"
    17   val add_cancel_end = thm "add_cancel_end"
    18   val add_left_cancel = thm "add_left_cancel"
    19   val add_assoc = thm "add_assoc"
    20   val add_commute = thm "add_commute"
    21   val add_left_commute = thm "add_left_commute"
    22   val add_0 = thm "add_0"
    23   val add_0_right = thm "add_0_right"
    24   
    25   val eq_diff_eq = thm "eq_diff_eq"
    26   
    27   val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
    28   fun dest_eqI th = 
    29       #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
    30 	      (HOLogic.dest_Trueprop (concl_of th)))  
    31 
    32   val diff_def		= thm "diff_def"
    33   val minus_add_distrib	= thm "minus_add_distrib"
    34   val minus_minus	= thm "minus_minus"
    35   val minus_0		= thm "minus_zero"
    36   val add_inverses	= [thm "right_minus", thm "left_minus"]
    37   val cancel_simps	= [thm "add_minus_cancel", thm "minus_add_cancel"]
    38 end;
    39 
    40 structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
    41 
    42 Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];