Restructured Arithmatic

--- a/src/HOL/Arith.ML	Tue Jan 12 15:49:13 1999 +0100
+++ b/src/HOL/Arith.ML	Tue Jan 12 15:59:35 1999 +0100
@@ -843,16 +843,14 @@
 (* 2. Linear arithmetic                                                      *)
 (*---------------------------------------------------------------------------*)
 
-(* Parameter data for general linear arithmetic functor *)
-structure Nat_LA_Data: LIN_ARITH_DATA =
+(* Parameters data for general linear arithmetic functor *)
+
+structure LA_Logic: LIN_ARITH_LOGIC =
 struct
 val ccontr = ccontr;
 val conjI = conjI;
-val lessD = Suc_leI;
-val neqE = nat_neqE;
+val neqE = linorder_neqE;
 val notI = notI;
-val not_leD = not_leE RS Suc_leI;
-val not_lessD = leI;
 val sym = sym;
 
 val mk_Eq = mk_eq;
@@ -861,6 +859,19 @@
 fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
   | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
 
+fun is_False thm =
+  let val _ $ t = #prop(rep_thm thm)
+  in t = Const("False",HOLogic.boolT) end;
+
+end;
+
+structure Nat_LA_Data: LIN_ARITH_DATA =
+struct
+
+val lessD = Suc_leI;
+val not_leD = not_leE RS Suc_leI;
+val not_lessD = leI;
+
 (* Turn term into list of summand * multiplicity plus a constant *)
 fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
   | poly(Const("op +",_) $ s $ t, pi) = poly(s,poly(t,pi))
@@ -908,10 +919,6 @@
  "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
 ];
 
-fun is_False thm =
-  let val _ $ t = #prop(rep_thm thm)
-  in t = Const("False",HOLogic.boolT) end;
-
 fun is_nat(t) = fastype_of1 t = HOLogic.natT;
 
 fun mk_nat_thm sg t =
@@ -920,7 +927,8 @@
 
 end;
 
-structure Fast_Nat_Arith = Fast_Lin_Arith(Nat_LA_Data);
+structure Fast_Nat_Arith =
+  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Nat_LA_Data);
 
 val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
 

--- a/src/HOL/Integ/Bin.ML	Tue Jan 12 15:49:13 1999 +0100
+++ b/src/HOL/Integ/Bin.ML	Tue Jan 12 15:59:35 1999 +0100
@@ -401,18 +401,10 @@
 
 structure Int_LA_Data: LIN_ARITH_DATA =
 struct
-val ccontr = ccontr;
-val conjI = conjI;
+
 val lessD = add1_zle_eq RS iffD2;
-val neqE = int_neqE;
-val notI = notI;
 val not_leD = not_zleE RS lessD;
 val not_lessD = zleI;
-val sym = sym;
-
-val mk_Trueprop = Nat_LA_Data.mk_Trueprop;
-val neg_prop = Nat_LA_Data.neg_prop;
-val mk_Eq = Nat_LA_Data.mk_Eq;
 
 val intT = Type("IntDef.int",[]);
 
@@ -483,17 +475,14 @@
  "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
 ];
 
-fun is_False thm =
-  let val _ $ t = #prop(rep_thm thm)
-  in t = Const("False",HOLogic.boolT) end;
-
 fun is_nat(t) = false;
 
 fun mk_nat_thm sg t = sys_error "Int/mk_nat_thm";
 
 end;
 
-structure Fast_Int_Arith = Fast_Lin_Arith(Int_LA_Data);
+structure Fast_Int_Arith =
+  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Int_LA_Data);
 
 val fast_int_arith_tac = Fast_Int_Arith.lin_arith_tac;