# HG changeset patch
# User nipkow
# Date 1237747401 -3600
# Node ID 226c91456e5435c0c2d1bb643b43fd7a64a57fae
# Parent  17365ef082f3511d85e2fc387f1282178278dd1a# Parent  57753e0ec1d4f13010a21f144740edea484fc78a
merged

diff -r 17365ef082f3 -r 226c91456e54 doc-src/IsarOverview/Isar/Induction.thy
--- a/doc-src/IsarOverview/Isar/Induction.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/IsarOverview/Isar/Induction.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -143,14 +143,14 @@
 universally quantifies all \emph{vars} before the induction.  Hence
 they can be replaced by \emph{arbitrary} values in the proof.
 
-The nice thing about generalization via @{text"arbitrary:"} is that in
-the induction step the claim is available in unquantified form but
+Generalization via @{text"arbitrary"} is particularly convenient
+if the induction step is a structured proof as opposed to the automatic
+example above. Then the claim is available in unquantified form but
 with the generalized variables replaced by @{text"?"}-variables, ready
-for instantiation. In the above example the
-induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"}.
+for instantiation. In the above example, in the @{const[source] Cons} case the
+induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"} (available
+under the name @{const[source] Cons}).
 
-For the curious: @{text"arbitrary:"} introduces @{text"\<And>"}
-behind the scenes.
 
 \subsection{Inductive proofs of conditional formulae}
 \label{sec:full-Ind}
diff -r 17365ef082f3 -r 226c91456e54 doc-src/IsarOverview/Isar/Logic.thy
--- a/doc-src/IsarOverview/Isar/Logic.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -30,8 +30,8 @@
   show A by(rule a)
 qed
 
-text{*\noindent Single-identifier formulae such as @{term A} need not
-be enclosed in double quotes. However, we will continue to do so for
+text{*\noindent As you see above, single-identifier formulae such as @{term A}
+need not be enclosed in double quotes. However, we will continue to do so for
 uniformity.
 
 Instead of applying fact @{text a} via the @{text rule} method, we can
diff -r 17365ef082f3 -r 226c91456e54 doc-src/IsarOverview/Isar/document/Induction.tex
--- a/doc-src/IsarOverview/Isar/document/Induction.tex	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Sun Mar 22 19:43:21 2009 +0100
@@ -342,14 +342,14 @@
 universally quantifies all \emph{vars} before the induction.  Hence
 they can be replaced by \emph{arbitrary} values in the proof.
 
-The nice thing about generalization via \isa{arbitrary{\isacharcolon}} is that in
-the induction step the claim is available in unquantified form but
+Generalization via \isa{arbitrary} is particularly convenient
+if the induction step is a structured proof as opposed to the automatic
+example above. Then the claim is available in unquantified form but
 with the generalized variables replaced by \isa{{\isacharquery}}-variables, ready
-for instantiation. In the above example the
-induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys}.
+for instantiation. In the above example, in the \isa{Cons} case the
+induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys} (available
+under the name \isa{Cons}).
 
-For the curious: \isa{arbitrary{\isacharcolon}} introduces \isa{{\isasymAnd}}
-behind the scenes.
 
 \subsection{Inductive proofs of conditional formulae}
 \label{sec:full-Ind}
diff -r 17365ef082f3 -r 226c91456e54 doc-src/IsarOverview/Isar/document/Logic.tex
--- a/doc-src/IsarOverview/Isar/document/Logic.tex	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Sun Mar 22 19:43:21 2009 +0100
@@ -93,8 +93,8 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-\noindent Single-identifier formulae such as \isa{A} need not
-be enclosed in double quotes. However, we will continue to do so for
+\noindent As you see above, single-identifier formulae such as \isa{A}
+need not be enclosed in double quotes. However, we will continue to do so for
 uniformity.
 
 Instead of applying fact \isa{a} via the \isa{rule} method, we can
diff -r 17365ef082f3 -r 226c91456e54 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -617,7 +617,7 @@
   same types as they have in the main goal statement.
 
   \medskip Several further kinds of antiquotations and options are
-  available \cite{isabelle-sys}.  Here are a few commonly used
+  available \cite{isabelle-isar-ref}.  Here are a few commonly used
   combinations:
 
   \medskip
diff -r 17365ef082f3 -r 226c91456e54 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Sun Mar 22 19:43:21 2009 +0100
@@ -691,7 +691,7 @@
   same types as they have in the main goal statement.
 
   \medskip Several further kinds of antiquotations and options are
-  available \cite{isabelle-sys}.  Here are a few commonly used
+  available \cite{isabelle-isar-ref}.  Here are a few commonly used
   combinations:
 
   \medskip
