merged
authorhaftmann
Thu Mar 12 23:01:25 2009 +0100 (2009-03-12)
changeset 304991a1a9ca977d6
parent 30490 d09b7f0c2c14
parent 30498 55f2933bef6e
child 30500 072daf3914c0
merged
src/HOL/Divides.thy
src/HOL/IsaMakefile
     1.1 --- a/lib/Tools/codegen	Thu Mar 12 22:16:25 2009 +0100
     1.2 +++ b/lib/Tools/codegen	Thu Mar 12 23:01:25 2009 +0100
     1.3 @@ -33,8 +33,8 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 -THY=$(echo $THY | sed -e 's/\\/\\\\"/g; s/"/\\\"/g')
     1.8 -ISAR="theory Codegen imports \"$THY\" begin export_code $CMD end"
     1.9 +CODE_CMD=$(echo $CMD | perl -pe 's/\\/\\\\/g; s/"/\\\"/g')
    1.10 +CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";"
    1.11 +FULL_CMD="val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD"
    1.12  
    1.13 -echo "$ISAR" | "$ISABELLE_PROCESS" -I "$IMAGE"
    1.14 -exit ${PIPESTATUS[1]}
    1.15 +"$ISABELLE" -q -e "$FULL_CMD" "$IMAGE" || exit 1
     2.1 --- a/src/HOL/Divides.thy	Thu Mar 12 22:16:25 2009 +0100
     2.2 +++ b/src/HOL/Divides.thy	Thu Mar 12 23:01:25 2009 +0100
     2.3 @@ -593,8 +593,8 @@
     2.4  val div_name = @{const_name div};
     2.5  val mod_name = @{const_name mod};
     2.6  val mk_binop = HOLogic.mk_binop;
     2.7 -val mk_sum = ArithData.mk_sum;
     2.8 -val dest_sum = ArithData.dest_sum;
     2.9 +val mk_sum = Nat_Arith.mk_sum;
    2.10 +val dest_sum = Nat_Arith.dest_sum;
    2.11  
    2.12  (*logic*)
    2.13  
    2.14 @@ -604,7 +604,7 @@
    2.15  
    2.16  val prove_eq_sums =
    2.17    let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
    2.18 -  in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
    2.19 +  in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
    2.20  
    2.21  end;
    2.22  
     3.1 --- a/src/HOL/Int.thy	Thu Mar 12 22:16:25 2009 +0100
     3.2 +++ b/src/HOL/Int.thy	Thu Mar 12 23:01:25 2009 +0100
     3.3 @@ -1527,7 +1527,7 @@
     3.4  
     3.5  use "~~/src/Provers/Arith/assoc_fold.ML"
     3.6  use "Tools/int_arith.ML"
     3.7 -declaration {* K int_arith_setup *}
     3.8 +declaration {* K Int_Arith.setup *}
     3.9  
    3.10  
    3.11  subsection{*Lemmas About Small Numerals*}
     4.1 --- a/src/HOL/IntDiv.thy	Thu Mar 12 22:16:25 2009 +0100
     4.2 +++ b/src/HOL/IntDiv.thy	Thu Mar 12 23:01:25 2009 +0100
     4.3 @@ -261,7 +261,7 @@
     4.4    val prove_eq_sums =
     4.5      let
     4.6        val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
     4.7 -    in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
     4.8 +    in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
     4.9  end)
    4.10  
    4.11  in
     5.1 --- a/src/HOL/IsaMakefile	Thu Mar 12 22:16:25 2009 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Thu Mar 12 23:01:25 2009 +0100
     5.3 @@ -175,6 +175,7 @@
     5.4    Tools/inductive_realizer.ML \
     5.5    Tools/inductive_set_package.ML \
     5.6    Tools/lin_arith.ML \
     5.7 +  Tools/nat_arith.ML \
     5.8    Tools/old_primrec_package.ML \
     5.9    Tools/primrec_package.ML \
    5.10    Tools/prop_logic.ML \
     6.1 --- a/src/HOL/Library/Random.thy	Thu Mar 12 22:16:25 2009 +0100
     6.2 +++ b/src/HOL/Library/Random.thy	Thu Mar 12 23:01:25 2009 +0100
     6.3 @@ -21,6 +21,7 @@
     6.4  fun log :: "index \<Rightarrow> index \<Rightarrow> index" where
     6.5    "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
     6.6  
     6.7 +
     6.8  subsection {* Random seeds *}
     6.9  
    6.10  types seed = "index \<times> index"
    6.11 @@ -57,29 +58,17 @@
    6.12  
    6.13  subsection {* Base selectors *}
    6.14  
    6.15 -function range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
    6.16 -  "range_aux k l s = (if k = 0 then (l, s) else
    6.17 -    let (v, s') = next s
    6.18 -  in range_aux (k - 1) (v + l * 2147483561) s')"
    6.19 -by pat_completeness auto
    6.20 -termination
    6.21 -  by (relation "measure (Code_Index.nat_of o fst)")
    6.22 -    (auto simp add: index)
    6.23 +fun %quote iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    6.24 +  "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
    6.25  
    6.26 -definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
    6.27 -  "range k = range_aux (log 2147483561 k) 1
    6.28 +definition %quote range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
    6.29 +  "range k = iterate (log 2147483561 k)
    6.30 +      (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
    6.31      o\<rightarrow> (\<lambda>v. Pair (v mod k))"
    6.32  
    6.33  lemma range:
    6.34 -  assumes "k > 0"
    6.35 -  shows "fst (range k s) < k"
    6.36 -proof -
    6.37 -  obtain v w where range_aux:
    6.38 -    "range_aux (log 2147483561 k) 1 s = (v, w)"
    6.39 -    by (cases "range_aux (log 2147483561 k) 1 s")
    6.40 -  with assms show ?thesis
    6.41 -    by (simp add: scomp_apply range_def del: range_aux.simps log.simps)
    6.42 -qed
    6.43 +  "k > 0 \<Longrightarrow> fst (range k s) < k"
    6.44 +  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
    6.45  
    6.46  definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    6.47    "select xs = range (Code_Index.of_nat (length xs))
     7.1 --- a/src/HOL/NSA/NSA.thy	Thu Mar 12 22:16:25 2009 +0100
     7.2 +++ b/src/HOL/NSA/NSA.thy	Thu Mar 12 23:01:25 2009 +0100
     7.3 @@ -684,7 +684,7 @@
     7.4  
     7.5  in
     7.6  val approx_reorient_simproc =
     7.7 -  Int_Numeral_Base_Simprocs.prep_simproc
     7.8 +  Arith_Data.prep_simproc
     7.9      ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
    7.10  end;
    7.11  
     8.1 --- a/src/HOL/Nat.thy	Thu Mar 12 22:16:25 2009 +0100
     8.2 +++ b/src/HOL/Nat.thy	Thu Mar 12 23:01:25 2009 +0100
     8.3 @@ -2,7 +2,7 @@
     8.4      Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
     8.5  
     8.6  Type "nat" is a linear order, and a datatype; arithmetic operators + -
     8.7 -and * (for div, mod and dvd, see theory Divides).
     8.8 +and * (for div and mod, see theory Divides).
     8.9  *)
    8.10  
    8.11  header {* Natural numbers *}
    8.12 @@ -12,7 +12,8 @@
    8.13  uses
    8.14    "~~/src/Tools/rat.ML"
    8.15    "~~/src/Provers/Arith/cancel_sums.ML"
    8.16 -  ("Tools/arith_data.ML")
    8.17 +  "Tools/arith_data.ML"
    8.18 +  ("Tools/nat_arith.ML")
    8.19    "~~/src/Provers/Arith/fast_lin_arith.ML"
    8.20    ("Tools/lin_arith.ML")
    8.21  begin
    8.22 @@ -1344,8 +1345,8 @@
    8.23    shows "u = s"
    8.24    using 2 1 by (rule trans)
    8.25  
    8.26 -use "Tools/arith_data.ML"
    8.27 -declaration {* K ArithData.setup *}
    8.28 +use "Tools/nat_arith.ML"
    8.29 +declaration {* K Nat_Arith.setup *}
    8.30  
    8.31  ML{*
    8.32  structure ArithFacts =
     9.1 --- a/src/HOL/NatBin.thy	Thu Mar 12 22:16:25 2009 +0100
     9.2 +++ b/src/HOL/NatBin.thy	Thu Mar 12 23:01:25 2009 +0100
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOL/NatBin.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7      Copyright   1999  University of Cambridge
     9.8  *)
    10.1 --- a/src/HOL/Tools/arith_data.ML	Thu Mar 12 22:16:25 2009 +0100
    10.2 +++ b/src/HOL/Tools/arith_data.ML	Thu Mar 12 23:01:25 2009 +0100
    10.3 @@ -1,155 +1,39 @@
    10.4  (*  Title:      HOL/arith_data.ML
    10.5      Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
    10.6  
    10.7 -Basic arithmetic proof tools.
    10.8 +Common arithmetic proof auxiliary.
    10.9  *)
   10.10  
   10.11  signature ARITH_DATA =
   10.12  sig
   10.13 -  val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
   10.14 +  val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
   10.15 +  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
   10.16 +  val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
   10.17    val simp_all_tac: thm list -> simpset -> tactic
   10.18 -
   10.19 -  val mk_sum: term list -> term
   10.20 -  val mk_norm_sum: term list -> term
   10.21 -  val dest_sum: term -> term list
   10.22 -
   10.23 -  val nat_cancel_sums_add: simproc list
   10.24 -  val nat_cancel_sums: simproc list
   10.25 -  val setup: Context.generic -> Context.generic
   10.26 +  val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
   10.27 +    -> simproc
   10.28  end;
   10.29  
   10.30 -structure ArithData: ARITH_DATA =
   10.31 +structure Arith_Data: ARITH_DATA =
   10.32  struct
   10.33  
   10.34 -(** generic proof tools **)
   10.35 +fun prove_conv_nohyps tacs ctxt (t, u) =
   10.36 +  if t aconv u then NONE
   10.37 +  else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
   10.38 +  in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
   10.39  
   10.40 -(* prove conversions *)
   10.41 +fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
   10.42  
   10.43 -fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
   10.44 +fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
   10.45    mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
   10.46        (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
   10.47      (K (EVERY [expand_tac, norm_tac ss]))));
   10.48  
   10.49 -(* rewriting *)
   10.50 -
   10.51  fun simp_all_tac rules =
   10.52    let val ss0 = HOL_ss addsimps rules
   10.53    in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
   10.54  
   10.55 -
   10.56 -(** abstract syntax of structure nat: 0, Suc, + **)
   10.57 -
   10.58 -local
   10.59 -
   10.60 -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
   10.61 -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
   10.62 -
   10.63 -in
   10.64 -
   10.65 -fun mk_sum [] = HOLogic.zero
   10.66 -  | mk_sum [t] = t
   10.67 -  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   10.68 -
   10.69 -(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
   10.70 -fun mk_norm_sum ts =
   10.71 -  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
   10.72 -    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
   10.73 -  end;
   10.74 -
   10.75 -
   10.76 -fun dest_sum tm =
   10.77 -  if HOLogic.is_zero tm then []
   10.78 -  else
   10.79 -    (case try HOLogic.dest_Suc tm of
   10.80 -      SOME t => HOLogic.Suc_zero :: dest_sum t
   10.81 -    | NONE =>
   10.82 -        (case try dest_plus tm of
   10.83 -          SOME (t, u) => dest_sum t @ dest_sum u
   10.84 -        | NONE => [tm]));
   10.85 +fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
   10.86 +  Simplifier.simproc (the_context ()) name pats proc;
   10.87  
   10.88  end;
   10.89 -
   10.90 -
   10.91 -(** cancel common summands **)
   10.92 -
   10.93 -structure Sum =
   10.94 -struct
   10.95 -  val mk_sum = mk_norm_sum;
   10.96 -  val dest_sum = dest_sum;
   10.97 -  val prove_conv = prove_conv;
   10.98 -  val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
   10.99 -    @{thm "add_0"}, @{thm "add_0_right"}];
  10.100 -  val norm_tac2 = simp_all_tac @{thms add_ac};
  10.101 -  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
  10.102 -end;
  10.103 -
  10.104 -fun gen_uncancel_tac rule ct =
  10.105 -  rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
  10.106 -
  10.107 -
  10.108 -(* nat eq *)
  10.109 -
  10.110 -structure EqCancelSums = CancelSumsFun
  10.111 -(struct
  10.112 -  open Sum;
  10.113 -  val mk_bal = HOLogic.mk_eq;
  10.114 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
  10.115 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
  10.116 -end);
  10.117 -
  10.118 -
  10.119 -(* nat less *)
  10.120 -
  10.121 -structure LessCancelSums = CancelSumsFun
  10.122 -(struct
  10.123 -  open Sum;
  10.124 -  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
  10.125 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
  10.126 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
  10.127 -end);
  10.128 -
  10.129 -
  10.130 -(* nat le *)
  10.131 -
  10.132 -structure LeCancelSums = CancelSumsFun
  10.133 -(struct
  10.134 -  open Sum;
  10.135 -  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
  10.136 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
  10.137 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
  10.138 -end);
  10.139 -
  10.140 -
  10.141 -(* nat diff *)
  10.142 -
  10.143 -structure DiffCancelSums = CancelSumsFun
  10.144 -(struct
  10.145 -  open Sum;
  10.146 -  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
  10.147 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
  10.148 -  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
  10.149 -end);
  10.150 -
  10.151 -
  10.152 -(* prepare nat_cancel simprocs *)
  10.153 -
  10.154 -val nat_cancel_sums_add =
  10.155 -  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
  10.156 -     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
  10.157 -     (K EqCancelSums.proc),
  10.158 -   Simplifier.simproc (the_context ()) "natless_cancel_sums"
  10.159 -     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
  10.160 -     (K LessCancelSums.proc),
  10.161 -   Simplifier.simproc (the_context ()) "natle_cancel_sums"
  10.162 -     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
  10.163 -     (K LeCancelSums.proc)];
  10.164 -
  10.165 -val nat_cancel_sums = nat_cancel_sums_add @
  10.166 -  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
  10.167 -    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
  10.168 -    (K DiffCancelSums.proc)];
  10.169 -
  10.170 -val setup =
  10.171 -  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
  10.172 -
  10.173 -end;
    11.1 --- a/src/HOL/Tools/int_arith.ML	Thu Mar 12 22:16:25 2009 +0100
    11.2 +++ b/src/HOL/Tools/int_arith.ML	Thu Mar 12 23:01:25 2009 +0100
    11.3 @@ -1,59 +1,32 @@
    11.4 -(*  Title:      HOL/Tools/int_arith1.ML
    11.5 -    Authors:    Larry Paulson and Tobias Nipkow
    11.6 -
    11.7 -Simprocs and decision procedure for linear arithmetic.
    11.8 -*)
    11.9 -
   11.10 -structure Int_Numeral_Base_Simprocs =
   11.11 -  struct
   11.12 -  fun prove_conv tacs ctxt (_: thm list) (t, u) =
   11.13 -    if t aconv u then NONE
   11.14 -    else
   11.15 -      let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
   11.16 -      in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end
   11.17 -
   11.18 -  fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
   11.19 -
   11.20 -  fun prep_simproc (name, pats, proc) =
   11.21 -    Simplifier.simproc (the_context()) name pats proc;
   11.22 -
   11.23 -  fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
   11.24 -    | is_numeral _ = false
   11.25 -
   11.26 -  fun simplify_meta_eq f_number_of_eq f_eq =
   11.27 -      mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
   11.28 +(* Authors: Larry Paulson and Tobias Nipkow
   11.29  
   11.30 -  (*reorientation simprules using ==, for the following simproc*)
   11.31 -  val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
   11.32 -  val meta_one_reorient = @{thm one_reorient} RS eq_reflection
   11.33 -  val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
   11.34 -
   11.35 -  (*reorientation simplification procedure: reorients (polymorphic) 
   11.36 -    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
   11.37 -  fun reorient_proc sg _ (_ $ t $ u) =
   11.38 -    case u of
   11.39 -        Const(@{const_name HOL.zero}, _) => NONE
   11.40 -      | Const(@{const_name HOL.one}, _) => NONE
   11.41 -      | Const(@{const_name Int.number_of}, _) $ _ => NONE
   11.42 -      | _ => SOME (case t of
   11.43 -          Const(@{const_name HOL.zero}, _) => meta_zero_reorient
   11.44 -        | Const(@{const_name HOL.one}, _) => meta_one_reorient
   11.45 -        | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
   11.46 -
   11.47 -  val reorient_simproc = 
   11.48 -      prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
   11.49 -
   11.50 -  end;
   11.51 -
   11.52 -
   11.53 -Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
   11.54 -
   11.55 +Simprocs and decision procedure for numerals and linear arithmetic.
   11.56 +*)
   11.57  
   11.58  structure Int_Numeral_Simprocs =
   11.59  struct
   11.60  
   11.61 -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
   11.62 -  isn't complicated by the abstract 0 and 1.*)
   11.63 +(*reorientation simprules using ==, for the following simproc*)
   11.64 +val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
   11.65 +val meta_one_reorient = @{thm one_reorient} RS eq_reflection
   11.66 +val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
   11.67 +
   11.68 +(*reorientation simplification procedure: reorients (polymorphic) 
   11.69 +  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
   11.70 +fun reorient_proc sg _ (_ $ t $ u) =
   11.71 +  case u of
   11.72 +      Const(@{const_name HOL.zero}, _) => NONE
   11.73 +    | Const(@{const_name HOL.one}, _) => NONE
   11.74 +    | Const(@{const_name Int.number_of}, _) $ _ => NONE
   11.75 +    | _ => SOME (case t of
   11.76 +        Const(@{const_name HOL.zero}, _) => meta_zero_reorient
   11.77 +      | Const(@{const_name HOL.one}, _) => meta_one_reorient
   11.78 +      | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
   11.79 +
   11.80 +val reorient_simproc = 
   11.81 +  Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
   11.82 +
   11.83 +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
   11.84  val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
   11.85  
   11.86  (** New term ordering so that AC-rewriting brings numerals to the front **)
   11.87 @@ -88,7 +61,7 @@
   11.88  
   11.89  fun numtermless tu = (numterm_ord tu = LESS);
   11.90  
   11.91 -(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
   11.92 +(*Defined in this file, but perhaps needed only for Int_Numeral_Simprocs of type nat.*)
   11.93  val num_ss = HOL_ss settermless numtermless;
   11.94  
   11.95  
   11.96 @@ -213,7 +186,7 @@
   11.97  val divide_1s = [@{thm divide_numeral_1}];
   11.98  
   11.99  (*To perform binary arithmetic.  The "left" rewriting handles patterns
  11.100 -  created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
  11.101 +  created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *)
  11.102  val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
  11.103                   @{thm add_number_of_left}, @{thm mult_number_of_left}] @
  11.104                  @{thms arith_simps} @ @{thms rel_simps};
  11.105 @@ -279,7 +252,7 @@
  11.106  
  11.107  structure EqCancelNumerals = CancelNumeralsFun
  11.108   (open CancelNumeralsCommon
  11.109 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  11.110 +  val prove_conv = Arith_Data.prove_conv
  11.111    val mk_bal   = HOLogic.mk_eq
  11.112    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
  11.113    val bal_add1 = @{thm eq_add_iff1} RS trans
  11.114 @@ -288,7 +261,7 @@
  11.115  
  11.116  structure LessCancelNumerals = CancelNumeralsFun
  11.117   (open CancelNumeralsCommon
  11.118 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  11.119 +  val prove_conv = Arith_Data.prove_conv
  11.120    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
  11.121    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
  11.122    val bal_add1 = @{thm less_add_iff1} RS trans
  11.123 @@ -297,7 +270,7 @@
  11.124  
  11.125  structure LeCancelNumerals = CancelNumeralsFun
  11.126   (open CancelNumeralsCommon
  11.127 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  11.128 +  val prove_conv = Arith_Data.prove_conv
  11.129    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
  11.130    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
  11.131    val bal_add1 = @{thm le_add_iff1} RS trans
  11.132 @@ -305,7 +278,7 @@
  11.133  );
  11.134  
  11.135  val cancel_numerals =
  11.136 -  map Int_Numeral_Base_Simprocs.prep_simproc
  11.137 +  map Arith_Data.prep_simproc
  11.138     [("inteq_cancel_numerals",
  11.139       ["(l::'a::number_ring) + m = n",
  11.140        "(l::'a::number_ring) = m + n",
  11.141 @@ -342,7 +315,7 @@
  11.142    val mk_coeff          = mk_coeff
  11.143    val dest_coeff        = dest_coeff 1
  11.144    val left_distrib      = @{thm combine_common_factor} RS trans
  11.145 -  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
  11.146 +  val prove_conv        = Arith_Data.prove_conv_nohyps
  11.147    val trans_tac         = fn _ => trans_tac
  11.148  
  11.149    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
  11.150 @@ -372,7 +345,7 @@
  11.151    val mk_coeff          = mk_fcoeff
  11.152    val dest_coeff        = dest_fcoeff 1
  11.153    val left_distrib      = @{thm combine_common_factor} RS trans
  11.154 -  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
  11.155 +  val prove_conv        = Arith_Data.prove_conv_nohyps
  11.156    val trans_tac         = fn _ => trans_tac
  11.157  
  11.158    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
  11.159 @@ -392,23 +365,42 @@
  11.160  structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
  11.161  
  11.162  val combine_numerals =
  11.163 -  Int_Numeral_Base_Simprocs.prep_simproc
  11.164 +  Arith_Data.prep_simproc
  11.165      ("int_combine_numerals", 
  11.166       ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
  11.167       K CombineNumerals.proc);
  11.168  
  11.169  val field_combine_numerals =
  11.170 -  Int_Numeral_Base_Simprocs.prep_simproc
  11.171 +  Arith_Data.prep_simproc
  11.172      ("field_combine_numerals", 
  11.173       ["(i::'a::{number_ring,field,division_by_zero}) + j",
  11.174        "(i::'a::{number_ring,field,division_by_zero}) - j"], 
  11.175       K FieldCombineNumerals.proc);
  11.176  
  11.177 +(** Constant folding for multiplication in semirings **)
  11.178 +
  11.179 +(*We do not need folding for addition: combine_numerals does the same thing*)
  11.180 +
  11.181 +structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
  11.182 +struct
  11.183 +  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
  11.184 +  val eq_reflection = eq_reflection
  11.185  end;
  11.186  
  11.187 +structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
  11.188 +
  11.189 +val assoc_fold_simproc =
  11.190 +  Arith_Data.prep_simproc
  11.191 +   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
  11.192 +    K Semiring_Times_Assoc.proc);
  11.193 +
  11.194 +end;
  11.195 +
  11.196 +Addsimprocs [Int_Numeral_Simprocs.reorient_simproc];
  11.197  Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
  11.198  Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
  11.199  Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
  11.200 +Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc];
  11.201  
  11.202  (*examples:
  11.203  print_depth 22;
  11.204 @@ -447,29 +439,6 @@
  11.205  test "(i + j + -12 + (k::int)) - -15 = y";
  11.206  *)
  11.207  
  11.208 -
  11.209 -(** Constant folding for multiplication in semirings **)
  11.210 -
  11.211 -(*We do not need folding for addition: combine_numerals does the same thing*)
  11.212 -
  11.213 -structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
  11.214 -struct
  11.215 -  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
  11.216 -  val eq_reflection = eq_reflection
  11.217 -end;
  11.218 -
  11.219 -structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
  11.220 -
  11.221 -val assoc_fold_simproc =
  11.222 -  Int_Numeral_Base_Simprocs.prep_simproc
  11.223 -   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
  11.224 -    K Semiring_Times_Assoc.proc);
  11.225 -
  11.226 -Addsimprocs [assoc_fold_simproc];
  11.227 -
  11.228 -
  11.229 -
  11.230 -
  11.231  (*** decision procedure for linear arithmetic ***)
  11.232  
  11.233  (*---------------------------------------------------------------------------*)
  11.234 @@ -480,8 +449,10 @@
  11.235  Instantiation of the generic linear arithmetic package for int.
  11.236  *)
  11.237  
  11.238 +structure Int_Arith =
  11.239 +struct
  11.240 +
  11.241  (* Update parameters of arithmetic prover *)
  11.242 -local
  11.243  
  11.244  (* reduce contradictory =/</<= to False *)
  11.245  
  11.246 @@ -489,25 +460,31 @@
  11.247     and m and n are ground terms over rings (roughly speaking).
  11.248     That is, m and n consist only of 1s combined with "+", "-" and "*".
  11.249  *)
  11.250 -local
  11.251 +
  11.252  val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
  11.253 +
  11.254  val lhss0 = [@{cpat "0::?'a::ring"}];
  11.255 +
  11.256  fun proc0 phi ss ct =
  11.257    let val T = ctyp_of_term ct
  11.258    in if typ_of T = @{typ int} then NONE else
  11.259       SOME (instantiate' [SOME T] [] zeroth)
  11.260    end;
  11.261 +
  11.262  val zero_to_of_int_zero_simproc =
  11.263    make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
  11.264    proc = proc0, identifier = []};
  11.265  
  11.266  val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
  11.267 +
  11.268  val lhss1 = [@{cpat "1::?'a::ring_1"}];
  11.269 +
  11.270  fun proc1 phi ss ct =
  11.271    let val T = ctyp_of_term ct
  11.272    in if typ_of T = @{typ int} then NONE else
  11.273       SOME (instantiate' [SOME T] [] oneth)
  11.274    end;
  11.275 +
  11.276  val one_to_of_int_one_simproc =
  11.277    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
  11.278    proc = proc1, identifier = []};
  11.279 @@ -533,15 +510,15 @@
  11.280       addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
  11.281  
  11.282  fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
  11.283 +
  11.284  val lhss' =
  11.285    [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
  11.286     @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
  11.287     @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
  11.288 -in
  11.289 +
  11.290  val zero_one_idom_simproc =
  11.291    make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
  11.292    proc = sproc, identifier = []}
  11.293 -end;
  11.294  
  11.295  val add_rules =
  11.296      simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
  11.297 @@ -556,13 +533,11 @@
  11.298  
  11.299  val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
  11.300  
  11.301 -val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc
  11.302 +val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
  11.303    :: Int_Numeral_Simprocs.combine_numerals
  11.304    :: Int_Numeral_Simprocs.cancel_numerals;
  11.305  
  11.306 -in
  11.307 -
  11.308 -val int_arith_setup =
  11.309 +val setup =
  11.310    LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
  11.311     {add_mono_thms = add_mono_thms,
  11.312      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
  11.313 @@ -570,13 +545,11 @@
  11.314      lessD = lessD @ [@{thm zless_imp_add1_zle}],
  11.315      neqE = neqE,
  11.316      simpset = simpset addsimps add_rules
  11.317 -                      addsimprocs Int_Numeral_Base_Simprocs
  11.318 +                      addsimprocs int_numeral_base_simprocs
  11.319                        addcongs [if_weak_cong]}) #>
  11.320    arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
  11.321    arith_discrete @{type_name Int.int}
  11.322  
  11.323 -end;
  11.324 -
  11.325  val fast_int_arith_simproc =
  11.326    Simplifier.simproc (the_context ())
  11.327    "fast_int_arith" 
  11.328 @@ -584,4 +557,6 @@
  11.329        "(m::'a::{ordered_idom,number_ring}) <= n",
  11.330        "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
  11.331  
  11.332 -Addsimprocs [fast_int_arith_simproc];
  11.333 +end;
  11.334 +
  11.335 +Addsimprocs [Int_Arith.fast_int_arith_simproc];
    12.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Thu Mar 12 22:16:25 2009 +0100
    12.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Thu Mar 12 23:01:25 2009 +0100
    12.3 @@ -49,7 +49,7 @@
    12.4  (*Version for integer division*)
    12.5  structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
    12.6   (open CancelNumeralFactorCommon
    12.7 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    12.8 +  val prove_conv = Arith_Data.prove_conv
    12.9    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   12.10    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
   12.11    val cancel = @{thm zdiv_zmult_zmult1} RS trans
   12.12 @@ -59,7 +59,7 @@
   12.13  (*Version for fields*)
   12.14  structure DivideCancelNumeralFactor = CancelNumeralFactorFun
   12.15   (open CancelNumeralFactorCommon
   12.16 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.17 +  val prove_conv = Arith_Data.prove_conv
   12.18    val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   12.19    val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   12.20    val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   12.21 @@ -68,7 +68,7 @@
   12.22  
   12.23  structure EqCancelNumeralFactor = CancelNumeralFactorFun
   12.24   (open CancelNumeralFactorCommon
   12.25 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.26 +  val prove_conv = Arith_Data.prove_conv
   12.27    val mk_bal   = HOLogic.mk_eq
   12.28    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   12.29    val cancel = @{thm mult_cancel_left} RS trans
   12.30 @@ -77,7 +77,7 @@
   12.31  
   12.32  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   12.33   (open CancelNumeralFactorCommon
   12.34 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.35 +  val prove_conv = Arith_Data.prove_conv
   12.36    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   12.37    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   12.38    val cancel = @{thm mult_less_cancel_left} RS trans
   12.39 @@ -86,7 +86,7 @@
   12.40  
   12.41  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   12.42   (open CancelNumeralFactorCommon
   12.43 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.44 +  val prove_conv = Arith_Data.prove_conv
   12.45    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   12.46    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   12.47    val cancel = @{thm mult_le_cancel_left} RS trans
   12.48 @@ -94,7 +94,7 @@
   12.49  )
   12.50  
   12.51  val cancel_numeral_factors =
   12.52 -  map Int_Numeral_Base_Simprocs.prep_simproc
   12.53 +  map Arith_Data.prep_simproc
   12.54     [("ring_eq_cancel_numeral_factor",
   12.55       ["(l::'a::{idom,number_ring}) * m = n",
   12.56        "(l::'a::{idom,number_ring}) = m * n"],
   12.57 @@ -118,7 +118,7 @@
   12.58  
   12.59  (* referenced by rat_arith.ML *)
   12.60  val field_cancel_numeral_factors =
   12.61 -  map Int_Numeral_Base_Simprocs.prep_simproc
   12.62 +  map Arith_Data.prep_simproc
   12.63     [("field_eq_cancel_numeral_factor",
   12.64       ["(l::'a::{field,number_ring}) * m = n",
   12.65        "(l::'a::{field,number_ring}) = m * n"],
   12.66 @@ -236,7 +236,7 @@
   12.67  (*mult_cancel_left requires a ring with no zero divisors.*)
   12.68  structure EqCancelFactor = ExtractCommonTermFun
   12.69   (open CancelFactorCommon
   12.70 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.71 +  val prove_conv = Arith_Data.prove_conv
   12.72    val mk_bal   = HOLogic.mk_eq
   12.73    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   12.74    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_cancel_left}
   12.75 @@ -245,7 +245,7 @@
   12.76  (*zdiv_zmult_zmult1_if is for integer division (div).*)
   12.77  structure IntDivCancelFactor = ExtractCommonTermFun
   12.78   (open CancelFactorCommon
   12.79 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.80 +  val prove_conv = Arith_Data.prove_conv
   12.81    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   12.82    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
   12.83    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
   12.84 @@ -253,7 +253,7 @@
   12.85  
   12.86  structure IntModCancelFactor = ExtractCommonTermFun
   12.87   (open CancelFactorCommon
   12.88 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.89 +  val prove_conv = Arith_Data.prove_conv
   12.90    val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   12.91    val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
   12.92    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
   12.93 @@ -261,7 +261,7 @@
   12.94  
   12.95  structure IntDvdCancelFactor = ExtractCommonTermFun
   12.96   (open CancelFactorCommon
   12.97 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   12.98 +  val prove_conv = Arith_Data.prove_conv
   12.99    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
  12.100    val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
  12.101    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
  12.102 @@ -270,14 +270,14 @@
  12.103  (*Version for all fields, including unordered ones (type complex).*)
  12.104  structure DivideCancelFactor = ExtractCommonTermFun
  12.105   (open CancelFactorCommon
  12.106 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  12.107 +  val prove_conv = Arith_Data.prove_conv
  12.108    val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
  12.109    val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
  12.110    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
  12.111  );
  12.112  
  12.113  val cancel_factors =
  12.114 -  map Int_Numeral_Base_Simprocs.prep_simproc
  12.115 +  map Arith_Data.prep_simproc
  12.116     [("ring_eq_cancel_factor",
  12.117       ["(l::'a::{idom}) * m = n",
  12.118        "(l::'a::{idom}) = m * n"],
    13.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Mar 12 22:16:25 2009 +0100
    13.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Mar 12 23:01:25 2009 +0100
    13.3 @@ -811,7 +811,7 @@
    13.4          @{thm "not_one_less_zero"}]
    13.5        addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
    13.6         (*abel_cancel helps it work in abstract algebraic domains*)
    13.7 -      addsimprocs ArithData.nat_cancel_sums_add}) #>
    13.8 +      addsimprocs Nat_Arith.nat_cancel_sums_add}) #>
    13.9    arith_discrete "nat";
   13.10  
   13.11  fun add_arith_facts ss =
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Tools/nat_arith.ML	Thu Mar 12 23:01:25 2009 +0100
    14.3 @@ -0,0 +1,112 @@
    14.4 +(* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
    14.5 +
    14.6 +Basic arithmetic for natural numbers.
    14.7 +*)
    14.8 +
    14.9 +signature NAT_ARITH =
   14.10 +sig
   14.11 +  val mk_sum: term list -> term
   14.12 +  val mk_norm_sum: term list -> term
   14.13 +  val dest_sum: term -> term list
   14.14 +
   14.15 +  val nat_cancel_sums_add: simproc list
   14.16 +  val nat_cancel_sums: simproc list
   14.17 +  val setup: Context.generic -> Context.generic
   14.18 +end;
   14.19 +
   14.20 +structure Nat_Arith: NAT_ARITH =
   14.21 +struct
   14.22 +
   14.23 +(** abstract syntax of structure nat: 0, Suc, + **)
   14.24 +
   14.25 +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
   14.26 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
   14.27 +
   14.28 +fun mk_sum [] = HOLogic.zero
   14.29 +  | mk_sum [t] = t
   14.30 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   14.31 +
   14.32 +(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
   14.33 +fun mk_norm_sum ts =
   14.34 +  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
   14.35 +    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
   14.36 +  end;
   14.37 +
   14.38 +fun dest_sum tm =
   14.39 +  if HOLogic.is_zero tm then []
   14.40 +  else
   14.41 +    (case try HOLogic.dest_Suc tm of
   14.42 +      SOME t => HOLogic.Suc_zero :: dest_sum t
   14.43 +    | NONE =>
   14.44 +        (case try dest_plus tm of
   14.45 +          SOME (t, u) => dest_sum t @ dest_sum u
   14.46 +        | NONE => [tm]));
   14.47 +
   14.48 +
   14.49 +(** cancel common summands **)
   14.50 +
   14.51 +structure CommonCancelSums =
   14.52 +struct
   14.53 +  val mk_sum = mk_norm_sum;
   14.54 +  val dest_sum = dest_sum;
   14.55 +  val prove_conv = Arith_Data.prove_conv2;
   14.56 +  val norm_tac1 = Arith_Data.simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
   14.57 +    @{thm "add_0"}, @{thm "add_0_right"}];
   14.58 +  val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
   14.59 +  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
   14.60 +  fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
   14.61 +    in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
   14.62 +end;
   14.63 +
   14.64 +structure EqCancelSums = CancelSumsFun
   14.65 +(struct
   14.66 +  open CommonCancelSums;
   14.67 +  val mk_bal = HOLogic.mk_eq;
   14.68 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   14.69 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
   14.70 +end);
   14.71 +
   14.72 +structure LessCancelSums = CancelSumsFun
   14.73 +(struct
   14.74 +  open CommonCancelSums;
   14.75 +  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
   14.76 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
   14.77 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
   14.78 +end);
   14.79 +
   14.80 +structure LeCancelSums = CancelSumsFun
   14.81 +(struct
   14.82 +  open CommonCancelSums;
   14.83 +  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
   14.84 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
   14.85 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
   14.86 +end);
   14.87 +
   14.88 +structure DiffCancelSums = CancelSumsFun
   14.89 +(struct
   14.90 +  open CommonCancelSums;
   14.91 +  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
   14.92 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
   14.93 +  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
   14.94 +end);
   14.95 +
   14.96 +val nat_cancel_sums_add =
   14.97 +  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
   14.98 +     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
   14.99 +     (K EqCancelSums.proc),
  14.100 +   Simplifier.simproc (the_context ()) "natless_cancel_sums"
  14.101 +     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
  14.102 +     (K LessCancelSums.proc),
  14.103 +   Simplifier.simproc (the_context ()) "natle_cancel_sums"
  14.104 +     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
  14.105 +     (K LeCancelSums.proc)];
  14.106 +
  14.107 +val nat_cancel_sums = nat_cancel_sums_add @
  14.108 +  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
  14.109 +    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
  14.110 +    (K DiffCancelSums.proc)];
  14.111 +
  14.112 +val setup =
  14.113 +  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
  14.114 +
  14.115 +end;
    15.1 --- a/src/HOL/Tools/nat_simprocs.ML	Thu Mar 12 22:16:25 2009 +0100
    15.2 +++ b/src/HOL/Tools/nat_simprocs.ML	Thu Mar 12 23:01:25 2009 +0100
    15.3 @@ -8,8 +8,7 @@
    15.4  struct
    15.5  
    15.6  (*Maps n to #n for n = 0, 1, 2*)
    15.7 -val numeral_syms =
    15.8 -       [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
    15.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];
   15.10  val numeral_sym_ss = HOL_ss addsimps numeral_syms;
   15.11  
   15.12  fun rename_numerals th =
   15.13 @@ -53,9 +52,6 @@
   15.14        @{thm Let_number_of}, @{thm nat_number_of}] @
   15.15       @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
   15.16  
   15.17 -fun prep_simproc (name, pats, proc) =
   15.18 -  Simplifier.simproc (the_context ()) name pats proc;
   15.19 -
   15.20  
   15.21  (*** CancelNumerals simprocs ***)
   15.22  
   15.23 @@ -169,7 +165,7 @@
   15.24  
   15.25  structure EqCancelNumerals = CancelNumeralsFun
   15.26   (open CancelNumeralsCommon
   15.27 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   15.28 +  val prove_conv = Arith_Data.prove_conv
   15.29    val mk_bal   = HOLogic.mk_eq
   15.30    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   15.31    val bal_add1 = @{thm nat_eq_add_iff1} RS trans
   15.32 @@ -178,7 +174,7 @@
   15.33  
   15.34  structure LessCancelNumerals = CancelNumeralsFun
   15.35   (open CancelNumeralsCommon
   15.36 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   15.37 +  val prove_conv = Arith_Data.prove_conv
   15.38    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   15.39    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   15.40    val bal_add1 = @{thm nat_less_add_iff1} RS trans
   15.41 @@ -187,7 +183,7 @@
   15.42  
   15.43  structure LeCancelNumerals = CancelNumeralsFun
   15.44   (open CancelNumeralsCommon
   15.45 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   15.46 +  val prove_conv = Arith_Data.prove_conv
   15.47    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   15.48    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   15.49    val bal_add1 = @{thm nat_le_add_iff1} RS trans
   15.50 @@ -196,7 +192,7 @@
   15.51  
   15.52  structure DiffCancelNumerals = CancelNumeralsFun
   15.53   (open CancelNumeralsCommon
   15.54 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   15.55 +  val prove_conv = Arith_Data.prove_conv
   15.56    val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
   15.57    val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
   15.58    val bal_add1 = @{thm nat_diff_add_eq1} RS trans
   15.59 @@ -205,7 +201,7 @@
   15.60  
   15.61  
   15.62  val cancel_numerals =
   15.63 -  map prep_simproc
   15.64 +  map Arith_Data.prep_simproc
   15.65     [("nateq_cancel_numerals",
   15.66       ["(l::nat) + m = n", "(l::nat) = m + n",
   15.67        "(l::nat) * m = n", "(l::nat) = m * n",
   15.68 @@ -240,7 +236,7 @@
   15.69    val mk_coeff          = mk_coeff
   15.70    val dest_coeff        = dest_coeff
   15.71    val left_distrib      = @{thm left_add_mult_distrib} RS trans
   15.72 -  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   15.73 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   15.74    val trans_tac         = fn _ => trans_tac
   15.75  
   15.76    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
   15.77 @@ -257,7 +253,7 @@
   15.78  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   15.79  
   15.80  val combine_numerals =
   15.81 -  prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
   15.82 +  Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
   15.83  
   15.84  
   15.85  (*** Applying CancelNumeralFactorFun ***)
   15.86 @@ -282,7 +278,7 @@
   15.87  
   15.88  structure DivCancelNumeralFactor = CancelNumeralFactorFun
   15.89   (open CancelNumeralFactorCommon
   15.90 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   15.91 +  val prove_conv = Arith_Data.prove_conv
   15.92    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   15.93    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   15.94    val cancel = @{thm nat_mult_div_cancel1} RS trans
   15.95 @@ -291,7 +287,7 @@
   15.96  
   15.97  structure DvdCancelNumeralFactor = CancelNumeralFactorFun
   15.98   (open CancelNumeralFactorCommon
   15.99 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  15.100 +  val prove_conv = Arith_Data.prove_conv
  15.101    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
  15.102    val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
  15.103    val cancel = @{thm nat_mult_dvd_cancel1} RS trans
  15.104 @@ -300,7 +296,7 @@
  15.105  
  15.106  structure EqCancelNumeralFactor = CancelNumeralFactorFun
  15.107   (open CancelNumeralFactorCommon
  15.108 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  15.109 +  val prove_conv = Arith_Data.prove_conv
  15.110    val mk_bal   = HOLogic.mk_eq
  15.111    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
  15.112    val cancel = @{thm nat_mult_eq_cancel1} RS trans
  15.113 @@ -309,7 +305,7 @@
  15.114  
  15.115  structure LessCancelNumeralFactor = CancelNumeralFactorFun
  15.116   (open CancelNumeralFactorCommon
  15.117 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  15.118 +  val prove_conv = Arith_Data.prove_conv
  15.119    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
  15.120    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
  15.121    val cancel = @{thm nat_mult_less_cancel1} RS trans
  15.122 @@ -318,7 +314,7 @@
  15.123  
  15.124  structure LeCancelNumeralFactor = CancelNumeralFactorFun
  15.125   (open CancelNumeralFactorCommon
  15.126 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  15.127 +  val prove_conv = Arith_Data.prove_conv
  15.128    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
  15.129    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
  15.130    val cancel = @{thm nat_mult_le_cancel1} RS trans
  15.131 @@ -326,7 +322,7 @@
  15.132  )
  15.133  
  15.134  val cancel_numeral_factors =
  15.135 -  map prep_simproc
  15.136 +  map Arith_Data.prep_simproc
  15.137     [("nateq_cancel_numeral_factors",
  15.138       ["(l::nat) * m = n", "(l::nat) = m * n"],
  15.139       K EqCancelNumeralFactor.proc),
  15.140 @@ -379,7 +375,7 @@
  15.141  
  15.142  structure EqCancelFactor = ExtractCommonTermFun
  15.143   (open CancelFactorCommon
  15.144 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  15.145 +  val prove_conv = Arith_Data.prove_conv
  15.146    val mk_bal   = HOLogic.mk_eq
  15.147    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
  15.148    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
  15.149 @@ -387,7 +383,7 @@
  15.150  
  15.151  structure LessCancelFactor = ExtractCommonTermFun
  15.152   (open CancelFactorCommon
  15.153 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  15.154 +  val prove_conv = Arith_Data.prove_conv
  15.155    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
  15.156    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
  15.157    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
  15.158 @@ -395,7 +391,7 @@
  15.159  
  15.160  structure LeCancelFactor = ExtractCommonTermFun
  15.161   (open CancelFactorCommon
  15.162 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  15.163 +  val prove_conv = Arith_Data.prove_conv
  15.164    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
  15.165    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
  15.166    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
  15.167 @@ -403,7 +399,7 @@
  15.168  
  15.169  structure DivideCancelFactor = ExtractCommonTermFun
  15.170   (open CancelFactorCommon
  15.171 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  15.172 +  val prove_conv = Arith_Data.prove_conv
  15.173    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
  15.174    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
  15.175    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
  15.176 @@ -411,14 +407,14 @@
  15.177  
  15.178  structure DvdCancelFactor = ExtractCommonTermFun
  15.179   (open CancelFactorCommon
  15.180 -  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  15.181 +  val prove_conv = Arith_Data.prove_conv
  15.182    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
  15.183    val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
  15.184    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
  15.185  );
  15.186  
  15.187  val cancel_factor =
  15.188 -  map prep_simproc
  15.189 +  map Arith_Data.prep_simproc
  15.190     [("nat_eq_cancel_factor",
  15.191       ["(l::nat) * m = n", "(l::nat) = m * n"],
  15.192       K EqCancelFactor.proc),
    16.1 --- a/src/HOL/Tools/rat_arith.ML	Thu Mar 12 22:16:25 2009 +0100
    16.2 +++ b/src/HOL/Tools/rat_arith.ML	Thu Mar 12 23:01:25 2009 +0100
    16.3 @@ -34,8 +34,6 @@
    16.4  
    16.5  in
    16.6  
    16.7 -val ratT = Type ("Rational.rat", [])
    16.8 -
    16.9  val rat_arith_setup =
   16.10    LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   16.11     {add_mono_thms = add_mono_thms,
   16.12 @@ -45,7 +43,7 @@
   16.13      neqE =  neqE,
   16.14      simpset = simpset addsimps simps
   16.15                        addsimprocs simprocs}) #>
   16.16 -  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> ratT) #>
   16.17 -  arith_inj_const (@{const_name of_int}, HOLogic.intT --> ratT)
   16.18 +  arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
   16.19 +  arith_inj_const (@{const_name of_int}, @{typ "int => rat"})
   16.20  
   16.21  end;
    17.1 --- a/src/Tools/code/code_target.ML	Thu Mar 12 22:16:25 2009 +0100
    17.2 +++ b/src/Tools/code/code_target.ML	Thu Mar 12 23:01:25 2009 +0100
    17.3 @@ -37,6 +37,7 @@
    17.4    val string: string list -> serialization -> string
    17.5    val code_of: theory -> string -> string
    17.6      -> string list -> (Code_Thingol.naming -> string list) -> string
    17.7 +  val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    17.8    val code_width: int ref
    17.9  
   17.10    val allow_abort: string -> theory -> theory
   17.11 @@ -527,13 +528,13 @@
   17.12  
   17.13  val (inK, module_nameK, fileK) = ("in", "module_name", "file");
   17.14  
   17.15 -fun code_exprP cmd =
   17.16 +val code_exprP =
   17.17    (Scan.repeat P.term_group
   17.18    -- Scan.repeat (P.$$$ inK |-- P.name
   17.19       -- Scan.option (P.$$$ module_nameK |-- P.name)
   17.20       -- Scan.option (P.$$$ fileK |-- P.name)
   17.21       -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
   17.22 -  ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
   17.23 +  ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
   17.24  
   17.25  val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
   17.26  
   17.27 @@ -594,7 +595,14 @@
   17.28  
   17.29  val _ =
   17.30    OuterSyntax.command "export_code" "generate executable code for constants"
   17.31 -    K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   17.32 +    K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   17.33 +
   17.34 +fun shell_command thyname cmd = Toplevel.program (fn _ =>
   17.35 +  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP)
   17.36 +    ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
   17.37 +   of SOME f => (writeln "Now generating code..."; f (theory thyname))
   17.38 +    | NONE => error ("Bad directive " ^ quote cmd)))
   17.39 +  handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
   17.40  
   17.41  end; (*local*)
   17.42