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];
```