src/HOL/OrderedGroup.ML
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 19330 eaf569aa8fd4
child 20129 95e84d2c9f2c
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/OrderedGroup.ML
     2     ID:         $Id$
     3     Author:     Steven Obua, Tobias Nipkow, Technische Universitaet Mnchen
     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 (fn a' => a = a') ["0", "HOL.plus", "HOL.uminus", "HOL.minus"];
    12 
    13 fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
    14 
    15 local
    16   val ac1 = mk_meta_eq (thm "add_assoc");
    17   val ac2 = mk_meta_eq (thm "add_commute");
    18   val ac3 = mk_meta_eq (thm "add_left_commute");
    19   fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
    20         SOME ac1
    21     | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
    22         if termless_agrp (y, x) then SOME ac3 else NONE
    23     | solve_add_ac thy _ (_ $ x $ y) =
    24         if termless_agrp (y, x) then SOME ac2 else NONE
    25     | solve_add_ac thy _ _ = NONE
    26 in
    27   val add_ac_proc = Simplifier.simproc (the_context ())
    28     "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
    29 end;
    30 
    31 val cancel_ss = HOL_basic_ss settermless termless_agrp
    32   addsimprocs [add_ac_proc] addsimps
    33   [thm "add_0", thm "add_0_right",
    34    thm "diff_def", thm "minus_add_distrib",
    35    thm "minus_minus", thm "minus_zero",
    36    thm "right_minus", thm "left_minus",
    37    thm "add_minus_cancel", thm "minus_add_cancel"];
    38   
    39   val eq_reflection = thm "eq_reflection"
    40   
    41   val thy_ref = Theory.self_ref (theory "OrderedGroup")
    42 
    43   val T = TFree("'a", ["OrderedGroup.ab_group_add"])
    44 
    45   val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
    46   fun dest_eqI th = 
    47       #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
    48 	      (HOLogic.dest_Trueprop (concl_of th)))  
    49 end;
    50 
    51 structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
    52 
    53 Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];