# HG changeset patch
# User haftmann
# Date 1236895285 -3600
# Node ID 1a1a9ca977d6aedd8b6129ffb8f94fb4bfd6ed84
# Parent  d09b7f0c2c140549cb87ac916400e68df0d33c47# Parent  55f2933bef6eeec94b882c2077b51c15604deade
merged

diff -r d09b7f0c2c14 -r 1a1a9ca977d6 lib/Tools/codegen
--- a/lib/Tools/codegen	Thu Mar 12 22:16:25 2009 +0100
+++ b/lib/Tools/codegen	Thu Mar 12 23:01:25 2009 +0100
@@ -33,8 +33,8 @@
 
 ## main
 
-THY=$(echo $THY | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
-ISAR="theory Codegen imports \"$THY\" begin export_code $CMD end"
+CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
+CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
+FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
 
-echo "$ISAR" | "$ISABELLE_PROCESS" -I "$IMAGE"
-exit ${PIPESTATUS[1]}
+"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Divides.thy	Thu Mar 12 23:01:25 2009 +0100
@@ -593,8 +593,8 @@
 val div_name = @{const_name div};
 val mod_name = @{const_name mod};
 val mk_binop = HOLogic.mk_binop;
-val mk_sum = ArithData.mk_sum;
-val dest_sum = ArithData.dest_sum;
+val mk_sum = Nat_Arith.mk_sum;
+val dest_sum = Nat_Arith.dest_sum;
 
 (*logic*)
 
@@ -604,7 +604,7 @@
 
 val prove_eq_sums =
   let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
-  in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
+  in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
 
 end;
 
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Int.thy	Thu Mar 12 23:01:25 2009 +0100
@@ -1527,7 +1527,7 @@
 
 use "~~/src/Provers/Arith/assoc_fold.ML"
 use "Tools/int_arith.ML"
-declaration {* K int_arith_setup *}
+declaration {* K Int_Arith.setup *}
 
 
 subsection{*Lemmas About Small Numerals*}
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/IntDiv.thy	Thu Mar 12 23:01:25 2009 +0100
@@ -261,7 +261,7 @@
   val prove_eq_sums =
     let
       val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
-    in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
+    in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
 end)
 
 in
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 12 23:01:25 2009 +0100
@@ -175,6 +175,7 @@
   Tools/inductive_realizer.ML \
   Tools/inductive_set_package.ML \
   Tools/lin_arith.ML \
+  Tools/nat_arith.ML \
   Tools/old_primrec_package.ML \
   Tools/primrec_package.ML \
   Tools/prop_logic.ML \
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Library/Random.thy
--- a/src/HOL/Library/Random.thy	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Library/Random.thy	Thu Mar 12 23:01:25 2009 +0100
@@ -21,6 +21,7 @@
 fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
   "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
 
+
 subsection {* Random seeds *}
 
 types seed = "index \<times> index"
@@ -57,29 +58,17 @@
 
 subsection {* Base selectors *}
 
