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