# HG changeset patch # User nipkow # Date 916153175 -3600 # Node ID dde00dc06f0d1c6ce3c4c332014c6c2b24304b59 # Parent 40d66bc3e83f845bce5a621e4fb3ad177003d48b Restructured Arithmatic diff -r 40d66bc3e83f -r dde00dc06f0d src/HOL/Arith.ML --- 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; diff -r 40d66bc3e83f -r dde00dc06f0d src/HOL/Integ/Bin.ML --- 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;