diff -r 17365ef082f3 -r 226c91456e54 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Sun Mar 22 19:43:21 2009 +0100
@@ -2138,11 +2138,11 @@
 
 \index{*insert (method)|(}%
 The \isa{insert} method
-inserts a given theorem as a new assumption of the current subgoal.  This
+inserts a given theorem as a new assumption of all subgoals.  This
 already is a forward step; moreover, we may (as always when using a
 theorem) apply
 \isa{of}, \isa{THEN} and other directives.  The new assumption can then
-be used to help prove the subgoal.
+be used to help prove the subgoals.
 
 For example, consider this theorem about the divides relation.  The first
 proof step inserts the distributive law for
diff -r 17365ef082f3 -r 226c91456e54 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Sun Mar 22 19:43:21 2009 +0100
@@ -299,7 +299,7 @@
 \isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
 \begin{isabelle}
 (b\ \isasymin\
-(\isasymUnion x\isasymin A. B\ x) =\ (\isasymexists x\isasymin A.\
+(\isasymUnion x\isasymin A. B\ x)) =\ (\isasymexists x\isasymin A.\
 b\ \isasymin\ B\ x)
 \rulenamedx{UN_iff}
 \end{isabelle}
@@ -414,12 +414,12 @@
 $k$-element subsets of~$A$ is \index{binomial coefficients}
 $\binom{n}{k}$.
 
-\begin{warn}
-The term \isa{finite\ A} is defined via a syntax translation as an
-abbreviation for \isa{A {\isasymin} Finites}, where the constant
-\cdx{Finites} denotes the set of all finite sets of a given type.  There
-is no constant \isa{finite}.
-\end{warn}
+%\begin{warn}
+%The term \isa{finite\ A} is defined via a syntax translation as an
+%abbreviation for \isa{A {\isasymin} Finites}, where the constant
+%\cdx{Finites} denotes the set of all finite sets of a given type.  There
+%is no constant \isa{finite}.
+%\end{warn}
 \index{sets|)}
 
 
diff -r 17365ef082f3 -r 226c91456e54 doc-src/TutorialI/Types/Overloading2.thy
--- a/doc-src/TutorialI/Types/Overloading2.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -15,7 +15,7 @@
               size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
 
 text{*\noindent
-The infix function @{text"!"} yields the nth element of a list.
+The infix function @{text"!"} yields the nth element of a list, starting with 0.
 
 \begin{warn}
 A type constructor can be instantiated in only one way to
diff -r 17365ef082f3 -r 226c91456e54 doc-src/TutorialI/Types/document/Overloading2.tex
--- a/doc-src/TutorialI/Types/document/Overloading2.tex	Sun Mar 22 11:56:32 2009 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Sun Mar 22 19:43:21 2009 +0100
@@ -46,7 +46,7 @@
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list.
+The infix function \isa{{\isacharbang}} yields the nth element of a list, starting with 0.
 
 \begin{warn}
 A type constructor can be instantiated in only one way to
diff -r 17365ef082f3 -r 226c91456e54 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -3783,8 +3783,7 @@
     also from mult_left_mono[OF xp] np have "?N s \<le> real n * x + ?N s" by simp
     finally have "?N (Floor s) \<le> real n * x + ?N s" .
     moreover
-    {from mult_strict_left_mono[OF x1] np 
-      have "real n *x + ?N s < real n + ?N s" by simp
+    {from x1 np have "real n *x + ?N s < real n + ?N s" by simp
       also from real_of_int_floor_add_one_gt[where r="?N s"] 
       have "\<dots> < real n + ?N (Floor s) + 1" by simp
       finally have "real n *x + ?N s < ?N (Floor s) + real (n+1)" by simp}
@@ -3809,8 +3808,7 @@
     moreover from mult_left_mono_neg[OF xp] nn have "?N s \<ge> real n * x + ?N s" by simp
     ultimately have "?N (Floor s) + 1 > real n * x + ?N s" by arith 
     moreover
-    {from mult_strict_left_mono_neg[OF x1, where c="real n"] nn
-      have "real n *x + ?N s \<ge> real n + ?N s" by simp 
+    {from x1 nn have "real n *x + ?N s \<ge> real n + ?N s" by simp
       moreover from real_of_int_floor_le[where r="?N s"]  have "real n + ?N s \<ge> real n + ?N (Floor s)" by simp
       ultimately have "real n *x + ?N s \<ge> ?N (Floor s) + real n" 
 	by (simp only: algebra_simps)}
diff -r 17365ef082f3 -r 226c91456e54 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -1494,8 +1494,7 @@
     have thy: "norm (y' - y) * norm x' < e / (2 * norm x + 2 * norm y + 2) * (1 + norm x)"
       using mult_strict_mono'[OF h(4) * norm_ge_zero norm_ge_zero] by auto
     also have "\<dots> \<le> e/2" apply simp unfolding divide_le_eq
-      using th1 th0 `e>0` apply auto
-      unfolding mult_assoc and real_mult_le_cancel_iff2[OF `e>0`] by auto
+      using th1 th0 `e>0` by auto
 
     finally have "norm x' * norm (y' - y) + norm (x' - x) * norm y < e"
       using thx and e by (simp add: field_simps)  }
@@ -3558,7 +3557,7 @@
     { fix y assume "dist y (c *s x) < e * \<bar>c\<bar>"
       hence "norm ((1 / c) *s y - x) < e" unfolding dist_def
 	using norm_mul[of c "(1 / c) *s y - x", unfolded vector_ssub_ldistrib, unfolded vector_smult_assoc] assms(1)
-	  mult_less_imp_less_left[of "abs c" "norm ((1 / c) *s y - x)" e, unfolded real_mult_commute[of "abs c" e]] assms(1)[unfolded zero_less_abs_iff[THEN sym]] by simp
+	  assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
       hence "y \<in> op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"]  e[THEN spec[where x="(1 / c) *s y"]]  assms(1) unfolding dist_def vector_smult_assoc by auto  }
     ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *s x) < e \<longrightarrow> x' \<in> op *s c ` s" apply(rule_tac x="e * abs c" in exI) by auto  }
   thus ?thesis unfolding open_def by auto
diff -r 17365ef082f3 -r 226c91456e54 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/src/HOL/Rational.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -691,7 +691,6 @@
     \<longleftrightarrow> Fract a b < Fract c d"
     using not_zero `b * d > 0`
     by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
-      (auto intro: mult_strict_right_mono mult_right_less_imp_less)
 qed
 
 lemma of_rat_less_eq:
diff -r 17365ef082f3 -r 226c91456e54 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -1136,6 +1136,27 @@
   "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
 by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
 
+lemma mult_le_cancel_left_pos:
+  "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
+by (auto simp: mult_le_cancel_left)
+
+lemma mult_le_cancel_left_neg:
+  "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
+by (auto simp: mult_le_cancel_left)
+
+end
+
+context ordered_ring_strict
+begin
+
+lemma mult_less_cancel_left_pos:
+  "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
+by (auto simp: mult_less_cancel_left)
+
+lemma mult_less_cancel_left_neg:
+  "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
+by (auto simp: mult_less_cancel_left)
+
 end
 
 text{*Legacy - use @{text algebra_simps} *}
diff -r 17365ef082f3 -r 226c91456e54 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/src/HOL/Series.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -557,7 +557,6 @@
 apply (induct_tac "na", auto)
 apply (rule_tac y = "c * norm (f (N + n))" in order_trans)
 apply (auto intro: mult_right_mono simp add: summable_def)
-apply (simp add: mult_ac)
 apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
 apply (rule sums_divide) 
 apply (rule sums_mult)
diff -r 17365ef082f3 -r 226c91456e54 src/HOL/Tools/int_factor_simprocs.ML
--- a/src/HOL/Tools/int_factor_simprocs.ML	Sun Mar 22 11:56:32 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Sun Mar 22 19:43:21 2009 +0100
@@ -218,9 +218,30 @@
 val simplify_one = Arith_Data.simplify_meta_eq  
   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
 
-fun cancel_simplify_meta_eq cancel_th ss th =
+fun cancel_simplify_meta_eq ss cancel_th th =
     simplify_one ss (([th, cancel_th]) MRS trans);
 
+local
+  val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop)
+  fun Eq_True_elim Eq = 
+    Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
+in
+fun sign_conv pos_th neg_th ss t =
+  let val T = fastype_of t;
+      val zero = Const(@{const_name HOL.zero}, T);
+      val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
+      val pos = less $ zero $ t and neg = less $ t $ zero
+      fun prove p =
+        Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
+        handle THM _ => NONE
+    in case prove pos of
+         SOME th => SOME(th RS pos_th)
+       | NONE => (case prove neg of
+                    SOME th => SOME(th RS neg_th)
+                  | NONE => NONE)
+    end;
+end
+
 structure CancelFactorCommon =
   struct
   val mk_sum            = long_mk_prod
