--- 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;