int --> IntInt.int
authorchaieb
Tue Jun 14 09:46:35 2005 +0200 (2005-06-14)
changeset 1638948832eba5b1e
parent 16388 1ff571813848
child 16390 305ce441869d
int --> IntInt.int
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/cooper_proof.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/cooper_proof.ML
     1.1 --- a/src/HOL/Integ/cooper_dec.ML	Tue Jun 14 04:05:15 2005 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Tue Jun 14 09:46:35 2005 +0200
     1.3 @@ -12,21 +12,21 @@
     1.4    exception COOPER
     1.5    exception COOPER_ORACLE of term
     1.6    val is_arith_rel : term -> bool
     1.7 -  val mk_numeral : int -> term
     1.8 -  val dest_numeral : term -> int
     1.9 +  val mk_numeral : IntInf.int -> term
    1.10 +  val dest_numeral : term -> IntInf.int
    1.11    val is_numeral : term -> bool
    1.12    val zero : term
    1.13    val one : term
    1.14 -  val linear_cmul : int -> term -> term
    1.15 +  val linear_cmul : IntInf.int -> term -> term
    1.16    val linear_add : string list -> term -> term -> term 
    1.17    val linear_sub : string list -> term -> term -> term 
    1.18    val linear_neg : term -> term
    1.19    val lint : string list -> term -> term
    1.20    val linform : string list -> term -> term
    1.21 -  val formlcm : term -> term -> int
    1.22 -  val adjustcoeff : term -> int -> term -> term
    1.23 +  val formlcm : term -> term -> IntInf.int
    1.24 +  val adjustcoeff : term -> IntInf.int -> term -> term
    1.25    val unitycoeff : term -> term -> term
    1.26 -  val divlcm : term -> term -> int
    1.27 +  val divlcm : term -> term -> IntInf.int
    1.28    val bset : term -> term -> term list
    1.29    val aset : term -> term -> term list
    1.30    val linrep : string list -> term -> term -> term -> term
    1.31 @@ -35,7 +35,7 @@
    1.32    val simpl : term -> term
    1.33    val fv : term -> string list
    1.34    val negate : term -> term
    1.35 -  val operations : (string * (int * int -> bool)) list
    1.36 +  val operations : (string * (IntInf.int * IntInf.int -> bool)) list
    1.37    val conjuncts : term -> term list
    1.38    val disjuncts : term -> term list
    1.39    val has_bound : term -> bool
    1.40 @@ -65,7 +65,7 @@
    1.41  (* ------------------------------------------------------------------------- *) 
    1.42   
    1.43  (*Assumption : The construction of atomar formulas in linearl arithmetic is based on 
    1.44 -relation operations of Type : [int,int]---> bool *) 
    1.45 +relation operations of Type : [IntInf.int,IntInf.int]---> bool *) 
    1.46   
    1.47  (* ------------------------------------------------------------------------- *) 
    1.48   
    1.49 @@ -85,14 +85,14 @@
    1.50   
    1.51  fun mk_numeral 0 = Const("0",HOLogic.intT)
    1.52     |mk_numeral 1 = Const("1",HOLogic.intT)
    1.53 -   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
    1.54 +   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
    1.55   
    1.56  (*Transform an Term to an natural number*)	  
    1.57  	  
    1.58  fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    1.59     |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    1.60     |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
    1.61 -       IntInf.toInt (HOLogic.dest_binum n);
    1.62 +       HOLogic.dest_binum n;
    1.63  (*Some terms often used for pattern matching*) 
    1.64   
    1.65  val zero = mk_numeral 0; 
    1.66 @@ -116,7 +116,7 @@
    1.67  (* Note that we're quite strict: the ci must be present even if 1            *) 
    1.68  (* (but if 0 we expect the monomial to be omitted) and k must be there       *) 
    1.69  (* even if it's zero. Thus, it's a constant iff not an addition term.        *) 
    1.70 -(* ------------------------------------------------------------------------- *) 
    1.71 +(* ------------------------------------------------------------------------- *)  
    1.72   
    1.73   
    1.74  fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
     2.1 --- a/src/HOL/Integ/cooper_proof.ML	Tue Jun 14 04:05:15 2005 +0200
     2.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Jun 14 09:46:35 2005 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4    val proof_of_evalc : Sign.sg -> term -> thm
     2.5    val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
     2.6    val proof_of_linform : Sign.sg -> string list -> term -> thm
     2.7 -  val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
     2.8 +  val proof_of_adjustcoeffeq : Sign.sg -> term -> IntInf.int -> term -> thm
     2.9    val prove_elementar : Sign.sg -> string -> term -> thm
    2.10    val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
    2.11  end;
     3.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jun 14 04:05:15 2005 +0200
     3.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jun 14 09:46:35 2005 +0200
     3.3 @@ -12,21 +12,21 @@
     3.4    exception COOPER
     3.5    exception COOPER_ORACLE of term
     3.6    val is_arith_rel : term -> bool
     3.7 -  val mk_numeral : int -> term
     3.8 -  val dest_numeral : term -> int
     3.9 +  val mk_numeral : IntInf.int -> term
    3.10 +  val dest_numeral : term -> IntInf.int
    3.11    val is_numeral : term -> bool
    3.12    val zero : term
    3.13    val one : term
    3.14 -  val linear_cmul : int -> term -> term
    3.15 +  val linear_cmul : IntInf.int -> term -> term
    3.16    val linear_add : string list -> term -> term -> term 
    3.17    val linear_sub : string list -> term -> term -> term 
    3.18    val linear_neg : term -> term
    3.19    val lint : string list -> term -> term
    3.20    val linform : string list -> term -> term
    3.21 -  val formlcm : term -> term -> int
    3.22 -  val adjustcoeff : term -> int -> term -> term
    3.23 +  val formlcm : term -> term -> IntInf.int
    3.24 +  val adjustcoeff : term -> IntInf.int -> term -> term
    3.25    val unitycoeff : term -> term -> term
    3.26 -  val divlcm : term -> term -> int
    3.27 +  val divlcm : term -> term -> IntInf.int
    3.28    val bset : term -> term -> term list
    3.29    val aset : term -> term -> term list
    3.30    val linrep : string list -> term -> term -> term -> term
    3.31 @@ -35,7 +35,7 @@
    3.32    val simpl : term -> term
    3.33    val fv : term -> string list
    3.34    val negate : term -> term
    3.35 -  val operations : (string * (int * int -> bool)) list
    3.36 +  val operations : (string * (IntInf.int * IntInf.int -> bool)) list
    3.37    val conjuncts : term -> term list
    3.38    val disjuncts : term -> term list
    3.39    val has_bound : term -> bool
    3.40 @@ -65,7 +65,7 @@
    3.41  (* ------------------------------------------------------------------------- *) 
    3.42   
    3.43  (*Assumption : The construction of atomar formulas in linearl arithmetic is based on 
    3.44 -relation operations of Type : [int,int]---> bool *) 
    3.45 +relation operations of Type : [IntInf.int,IntInf.int]---> bool *) 
    3.46   
    3.47  (* ------------------------------------------------------------------------- *) 
    3.48   
    3.49 @@ -85,14 +85,14 @@
    3.50   
    3.51  fun mk_numeral 0 = Const("0",HOLogic.intT)
    3.52     |mk_numeral 1 = Const("1",HOLogic.intT)
    3.53 -   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
    3.54 +   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
    3.55   
    3.56  (*Transform an Term to an natural number*)	  
    3.57  	  
    3.58  fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    3.59     |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    3.60     |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
    3.61 -       IntInf.toInt (HOLogic.dest_binum n);
    3.62 +       HOLogic.dest_binum n;
    3.63  (*Some terms often used for pattern matching*) 
    3.64   
    3.65  val zero = mk_numeral 0; 
    3.66 @@ -116,7 +116,7 @@
    3.67  (* Note that we're quite strict: the ci must be present even if 1            *) 
    3.68  (* (but if 0 we expect the monomial to be omitted) and k must be there       *) 
    3.69  (* even if it's zero. Thus, it's a constant iff not an addition term.        *) 
    3.70 -(* ------------------------------------------------------------------------- *) 
    3.71 +(* ------------------------------------------------------------------------- *)  
    3.72   
    3.73   
    3.74  fun linear_cmul n tm =  if n = 0 then zero else let fun times n k = n*k in  
     4.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Jun 14 04:05:15 2005 +0200
     4.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Jun 14 09:46:35 2005 +0200
     4.3 @@ -21,7 +21,7 @@
     4.4    val proof_of_evalc : Sign.sg -> term -> thm
     4.5    val proof_of_cnnf : Sign.sg -> term -> (term -> thm) -> thm
     4.6    val proof_of_linform : Sign.sg -> string list -> term -> thm
     4.7 -  val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
     4.8 +  val proof_of_adjustcoeffeq : Sign.sg -> term -> IntInf.int -> term -> thm
     4.9    val prove_elementar : Sign.sg -> string -> term -> thm
    4.10    val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
    4.11  end;