@@ -231,6 +252,7 @@
   val trans_tac         = K Arith_Data.trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
+  val simplify_meta_eq  = cancel_simplify_meta_eq 
   end;
 
 (*mult_cancel_left requires a ring with no zero divisors.*)
@@ -239,7 +261,27 @@
   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}
+  val simp_conv = K (K (SOME @{thm mult_cancel_left}))
+);
+
+(*for ordered rings*)
+structure LeCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  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 simp_conv = sign_conv
+    @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
+);
+
+(*for ordered rings*)
+structure LessCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  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 simp_conv = sign_conv
+    @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
 );
 
 (*zdiv_zmult_zmult1_if is for integer division (div).*)
@@ -248,7 +290,7 @@
   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}
+  val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if}))
 );
 
 structure IntModCancelFactor = ExtractCommonTermFun
@@ -256,7 +298,7 @@
   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}
+  val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1}))
 );
 
 structure IntDvdCancelFactor = ExtractCommonTermFun
@@ -264,7 +306,7 @@
   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}
+  val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
 );
 
 (*Version for all fields, including unordered ones (type complex).*)
@@ -273,7 +315,7 @@
   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 simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
 );
 
 val cancel_factors =
@@ -281,7 +323,15 @@
    [("ring_eq_cancel_factor",
      ["(l::'a::{idom}) * m = n",
       "(l::'a::{idom}) = m * n"],
-    K EqCancelFactor.proc),
+     K EqCancelFactor.proc),
+    ("ordered_ring_le_cancel_factor",
+     ["(l::'a::ordered_ring) * m <= n",
+      "(l::'a::ordered_ring) <= m * n"],
+     K LeCancelFactor.proc),
+    ("ordered_ring_less_cancel_factor",
+     ["(l::'a::ordered_ring) * m < n",
+      "(l::'a::ordered_ring) < m * n"],
+     K LessCancelFactor.proc),
     ("int_div_cancel_factor",
      ["((l::int) * m) div n", "(l::int) div (m * n)"],
      K IntDivCancelFactor.proc),
