Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Integ/int_arith1.ML
changeset 14738 83f1a514dcb4
parent 14474 00292f6f8d13
child 15013 34264f5e4691
equal deleted inserted replaced
14737:77ea79aed99d 14738:83f1a514dcb4 
   381       "(l::'a::number_ring) = m - n",
 
   381       "(l::'a::number_ring) = m - n",
 
   382       "(l::'a::number_ring) * m = n",
 
   382       "(l::'a::number_ring) * m = n",
 
   383       "(l::'a::number_ring) = m * n"],
 
   383       "(l::'a::number_ring) = m * n"],
 
   384      EqCancelNumerals.proc),
 
   384      EqCancelNumerals.proc),
 
   385     ("intless_cancel_numerals",
 
   385     ("intless_cancel_numerals",
 
   386      ["(l::'a::{ordered_ring,number_ring}) + m < n",
 
   386      ["(l::'a::{ordered_idom,number_ring}) + m < n",
 
   387       "(l::'a::{ordered_ring,number_ring}) < m + n",
 
   387       "(l::'a::{ordered_idom,number_ring}) < m + n",
 
   388       "(l::'a::{ordered_ring,number_ring}) - m < n",
 
   388       "(l::'a::{ordered_idom,number_ring}) - m < n",
 
   389       "(l::'a::{ordered_ring,number_ring}) < m - n",
 
   389       "(l::'a::{ordered_idom,number_ring}) < m - n",
 
   390       "(l::'a::{ordered_ring,number_ring}) * m < n",
 
   390       "(l::'a::{ordered_idom,number_ring}) * m < n",
 
   391       "(l::'a::{ordered_ring,number_ring}) < m * n"],
 
   391       "(l::'a::{ordered_idom,number_ring}) < m * n"],
 
   392      LessCancelNumerals.proc),
 
   392      LessCancelNumerals.proc),
 
   393     ("intle_cancel_numerals",
 
   393     ("intle_cancel_numerals",
 
   394      ["(l::'a::{ordered_ring,number_ring}) + m <= n",
 
   394      ["(l::'a::{ordered_idom,number_ring}) + m <= n",
 
   395       "(l::'a::{ordered_ring,number_ring}) <= m + n",
 
   395       "(l::'a::{ordered_idom,number_ring}) <= m + n",
 
   396       "(l::'a::{ordered_ring,number_ring}) - m <= n",
 
   396       "(l::'a::{ordered_idom,number_ring}) - m <= n",
 
   397       "(l::'a::{ordered_ring,number_ring}) <= m - n",
 
   397       "(l::'a::{ordered_idom,number_ring}) <= m - n",
 
   398       "(l::'a::{ordered_ring,number_ring}) * m <= n",
 
   398       "(l::'a::{ordered_idom,number_ring}) * m <= n",
 
   399       "(l::'a::{ordered_ring,number_ring}) <= m * n"],
 
   399       "(l::'a::{ordered_idom,number_ring}) <= m * n"],
 
   400      LeCancelNumerals.proc)];
 
   400      LeCancelNumerals.proc)];
 
   401 
   401 
   402 
   402 
   403 structure CombineNumeralsData =
 
   403 structure CombineNumeralsData =
 
   404   struct
 
   404   struct
 
   486 
   486 
   487 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
 
   487 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
 
   488 
   488 
   489 val assoc_fold_simproc =
 
   489 val assoc_fold_simproc =
 
   490   Bin_Simprocs.prep_simproc
 
   490   Bin_Simprocs.prep_simproc
 
   491    ("semiring_assoc_fold", ["(a::'a::semiring) * b"],
 
   491    ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
 
   492     Semiring_Times_Assoc.proc);
 
   492     Semiring_Times_Assoc.proc);
 
   493 
   493 
   494 Addsimprocs [assoc_fold_simproc];
 
   494 Addsimprocs [assoc_fold_simproc];
 
   495 
   495 
   496 
   496 
   543 end;
 
   543 end;
 
   544 
   544 
   545 val fast_int_arith_simproc =
 
   545 val fast_int_arith_simproc =
 
   546   Simplifier.simproc (Theory.sign_of (the_context()))
 
   546   Simplifier.simproc (Theory.sign_of (the_context()))
 
   547   "fast_int_arith" 
   547   "fast_int_arith" 
   548      ["(m::'a::{ordered_ring,number_ring}) < n",
 
   548      ["(m::'a::{ordered_idom,number_ring}) < n",
 
   549       "(m::'a::{ordered_ring,number_ring}) <= n",
 
   549       "(m::'a::{ordered_idom,number_ring}) <= n",
 
   550       "(m::'a::{ordered_ring,number_ring}) = n"] Fast_Arith.lin_arith_prover;
 
   550       "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover;
 
   551 
   551 
   552 Addsimprocs [fast_int_arith_simproc]
 
   552 Addsimprocs [fast_int_arith_simproc]
 
   553 
   553 
   554 
   554 
   555 (* Some test data
 
   555 (* Some test data
wneuper/isa