-function range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
-  "range_aux k l s = (if k = 0 then (l, s) else
-    let (v, s') = next s
-  in range_aux (k - 1) (v + l * 2147483561) s')"
-by pat_completeness auto
-termination
-  by (relation "measure (Code_Index.nat_of o fst)")
-    (auto simp add: index)
+fun %quote iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+  "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
 
-definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
-  "range k = range_aux (log 2147483561 k) 1
+definition %quote range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
+  "range k = iterate (log 2147483561 k)
+      (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
     o\<rightarrow> (\<lambda>v. Pair (v mod k))"
 
 lemma range:
-  assumes "k > 0"
-  shows "fst (range k s) < k"
-proof -
-  obtain v w where range_aux:
-    "range_aux (log 2147483561 k) 1 s = (v, w)"
-    by (cases "range_aux (log 2147483561 k) 1 s")
-  with assms show ?thesis
-    by (simp add: scomp_apply range_def del: range_aux.simps log.simps)
-qed
+  "k > 0 \<Longrightarrow> fst (range k s) < k"
+  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
 
 definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   "select xs = range (Code_Index.of_nat (length xs))
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/NSA/NSA.thy	Thu Mar 12 23:01:25 2009 +0100
@@ -684,7 +684,7 @@
 
 in
 val approx_reorient_simproc =
-  Int_Numeral_Base_Simprocs.prep_simproc
+  Arith_Data.prep_simproc
     ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
 end;
 
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Nat.thy	Thu Mar 12 23:01:25 2009 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
 
 Type "nat" is a linear order, and a datatype; arithmetic operators + -
-and * (for div, mod and dvd, see theory Divides).
+and * (for div and mod, see theory Divides).
 *)
 
 header {* Natural numbers *}
@@ -12,7 +12,8 @@
 uses
   "~~/src/Tools/rat.ML"
   "~~/src/Provers/Arith/cancel_sums.ML"
-  ("Tools/arith_data.ML")
+  "Tools/arith_data.ML"
+  ("Tools/nat_arith.ML")
   "~~/src/Provers/Arith/fast_lin_arith.ML"
   ("Tools/lin_arith.ML")
 begin
@@ -1344,8 +1345,8 @@
   shows "u = s"
   using 2 1 by (rule trans)
 
-use "Tools/arith_data.ML"
-declaration {* K ArithData.setup *}
+use "Tools/nat_arith.ML"
+declaration {* K Nat_Arith.setup *}
 
 ML{*
 structure ArithFacts =
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/NatBin.thy	Thu Mar 12 23:01:25 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/NatBin.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
 *)
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Thu Mar 12 23:01:25 2009 +0100
@@ -1,155 +1,39 @@
 (*  Title:      HOL/arith_data.ML
     Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
 
-Basic arithmetic proof tools.
+Common arithmetic proof auxiliary.
 *)
 
 signature ARITH_DATA =
 sig
-  val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
+  val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
+  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
+  val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
   val simp_all_tac: thm list -> simpset -> tactic
-
-  val mk_sum: term list -> term
-  val mk_norm_sum: term list -> term
-  val dest_sum: term -> term list
-
-  val nat_cancel_sums_add: simproc list
-  val nat_cancel_sums: simproc list
-  val setup: Context.generic -> Context.generic
+  val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
+    -> simproc
 end;
 
-structure ArithData: ARITH_DATA =
+structure Arith_Data: ARITH_DATA =
 struct
 
-(** generic proof tools **)
+fun prove_conv_nohyps tacs ctxt (t, u) =
+  if t aconv u then NONE
+  else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
+  in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
 
-(* prove conversions *)
+fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
 
-fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
+fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
   mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
     (K (EVERY [expand_tac, norm_tac ss]))));
 
-(* rewriting *)
-
 fun simp_all_tac rules =
   let val ss0 = HOL_ss addsimps rules
   in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
 
-
-(** abstract syntax of structure nat: 0, Suc, + **)
-
-local
-
-val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
-val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
-
-in
-
-fun mk_sum [] = HOLogic.zero
-  | mk_sum [t] = t
-  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
-fun mk_norm_sum ts =
-  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
-    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
-  end;
-
-
-fun dest_sum tm =
-  if HOLogic.is_zero tm then []
-  else
-    (case try HOLogic.dest_Suc tm of
-      SOME t => HOLogic.Suc_zero :: dest_sum t
-    | NONE =>
-        (case try dest_plus tm of
-          SOME (t, u) => dest_sum t @ dest_sum u
-        | NONE => [tm]));
+fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
+  Simplifier.simproc (the_context ()) name pats proc;
 
 end;
