Restructured Arithmatic
authornipkow
Tue Jan 12 15:59:35 1999 +0100 (1999-01-12)
changeset 6101dde00dc06f0d
parent 6100 40d66bc3e83f
child 6102 b985e2184868
Restructured Arithmatic
src/HOL/Arith.ML
src/HOL/Integ/Bin.ML
     1.1 --- a/src/HOL/Arith.ML	Tue Jan 12 15:49:13 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Tue Jan 12 15:59:35 1999 +0100
     1.3 @@ -843,16 +843,14 @@
     1.4  (* 2. Linear arithmetic                                                      *)
     1.5  (*---------------------------------------------------------------------------*)
     1.6  
     1.7 -(* Parameter data for general linear arithmetic functor *)
     1.8 -structure Nat_LA_Data: LIN_ARITH_DATA =
     1.9 +(* Parameters data for general linear arithmetic functor *)
    1.10 +
    1.11 +structure LA_Logic: LIN_ARITH_LOGIC =
    1.12  struct
    1.13  val ccontr = ccontr;
    1.14  val conjI = conjI;
    1.15 -val lessD = Suc_leI;
    1.16 -val neqE = nat_neqE;
    1.17 +val neqE = linorder_neqE;
    1.18  val notI = notI;
    1.19 -val not_leD = not_leE RS Suc_leI;
    1.20 -val not_lessD = leI;
    1.21  val sym = sym;
    1.22  
    1.23  val mk_Eq = mk_eq;
    1.24 @@ -861,6 +859,19 @@
    1.25  fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
    1.26    | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
    1.27  
    1.28 +fun is_False thm =
    1.29 +  let val _ $ t = #prop(rep_thm thm)
    1.30 +  in t = Const("False",HOLogic.boolT) end;
    1.31 +
    1.32 +end;
    1.33 +
    1.34 +structure Nat_LA_Data: LIN_ARITH_DATA =
    1.35 +struct
    1.36 +
    1.37 +val lessD = Suc_leI;
    1.38 +val not_leD = not_leE RS Suc_leI;
    1.39 +val not_lessD = leI;
    1.40 +
    1.41  (* Turn term into list of summand * multiplicity plus a constant *)
    1.42  fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
    1.43    | poly(Const("op +",_) $ s $ t, pi) = poly(s,poly(t,pi))
    1.44 @@ -908,10 +919,6 @@
    1.45   "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
    1.46  ];
    1.47  
    1.48 -fun is_False thm =
    1.49 -  let val _ $ t = #prop(rep_thm thm)
    1.50 -  in t = Const("False",HOLogic.boolT) end;
    1.51 -
    1.52  fun is_nat(t) = fastype_of1 t = HOLogic.natT;
    1.53  
    1.54  fun mk_nat_thm sg t =
    1.55 @@ -920,7 +927,8 @@
    1.56  
    1.57  end;
    1.58  
    1.59 -structure Fast_Nat_Arith = Fast_Lin_Arith(Nat_LA_Data);
    1.60 +structure Fast_Nat_Arith =
    1.61 +  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Nat_LA_Data);
    1.62  
    1.63  val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
    1.64  
     2.1 --- a/src/HOL/Integ/Bin.ML	Tue Jan 12 15:49:13 1999 +0100
     2.2 +++ b/src/HOL/Integ/Bin.ML	Tue Jan 12 15:59:35 1999 +0100
     2.3 @@ -401,18 +401,10 @@
     2.4  
     2.5  structure Int_LA_Data: LIN_ARITH_DATA =
     2.6  struct
     2.7 -val ccontr = ccontr;
     2.8 -val conjI = conjI;
     2.9 +
    2.10  val lessD = add1_zle_eq RS iffD2;
    2.11 -val neqE = int_neqE;
    2.12 -val notI = notI;
    2.13  val not_leD = not_zleE RS lessD;
    2.14  val not_lessD = zleI;
    2.15 -val sym = sym;
    2.16 -
    2.17 -val mk_Trueprop = Nat_LA_Data.mk_Trueprop;
    2.18 -val neg_prop = Nat_LA_Data.neg_prop;
    2.19 -val mk_Eq = Nat_LA_Data.mk_Eq;
    2.20  
    2.21  val intT = Type("IntDef.int",[]);
    2.22  
    2.23 @@ -483,17 +475,14 @@
    2.24   "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
    2.25  ];
    2.26  
    2.27 -fun is_False thm =
    2.28 -  let val _ $ t = #prop(rep_thm thm)
    2.29 -  in t = Const("False",HOLogic.boolT) end;
    2.30 -
    2.31  fun is_nat(t) = false;
    2.32  
    2.33  fun mk_nat_thm sg t = sys_error "Int/mk_nat_thm";
    2.34  
    2.35  end;
    2.36  
    2.37 -structure Fast_Int_Arith = Fast_Lin_Arith(Int_LA_Data);
    2.38 +structure Fast_Int_Arith =
    2.39 +  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Int_LA_Data);
    2.40  
    2.41  val fast_int_arith_tac = Fast_Int_Arith.lin_arith_tac;
    2.42