# HG changeset patch
# User huffman
# Date 1326814254 -3600
# Node ID 933f35c4e1260b3f729003527082bf689a5b3add
# Parent  fcfb4aa8e6e6dd26f81ec76bc2de8e78d54fae6c
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero

diff -r fcfb4aa8e6e6 -r 933f35c4e126 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Fact.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -255,8 +255,6 @@
     fact m < fact ((m + 1) + k)"
   apply (induct k rule: int_ge_induct)
   apply (simp add: fact_plus_one_int)
-  apply (subst mult_less_cancel_right1)
-  apply (insert fact_gt_zero_int [of m], arith)
   apply (subst (2) fact_reduce_int)
   apply (auto simp add: add_ac)
   apply (erule order_less_le_trans)
diff -r fcfb4aa8e6e6 -r 933f35c4e126 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -723,8 +723,6 @@
         using t(1,2) m(2)[rule_format, OF tw] w0
         apply (simp only: )
         apply auto
-        apply (rule mult_mono, simp_all add: norm_ge_zero)+
-        apply (simp add: zero_le_mult_iff zero_le_power)
         done
       with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
       from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
diff -r fcfb4aa8e6e6 -r 933f35c4e126 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Jan 17 16:30:54 2012 +0100
@@ -461,8 +461,9 @@
       val zero = Const(@{const_name Groups.zero}, T);
       val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
       val pos = less $ zero $ t and neg = less $ t $ zero
+      val thy = Proof_Context.theory_of (Simplifier.the_context ss)
       fun prove p =
-        Option.map Eq_True_elim (Lin_Arith.simproc ss p)
+        SOME (Eq_True_elim (Simplifier.asm_rewrite ss (Thm.cterm_of thy p)))
         handle THM _ => NONE
     in case prove pos of
          SOME th => SOME(th RS pos_th)
diff -r fcfb4aa8e6e6 -r 933f35c4e126 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Transcendental.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -1478,9 +1478,6 @@
   thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
 qed
 
-lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
-by simp
-
 lemma real_mult_inverse_cancel:
      "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
       ==> inverse x * y < inverse x1 * u"
@@ -1516,11 +1513,7 @@
 unfolding One_nat_def
 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric]
             del: fact_Suc)
-apply (rule real_mult_inverse_cancel2)
-apply (simp del: fact_Suc)
-apply (simp del: fact_Suc)
-apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
-apply (subst fact_lemma)
+apply (simp add: inverse_eq_divide less_divide_eq del: fact_Suc)
 apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
 apply (simp only: real_of_nat_mult)
 apply (rule mult_strict_mono, force)
diff -r fcfb4aa8e6e6 -r 933f35c4e126 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -318,9 +318,7 @@
    apply clarsimp
   apply clarsimp
   apply safe
-  apply (drule meta_spec, erule xtr8 [rotated],
-         simp add: numeral_simps algebra_simps BIT_simps
-         cong add: number_of_False_cong)+
+  apply (drule meta_spec, erule xtr8 [rotated], simp add: Bit_def)+
   done
 
 lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
diff -r fcfb4aa8e6e6 -r 933f35c4e126 src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Tue Jan 17 11:15:36 2012 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy	Tue Jan 17 16:30:54 2012 +0100
@@ -366,6 +366,14 @@
   next
     assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
       by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
+  next
+    txt "This simproc now uses the simplifier to prove that terms to
+      be canceled are positive/negative."
+    assume z_pos: "0 < z"
+    assume "x < y" have "z*x < z*y"
+      by (tactic {* CHANGED (asm_simp_tac (HOL_basic_ss
+        addsimprocs [@{simproc linordered_ring_less_cancel_factor}]
+        addsimps [@{thm z_pos}]) 1) *}) fact
   }
 end