-
-
-(** cancel common summands **)
-
-structure Sum =
-struct
-  val mk_sum = mk_norm_sum;
-  val dest_sum = dest_sum;
-  val prove_conv = prove_conv;
-  val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
-    @{thm "add_0"}, @{thm "add_0_right"}];
-  val norm_tac2 = simp_all_tac @{thms add_ac};
-  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
-end;
-
-fun gen_uncancel_tac rule ct =
-  rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
-
-
-(* nat eq *)
-
-structure EqCancelSums = CancelSumsFun
-(struct
-  open Sum;
-  val mk_bal = HOLogic.mk_eq;
-  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
-end);
-
-
-(* nat less *)
-
-structure LessCancelSums = CancelSumsFun
-(struct
-  open Sum;
-  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
-end);
-
-
-(* nat le *)
-
-structure LeCancelSums = CancelSumsFun
-(struct
-  open Sum;
-  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
-end);
-
-
-(* nat diff *)
-
-structure DiffCancelSums = CancelSumsFun
-(struct
-  open Sum;
-  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
-end);
-
-
-(* prepare nat_cancel simprocs *)
-
-val nat_cancel_sums_add =
-  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
-     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
-     (K EqCancelSums.proc),
-   Simplifier.simproc (the_context ()) "natless_cancel_sums"
-     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
-     (K LessCancelSums.proc),
-   Simplifier.simproc (the_context ()) "natle_cancel_sums"
-     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
-     (K LeCancelSums.proc)];
-
-val nat_cancel_sums = nat_cancel_sums_add @
-  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
-    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
-    (K DiffCancelSums.proc)];
-
-val setup =
-  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
-
-end;
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Tools/int_arith.ML	Thu Mar 12 23:01:25 2009 +0100
@@ -1,59 +1,32 @@
-(*  Title:      HOL/Tools/int_arith1.ML
-    Authors:    Larry Paulson and Tobias Nipkow
-
-Simprocs and decision procedure for linear arithmetic.
-*)
-
-structure Int_Numeral_Base_Simprocs =
-  struct
-  fun prove_conv tacs ctxt (_: thm list) (t, u) =
-    if t aconv u then NONE
-    else
-      let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
-      in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end
-
-  fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
-
-  fun prep_simproc (name, pats, proc) =
-    Simplifier.simproc (the_context()) name pats proc;
-
-  fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
-    | is_numeral _ = false
-
-  fun simplify_meta_eq f_number_of_eq f_eq =
-      mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
+(* Authors: Larry Paulson and Tobias Nipkow
 
-  (*reorientation simprules using ==, for the following simproc*)
-  val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
-  val meta_one_reorient = @{thm one_reorient} RS eq_reflection
-  val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
-
-  (*reorientation simplification procedure: reorients (polymorphic) 
-    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
-  fun reorient_proc sg _ (_ $ t $ u) =
-    case u of
-        Const(@{const_name HOL.zero}, _) => NONE
-      | Const(@{const_name HOL.one}, _) => NONE
-      | Const(@{const_name Int.number_of}, _) $ _ => NONE
-      | _ => SOME (case t of
-          Const(@{const_name HOL.zero}, _) => meta_zero_reorient
-        | Const(@{const_name HOL.one}, _) => meta_one_reorient
-        | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
-
-  val reorient_simproc = 
-      prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
-
-  end;
-
-
-Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
-
+Simprocs and decision procedure for numerals and linear arithmetic.
+*)
 
 structure Int_Numeral_Simprocs =
 struct
 
-(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
-  isn't complicated by the abstract 0 and 1.*)
+(*reorientation simprules using ==, for the following simproc*)
+val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
+val meta_one_reorient = @{thm one_reorient} RS eq_reflection
+val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
+
+(*reorientation simplification procedure: reorients (polymorphic) 
+  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
+fun reorient_proc sg _ (_ $ t $ u) =
+  case u of
+      Const(@{const_name HOL.zero}, _) => NONE
+    | Const(@{const_name HOL.one}, _) => NONE
+    | Const(@{const_name Int.number_of}, _) $ _ => NONE
+    | _ => SOME (case t of
+        Const(@{const_name HOL.zero}, _) => meta_zero_reorient
+      | Const(@{const_name HOL.one}, _) => meta_one_reorient
+      | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
+
+val reorient_simproc = 
+  Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
+
+(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
 val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
 
 (** New term ordering so that AC-rewriting brings numerals to the front **)
@@ -88,7 +61,7 @@
 
 fun numtermless tu = (numterm_ord tu = LESS);
 
-(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
+(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
 val num_ss = HOL_ss settermless numtermless;
 
 
@@ -213,7 +186,7 @@
 val divide_1s = [@{thm divide_numeral_1}];
 
 (*To perform binary arithmetic.  The "left" rewriting handles patterns
-  created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
+  created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *)
 val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
                  @{thm add_number_of_left}, @{thm mult_number_of_left}] @
                 @{thms arith_simps} @ @{thms rel_simps};
@@ -279,7 +252,7 @@
 
 structure EqCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   val bal_add1 = @{thm eq_add_iff1} RS trans
@@ -288,7 +261,7 @@
 
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   val bal_add1 = @{thm less_add_iff1} RS trans
@@ -297,7 +270,7 @@
 
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   val bal_add1 = @{thm le_add_iff1} RS trans
@@ -305,7 +278,7 @@
 );
 
 val cancel_numerals =
-  map Int_Numeral_Base_Simprocs.prep_simproc
+  map Arith_Data.prep_simproc
    [("inteq_cancel_numerals",
      ["(l::'a::number_ring) + m = n",
       "(l::'a::number_ring) = m + n",
@@ -342,7 +315,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val left_distrib      = @{thm combine_common_factor} RS trans
-  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
+  val prove_conv        = Arith_Data.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
@@ -372,7 +345,7 @@
   val mk_coeff          = mk_fcoeff
   val dest_coeff        = dest_fcoeff 1
   val left_distrib      = @{thm combine_common_factor} RS trans
-  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
+  val prove_conv        = Arith_Data.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
@@ -392,23 +365,42 @@
 structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
 
 val combine_numerals =
-  Int_Numeral_Base_Simprocs.prep_simproc
+  Arith_Data.prep_simproc
     ("int_combine_numerals", 
      ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
      K CombineNumerals.proc);
 
 val field_combine_numerals =
-  Int_Numeral_Base_Simprocs.prep_simproc
+  Arith_Data.prep_simproc
     ("field_combine_numerals", 
      ["(i::'a::{number_ring,field,division_by_zero}) + j",
       "(i::'a::{number_ring,field,division_by_zero}) - j"], 
      K FieldCombineNumerals.proc);
 
+(** Constant folding for multiplication in semirings **)
+
+(*We do not need folding for addition: combine_numerals does the same thing*)
+
+structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
+struct
+  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
+  val eq_reflection = eq_reflection
 end;
 
+structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
+
+val assoc_fold_simproc =
+  Arith_Data.prep_simproc
+   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
+    K Semiring_Times_Assoc.proc);
+
+end;
+
+Addsimprocs [Int_Numeral_Simprocs.reorient_simproc];
 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
 Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
 Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
+Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc];
 
 (*examples:
 print_depth 22;
@@ -447,29 +439,6 @@
 test "(i + j + -12 + (k::int)) - -15 = y";
 *)
 
-
-(** Constant folding for multiplication in semirings **)
-
-(*We do not need folding for addition: combine_numerals does the same thing*)
-
-structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
-struct
-  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
-  val eq_reflection = eq_reflection
-end;
-
-structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
-
-val assoc_fold_simproc =
-  Int_Numeral_Base_Simprocs.prep_simproc
-   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
-    K Semiring_Times_Assoc.proc);
-
-Addsimprocs [assoc_fold_simproc];
-
-
-
-
 (*** decision procedure for linear arithmetic ***)
 
 (*---------------------------------------------------------------------------*)
@@ -480,8 +449,10 @@
 Instantiation of the generic linear arithmetic package for int.
 *)
 
+structure Int_Arith =
+struct
+
 (* Update parameters of arithmetic prover *)
-local
 
 (* reduce contradictory =/</<= to False *)
 
@@ -489,25 +460,31 @@
    and m and n are ground terms over rings (roughly speaking).
    That is, m and n consist only of 1s combined with "+", "-" and "*".
 *)
-local
+
 val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
+
 val lhss0 = [@{cpat "0::?'a::ring"}];
+
 fun proc0 phi ss ct =
   let val T = ctyp_of_term ct
   in if typ_of T = @{typ int} then NONE else
      SOME (instantiate' [SOME T] [] zeroth)
   end;
+
 val zero_to_of_int_zero_simproc =
   make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
   proc = proc0, identifier = []};
 
 val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
+
 val lhss1 = [@{cpat "1::?'a::ring_1"}];
+
 fun proc1 phi ss ct =
   let val T = ctyp_of_term ct
   in if typ_of T = @{typ int} then NONE else
      SOME (instantiate' [SOME T] [] oneth)
   end;
+
 val one_to_of_int_one_simproc =
   make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   proc = proc1, identifier = []};
@@ -533,15 +510,15 @@
      addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
 
 fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
+
 val lhss' =
   [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
    @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
    @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
-in
+
 val zero_one_idom_simproc =
   make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
   proc = sproc, identifier = []}
-end;
 
 val add_rules =
     simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
@@ -556,13 +533,11 @@
 
 val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
 
-val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc
+val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
   :: Int_Numeral_Simprocs.combine_numerals
   :: Int_Numeral_Simprocs.cancel_numerals;
 
-in
-
-val int_arith_setup =
+val setup =
   LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
@@ -570,13 +545,11 @@
     lessD = lessD @ [@{thm zless_imp_add1_zle}],
     neqE = neqE,
     simpset = simpset addsimps add_rules
-                      addsimprocs Int_Numeral_Base_Simprocs
+                      addsimprocs int_numeral_base_simprocs
                       addcongs [if_weak_cong]}) #>
   arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
   arith_discrete @{type_name Int.int}
 
-end;
-
 val fast_int_arith_simproc =
   Simplifier.simproc (the_context ())
   "fast_int_arith" 
@@ -584,4 +557,6 @@
       "(m::'a::{ordered_idom,number_ring}) <= n",
       "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
 
-Addsimprocs [fast_int_arith_simproc];
+end;
+
+Addsimprocs [Int_Arith.fast_int_arith_simproc];
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Tools/int_factor_simprocs.ML
--- a/src/HOL/Tools/int_factor_simprocs.ML	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Thu Mar 12 23:01:25 2009 +0100
@@ -49,7 +49,7 @@
 (*Version for integer division*)
 structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
   val cancel = @{thm zdiv_zmult_zmult1} RS trans
@@ -59,7 +59,7 @@
 (*Version for fields*)
 structure DivideCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   val cancel = @{thm mult_divide_mult_cancel_left} RS trans
@@ -68,7 +68,7 @@
 
 structure EqCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   val cancel = @{thm mult_cancel_left} RS trans
@@ -77,7 +77,7 @@
 
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   val cancel = @{thm mult_less_cancel_left} RS trans
@@ -86,7 +86,7 @@
 
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   val cancel = @{thm mult_le_cancel_left} RS trans
@@ -94,7 +94,7 @@
 )
 
 val cancel_numeral_factors =
-  map Int_Numeral_Base_Simprocs.prep_simproc
+  map Arith_Data.prep_simproc
    [("ring_eq_cancel_numeral_factor",
      ["(l::'a::{idom,number_ring}) * m = n",
       "(l::'a::{idom,number_ring}) = m * n"],
@@ -118,7 +118,7 @@
 
 (* referenced by rat_arith.ML *)
 val field_cancel_numeral_factors =
-  map Int_Numeral_Base_Simprocs.prep_simproc
+  map Arith_Data.prep_simproc
    [("field_eq_cancel_numeral_factor",
      ["(l::'a::{field,number_ring}) * m = n",
       "(l::'a::{field,number_ring}) = m * n"],
@@ -236,7 +236,7 @@
 (*mult_cancel_left requires a ring with no zero divisors.*)
 structure EqCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_cancel_left}
@@ -245,7 +245,7 @@
 (*zdiv_zmult_zmult1_if is for integer division (div).*)
 structure IntDivCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
@@ -253,7 +253,7 @@
 
 structure IntModCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
@@ -261,7 +261,7 @@
 
 structure IntDvdCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
@@ -270,14 +270,14 @@
 (*Version for all fields, including unordered ones (type complex).*)
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
 );
 
 val cancel_factors =
-  map Int_Numeral_Base_Simprocs.prep_simproc
+  map Arith_Data.prep_simproc
    [("ring_eq_cancel_factor",
      ["(l::'a::{idom}) * m = n",
       "(l::'a::{idom}) = m * n"],
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Thu Mar 12 23:01:25 2009 +0100
@@ -811,7 +811,7 @@
         @{thm "not_one_less_zero"}]
       addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
        (*abel_cancel helps it work in abstract algebraic domains*)
-      addsimprocs ArithData.nat_cancel_sums_add}) #>
+      addsimprocs Nat_Arith.nat_cancel_sums_add}) #>
   arith_discrete "nat";
 
 fun add_arith_facts ss =
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Tools/nat_arith.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/nat_arith.ML	Thu Mar 12 23:01:25 2009 +0100
@@ -0,0 +1,112 @@
+(* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
+
+Basic arithmetic for natural numbers.
+*)
+
+signature NAT_ARITH =
+sig
+  val mk_sum: term list -> term
+  val mk_norm_sum: term list -> term
+  val dest_sum: term -> term list
+
+  val nat_cancel_sums_add: simproc list
+  val nat_cancel_sums: simproc list
+  val setup: Context.generic -> Context.generic
+end;
+
+structure Nat_Arith: NAT_ARITH =
+struct
+
+(** abstract syntax of structure nat: 0, Suc, + **)
+
+val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
+val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
+
+fun mk_sum [] = HOLogic.zero
+  | mk_sum [t] = t
+  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
+fun mk_norm_sum ts =
+  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
+    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
+  end;
+
+fun dest_sum tm =
+  if HOLogic.is_zero tm then []
+  else
+    (case try HOLogic.dest_Suc tm of
+      SOME t => HOLogic.Suc_zero :: dest_sum t
+    | NONE =>
+        (case try dest_plus tm of
+          SOME (t, u) => dest_sum t @ dest_sum u
+        | NONE => [tm]));
+
+
+(** cancel common summands **)
+
+structure CommonCancelSums =
+struct
+  val mk_sum = mk_norm_sum;
+  val dest_sum = dest_sum;
+  val prove_conv = Arith_Data.prove_conv2;
+  val norm_tac1 = Arith_Data.simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
+    @{thm "add_0"}, @{thm "add_0_right"}];
+  val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
+  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
+  fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
+    in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
+end;
+
+structure EqCancelSums = CancelSumsFun
+(struct
+  open CommonCancelSums;
+  val mk_bal = HOLogic.mk_eq;
+  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
+end);
+
+structure LessCancelSums = CancelSumsFun
+(struct
+  open CommonCancelSums;
+  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
+end);
+
+structure LeCancelSums = CancelSumsFun
+(struct
+  open CommonCancelSums;
+  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
+end);
+
+structure DiffCancelSums = CancelSumsFun
+(struct
+  open CommonCancelSums;
+  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
+end);
+
+val nat_cancel_sums_add =
+  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
+     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
+     (K EqCancelSums.proc),
+   Simplifier.simproc (the_context ()) "natless_cancel_sums"
+     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
+     (K LessCancelSums.proc),
+   Simplifier.simproc (the_context ()) "natle_cancel_sums"
+     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
+     (K LeCancelSums.proc)];
+
+val nat_cancel_sums = nat_cancel_sums_add @
+  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
+    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
+    (K DiffCancelSums.proc)];
+
+val setup =
+  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
+
+end;
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Tools/nat_simprocs.ML
--- a/src/HOL/Tools/nat_simprocs.ML	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML	Thu Mar 12 23:01:25 2009 +0100
@@ -8,8 +8,7 @@
 struct
 
 (*Maps n to #n for n = 0, 1, 2*)
-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];
+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];
 val numeral_sym_ss = HOL_ss addsimps numeral_syms;
 
 fun rename_numerals th =
