1.1 --- a/doc-src/IsarOverview/Isar/Induction.thy	Sat Mar 21 12:37:13 2009 +0100
     1.2 +++ b/doc-src/IsarOverview/Isar/Induction.thy	Sun Mar 22 19:36:04 2009 +0100
     1.3 @@ -143,14 +143,14 @@
     1.4  universally quantifies all \emph{vars} before the induction.  Hence
     1.5  they can be replaced by \emph{arbitrary} values in the proof.
     1.6  
     1.7 -The nice thing about generalization via @{text"arbitrary:"} is that in
     1.8 -the induction step the claim is available in unquantified form but
     1.9 +Generalization via @{text"arbitrary"} is particularly convenient
    1.10 +if the induction step is a structured proof as opposed to the automatic
    1.11 +example above. Then the claim is available in unquantified form but
    1.12  with the generalized variables replaced by @{text"?"}-variables, ready
    1.13 -for instantiation. In the above example the
    1.14 -induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"}.
    1.15 +for instantiation. In the above example, in the @{const[source] Cons} case the
    1.16 +induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"} (available
    1.17 +under the name @{const[source] Cons}).
    1.18  
    1.19 -For the curious: @{text"arbitrary:"} introduces @{text"\<And>"}
    1.20 -behind the scenes.
    1.21  
    1.22  \subsection{Inductive proofs of conditional formulae}
    1.23  \label{sec:full-Ind}

     2.1 --- a/doc-src/IsarOverview/Isar/Logic.thy	Sat Mar 21 12:37:13 2009 +0100
     2.2 +++ b/doc-src/IsarOverview/Isar/Logic.thy	Sun Mar 22 19:36:04 2009 +0100
     2.3 @@ -30,8 +30,8 @@
     2.4    show A by(rule a)
     2.5  qed
     2.6  
     2.7 -text{*\noindent Single-identifier formulae such as @{term A} need not
     2.8 -be enclosed in double quotes. However, we will continue to do so for
     2.9 +text{*\noindent As you see above, single-identifier formulae such as @{term A}
    2.10 +need not be enclosed in double quotes. However, we will continue to do so for
    2.11  uniformity.
    2.12  
    2.13  Instead of applying fact @{text a} via the @{text rule} method, we can

     3.1 --- a/doc-src/IsarOverview/Isar/document/Induction.tex	Sat Mar 21 12:37:13 2009 +0100
     3.2 +++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Sun Mar 22 19:36:04 2009 +0100
     3.3 @@ -342,14 +342,14 @@
     3.4  universally quantifies all \emph{vars} before the induction.  Hence
     3.5  they can be replaced by \emph{arbitrary} values in the proof.
     3.6  
     3.7 -The nice thing about generalization via \isa{arbitrary{\isacharcolon}} is that in
     3.8 -the induction step the claim is available in unquantified form but
     3.9 +Generalization via \isa{arbitrary} is particularly convenient
    3.10 +if the induction step is a structured proof as opposed to the automatic
    3.11 +example above. Then the claim is available in unquantified form but
    3.12  with the generalized variables replaced by \isa{{\isacharquery}}-variables, ready
    3.13 -for instantiation. In the above example the
    3.14 -induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys}.
    3.15 +for instantiation. In the above example, in the \isa{Cons} case the
    3.16 +induction hypothesis is \isa{itrev\ xs\ {\isacharquery}ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ {\isacharquery}ys} (available
    3.17 +under the name \isa{Cons}).
    3.18  
    3.19 -For the curious: \isa{arbitrary{\isacharcolon}} introduces \isa{{\isasymAnd}}
    3.20 -behind the scenes.
    3.21  
    3.22  \subsection{Inductive proofs of conditional formulae}
    3.23  \label{sec:full-Ind}

     4.1 --- a/doc-src/IsarOverview/Isar/document/Logic.tex	Sat Mar 21 12:37:13 2009 +0100
     4.2 +++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Sun Mar 22 19:36:04 2009 +0100
     4.3 @@ -93,8 +93,8 @@
     4.4  \endisadelimproof
     4.5  %
     4.6  \begin{isamarkuptext}%
     4.7 -\noindent Single-identifier formulae such as \isa{A} need not
     4.8 -be enclosed in double quotes. However, we will continue to do so for
     4.9 +\noindent As you see above, single-identifier formulae such as \isa{A}
    4.10 +need not be enclosed in double quotes. However, we will continue to do so for
    4.11  uniformity.
    4.12  
    4.13  Instead of applying fact \isa{a} via the \isa{rule} method, we can

     5.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Sat Mar 21 12:37:13 2009 +0100
     5.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Sun Mar 22 19:36:04 2009 +0100
     5.3 @@ -617,7 +617,7 @@
     5.4    same types as they have in the main goal statement.
     5.5  
     5.6    \medskip Several further kinds of antiquotations and options are
     5.7 -  available \cite{isabelle-sys}.  Here are a few commonly used
     5.8 +  available \cite{isabelle-isar-ref}.  Here are a few commonly used
     5.9    combinations:
    5.10  
    5.11    \medskip

     6.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Sat Mar 21 12:37:13 2009 +0100
     6.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Sun Mar 22 19:36:04 2009 +0100
     6.3 @@ -691,7 +691,7 @@
     6.4    same types as they have in the main goal statement.
     6.5  
     6.6    \medskip Several further kinds of antiquotations and options are
     6.7 -  available \cite{isabelle-sys}.  Here are a few commonly used
     6.8 +  available \cite{isabelle-isar-ref}.  Here are a few commonly used
     6.9    combinations:
    6.10  
    6.11    \medskip

     7.1 --- a/doc-src/TutorialI/Rules/rules.tex	Sat Mar 21 12:37:13 2009 +0100
     7.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Sun Mar 22 19:36:04 2009 +0100
     7.3 @@ -2138,11 +2138,11 @@
     7.4  
     7.5  \index{*insert (method)|(}%
     7.6  The \isa{insert} method
     7.7 -inserts a given theorem as a new assumption of the current subgoal.  This
     7.8 +inserts a given theorem as a new assumption of all subgoals.  This
     7.9  already is a forward step; moreover, we may (as always when using a
    7.10  theorem) apply
    7.11  \isa{of}, \isa{THEN} and other directives.  The new assumption can then
    7.12 -be used to help prove the subgoal.
    7.13 +be used to help prove the subgoals.
    7.14  
    7.15  For example, consider this theorem about the divides relation.  The first
    7.16  proof step inserts the distributive law for

     8.1 --- a/doc-src/TutorialI/Sets/sets.tex	Sat Mar 21 12:37:13 2009 +0100
     8.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Sun Mar 22 19:36:04 2009 +0100
     8.3 @@ -299,7 +299,7 @@
     8.4  \isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
     8.5  \begin{isabelle}
     8.6  (b\ \isasymin\
     8.7 -(\isasymUnion x\isasymin A. B\ x) =\ (\isasymexists x\isasymin A.\
     8.8 +(\isasymUnion x\isasymin A. B\ x)) =\ (\isasymexists x\isasymin A.\
     8.9  b\ \isasymin\ B\ x)
    8.10  \rulenamedx{UN_iff}
    8.11  \end{isabelle}
    8.12 @@ -414,12 +414,12 @@
    8.13  $k$-element subsets of~$A$ is \index{binomial coefficients}
    8.14  $\binom{n}{k}$.
    8.15  
    8.16 -\begin{warn}
    8.17 -The term \isa{finite\ A} is defined via a syntax translation as an
    8.18 -abbreviation for \isa{A {\isasymin} Finites}, where the constant
    8.19 -\cdx{Finites} denotes the set of all finite sets of a given type.  There
    8.20 -is no constant \isa{finite}.
    8.21 -\end{warn}
    8.22 +%\begin{warn}
    8.23 +%The term \isa{finite\ A} is defined via a syntax translation as an
    8.24 +%abbreviation for \isa{A {\isasymin} Finites}, where the constant
    8.25 +%\cdx{Finites} denotes the set of all finite sets of a given type.  There
    8.26 +%is no constant \isa{finite}.
    8.27 +%\end{warn}
    8.28  \index{sets|)}
    8.29  
    8.30  

     9.1 --- a/doc-src/TutorialI/Types/Overloading2.thy	Sat Mar 21 12:37:13 2009 +0100
     9.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy	Sun Mar 22 19:36:04 2009 +0100
     9.3 @@ -15,7 +15,7 @@
     9.4                size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
     9.5  
     9.6  text{*\noindent
     9.7 -The infix function @{text"!"} yields the nth element of a list.
     9.8 +The infix function @{text"!"} yields the nth element of a list, starting with 0.
     9.9  
    9.10  \begin{warn}
    9.11  A type constructor can be instantiated in only one way to

    10.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex	Sat Mar 21 12:37:13 2009 +0100
    10.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Sun Mar 22 19:36:04 2009 +0100
    10.3 @@ -46,7 +46,7 @@
    10.4  \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequoteclose}%
    10.5  \begin{isamarkuptext}%
    10.6  \noindent
    10.7 -The infix function \isa{{\isacharbang}} yields the nth element of a list.
    10.8 +The infix function \isa{{\isacharbang}} yields the nth element of a list, starting with 0.
    10.9  
   10.10  \begin{warn}
   10.11  A type constructor can be instantiated in only one way to

    11.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Mar 21 12:37:13 2009 +0100
    11.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Mar 22 19:36:04 2009 +0100
    11.3 @@ -3783,8 +3783,7 @@
    11.4      also from mult_left_mono[OF xp] np have "?N s \<le> real n * x + ?N s" by simp
    11.5      finally have "?N (Floor s) \<le> real n * x + ?N s" .
    11.6      moreover
    11.7 -    {from mult_strict_left_mono[OF x1] np 
    11.8 -      have "real n *x + ?N s < real n + ?N s" by simp
    11.9 +    {from x1 np have "real n *x + ?N s < real n + ?N s" by simp
   11.10        also from real_of_int_floor_add_one_gt[where r="?N s"] 
   11.11        have "\<dots> < real n + ?N (Floor s) + 1" by simp
   11.12        finally have "real n *x + ?N s < ?N (Floor s) + real (n+1)" by simp}
   11.13 @@ -3809,8 +3808,7 @@
   11.14      moreover from mult_left_mono_neg[OF xp] nn have "?N s \<ge> real n * x + ?N s" by simp
   11.15      ultimately have "?N (Floor s) + 1 > real n * x + ?N s" by arith 
   11.16      moreover
   11.17 -    {from mult_strict_left_mono_neg[OF x1, where c="real n"] nn
   11.18 -      have "real n *x + ?N s \<ge> real n + ?N s" by simp 
   11.19 +    {from x1 nn have "real n *x + ?N s \<ge> real n + ?N s" by simp
   11.20        moreover from real_of_int_floor_le[where r="?N s"]  have "real n + ?N s \<ge> real n + ?N (Floor s)" by simp
   11.21        ultimately have "real n *x + ?N s \<ge> ?N (Floor s) + real n" 
   11.22  	by (simp only: algebra_simps)}

    12.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sat Mar 21 12:37:13 2009 +0100
    12.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Mar 22 19:36:04 2009 +0100
    12.3 @@ -1494,8 +1494,7 @@
    12.4      have thy: "norm (y' - y) * norm x' < e / (2 * norm x + 2 * norm y + 2) * (1 + norm x)"
    12.5        using mult_strict_mono'[OF h(4) * norm_ge_zero norm_ge_zero] by auto
    12.6      also have "\<dots> \<le> e/2" apply simp unfolding divide_le_eq
    12.7 -      using th1 th0 `e>0` apply auto
    12.8 -      unfolding mult_assoc and real_mult_le_cancel_iff2[OF `e>0`] by auto
    12.9 +      using th1 th0 `e>0` by auto
   12.10  
   12.11      finally have "norm x' * norm (y' - y) + norm (x' - x) * norm y < e"
   12.12        using thx and e by (simp add: field_simps)  }
   12.13 @@ -3558,7 +3557,7 @@
   12.14      { fix y assume "dist y (c *s x) < e * \<bar>c\<bar>"
   12.15        hence "norm ((1 / c) *s y - x) < e" unfolding dist_def
   12.16  	using norm_mul[of c "(1 / c) *s y - x", unfolded vector_ssub_ldistrib, unfolded vector_smult_assoc] assms(1)
   12.17 -	  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
   12.18 +	  assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
   12.19        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  }
   12.20      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  }
   12.21    thus ?thesis unfolding open_def by auto

    13.1 --- a/src/HOL/Rational.thy	Sat Mar 21 12:37:13 2009 +0100
    13.2 +++ b/src/HOL/Rational.thy	Sun Mar 22 19:36:04 2009 +0100
    13.3 @@ -691,7 +691,6 @@
    13.4      \<longleftrightarrow> Fract a b < Fract c d"
    13.5      using not_zero `b * d > 0`
    13.6      by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
    13.7 -      (auto intro: mult_strict_right_mono mult_right_less_imp_less)
    13.8  qed
    13.9  
   13.10  lemma of_rat_less_eq:

    14.1 --- a/src/HOL/Ring_and_Field.thy	Sat Mar 21 12:37:13 2009 +0100
    14.2 +++ b/src/HOL/Ring_and_Field.thy	Sun Mar 22 19:36:04 2009 +0100
    14.3 @@ -987,6 +987,27 @@
    14.4    "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
    14.5  by (simp add: not_less [symmetric] mult_less_cancel_left_disj)
    14.6  
    14.7 +lemma mult_le_cancel_left_pos:
    14.8 +  "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b"
    14.9 +by (auto simp: mult_le_cancel_left)
   14.10 +
   14.11 +lemma mult_le_cancel_left_neg:
   14.12 +  "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a"
   14.13 +by (auto simp: mult_le_cancel_left)
   14.14 +
   14.15 +end
   14.16 +
   14.17 +context ordered_ring_strict
   14.18 +begin
   14.19 +
   14.20 +lemma mult_less_cancel_left_pos:
   14.21 +  "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b"
   14.22 +by (auto simp: mult_less_cancel_left)
   14.23 +
   14.24 +lemma mult_less_cancel_left_neg:
   14.25 +  "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a"
   14.26 +by (auto simp: mult_less_cancel_left)
   14.27 +
   14.28  end
   14.29  
   14.30  text{*Legacy - use @{text algebra_simps} *}

    15.1 --- a/src/HOL/Series.thy	Sat Mar 21 12:37:13 2009 +0100
    15.2 +++ b/src/HOL/Series.thy	Sun Mar 22 19:36:04 2009 +0100
    15.3 @@ -557,7 +557,6 @@
    15.4  apply (induct_tac "na", auto)
    15.5  apply (rule_tac y = "c * norm (f (N + n))" in order_trans)
    15.6  apply (auto intro: mult_right_mono simp add: summable_def)
    15.7 -apply (simp add: mult_ac)
    15.8  apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
    15.9  apply (rule sums_divide) 
   15.10  apply (rule sums_mult)

    16.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Sat Mar 21 12:37:13 2009 +0100
    16.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Sun Mar 22 19:36:04 2009 +0100
    16.3 @@ -218,9 +218,30 @@
    16.4  val simplify_one = Arith_Data.simplify_meta_eq  
    16.5    [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
    16.6  
    16.7 -fun cancel_simplify_meta_eq cancel_th ss th =
    16.8 +fun cancel_simplify_meta_eq ss cancel_th th =
    16.9      simplify_one ss (([th, cancel_th]) MRS trans);
   16.10  
   16.11 +local
   16.12 +  val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop)
   16.13 +  fun Eq_True_elim Eq = 
   16.14 +    Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
   16.15 +in
   16.16 +fun sign_conv pos_th neg_th ss t =
   16.17 +  let val T = fastype_of t;
   16.18 +      val zero = Const(@{const_name HOL.zero}, T);
   16.19 +      val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
   16.20 +      val pos = less $ zero $ t and neg = less $ t $ zero
   16.21 +      fun prove p =
   16.22 +        Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
   16.23 +        handle THM _ => NONE
   16.24 +    in case prove pos of
   16.25 +         SOME th => SOME(th RS pos_th)
   16.26 +       | NONE => (case prove neg of
   16.27 +                    SOME th => SOME(th RS neg_th)
   16.28 +                  | NONE => NONE)
   16.29 +    end;
   16.30 +end
   16.31 +
   16.32  structure CancelFactorCommon =
   16.33    struct
   16.34    val mk_sum            = long_mk_prod
   16.35 @@ -231,6 +252,7 @@
   16.36    val trans_tac         = K Arith_Data.trans_tac
   16.37    val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   16.38    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   16.39 +  val simplify_meta_eq  = cancel_simplify_meta_eq 
   16.40    end;
   16.41  
   16.42  (*mult_cancel_left requires a ring with no zero divisors.*)
   16.43 @@ -239,7 +261,27 @@
   16.44    val prove_conv = Arith_Data.prove_conv
   16.45    val mk_bal   = HOLogic.mk_eq
   16.46    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   16.47 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_cancel_left}
   16.48 +  val simp_conv = K (K (SOME @{thm mult_cancel_left}))
   16.49 +);
   16.50 +
   16.51 +(*for ordered rings*)
   16.52 +structure LeCancelFactor = ExtractCommonTermFun
   16.53 + (open CancelFactorCommon
   16.54 +  val prove_conv = Arith_Data.prove_conv
   16.55 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   16.56 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   16.57 +  val simp_conv = sign_conv
   16.58 +    @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
   16.59 +);
   16.60 +
   16.61 +(*for ordered rings*)
   16.62 +structure LessCancelFactor = ExtractCommonTermFun
   16.63 + (open CancelFactorCommon
   16.64 +  val prove_conv = Arith_Data.prove_conv
   16.65 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   16.66 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   16.67 +  val simp_conv = sign_conv
   16.68 +    @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
   16.69  );
   16.70  
   16.71  (*zdiv_zmult_zmult1_if is for integer division (div).*)
   16.72 @@ -248,7 +290,7 @@
   16.73    val prove_conv = Arith_Data.prove_conv
   16.74    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   16.75    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
   16.76 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
   16.77 +  val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if}))
   16.78  );
   16.79  
   16.80  structure IntModCancelFactor = ExtractCommonTermFun
   16.81 @@ -256,7 +298,7 @@
   16.82    val prove_conv = Arith_Data.prove_conv
   16.83    val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   16.84    val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
   16.85 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
   16.86 +  val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1}))
   16.87  );
   16.88  
   16.89  structure IntDvdCancelFactor = ExtractCommonTermFun
   16.90 @@ -264,7 +306,7 @@
   16.91    val prove_conv = Arith_Data.prove_conv
   16.92    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   16.93    val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
   16.94 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
   16.95 +  val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
   16.96  );
   16.97  
   16.98  (*Version for all fields, including unordered ones (type complex).*)
   16.99 @@ -273,7 +315,7 @@
  16.100    val prove_conv = Arith_Data.prove_conv
  16.101    val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
  16.102    val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
  16.103 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
  16.104 +  val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
  16.105  );
  16.106  
  16.107  val cancel_factors =
  16.108 @@ -281,7 +323,15 @@
  16.109     [("ring_eq_cancel_factor",
  16.110       ["(l::'a::{idom}) * m = n",
  16.111        "(l::'a::{idom}) = m * n"],
  16.112 -    K EqCancelFactor.proc),
  16.113 +     K EqCancelFactor.proc),
  16.114 +    ("ordered_ring_le_cancel_factor",
  16.115 +     ["(l::'a::ordered_ring) * m <= n",
  16.116 +      "(l::'a::ordered_ring) <= m * n"],
  16.117 +     K LeCancelFactor.proc),
  16.118 +    ("ordered_ring_less_cancel_factor",
  16.119 +     ["(l::'a::ordered_ring) * m < n",
  16.120 +      "(l::'a::ordered_ring) < m * n"],
  16.121 +     K LessCancelFactor.proc),
  16.122      ("int_div_cancel_factor",
  16.123       ["((l::int) * m) div n", "(l::int) div (m * n)"],
  16.124       K IntDivCancelFactor.proc),

    17.1 --- a/src/HOL/Tools/nat_simprocs.ML	Sat Mar 21 12:37:13 2009 +0100
    17.2 +++ b/src/HOL/Tools/nat_simprocs.ML	Sun Mar 22 19:36:04 2009 +0100
    17.3 @@ -352,7 +352,7 @@
    17.4  val simplify_one = Arith_Data.simplify_meta_eq  
    17.5    [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
    17.6  
    17.7 -fun cancel_simplify_meta_eq cancel_th ss th =
    17.8 +fun cancel_simplify_meta_eq ss cancel_th th =
    17.9      simplify_one ss (([th, cancel_th]) MRS trans);
   17.10  
   17.11  structure CancelFactorCommon =
   17.12 @@ -365,6 +365,7 @@
   17.13    val trans_tac         = K Arith_Data.trans_tac
   17.14    val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   17.15    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   17.16 +  val simplify_meta_eq  = cancel_simplify_meta_eq
   17.17    end;
   17.18  
   17.19  structure EqCancelFactor = ExtractCommonTermFun
   17.20 @@ -372,7 +373,7 @@
   17.21    val prove_conv = Arith_Data.prove_conv
   17.22    val mk_bal   = HOLogic.mk_eq
   17.23    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   17.24 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
   17.25 +  val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
   17.26  );
   17.27  
   17.28  structure LessCancelFactor = ExtractCommonTermFun
   17.29 @@ -380,7 +381,7 @@
   17.30    val prove_conv = Arith_Data.prove_conv
   17.31    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   17.32    val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   17.33 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
   17.34 +  val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
   17.35  );
   17.36  
   17.37  structure LeCancelFactor = ExtractCommonTermFun
   17.38 @@ -388,7 +389,7 @@
   17.39    val prove_conv = Arith_Data.prove_conv
   17.40    val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   17.41    val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   17.42 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
   17.43 +  val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
   17.44  );
   17.45  
   17.46  structure DivideCancelFactor = ExtractCommonTermFun
   17.47 @@ -396,7 +397,7 @@
   17.48    val prove_conv = Arith_Data.prove_conv
   17.49    val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   17.50    val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   17.51 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
   17.52 +  val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
   17.53  );
   17.54  
   17.55  structure DvdCancelFactor = ExtractCommonTermFun
   17.56 @@ -404,7 +405,7 @@
   17.57    val prove_conv = Arith_Data.prove_conv
   17.58    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   17.59    val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
   17.60 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
   17.61 +  val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
   17.62  );
   17.63  
   17.64  val cancel_factor =

    18.1 --- a/src/HOL/Word/WordArith.thy	Sat Mar 21 12:37:13 2009 +0100
    18.2 +++ b/src/HOL/Word/WordArith.thy	Sun Mar 22 19:36:04 2009 +0100
    18.3 @@ -701,6 +701,7 @@
    18.4    apply (erule (2) udvd_decr0)
    18.5    done
    18.6  
    18.7 +ML{*Delsimprocs cancel_factors*}
    18.8  lemma udvd_incr2_K: 
    18.9    "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 
   18.10      0 < K ==> p <= p + K & p + K <= a + s"
   18.11 @@ -716,6 +717,7 @@
   18.12     apply arith
   18.13    apply simp
   18.14    done
   18.15 +ML{*Delsimprocs cancel_factors*}
   18.16  
   18.17  (* links with rbl operations *)
   18.18  lemma word_succ_rbl:

    19.1 --- a/src/Provers/Arith/extract_common_term.ML	Sat Mar 21 12:37:13 2009 +0100
    19.2 +++ b/src/Provers/Arith/extract_common_term.ML	Sun Mar 22 19:36:04 2009 +0100
    19.3 @@ -25,7 +25,8 @@
    19.4    (*proof tools*)
    19.5    val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
    19.6    val norm_tac: simpset -> tactic                (*proves the result*)
    19.7 -  val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the result*)
    19.8 +  val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*)
    19.9 +  val simp_conv: simpset -> term -> thm option  (*proves simp thm*)
   19.10  end;
   19.11  
   19.12  
   19.13 @@ -58,6 +59,9 @@
   19.14      and terms2 = Data.dest_sum t2
   19.15  
   19.16      val u = find_common (terms1,terms2)
   19.17 +    val simp_th =
   19.18 +          case Data.simp_conv ss u of NONE => raise TERM("no simp", [])
   19.19 +          | SOME th => th
   19.20      val terms1' = Data.find_first u terms1
   19.21      and terms2' = Data.find_first u terms2
   19.22      and T = Term.fastype_of u
   19.23 @@ -66,7 +70,7 @@
   19.24        Data.prove_conv [Data.norm_tac ss] ctxt prems
   19.25          (t', Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')))
   19.26    in
   19.27 -    Option.map (export o Data.simplify_meta_eq ss) reshape
   19.28 +    Option.map (export o Data.simplify_meta_eq ss simp_th) reshape
   19.29    end
   19.30    (* FIXME avoid handling of generic exceptions *)
   19.31    handle TERM _ => NONE