diff -r 17365ef082f3 -r 226c91456e54 src/HOL/Tools/nat_simprocs.ML
--- a/src/HOL/Tools/nat_simprocs.ML	Sun Mar 22 11:56:32 2009 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML	Sun Mar 22 19:43:21 2009 +0100
@@ -352,7 +352,7 @@
 val simplify_one = Arith_Data.simplify_meta_eq  
   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
 
-fun cancel_simplify_meta_eq cancel_th ss th =
+fun cancel_simplify_meta_eq ss cancel_th th =
     simplify_one ss (([th, cancel_th]) MRS trans);
 
 structure CancelFactorCommon =
@@ -365,6 +365,7 @@
   val trans_tac         = K Arith_Data.trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
+  val simplify_meta_eq  = cancel_simplify_meta_eq
   end;
 
 structure EqCancelFactor = ExtractCommonTermFun
@@ -372,7 +373,7 @@
   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}
+  val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
 );
 
 structure LessCancelFactor = ExtractCommonTermFun
@@ -380,7 +381,7 @@
   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}
+  val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
 );
 
 structure LeCancelFactor = ExtractCommonTermFun
@@ -388,7 +389,7 @@
   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}
+  val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
 );
 
 structure DivideCancelFactor = ExtractCommonTermFun
@@ -396,7 +397,7 @@
   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}
+  val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
 );
 
 structure DvdCancelFactor = ExtractCommonTermFun
@@ -404,7 +405,7 @@
   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 simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
 );
 
 val cancel_factor =
diff -r 17365ef082f3 -r 226c91456e54 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Sun Mar 22 11:56:32 2009 +0100
+++ b/src/HOL/Word/WordArith.thy	Sun Mar 22 19:43:21 2009 +0100
@@ -701,6 +701,7 @@
   apply (erule (2) udvd_decr0)
   done
 
+ML{*Delsimprocs cancel_factors*}
 lemma udvd_incr2_K: 
   "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 
     0 < K ==> p <= p + K & p + K <= a + s"
@@ -716,6 +717,7 @@
    apply arith
   apply simp
   done
+ML{*Delsimprocs cancel_factors*}
 
 (* links with rbl operations *)
 lemma word_succ_rbl:
diff -r 17365ef082f3 -r 226c91456e54 src/Provers/Arith/extract_common_term.ML
--- a/src/Provers/Arith/extract_common_term.ML	Sun Mar 22 11:56:32 2009 +0100
+++ b/src/Provers/Arith/extract_common_term.ML	Sun Mar 22 19:43:21 2009 +0100
@@ -25,7 +25,8 @@
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
   val norm_tac: simpset -> tactic                (*proves the result*)
-  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the result*)
+  val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*)
+  val simp_conv: simpset -> term -> thm option  (*proves simp thm*)
 end;
 
 
@@ -58,6 +59,9 @@
     and terms2 = Data.dest_sum t2
 
     val u = find_common (terms1,terms2)
+    val simp_th =
+          case Data.simp_conv ss u of NONE => raise TERM("no simp", [])
+          | SOME th => th
     val terms1' = Data.find_first u terms1
     and terms2' = Data.find_first u terms2
     and T = Term.fastype_of u
@@ -66,7 +70,7 @@
       Data.prove_conv [Data.norm_tac ss] ctxt prems
         (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')))
   in
-    Option.map (export o Data.simplify_meta_eq ss) reshape
+    Option.map (export o Data.simplify_meta_eq ss simp_th) reshape
   end
   (* FIXME avoid handling of generic exceptions *)
   handle TERM _ => NONE