@@ -53,9 +52,6 @@
       @{thm Let_number_of}, @{thm nat_number_of}] @
      @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
 
-fun prep_simproc (name, pats, proc) =
-  Simplifier.simproc (the_context ()) name pats proc;
-
 
 (*** CancelNumerals simprocs ***)
 
@@ -169,7 +165,7 @@
 
 structure EqCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   val bal_add1 = @{thm nat_eq_add_iff1} RS trans
@@ -178,7 +174,7 @@
 
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   val bal_add1 = @{thm nat_less_add_iff1} RS trans
@@ -187,7 +183,7 @@
 
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   val bal_add1 = @{thm nat_le_add_iff1} RS trans
@@ -196,7 +192,7 @@
 
 structure DiffCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
   val bal_add1 = @{thm nat_diff_add_eq1} RS trans
@@ -205,7 +201,7 @@
 
 
 val cancel_numerals =
-  map prep_simproc
+  map Arith_Data.prep_simproc
    [("nateq_cancel_numerals",
      ["(l::nat) + m = n", "(l::nat) = m + n",
       "(l::nat) * m = n", "(l::nat) = m * n",
@@ -240,7 +236,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val left_distrib      = @{thm left_add_mult_distrib} RS trans
-  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
+  val prove_conv        = Arith_Data.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
@@ -257,7 +253,7 @@
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
 
 val combine_numerals =
-  prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
+  Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
 
 
 (*** Applying CancelNumeralFactorFun ***)
@@ -282,7 +278,7 @@
 
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   val cancel = @{thm nat_mult_div_cancel1} RS trans
@@ -291,7 +287,7 @@
 
 structure DvdCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
   val cancel = @{thm nat_mult_dvd_cancel1} RS trans
@@ -300,7 +296,7 @@
 
 structure EqCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   val cancel = @{thm nat_mult_eq_cancel1} RS trans
@@ -309,7 +305,7 @@
 
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   val cancel = @{thm nat_mult_less_cancel1} RS trans
@@ -318,7 +314,7 @@
 
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   val cancel = @{thm nat_mult_le_cancel1} RS trans
@@ -326,7 +322,7 @@
 )
 
 val cancel_numeral_factors =
-  map prep_simproc
+  map Arith_Data.prep_simproc
    [("nateq_cancel_numeral_factors",
      ["(l::nat) * m = n", "(l::nat) = m * n"],
      K EqCancelNumeralFactor.proc),
@@ -379,7 +375,7 @@
 
 structure EqCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
@@ -387,7 +383,7 @@
 
 structure LessCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
@@ -395,7 +391,7 @@
 
 structure LeCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
@@ -403,7 +399,7 @@
 
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
@@ -411,14 +407,14 @@
 
 structure DvdCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
-  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
 );
 
 val cancel_factor =
-  map prep_simproc
+  map Arith_Data.prep_simproc
    [("nat_eq_cancel_factor",
      ["(l::nat) * m = n", "(l::nat) = m * n"],
      K EqCancelFactor.proc),
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/HOL/Tools/rat_arith.ML
--- a/src/HOL/Tools/rat_arith.ML	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/HOL/Tools/rat_arith.ML	Thu Mar 12 23:01:25 2009 +0100
@@ -34,8 +34,6 @@
 
 in
 
-val ratT = Type ("Rational.rat", [])
-
 val rat_arith_setup =
   LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
@@ -45,7 +43,7 @@
     neqE =  neqE,
     simpset = simpset addsimps simps
                       addsimprocs simprocs}) #>
-  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> ratT) #>
-  arith_inj_const (@{const_name of_int}, HOLogic.intT --> ratT)
+  arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
+  arith_inj_const (@{const_name of_int}, @{typ "int => rat"})
 
 end;
