# HG changeset patch
# User huffman
# Date 1319694417 -7200
# Node ID d5b5c9259afdaa276be96677e31b30bf8aaead9f
# Parent  66823a0066db163da40563371c0710970988c514
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left

diff -r 66823a0066db -r d5b5c9259afd src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/GCD.thy	Thu Oct 27 07:46:57 2011 +0200
@@ -357,7 +357,7 @@
   apply (induct m n rule: gcd_nat_induct)
   apply simp
   apply (case_tac "k = 0")
-  apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
+  apply (simp_all add: gcd_non_0_nat)
 done
 
 lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
diff -r 66823a0066db -r d5b5c9259afd src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/Library/BigO.thy	Thu Oct 27 07:46:57 2011 +0200
@@ -129,9 +129,6 @@
   apply (erule order_trans)
   apply (simp add: ring_distribs)
   apply (rule mult_left_mono)
-  apply assumption
-  apply (simp add: order_less_le)
-  apply (rule mult_left_mono)
   apply (simp add: abs_triangle_ineq)
   apply (simp add: order_less_le)
   apply (rule mult_nonneg_nonneg)
@@ -150,9 +147,6 @@
   apply (erule order_trans)
   apply (simp add: ring_distribs)
   apply (rule mult_left_mono)
-  apply (simp add: order_less_le)
-  apply (simp add: order_less_le)
-  apply (rule mult_left_mono)
   apply (rule abs_triangle_ineq)
   apply (simp add: order_less_le)
   apply (rule mult_nonneg_nonneg)
diff -r 66823a0066db -r d5b5c9259afd src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Oct 27 07:46:57 2011 +0200
@@ -196,9 +196,6 @@
   apply (erule order_trans)
   apply (simp add: ring_distribs)
   apply (rule mult_left_mono)
-  apply assumption
-  apply (simp add: order_less_le)
-  apply (rule mult_left_mono)
   apply (simp add: abs_triangle_ineq)
   apply (simp add: order_less_le)
   apply (rule mult_nonneg_nonneg)
@@ -217,9 +214,6 @@
   apply (erule order_trans)
   apply (simp add: ring_distribs)
   apply (rule mult_left_mono)
-  apply (simp add: order_less_le)
-  apply (simp add: order_less_le)
-  apply (rule mult_left_mono)
   apply (rule abs_triangle_ineq)
   apply (simp add: order_less_le)
 apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
diff -r 66823a0066db -r d5b5c9259afd src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Oct 27 07:46:57 2011 +0200
@@ -5298,12 +5298,12 @@
     then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
       using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
     { fix n assume "n\<ge>N"
-      hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding f.diff[THEN sym] by auto
-      moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
+      have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
         using subspace_sub[OF s, of "x n" "x N"] using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
         using normf[THEN bspec[where x="x n - x N"]] by auto
-      ultimately have "norm (x n - x N) < d" using `e>0`
-        using mult_left_less_imp_less[of e "norm (x n - x N)" d] by auto   }
+      also have "norm (f (x n - x N)) < e * d"
+        using `N \<le> n` N unfolding f.diff[THEN sym] by auto
+      finally have "norm (x n - x N) < d" using `e>0` by simp }
     hence "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto }
   thus ?thesis unfolding cauchy and dist_norm by auto
 qed
diff -r 66823a0066db -r d5b5c9259afd src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Oct 27 07:46:57 2011 +0200
@@ -134,7 +134,7 @@
   apply (induct m n rule: gcd_induct)
    apply simp
   apply (case_tac "k = 0")
-   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
+   apply (simp_all add: gcd_non_0)
   done
 
 lemma gcd_mult [simp, algebra]: "gcd k (k * n) = k"
diff -r 66823a0066db -r d5b5c9259afd src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Oct 27 07:46:57 2011 +0200
@@ -366,6 +366,7 @@
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq
   val prove_conv = Arith_Data.prove_conv
+  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
 end;
 
 structure EqCancelFactor = ExtractCommonTermFun
diff -r 66823a0066db -r d5b5c9259afd src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 27 07:46:57 2011 +0200
@@ -512,6 +512,7 @@
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq 
   val prove_conv = Arith_Data.prove_conv
+  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
 end;
 
 (*mult_cancel_left requires a ring with no zero divisors.*)
diff -r 66823a0066db -r d5b5c9259afd src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy	Thu Oct 27 07:46:57 2011 +0200
@@ -374,9 +374,8 @@
 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
 by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
 
-lemma "(0::rat) < z \<Longrightarrow> z*x < z*y"
-apply (tactic {* test [linordered_ring_less_cancel_factor] *})?
-oops -- "FIXME: test fails"
+lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y"
+by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
 
 
 subsection {* @{text linordered_ring_le_cancel_factor} *}
@@ -385,8 +384,7 @@
 by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
 
 lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
-apply (tactic {* test [linordered_ring_le_cancel_factor] *})?
-oops -- "FIXME: test fails"
+by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
 
 
 subsection {* @{text field_combine_numerals} *}
diff -r 66823a0066db -r d5b5c9259afd src/Provers/Arith/extract_common_term.ML
--- a/src/Provers/Arith/extract_common_term.ML	Tue Oct 25 16:37:11 2011 +0200
+++ b/src/Provers/Arith/extract_common_term.ML	Thu Oct 27 07:46:57 2011 +0200
@@ -22,6 +22,7 @@
   val dest_bal: term -> term * term
   val find_first: term -> term list -> term list
   (*proof tools*)
+  val mk_eq: term * term -> term
   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 -> thm (*simplifies the result*)
@@ -65,11 +66,12 @@
     and terms2' = Data.find_first u terms2
     and T = Term.fastype_of u
 
+    val t'' = Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2'))
     val reshape =
-      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')))
+      Goal.prove ctxt [] [] (Data.mk_eq (t', t'')) (K (Data.norm_tac ss))
+
   in
-    Option.map (export o Data.simplify_meta_eq ss simp_th) reshape
+    SOME (export (Data.simplify_meta_eq ss simp_th reshape))
   end
   (* FIXME avoid handling of generic exceptions *)
   handle TERM _ => NONE