# HG changeset patch
# User haftmann
# Date 1174402359 -3600
# Node ID 8fc3d7237e03464554c465e4b773d90d8a653e32
# Parent  79c2724c36b5c670720f36b3f9330b6c6bdef49f
dropped OrderedGroup.ML

diff -r 79c2724c36b5 -r 8fc3d7237e03 src/HOL/IsaMakefile
--- 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	\
diff -r 79c2724c36b5 -r 8fc3d7237e03 src/HOL/OrderedGroup.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];
diff -r 79c2724c36b5 -r 8fc3d7237e03 src/HOL/OrderedGroup.thy
--- 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";