src/HOL/Tools/int_arith.ML
changeset 29269 5c25a2012975
parent 28952 15a4b2cf8c34
child 30496 7cdcc9dd95cb
equal deleted inserted replaced
29268:6aefc5ff8e63 29269:5c25a2012975
     1 (*  Title:      HOL/int_arith1.ML
     1 (*  Title:      HOL/Tools/int_arith1.ML
     2     ID:         $Id$
       
     3     Authors:    Larry Paulson and Tobias Nipkow
     2     Authors:    Larry Paulson and Tobias Nipkow
     4 
     3 
     5 Simprocs and decision procedure for linear arithmetic.
     4 Simprocs and decision procedure for linear arithmetic.
     6 *)
     5 *)
     7 
     6 
    64 fun num_ord (i,j) =
    63 fun num_ord (i,j) =
    65   (case int_ord (abs i, abs j) of
    64   (case int_ord (abs i, abs j) of
    66     EQUAL => int_ord (Int.sign i, Int.sign j) 
    65     EQUAL => int_ord (Int.sign i, Int.sign j) 
    67   | ord => ord);
    66   | ord => ord);
    68 
    67 
    69 (*This resembles Term.term_ord, but it puts binary numerals before other
    68 (*This resembles TermOrd.term_ord, but it puts binary numerals before other
    70   non-atomic terms.*)
    69   non-atomic terms.*)
    71 local open Term 
    70 local open Term 
    72 in 
    71 in 
    73 fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
    72 fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
    74       (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
    73       (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
    75   | numterm_ord
    74   | numterm_ord
    76      (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
    75      (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
    77      num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
    76      num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
    78   | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
    77   | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
    79   | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
    78   | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
    80   | numterm_ord (t, u) =
    79   | numterm_ord (t, u) =
    81       (case int_ord (size_of_term t, size_of_term u) of
    80       (case int_ord (size_of_term t, size_of_term u) of
    82         EQUAL =>
    81         EQUAL =>
    83           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    82           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    84             (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    83             (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    85           end
    84           end
    86       | ord => ord)
    85       | ord => ord)
    87 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    86 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    88 end;
    87 end;
    89 
    88 
   162 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
   161 fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
   163 
   162 
   164 (*Express t as a product of (possibly) a numeral with other sorted terms*)
   163 (*Express t as a product of (possibly) a numeral with other sorted terms*)
   165 fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
   164 fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
   166   | dest_coeff sign t =
   165   | dest_coeff sign t =
   167     let val ts = sort Term.term_ord (dest_prod t)
   166     let val ts = sort TermOrd.term_ord (dest_prod t)
   168         val (n, ts') = find_first_numeral [] ts
   167         val (n, ts') = find_first_numeral [] ts
   169                           handle TERM _ => (1, ts)
   168                           handle TERM _ => (1, ts)
   170     in (sign*n, mk_prod (Term.fastype_of t) ts') end;
   169     in (sign*n, mk_prod (Term.fastype_of t) ts') end;
   171 
   170 
   172 (*Find first coefficient-term THAT MATCHES u*)
   171 (*Find first coefficient-term THAT MATCHES u*)