--- a/src/HOL/IsaMakefile Tue Mar 20 15:52:38 2007 +0100
+++ b/src/HOL/IsaMakefile Tue Mar 20 15:52:39 2007 +0100
@@ -93,7 +93,7 @@
Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML Integ/presburger.ML \
Integ/qelim.ML Integ/reflected_cooper.ML Integ/reflected_presburger.ML \
Lattices.thy List.thy Main.thy Map.thy Nat.ML Nat.thy \
- OrderedGroup.ML OrderedGroup.thy Orderings.thy Power.thy Predicate.thy PreList.thy \
+ OrderedGroup.thy Orderings.thy Power.thy Predicate.thy PreList.thy \
Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy Relation.thy \
Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy \
Sum_Type.thy Tools/res_reconstruct.ML Tools/ATP/reduce_axiomsN.ML \
--- a/src/HOL/OrderedGroup.ML Tue Mar 20 15:52:38 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-(* Title: HOL/OrderedGroup.ML
- ID: $Id$
- Author: Steven Obua, Tobias Nipkow, Technische Universitaet Muenchen
-*)
-
-structure ab_group_add_cancel_data :> ABEL_CANCEL =
-struct
-
-(*** Term order for abelian groups ***)
-
-fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a') ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
- | agrp_ord _ = ~1;
-
-fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
-
-local
- val ac1 = mk_meta_eq (thm "add_assoc");
- val ac2 = mk_meta_eq (thm "add_commute");
- val ac3 = mk_meta_eq (thm "add_left_commute");
- fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
- SOME ac1
- | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
- if termless_agrp (y, x) then SOME ac3 else NONE
- | solve_add_ac thy _ (_ $ x $ y) =
- if termless_agrp (y, x) then SOME ac2 else NONE
- | solve_add_ac thy _ _ = NONE
-in
- val add_ac_proc = Simplifier.simproc (the_context ())
- "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
-end;
-
-val cancel_ss = HOL_basic_ss settermless termless_agrp
- addsimprocs [add_ac_proc] addsimps
- [thm "add_0", thm "add_0_right",
- thm "diff_def", thm "minus_add_distrib",
- thm "minus_minus", thm "minus_zero",
- thm "right_minus", thm "left_minus",
- thm "add_minus_cancel", thm "minus_add_cancel"];
-
- val eq_reflection = thm "eq_reflection"
-
- val thy_ref = Theory.self_ref (theory "OrderedGroup")
-
- val T = TFree("'a", ["OrderedGroup.ab_group_add"])
-
- val eqI_rules = [thm "less_eqI", thm "le_eqI", thm "eq_eqI"]
- fun dest_eqI th =
- #1 (HOLogic.dest_bin "op =" HOLogic.boolT
- (HOLogic.dest_Trueprop (concl_of th)))
-end;
-
-structure ab_group_add_cancel = Abel_Cancel (ab_group_add_cancel_data);
-
-Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
--- a/src/HOL/OrderedGroup.thy Tue Mar 20 15:52:38 2007 +0100
+++ b/src/HOL/OrderedGroup.thy Tue Mar 20 15:52:39 2007 +0100
@@ -1042,6 +1042,9 @@
show ?thesis by (rule le_add_right_mono[OF 2 3])
qed
+
+subsection {* Tools setup *}
+
text{*Simplification of @{term "x-y < 0"}, etc.*}
lemmas diff_less_0_iff_less = less_iff_diff_less_0 [symmetric]
lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric]
@@ -1050,6 +1053,58 @@
declare diff_eq_0_iff_eq [simp]
declare diff_le_0_iff_le [simp]
+ML {*
+structure ab_group_add_cancel = Abel_Cancel(
+struct
+
+(* term order for abelian groups *)
+
+fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
+ ["HOL.zero", "HOL.plus", "HOL.uminus", "HOL.minus"]
+ | agrp_ord _ = ~1;
+
+fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
+
+local
+ val ac1 = mk_meta_eq @{thm add_assoc};
+ val ac2 = mk_meta_eq @{thm add_commute};
+ val ac3 = mk_meta_eq @{thm add_left_commute};
+ fun solve_add_ac thy _ (_ $ (Const ("HOL.plus",_) $ _ $ _) $ _) =
+ SOME ac1
+ | solve_add_ac thy _ (_ $ x $ (Const ("HOL.plus",_) $ y $ z)) =
+ if termless_agrp (y, x) then SOME ac3 else NONE
+ | solve_add_ac thy _ (_ $ x $ y) =
+ if termless_agrp (y, x) then SOME ac2 else NONE
+ | solve_add_ac thy _ _ = NONE
+in
+ val add_ac_proc = Simplifier.simproc @{theory}
+ "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
+end;
+
+val cancel_ss = HOL_basic_ss settermless termless_agrp
+ addsimprocs [add_ac_proc] addsimps
+ [@{thm add_0}, @{thm add_0_right}, @{thm diff_def},
+ @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
+ @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
+ @{thm minus_add_cancel}];
+
+val eq_reflection = @{thm eq_reflection}
+
+val thy_ref = Theory.self_ref @{theory}
+
+val T = TFree("'a", ["OrderedGroup.ab_group_add"])
+
+val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}]
+
+val dest_eqI =
+ fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
+
+end);
+*}
+
+ML_setup {*
+ Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
+*}
ML {*
val add_assoc = thm "add_assoc";