diff -r d09b7f0c2c14 -r 1a1a9ca977d6 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Thu Mar 12 22:16:25 2009 +0100
+++ b/src/Tools/code/code_target.ML	Thu Mar 12 23:01:25 2009 +0100
@@ -37,6 +37,7 @@
   val string: string list -> serialization -> string
   val code_of: theory -> string -> string
     -> string list -> (Code_Thingol.naming -> string list) -> string
+  val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
   val code_width: int ref
 
   val allow_abort: string -> theory -> theory
@@ -527,13 +528,13 @@
 
 val (inK, module_nameK, fileK) = ("in", "module_name", "file");
 
-fun code_exprP cmd =
+val code_exprP =
   (Scan.repeat P.term_group
   -- Scan.repeat (P.$$$ inK |-- P.name
      -- Scan.option (P.$$$ module_nameK |-- P.name)
      -- Scan.option (P.$$$ fileK |-- P.name)
      -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
-  ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
+  ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
 
 val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
 
@@ -594,7 +595,14 @@
 
 val _ =
   OuterSyntax.command "export_code" "generate executable code for constants"
-    K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+    K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+
+fun shell_command thyname cmd = Toplevel.program (fn _ =>
+  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP)
+    ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
+   of SOME f => (writeln "Now generating code..."; f (theory thyname))
+    | NONE => error ("Bad directive " ^ quote cmd)))
+  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
 
 end; (*local*)