author | wenzelm |
Wed, 08 Nov 2006 13:48:29 +0100 | |
changeset 21243 | afffe1f72143 |
parent 20713 | 823967ef47f1 |
permissions | -rw-r--r-- |
14755 | 1 |
(* Title: HOL/OrderedGroup.ML |
2 |
ID: $Id$ |
|
20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
19330
diff
changeset
|
3 |
Author: Steven Obua, Tobias Nipkow, Technische Universitaet Muenchen |
14755 | 4 |
*) |
5 |
||
6 |
structure ab_group_add_cancel_data :> ABEL_CANCEL = |
|
7 |
struct |
|
16568 | 8 |
|
9 |
(*** Term order for abelian groups ***) |
|
10 |
||
20713
823967ef47f1
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann
parents:
20129
diff
changeset
|
11 |
fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"] |
20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
19330
diff
changeset
|
12 |
| agrp_ord _ = ~1; |
16568 | 13 |
|
14 |
fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS); |
|
15 |
||
18925 | 16 |
local |
17 |
val ac1 = mk_meta_eq (thm "add_assoc"); |
|
18 |
val ac2 = mk_meta_eq (thm "add_commute"); |
|
19 |
val ac3 = mk_meta_eq (thm "add_left_commute"); |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18925
diff
changeset
|
20 |
fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) = |
18925 | 21 |
SOME ac1 |
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
18925
diff
changeset
|
22 |
| solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) = |
18925 | 23 |
if termless_agrp (y, x) then SOME ac3 else NONE |
24 |
| solve_add_ac thy _ (_ $ x $ y) = |
|
25 |
if termless_agrp (y, x) then SOME ac2 else NONE |
|
26 |
| solve_add_ac thy _ _ = NONE |
|
27 |
in |
|
28 |
val add_ac_proc = Simplifier.simproc (the_context ()) |
|
29 |
"add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac; |
|
30 |
end; |
|
31 |
||
32 |
val cancel_ss = HOL_basic_ss settermless termless_agrp |
|
33 |
addsimprocs [add_ac_proc] addsimps |
|
34 |
[thm "add_0", thm "add_0_right", |
|
16568 | 35 |
thm "diff_def", thm "minus_add_distrib", |
36 |
thm "minus_minus", thm "minus_zero", |
|
37 |
thm "right_minus", thm "left_minus", |
|
38 |
thm "add_minus_cancel", thm "minus_add_cancel"]; |
|
39 |
||
14755 | 40 |
val eq_reflection = thm "eq_reflection" |
41 |
||
16423 | 42 |
val thy_ref = Theory.self_ref (theory "OrderedGroup") |
14755 | 43 |
|
44 |
val T = TFree("'a", ["OrderedGroup.ab_group_add"]) |
|
16568 | 45 |
|
14755 | 46 |
val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"] |
47 |
fun dest_eqI th = |
|
48 |
#1 (HOLogic.dest_bin "op =" HOLogic.boolT |
|
49 |
(HOLogic.dest_Trueprop (concl_of th))) |
|
50 |
end; |
|
51 |
||
52 |
structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data); |
|
53 |
||
54 |
Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]; |