--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 16:57:59 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 17:00:46 2010 +0200
@@ -36,7 +36,7 @@
structure Normalizer: NORMALIZER =
struct
-(* data *)
+(** data **)
type entry =
{vars: cterm list,
@@ -60,9 +60,6 @@
val get = Data.get o Context.Proof;
-
-(* match data *)
-
fun match ctxt tm =
let
fun match_inst
@@ -173,52 +170,6 @@
in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
-(* concrete syntax *)
-
-local
-
-fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
-fun keyword3 k1 k2 k3 =
- Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
-
-val opsN = "ops";
-val rulesN = "rules";
-
-val normN = "norm";
-val constN = "const";
-val delN = "del";
-
-val any_keyword =
- keyword2 semiringN opsN || keyword2 semiringN rulesN ||
- keyword2 ringN opsN || keyword2 ringN rulesN ||
- keyword2 fieldN opsN || keyword2 fieldN rulesN ||
- keyword2 idomN rulesN || keyword2 idealN rulesN;
-
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-val terms = thms >> map Drule.dest_term;
-
-fun optional scan = Scan.optional scan [];
-
-in
-
-val normalizer_setup =
- Attrib.setup @{binding normalizer}
- (Scan.lift (Args.$$$ delN >> K del) ||
- ((keyword2 semiringN opsN |-- terms) --
- (keyword2 semiringN rulesN |-- thms)) --
- (optional (keyword2 ringN opsN |-- terms) --
- optional (keyword2 ringN rulesN |-- thms)) --
- (optional (keyword2 fieldN opsN |-- terms) --
- optional (keyword2 fieldN rulesN |-- thms)) --
- optional (keyword2 idomN rulesN |-- thms) --
- optional (keyword2 idealN rulesN |-- thms)
- >> (fn ((((sr, r), f), id), idl) =>
- add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
- "semiring normalizer data";
-
-end;
-
open Conv;
(* Very basic stuff for terms *)
@@ -859,8 +810,51 @@
fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
-(* theory setup *)
+
+(** Isar setup **)
+
+local
+
+fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K ();
+fun keyword3 k1 k2 k3 =
+ Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K ();
+
+val opsN = "ops";
+val rulesN = "rules";
+
+val normN = "norm";
+val constN = "const";
+val delN = "del";
-val setup = normalizer_setup
+val any_keyword =
+ keyword2 semiringN opsN || keyword2 semiringN rulesN ||
+ keyword2 ringN opsN || keyword2 ringN rulesN ||
+ keyword2 fieldN opsN || keyword2 fieldN rulesN ||
+ keyword2 idomN rulesN || keyword2 idealN rulesN;
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val terms = thms >> map Drule.dest_term;
+
+fun optional scan = Scan.optional scan [];
+
+in
+
+val setup =
+ Attrib.setup @{binding normalizer}
+ (Scan.lift (Args.$$$ delN >> K del) ||
+ ((keyword2 semiringN opsN |-- terms) --
+ (keyword2 semiringN rulesN |-- thms)) --
+ (optional (keyword2 ringN opsN |-- terms) --
+ optional (keyword2 ringN rulesN |-- thms)) --
+ (optional (keyword2 fieldN opsN |-- terms) --
+ optional (keyword2 fieldN rulesN |-- thms)) --
+ optional (keyword2 idomN rulesN |-- thms) --
+ optional (keyword2 idealN rulesN |-- thms)
+ >> (fn ((((sr, r), f), id), idl) =>
+ add {semiring = sr, ring = r, field = f, idom = id, ideal = idl}))
+ "semiring normalizer data";
end;
+
+end;