|
14755
|
1 |
(* Title: HOL/OrderedGroup.ML
|
|
|
2 |
ID: $Id$
|
|
18925
|
3 |
Author: Steven Obua, Tobias Nipkow, Technische Universit� Mnchen
|
|
14755
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
structure ab_group_add_cancel_data :> ABEL_CANCEL =
|
|
|
7 |
struct
|
|
16568
|
8 |
|
|
|
9 |
(*** Term order for abelian groups ***)
|
|
|
10 |
|
|
|
11 |
fun agrp_ord a = find_index_eq a ["0", "op +", "uminus", "op -"];
|
|
|
12 |
|
|
|
13 |
fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
|
|
|
14 |
|
|
18925
|
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 ("op +",_) $ _ $ _) $ _) =
|
|
|
20 |
SOME ac1
|
|
|
21 |
| solve_add_ac thy _ (_ $ x $ (Const ("op +",_) $ 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",
|
|
16568
|
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 |
|
|
14755
|
39 |
val eq_reflection = thm "eq_reflection"
|
|
|
40 |
|
|
16423
|
41 |
val thy_ref = Theory.self_ref (theory "OrderedGroup")
|
|
14755
|
42 |
|
|
|
43 |
val T = TFree("'a", ["OrderedGroup.ab_group_add"])
|
|
16568
|
44 |
|
|
14755
|
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];
|