vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
authorhaftmann
Thu Mar 12 18:01:26 2009 +0100 (2009-03-12)
changeset 304967cdcc9dd95cb
parent 30495 a5f1e4f46d14
child 30497 45b434d8ef8d
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
src/HOL/Divides.thy
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/IsaMakefile
src/HOL/NSA/NSA.thy
src/HOL/Nat.thy
src/HOL/Tools/arith_data.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/int_factor_simprocs.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/nat_arith.ML
src/HOL/Tools/nat_simprocs.ML
     1.1 --- a/src/HOL/Divides.thy	Thu Mar 12 18:01:25 2009 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Mar 12 18:01:26 2009 +0100
     1.3 @@ -572,8 +572,8 @@
     1.4  val div_name = @{const_name div};
     1.5  val mod_name = @{const_name mod};
     1.6  val mk_binop = HOLogic.mk_binop;
     1.7 -val mk_sum = ArithData.mk_sum;
     1.8 -val dest_sum = ArithData.dest_sum;
     1.9 +val mk_sum = Nat_Arith.mk_sum;
    1.10 +val dest_sum = Nat_Arith.dest_sum;
    1.11  
    1.12  (*logic*)
    1.13  
    1.14 @@ -583,7 +583,7 @@
    1.15  
    1.16  val prove_eq_sums =
    1.17    let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
    1.18 -  in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
    1.19 +  in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
    1.20  
    1.21  end;
    1.22  
     2.1 --- a/src/HOL/Int.thy	Thu Mar 12 18:01:25 2009 +0100
     2.2 +++ b/src/HOL/Int.thy	Thu Mar 12 18:01:26 2009 +0100
     2.3 @@ -1527,7 +1527,7 @@
     2.4  
     2.5  use "~~/src/Provers/Arith/assoc_fold.ML"
     2.6  use "Tools/int_arith.ML"
     2.7 -declaration {* K int_arith_setup *}
     2.8 +declaration {* K Int_Arith.setup *}
     2.9  
    2.10  
    2.11  subsection{*Lemmas About Small Numerals*}
     3.1 --- a/src/HOL/IntDiv.thy	Thu Mar 12 18:01:25 2009 +0100
     3.2 +++ b/src/HOL/IntDiv.thy	Thu Mar 12 18:01:26 2009 +0100
     3.3 @@ -261,7 +261,7 @@
     3.4    val prove_eq_sums =
     3.5      let
     3.6        val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
     3.7 -    in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
     3.8 +    in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
     3.9  end)
    3.10  
    3.11  in
     4.1 --- a/src/HOL/IsaMakefile	Thu Mar 12 18:01:25 2009 +0100
     4.2 +++ b/src/HOL/IsaMakefile	Thu Mar 12 18:01:26 2009 +0100
     4.3 @@ -175,6 +175,7 @@
     4.4    Tools/inductive_realizer.ML \
     4.5    Tools/inductive_set_package.ML \
     4.6    Tools/lin_arith.ML \
     4.7 +  Tools/nat_arith.ML \
     4.8    Tools/old_primrec_package.ML \
     4.9    Tools/primrec_package.ML \
    4.10    Tools/prop_logic.ML \
     5.1 --- a/src/HOL/NSA/NSA.thy	Thu Mar 12 18:01:25 2009 +0100
     5.2 +++ b/src/HOL/NSA/NSA.thy	Thu Mar 12 18:01:26 2009 +0100
     5.3 @@ -684,7 +684,7 @@
     5.4  
     5.5  in
     5.6  val approx_reorient_simproc =
     5.7 -  Int_Numeral_Base_Simprocs.prep_simproc
     5.8 +  Arith_Data.prep_simproc
     5.9      ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
    5.10  end;
    5.11  
     6.1 --- a/src/HOL/Nat.thy	Thu Mar 12 18:01:25 2009 +0100
     6.2 +++ b/src/HOL/Nat.thy	Thu Mar 12 18:01:26 2009 +0100
     6.3 @@ -2,7 +2,7 @@
     6.4      Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
     6.5  
     6.6  Type "nat" is a linear order, and a datatype; arithmetic operators + -
     6.7 -and * (for div, mod and dvd, see theory Divides).
     6.8 +and * (for div and mod, see theory Divides).
     6.9  *)
    6.10  
    6.11  header {* Natural numbers *}
    6.12 @@ -12,7 +12,8 @@
    6.13  uses
    6.14    "~~/src/Tools/rat.ML"
    6.15    "~~/src/Provers/Arith/cancel_sums.ML"
    6.16 -  ("Tools/arith_data.ML")
    6.17 +  "Tools/arith_data.ML"
    6.18 +  ("Tools/nat_arith.ML")
    6.19    "~~/src/Provers/Arith/fast_lin_arith.ML"
    6.20    ("Tools/lin_arith.ML")
    6.21  begin
    6.22 @@ -1344,8 +1345,8 @@
    6.23    shows "u = s"
    6.24    using 2 1 by (rule trans)
    6.25  
    6.26 -use "Tools/arith_data.ML"
    6.27 -declaration {* K ArithData.setup *}
    6.28 +use "Tools/nat_arith.ML"
    6.29 +declaration {* K Nat_Arith.setup *}
    6.30  
    6.31  ML{*
    6.32  structure ArithFacts =
     7.1 --- a/src/HOL/Tools/arith_data.ML	Thu Mar 12 18:01:25 2009 +0100
     7.2 +++ b/src/HOL/Tools/arith_data.ML	Thu Mar 12 18:01:26 2009 +0100
     7.3 @@ -1,155 +1,39 @@
     7.4  (*  Title:      HOL/arith_data.ML
     7.5      Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
     7.6  
     7.7 -Basic arithmetic proof tools.
     7.8 +Common arithmetic proof auxiliary.
     7.9  *)
    7.10  
    7.11  signature ARITH_DATA =
    7.12  sig
    7.13 -  val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
    7.14 +  val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
    7.15 +  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
    7.16 +  val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
    7.17    val simp_all_tac: thm list -> simpset -> tactic
    7.18 -
    7.19 -  val mk_sum: term list -> term
    7.20 -  val mk_norm_sum: term list -> term
    7.21 -  val dest_sum: term -> term list
    7.22 -
    7.23 -  val nat_cancel_sums_add: simproc list
    7.24 -  val nat_cancel_sums: simproc list
    7.25 -  val setup: Context.generic -> Context.generic
    7.26 +  val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
    7.27 +    -> simproc
    7.28  end;
    7.29  
    7.30 -structure ArithData: ARITH_DATA =
    7.31 +structure Arith_Data: ARITH_DATA =
    7.32  struct
    7.33  
    7.34 -(** generic proof tools **)
    7.35 +fun prove_conv_nohyps tacs ctxt (t, u) =
    7.36 +  if t aconv u then NONE
    7.37 +  else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
    7.38 +  in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
    7.39  
    7.40 -(* prove conversions *)
    7.41 +fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
    7.42  
    7.43 -fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
    7.44 +fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
    7.45    mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    7.46        (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    7.47      (K (EVERY [expand_tac, norm_tac ss]))));
    7.48  
    7.49 -(* rewriting *)
    7.50 -
    7.51  fun simp_all_tac rules =
    7.52    let val ss0 = HOL_ss addsimps rules
    7.53    in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    7.54  
    7.55 -
    7.56 -(** abstract syntax of structure nat: 0, Suc, + **)
    7.57 -
    7.58 -local
    7.59 -
    7.60 -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    7.61 -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    7.62 -
    7.63 -in
    7.64 -
    7.65 -fun mk_sum [] = HOLogic.zero
    7.66 -  | mk_sum [t] = t
    7.67 -  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    7.68 -
    7.69 -(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    7.70 -fun mk_norm_sum ts =
    7.71 -  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
    7.72 -    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    7.73 -  end;
    7.74 -
    7.75 -
    7.76 -fun dest_sum tm =
    7.77 -  if HOLogic.is_zero tm then []
    7.78 -  else
    7.79 -    (case try HOLogic.dest_Suc tm of
    7.80 -      SOME t => HOLogic.Suc_zero :: dest_sum t
    7.81 -    | NONE =>
    7.82 -        (case try dest_plus tm of
    7.83 -          SOME (t, u) => dest_sum t @ dest_sum u
    7.84 -        | NONE => [tm]));
    7.85 +fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
    7.86 +  Simplifier.simproc (the_context ()) name pats proc;
    7.87  
    7.88  end;
    7.89 -
    7.90 -
    7.91 -(** cancel common summands **)
    7.92 -
    7.93 -structure Sum =
    7.94 -struct
    7.95 -  val mk_sum = mk_norm_sum;
    7.96 -  val dest_sum = dest_sum;
    7.97 -  val prove_conv = prove_conv;
    7.98 -  val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
    7.99 -    @{thm "add_0"}, @{thm "add_0_right"}];
   7.100 -  val norm_tac2 = simp_all_tac @{thms add_ac};
   7.101 -  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
   7.102 -end;
   7.103 -
   7.104 -fun gen_uncancel_tac rule ct =
   7.105 -  rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
   7.106 -
   7.107 -
   7.108 -(* nat eq *)
   7.109 -
   7.110 -structure EqCancelSums = CancelSumsFun
   7.111 -(struct
   7.112 -  open Sum;
   7.113 -  val mk_bal = HOLogic.mk_eq;
   7.114 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   7.115 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
   7.116 -end);
   7.117 -
   7.118 -
   7.119 -(* nat less *)
   7.120 -
   7.121 -structure LessCancelSums = CancelSumsFun
   7.122 -(struct
   7.123 -  open Sum;
   7.124 -  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
   7.125 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
   7.126 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
   7.127 -end);
   7.128 -
   7.129 -
   7.130 -(* nat le *)
   7.131 -
   7.132 -structure LeCancelSums = CancelSumsFun
   7.133 -(struct
   7.134 -  open Sum;
   7.135 -  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
   7.136 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
   7.137 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
   7.138 -end);
   7.139 -
   7.140 -
   7.141 -(* nat diff *)
   7.142 -
   7.143 -structure DiffCancelSums = CancelSumsFun
   7.144 -(struct
   7.145 -  open Sum;
   7.146 -  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
   7.147 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
   7.148 -  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
   7.149 -end);
   7.150 -
   7.151 -
   7.152 -(* prepare nat_cancel simprocs *)
   7.153 -
   7.154 -val nat_cancel_sums_add =
   7.155 -  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
   7.156 -     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
   7.157 -     (K EqCancelSums.proc),
   7.158 -   Simplifier.simproc (the_context ()) "natless_cancel_sums"
   7.159 -     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
   7.160 -     (K LessCancelSums.proc),
   7.161 -   Simplifier.simproc (the_context ()) "natle_cancel_sums"
   7.162 -     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
   7.163 -     (K LeCancelSums.proc)];
   7.164 -
   7.165 -val nat_cancel_sums = nat_cancel_sums_add @
   7.166 -  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
   7.167 -    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
   7.168 -    (K DiffCancelSums.proc)];
   7.169 -
   7.170 -val setup =
   7.171 -  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
   7.172 -
   7.173 -end;
     8.1 --- a/src/HOL/Tools/int_arith.ML	Thu Mar 12 18:01:25 2009 +0100
     8.2 +++ b/src/HOL/Tools/int_arith.ML	Thu Mar 12 18:01:26 2009 +0100
     8.3 @@ -1,59 +1,32 @@
     8.4 -(*  Title:      HOL/Tools/int_arith1.ML
     8.5 -    Authors:    Larry Paulson and Tobias Nipkow
     8.6 -
     8.7 -Simprocs and decision procedure for linear arithmetic.
     8.8 -*)
     8.9 -
    8.10 -structure Int_Numeral_Base_Simprocs =
    8.11 -  struct
    8.12 -  fun prove_conv tacs ctxt (_: thm list) (t, u) =
    8.13 -    if t aconv u then NONE
    8.14 -    else
    8.15 -      let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
    8.16 -      in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end
    8.17 -
    8.18 -  fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
    8.19 -
    8.20 -  fun prep_simproc (name, pats, proc) =
    8.21 -    Simplifier.simproc (the_context()) name pats proc;
    8.22 -
    8.23 -  fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
    8.24 -    | is_numeral _ = false
    8.25 -
    8.26 -  fun simplify_meta_eq f_number_of_eq f_eq =
    8.27 -      mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
    8.28 +(* Authors: Larry Paulson and Tobias Nipkow
    8.29  
    8.30 -  (*reorientation simprules using ==, for the following simproc*)
    8.31 -  val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
    8.32 -  val meta_one_reorient = @{thm one_reorient} RS eq_reflection
    8.33 -  val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
    8.34 -
    8.35 -  (*reorientation simplification procedure: reorients (polymorphic) 
    8.36 -    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
    8.37 -  fun reorient_proc sg _ (_ $ t $ u) =
    8.38 -    case u of
    8.39 -        Const(@{const_name HOL.zero}, _) => NONE
    8.40 -      | Const(@{const_name HOL.one}, _) => NONE
    8.41 -      | Const(@{const_name Int.number_of}, _) $ _ => NONE
    8.42 -      | _ => SOME (case t of
    8.43 -          Const(@{const_name HOL.zero}, _) => meta_zero_reorient
    8.44 -        | Const(@{const_name HOL.one}, _) => meta_one_reorient
    8.45 -        | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
    8.46 -
    8.47 -  val reorient_simproc = 
    8.48 -      prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
    8.49 -
    8.50 -  end;
    8.51 -
    8.52 -
    8.53 -Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
    8.54 -
    8.55 +Simprocs and decision procedure for numerals and linear arithmetic.
    8.56 +*)
    8.57  
    8.58  structure Int_Numeral_Simprocs =
    8.59  struct
    8.60  
    8.61 -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
    8.62 -  isn't complicated by the abstract 0 and 1.*)
    8.63 +(*reorientation simprules using ==, for the following simproc*)
    8.64 +val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
    8.65 +val meta_one_reorient = @{thm one_reorient} RS eq_reflection
    8.66 +val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
    8.67 +
    8.68 +(*reorientation simplification procedure: reorients (polymorphic) 
    8.69 +  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
    8.70 +fun reorient_proc sg _ (_ $ t $ u) =
    8.71 +  case u of
    8.72 +      Const(@{const_name HOL.zero}, _) => NONE
    8.73 +    | Const(@{const_name HOL.one}, _) => NONE
    8.74 +    | Const(@{const_name Int.number_of}, _) $ _ => NONE
    8.75 +    | _ => SOME (case t of
    8.76 +        Const(@{const_name HOL.zero}, _) => meta_zero_reorient
    8.77 +      | Const(@{const_name HOL.one}, _) => meta_one_reorient
    8.78 +      | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
    8.79 +
    8.80 +val reorient_simproc = 
    8.81 +  Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
    8.82 +
    8.83 +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
    8.84  val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
    8.85  
    8.86  (** New term ordering so that AC-rewriting brings numerals to the front **)
    8.87 @@ -88,7 +61,7 @@
    8.88  
    8.89  fun numtermless tu = (numterm_ord tu = LESS);
    8.90  
    8.91 -(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
    8.92 +(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
    8.93  val num_ss = HOL_ss settermless numtermless;
    8.94  
    8.95  
    8.96 @@ -213,7 +186,7 @@
    8.97  val divide_1s = [@{thm divide_numeral_1}];
    8.98  
    8.99  (*To perform binary arithmetic.  The "left" rewriting handles patterns
   8.100 -  created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
   8.101 +  created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *)
   8.102  val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
   8.103                   @{thm add_number_of_left}, @{thm mult_number_of_left}] @
   8.104                  @{thms arith_simps} @ @{thms rel_simps};
   8.105 @@ -279,7 +252,7 @@
   8.106  
   8.107  structure EqCancelNumerals = CancelNumeralsFun
   8.108   (open CancelNumeralsCommon
   8.109 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   8.110 +  val prove_conv = Arith_Data.prove_conv
   8.111    val mk_bal   = HOLogic.mk_eq
   8.112    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   8.113    val bal_add1 = @{thm eq_add_iff1} RS trans
   8.114 @@ -288,7 +261,7 @@
   8.115  
   8.116  structure LessCancelNumerals = CancelNumeralsFun
   8.117   (open CancelNumeralsCommon
   8.118 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   8.119 +  val prove_conv = Arith_Data.prove_conv
   8.120    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   8.121    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   8.122    val bal_add1 = @{thm less_add_iff1} RS trans
   8.123 @@ -297,7 +270,7 @@
   8.124  
   8.125  structure LeCancelNumerals = CancelNumeralsFun
   8.126   (open CancelNumeralsCommon
   8.127 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   8.128 +  val prove_conv = Arith_Data.prove_conv
   8.129    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   8.130    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   8.131    val bal_add1 = @{thm le_add_iff1} RS trans
   8.132 @@ -305,7 +278,7 @@
   8.133  );
   8.134  
   8.135  val cancel_numerals =
   8.136 -  map Int_Numeral_Base_Simprocs.prep_simproc
   8.137 +  map Arith_Data.prep_simproc
   8.138     [("inteq_cancel_numerals",
   8.139       ["(l::'a::number_ring) + m = n",
   8.140        "(l::'a::number_ring) = m + n",
   8.141 @@ -342,7 +315,7 @@
   8.142    val mk_coeff          = mk_coeff
   8.143    val dest_coeff        = dest_coeff 1
   8.144    val left_distrib      = @{thm combine_common_factor} RS trans
   8.145 -  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   8.146 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   8.147    val trans_tac         = fn _ => trans_tac
   8.148  
   8.149    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   8.150 @@ -372,7 +345,7 @@
   8.151    val mk_coeff          = mk_fcoeff
   8.152    val dest_coeff        = dest_fcoeff 1
   8.153    val left_distrib      = @{thm combine_common_factor} RS trans
   8.154 -  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   8.155 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   8.156    val trans_tac         = fn _ => trans_tac
   8.157  
   8.158    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   8.159 @@ -392,23 +365,42 @@
   8.160  structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
   8.161  
   8.162  val combine_numerals =
   8.163 -  Int_Numeral_Base_Simprocs.prep_simproc
   8.164 +  Arith_Data.prep_simproc
   8.165      ("int_combine_numerals", 
   8.166       ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
   8.167       K CombineNumerals.proc);
   8.168  
   8.169  val field_combine_numerals =
   8.170 -  Int_Numeral_Base_Simprocs.prep_simproc
   8.171 +  Arith_Data.prep_simproc
   8.172      ("field_combine_numerals", 
   8.173       ["(i::'a::{number_ring,field,division_by_zero}) + j",
   8.174        "(i::'a::{number_ring,field,division_by_zero}) - j"], 
   8.175       K FieldCombineNumerals.proc);
   8.176  
   8.177 +(** Constant folding for multiplication in semirings **)
   8.178 +
   8.179 +(*We do not need folding for addition: combine_numerals does the same thing*)
   8.180 +
   8.181 +structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   8.182 +struct
   8.183 +  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   8.184 +  val eq_reflection = eq_reflection
   8.185  end;
   8.186  
   8.187 +structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
   8.188 +
   8.189 +val assoc_fold_simproc =
   8.190 +  Arith_Data.prep_simproc
   8.191 +   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
   8.192 +    K Semiring_Times_Assoc.proc);
   8.193 +
   8.194 +end;
   8.195 +
   8.196 +Addsimprocs [Int_Numeral_Simprocs.reorient_simproc];
   8.197  Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   8.198  Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
   8.199  Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
   8.200 +Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc];
   8.201  
   8.202  (*examples:
   8.203  print_depth 22;
   8.204 @@ -447,29 +439,6 @@
   8.205  test "(i + j + -12 + (k::int)) - -15 = y";
   8.206  *)
   8.207  
   8.208 -
   8.209 -(** Constant folding for multiplication in semirings **)
   8.210 -
   8.211 -(*We do not need folding for addition: combine_numerals does the same thing*)
   8.212 -
   8.213 -structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   8.214 -struct
   8.215 -  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   8.216 -  val eq_reflection = eq_reflection
   8.217 -end;
   8.218 -
   8.219 -structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
   8.220 -
   8.221 -val assoc_fold_simproc =
   8.222 -  Int_Numeral_Base_Simprocs.prep_simproc
   8.223 -   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
   8.224 -    K Semiring_Times_Assoc.proc);
   8.225 -
   8.226 -Addsimprocs [assoc_fold_simproc];
   8.227 -
   8.228 -
   8.229 -
   8.230 -
   8.231  (*** decision procedure for linear arithmetic ***)
   8.232  
   8.233  (*---------------------------------------------------------------------------*)
   8.234 @@ -480,8 +449,10 @@
   8.235  Instantiation of the generic linear arithmetic package for int.
   8.236  *)
   8.237  
   8.238 +structure Int_Arith =
   8.239 +struct
   8.240 +
   8.241  (* Update parameters of arithmetic prover *)
   8.242 -local
   8.243  
   8.244  (* reduce contradictory =/</<= to False *)
   8.245  
   8.246 @@ -489,25 +460,31 @@
   8.247     and m and n are ground terms over rings (roughly speaking).
   8.248     That is, m and n consist only of 1s combined with "+", "-" and "*".
   8.249  *)
   8.250 -local
   8.251 +
   8.252  val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
   8.253 +
   8.254  val lhss0 = [@{cpat "0::?'a::ring"}];
   8.255 +
   8.256  fun proc0 phi ss ct =
   8.257    let val T = ctyp_of_term ct
   8.258    in if typ_of T = @{typ int} then NONE else
   8.259       SOME (instantiate' [SOME T] [] zeroth)
   8.260    end;
   8.261 +
   8.262  val zero_to_of_int_zero_simproc =
   8.263    make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
   8.264    proc = proc0, identifier = []};
   8.265  
   8.266  val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
   8.267 +
   8.268  val lhss1 = [@{cpat "1::?'a::ring_1"}];
   8.269 +
   8.270  fun proc1 phi ss ct =
   8.271    let val T = ctyp_of_term ct
   8.272    in if typ_of T = @{typ int} then NONE else
   8.273       SOME (instantiate' [SOME T] [] oneth)
   8.274    end;
   8.275 +
   8.276  val one_to_of_int_one_simproc =
   8.277    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   8.278    proc = proc1, identifier = []};
   8.279 @@ -533,15 +510,15 @@
   8.280       addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
   8.281  
   8.282  fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
   8.283 +
   8.284  val lhss' =
   8.285    [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
   8.286     @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
   8.287     @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
   8.288 -in
   8.289 +
   8.290  val zero_one_idom_simproc =
   8.291    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
   8.292    proc = sproc, identifier = []}
   8.293 -end;
   8.294  
   8.295  val add_rules =
   8.296      simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
   8.297 @@ -556,13 +533,11 @@
   8.298  
   8.299  val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   8.300  
   8.301 -val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc
   8.302 +val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
   8.303    :: Int_Numeral_Simprocs.combine_numerals
   8.304    :: Int_Numeral_Simprocs.cancel_numerals;
   8.305  
   8.306 -in
   8.307 -
   8.308 -val int_arith_setup =
   8.309 +val setup =
   8.310    LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   8.311     {add_mono_thms = add_mono_thms,
   8.312      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
   8.313 @@ -570,13 +545,11 @@
   8.314      lessD = lessD @ [@{thm zless_imp_add1_zle}],
   8.315      neqE = neqE,
   8.316      simpset = simpset addsimps add_rules
   8.317 -                      addsimprocs Int_Numeral_Base_Simprocs
   8.318 +                      addsimprocs int_numeral_base_simprocs
   8.319                        addcongs [if_weak_cong]}) #>
   8.320    arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
   8.321    arith_discrete @{type_name Int.int}
   8.322  
   8.323 -end;
   8.324 -
   8.325  val fast_int_arith_simproc =
   8.326    Simplifier.simproc (the_context ())
   8.327    "fast_int_arith" 
   8.328 @@ -584,4 +557,6 @@
   8.329        "(m::'a::{ordered_idom,number_ring}) <= n",
   8.330        "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
   8.331  
   8.332 -Addsimprocs [fast_int_arith_simproc];
   8.333 +end;
   8.334 +
   8.335 +Addsimprocs [Int_Arith.fast_int_arith_simproc];
     9.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Thu Mar 12 18:01:25 2009 +0100
     9.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Thu Mar 12 18:01:26 2009 +0100
     9.3 @@ -49,7 +49,7 @@
     9.4  (*Version for integer division*)
     9.5  structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
     9.6   (open CancelNumeralFactorCommon
     9.7 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
     9.8 +  val prove_conv = Arith_Data.prove_conv
     9.9    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
    9.10    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
    9.11    val cancel = @{thm zdiv_zmult_zmult1} RS trans
    9.12 @@ -59,7 +59,7 @@
    9.13  (*Version for fields*)
    9.14  structure DivideCancelNumeralFactor = CancelNumeralFactorFun
    9.15   (open CancelNumeralFactorCommon
    9.16 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    9.17 +  val prove_conv = Arith_Data.prove_conv
    9.18    val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
    9.19    val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
    9.20    val cancel = @{thm mult_divide_mult_cancel_left} RS trans
    9.21 @@ -68,7 +68,7 @@
    9.22  
    9.23  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    9.24   (open CancelNumeralFactorCommon
    9.25 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    9.26 +  val prove_conv = Arith_Data.prove_conv
    9.27    val mk_bal   = HOLogic.mk_eq
    9.28    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    9.29    val cancel = @{thm mult_cancel_left} RS trans
    9.30 @@ -77,7 +77,7 @@
    9.31  
    9.32  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    9.33   (open CancelNumeralFactorCommon
    9.34 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    9.35 +  val prove_conv = Arith_Data.prove_conv
    9.36    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
    9.37    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
    9.38    val cancel = @{thm mult_less_cancel_left} RS trans
    9.39 @@ -86,7 +86,7 @@
    9.40  
    9.41  structure LeCancelNumeralFactor = CancelNumeralFactorFun
    9.42   (open CancelNumeralFactorCommon
    9.43 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    9.44 +  val prove_conv = Arith_Data.prove_conv
    9.45    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
    9.46    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
    9.47    val cancel = @{thm mult_le_cancel_left} RS trans
    9.48 @@ -94,7 +94,7 @@
    9.49  )
    9.50  
    9.51  val cancel_numeral_factors =
    9.52 -  map Int_Numeral_Base_Simprocs.prep_simproc
    9.53 +  map Arith_Data.prep_simproc
    9.54     [("ring_eq_cancel_numeral_factor",
    9.55       ["(l::'a::{idom,number_ring}) * m = n",
    9.56        "(l::'a::{idom,number_ring}) = m * n"],
    9.57 @@ -118,7 +118,7 @@
    9.58  
    9.59  (* referenced by rat_arith.ML *)
    9.60  val field_cancel_numeral_factors =
    9.61 -  map Int_Numeral_Base_Simprocs.prep_simproc
    9.62 +  map Arith_Data.prep_simproc
    9.63     [("field_eq_cancel_numeral_factor",
    9.64       ["(l::'a::{field,number_ring}) * m = n",
    9.65        "(l::'a::{field,number_ring}) = m * n"],
    9.66 @@ -236,7 +236,7 @@
    9.67  (*mult_cancel_left requires a ring with no zero divisors.*)
    9.68  structure EqCancelFactor = ExtractCommonTermFun
    9.69   (open CancelFactorCommon
    9.70 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    9.71 +  val prove_conv = Arith_Data.prove_conv
    9.72    val mk_bal   = HOLogic.mk_eq
    9.73    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    9.74    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_cancel_left}
    9.75 @@ -245,7 +245,7 @@
    9.76  (*zdiv_zmult_zmult1_if is for integer division (div).*)
    9.77  structure IntDivCancelFactor = ExtractCommonTermFun
    9.78   (open CancelFactorCommon
    9.79 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    9.80 +  val prove_conv = Arith_Data.prove_conv
    9.81    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
    9.82    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
    9.83    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
    9.84 @@ -253,7 +253,7 @@
    9.85  
    9.86  structure IntModCancelFactor = ExtractCommonTermFun
    9.87   (open CancelFactorCommon
    9.88 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    9.89 +  val prove_conv = Arith_Data.prove_conv
    9.90    val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
    9.91    val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
    9.92    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
    9.93 @@ -261,7 +261,7 @@
    9.94  
    9.95  structure IntDvdCancelFactor = ExtractCommonTermFun
    9.96   (open CancelFactorCommon
    9.97 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    9.98 +  val prove_conv = Arith_Data.prove_conv
    9.99    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   9.100    val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
   9.101    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
   9.102 @@ -270,14 +270,14 @@
   9.103  (*Version for all fields, including unordered ones (type complex).*)
   9.104  structure DivideCancelFactor = ExtractCommonTermFun
   9.105   (open CancelFactorCommon
   9.106 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   9.107 +  val prove_conv = Arith_Data.prove_conv
   9.108    val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   9.109    val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   9.110    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
   9.111  );
   9.112  
   9.113  val cancel_factors =
   9.114 -  map Int_Numeral_Base_Simprocs.prep_simproc
   9.115 +  map Arith_Data.prep_simproc
   9.116     [("ring_eq_cancel_factor",
   9.117       ["(l::'a::{idom}) * m = n",
   9.118        "(l::'a::{idom}) = m * n"],
    10.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Mar 12 18:01:25 2009 +0100
    10.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Mar 12 18:01:26 2009 +0100
    10.3 @@ -811,7 +811,7 @@
    10.4          @{thm "not_one_less_zero"}]
    10.5        addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
    10.6         (*abel_cancel helps it work in abstract algebraic domains*)
    10.7 -      addsimprocs ArithData.nat_cancel_sums_add}) #>
    10.8 +      addsimprocs Nat_Arith.nat_cancel_sums_add}) #>
    10.9    arith_discrete "nat";
   10.10  
   10.11  fun add_arith_facts ss =
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/nat_arith.ML	Thu Mar 12 18:01:26 2009 +0100
    11.3 @@ -0,0 +1,112 @@
    11.4 +(* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
    11.5 +
    11.6 +Basic arithmetic for natural numbers.
    11.7 +*)
    11.8 +
    11.9 +signature NAT_ARITH =
   11.10 +sig
   11.11 +  val mk_sum: term list -> term
   11.12 +  val mk_norm_sum: term list -> term
   11.13 +  val dest_sum: term -> term list
   11.14 +
   11.15 +  val nat_cancel_sums_add: simproc list
   11.16 +  val nat_cancel_sums: simproc list
   11.17 +  val setup: Context.generic -> Context.generic
   11.18 +end;
   11.19 +
   11.20 +structure Nat_Arith: NAT_ARITH =
   11.21 +struct
   11.22 +
   11.23 +(** abstract syntax of structure nat: 0, Suc, + **)
   11.24 +
   11.25 +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
   11.26 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
   11.27 +
   11.28 +fun mk_sum [] = HOLogic.zero
   11.29 +  | mk_sum [t] = t
   11.30 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   11.31 +
   11.32 +(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
   11.33 +fun mk_norm_sum ts =
   11.34 +  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
   11.35 +    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
   11.36 +  end;
   11.37 +
   11.38 +fun dest_sum tm =
   11.39 +  if HOLogic.is_zero tm then []
   11.40 +  else
   11.41 +    (case try HOLogic.dest_Suc tm of
   11.42 +      SOME t => HOLogic.Suc_zero :: dest_sum t
   11.43 +    | NONE =>
   11.44 +        (case try dest_plus tm of
   11.45 +          SOME (t, u) => dest_sum t @ dest_sum u
   11.46 +        | NONE => [tm]));
   11.47 +
   11.48 +
   11.49 +(** cancel common summands **)
   11.50 +
   11.51 +structure CommonCancelSums =
   11.52 +struct
   11.53 +  val mk_sum = mk_norm_sum;
   11.54 +  val dest_sum = dest_sum;
   11.55 +  val prove_conv = Arith_Data.prove_conv2;
   11.56 +  val norm_tac1 = Arith_Data.simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
   11.57 +    @{thm "add_0"}, @{thm "add_0_right"}];
   11.58 +  val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
   11.59 +  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
   11.60 +  fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
   11.61 +    in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
   11.62 +end;
   11.63 +
   11.64 +structure EqCancelSums = CancelSumsFun
   11.65 +(struct
   11.66 +  open CommonCancelSums;
   11.67 +  val mk_bal = HOLogic.mk_eq;
   11.68 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   11.69 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
   11.70 +end);
   11.71 +
   11.72 +structure LessCancelSums = CancelSumsFun
   11.73 +(struct
   11.74 +  open CommonCancelSums;
   11.75 +  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
   11.76 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
   11.77 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
   11.78 +end);
   11.79 +
   11.80 +structure LeCancelSums = CancelSumsFun
   11.81 +(struct
   11.82 +  open CommonCancelSums;
   11.83 +  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
   11.84 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
   11.85 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
   11.86 +end);
   11.87 +
   11.88 +structure DiffCancelSums = CancelSumsFun
   11.89 +(struct
   11.90 +  open CommonCancelSums;
   11.91 +  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
   11.92 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
   11.93 +  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
   11.94 +end);
   11.95 +
   11.96 +val nat_cancel_sums_add =
   11.97 +  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
   11.98 +     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
   11.99 +     (K EqCancelSums.proc),
  11.100 +   Simplifier.simproc (the_context ()) "natless_cancel_sums"
  11.101 +     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
  11.102 +     (K LessCancelSums.proc),
  11.103 +   Simplifier.simproc (the_context ()) "natle_cancel_sums"
  11.104 +     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
  11.105 +     (K LeCancelSums.proc)];
  11.106 +
  11.107 +val nat_cancel_sums = nat_cancel_sums_add @
  11.108 +  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
  11.109 +    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
  11.110 +    (K DiffCancelSums.proc)];
  11.111 +
  11.112 +val setup =
  11.113 +  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
  11.114 +
  11.115 +end;
    12.1 --- a/src/HOL/Tools/nat_simprocs.ML	Thu Mar 12 18:01:25 2009 +0100
    12.2 +++ b/src/HOL/Tools/nat_simprocs.ML	Thu Mar 12 18:01:26 2009 +0100
    12.3 @@ -8,8 +8,7 @@
    12.4  struct
    12.5  
    12.6  (*Maps n to #n for n = 0, 1, 2*)
    12.7 -val numeral_syms =
    12.8 -       [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
    12.9 +val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
   12.10  val numeral_sym_ss = HOL_ss addsimps numeral_syms;
   12.11  
   12.12  fun rename_numerals th =
   12.13 @@ -53,9 +52,6 @@
   12.14        @{thm Let_number_of}, @{thm nat_number_of}] @
   12.15       @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
   12.16  
   12.17 -fun prep_simproc (name, pats, proc) =
   12.18 -  Simplifier.simproc (the_context ()) name pats proc;
   12.19 -
   12.20  
   12.21  (*** CancelNumerals simprocs ***)
   12.22  
   12.23 @@ -169,7 +165,7 @@
   12.24  
   12.25  structure EqCancelNumerals = CancelNumeralsFun
   12.26   (open CancelNumeralsCommon
   12.27 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.28 +  val prove_conv = Arith_Data.prove_conv
   12.29    val mk_bal   = HOLogic.mk_eq
   12.30    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   12.31    val bal_add1 = @{thm nat_eq_add_iff1} RS trans
   12.32 @@ -178,7 +174,7 @@
   12.33  
   12.34  structure LessCancelNumerals = CancelNumeralsFun
   12.35   (open CancelNumeralsCommon
   12.36 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.37 +  val prove_conv = Arith_Data.prove_conv
   12.38    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   12.39    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   12.40    val bal_add1 = @{thm nat_less_add_iff1} RS trans
   12.41 @@ -187,7 +183,7 @@
   12.42  
   12.43  structure LeCancelNumerals = CancelNumeralsFun
   12.44   (open CancelNumeralsCommon
   12.45 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.46 +  val prove_conv = Arith_Data.prove_conv
   12.47    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   12.48    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   12.49    val bal_add1 = @{thm nat_le_add_iff1} RS trans
   12.50 @@ -196,7 +192,7 @@
   12.51  
   12.52  structure DiffCancelNumerals = CancelNumeralsFun
   12.53   (open CancelNumeralsCommon
   12.54 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.55 +  val prove_conv = Arith_Data.prove_conv
   12.56    val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
   12.57    val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
   12.58    val bal_add1 = @{thm nat_diff_add_eq1} RS trans
   12.59 @@ -205,7 +201,7 @@
   12.60  
   12.61  
   12.62  val cancel_numerals =
   12.63 -  map prep_simproc
   12.64 +  map Arith_Data.prep_simproc
   12.65     [("nateq_cancel_numerals",
   12.66       ["(l::nat) + m = n", "(l::nat) = m + n",
   12.67        "(l::nat) * m = n", "(l::nat) = m * n",
   12.68 @@ -240,7 +236,7 @@
   12.69    val mk_coeff          = mk_coeff
   12.70    val dest_coeff        = dest_coeff
   12.71    val left_distrib      = @{thm left_add_mult_distrib} RS trans
   12.72 -  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   12.73 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   12.74    val trans_tac         = fn _ => trans_tac
   12.75  
   12.76    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
   12.77 @@ -257,7 +253,7 @@
   12.78  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   12.79  
   12.80  val combine_numerals =
   12.81 -  prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
   12.82 +  Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
   12.83  
   12.84  
   12.85  (*** Applying CancelNumeralFactorFun ***)
   12.86 @@ -282,7 +278,7 @@
   12.87  
   12.88  structure DivCancelNumeralFactor = CancelNumeralFactorFun
   12.89   (open CancelNumeralFactorCommon
   12.90 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.91 +  val prove_conv = Arith_Data.prove_conv
   12.92    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   12.93    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   12.94    val cancel = @{thm nat_mult_div_cancel1} RS trans
   12.95 @@ -291,7 +287,7 @@
   12.96  
   12.97  structure DvdCancelNumeralFactor = CancelNumeralFactorFun
   12.98   (open CancelNumeralFactorCommon
   12.99 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.100 +  val prove_conv = Arith_Data.prove_conv
  12.101    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
  12.102    val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
  12.103    val cancel = @{thm nat_mult_dvd_cancel1} RS trans
  12.104 @@ -300,7 +296,7 @@
  12.105  
  12.106  structure EqCancelNumeralFactor = CancelNumeralFactorFun
  12.107   (open CancelNumeralFactorCommon
  12.108 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.109 +  val prove_conv = Arith_Data.prove_conv
  12.110    val mk_bal   = HOLogic.mk_eq
  12.111    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
  12.112    val cancel = @{thm nat_mult_eq_cancel1} RS trans
  12.113 @@ -309,7 +305,7 @@
  12.114  
  12.115  structure LessCancelNumeralFactor = CancelNumeralFactorFun
  12.116   (open CancelNumeralFactorCommon
  12.117 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.118 +  val prove_conv = Arith_Data.prove_conv
  12.119    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
  12.120    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
  12.121    val cancel = @{thm nat_mult_less_cancel1} RS trans
  12.122 @@ -318,7 +314,7 @@
  12.123  
  12.124  structure LeCancelNumeralFactor = CancelNumeralFactorFun
  12.125   (open CancelNumeralFactorCommon
  12.126 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.127 +  val prove_conv = Arith_Data.prove_conv
  12.128    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
  12.129    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
  12.130    val cancel = @{thm nat_mult_le_cancel1} RS trans
  12.131 @@ -326,7 +322,7 @@
  12.132  )
  12.133  
  12.134  val cancel_numeral_factors =
  12.135 -  map prep_simproc
  12.136 +  map Arith_Data.prep_simproc
  12.137     [("nateq_cancel_numeral_factors",
  12.138       ["(l::nat) * m = n", "(l::nat) = m * n"],
  12.139       K EqCancelNumeralFactor.proc),
  12.140 @@ -379,7 +375,7 @@
  12.141  
  12.142  structure EqCancelFactor = ExtractCommonTermFun
  12.143   (open CancelFactorCommon
  12.144 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.145 +  val prove_conv = Arith_Data.prove_conv
  12.146    val mk_bal   = HOLogic.mk_eq
  12.147    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
  12.148    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
  12.149 @@ -387,7 +383,7 @@
  12.150  
  12.151  structure LessCancelFactor = ExtractCommonTermFun
  12.152   (open CancelFactorCommon
  12.153 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.154 +  val prove_conv = Arith_Data.prove_conv
  12.155    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
  12.156    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
  12.157    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
  12.158 @@ -395,7 +391,7 @@
  12.159  
  12.160  structure LeCancelFactor = ExtractCommonTermFun
  12.161   (open CancelFactorCommon
  12.162 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.163 +  val prove_conv = Arith_Data.prove_conv
  12.164    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
  12.165    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
  12.166    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
  12.167 @@ -403,7 +399,7 @@
  12.168  
  12.169  structure DivideCancelFactor = ExtractCommonTermFun
  12.170   (open CancelFactorCommon
  12.171 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.172 +  val prove_conv = Arith_Data.prove_conv
  12.173    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
  12.174    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
  12.175    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
  12.176 @@ -411,14 +407,14 @@
  12.177  
  12.178  structure DvdCancelFactor = ExtractCommonTermFun
  12.179   (open CancelFactorCommon
  12.180 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.181 +  val prove_conv = Arith_Data.prove_conv
  12.182    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
  12.183    val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
  12.184    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
  12.185  );
  12.186  
  12.187  val cancel_factor =
  12.188 -  map prep_simproc
  12.189 +  map Arith_Data.prep_simproc
  12.190     [("nat_eq_cancel_factor",
  12.191       ["(l::nat) * m = n", "(l::nat) = m * n"],
  12.192       K EqCancelFactor.proc),